Le 24/10/12 14:58, Vincent Aravantinos a écrit :
does anybody know of something providing in HOL-Light the same
functionality as the Q module in HOL4?
It was actually easy to define mine, see
<http://users.encs.concordia.ca/~vincent/Software_files/q.ml> if interested.
Summary:
The module si called "Pa" (short for "Parse) because HOL-Light does not allow
"Q"
as a valid module name. All functions have the same signature as their
standard
HOL-Light counterpart, except the type "term" is replaced by "string".
The following functions are provided:
val EXISTS_TAC : string -> tactic
val SUBGOAL_THEN : string -> thm_tactic -> tactic
val SPEC_TAC : string * string -> tactic
val SPEC : string -> thm -> thm
val SPECL : string list -> thm -> thm
val GEN : string -> thm -> thm
val GENL : string list -> thm -> thm
val X_GEN_TAC : string -> tactic
val REAL_ARITH : string -> thm
val REAL_FIELD : string -> thm
val REAL_RING : string -> thm
val ARITH_RULE : string -> thm
val NUM_RING : string -> thm
val INT_ARITH : string -> thm
val PARSE_IN_CONTEXT : (term -> tactic) -> (string -> tactic)
Ex:
The goal:
# g `!x:real. P x ==> ?y. P y`
can be reduced by the following tactic:
# e (REPEAT STRIP_TAC THEN Pa.EXISTS_TAC "x")
Its standard equivalent would be the following, which requires a type
annotation:
# e (REPEAT STRIP_TAC THEN EXISTS_TAC `x:real`)
Regards,
V.
--
Vincent ARAVANTINOS - PostDoctoral Fellow - Concordia University, Hardware
Verification Group
http://users.encs.concordia.ca/~vincent/
------------------------------------------------------------------------------
Everyone hates slow websites. So do we.
Make your web apps faster with AppDynamics
Download AppDynamics Lite for free today:
http://p.sf.net/sfu/appdyn_sfd2d_oct
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
