Petros, your code worked great, and I now have consider working the way I
wanted, included below. I couldn't use it for cases, and that's a good place
to try Vincent's quotexpander idea. I put your code into BuildExist, and
borrowed some of Marco Maggesi's HYP ideas to turn a string into a list of term
variables. Below I'll give an example, my version of the HOL Light tutorial
readable proof that the square root of 2 is irrational. Perhaps you'll have a
suggestion. I don't quite know what all your code means yet.
--
Best,
Bill
let TACtoThmTactic tac = fun ths -> MAP_EVERY MP_TAC ths THEN tac;;
let NUM_RING_thmTAC = TACtoThmTactic (CONV_TAC NUM_RING);;
let ARITH_thmTAC = TACtoThmTactic ARITH_TAC;;
let so = fun tac -> FIRST_ASSUM MP_TAC THEN tac;;
let BuildExist x t =
let try_type tp tm =
try inst (type_match (type_of tm) tp []) tm
with Failure _ -> tm in
(* Check if two variables match allowing only type instantiations: *)
let vars_match tm1 tm2 =
let inst = try term_match [] tm1 tm2 with Failure _ -> [],[tm2,tm1],[] in
match inst with
[],[],_ -> tm2
| _ -> failwith "vars_match: no match" in
(* Find the type of a matching variable in t. *)
let tp = try type_of (tryfind (vars_match x) (frees t))
with Failure _ ->
warn true ("BuildExist: `" ^ string_of_term x ^ "` not be found in
`" ^ string_of_term t ^ "`") ;
type_of x in
(* Try to force x to type tp. *)
let x' = try_type tp x in
mk_exists (x',t);;
let consider vars_SuchThat t prfs lab =
(* Functions ident and parse_using borrowed from HYP in tactics.ml *)
let ident = function
Ident s::rest when isalnum s -> s,rest
| _ -> raise Noparse in
let parse_using = many ident in
let rec findSuchThat = function
n -> if String.sub vars_SuchThat n 9 = "such that" then n
else findSuchThat (n + 1) in
let n = findSuchThat 1 in
let vars = String.sub vars_SuchThat 0 (n - 1) in
let xl = map parse_term ((fst o parse_using o lex o explode) vars) in
let tm = itlist BuildExist xl t in
match prfs with
p::ps -> (warn (ps <> []) "consider: additional subproofs ignored";
SUBGOAL_THEN tm (DESTRUCT_TAC ("@" ^ vars ^ "." ^ lab))
THENL [p; ALL_TAC])
| [] -> failwith "consider: no subproof given";;
let cases sDestruct disjthm tac =
SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
(DESTRUCT_TAC sDestruct);;
let NSQRT_2 = prove
(`!p q. p * p = 2 * q * q ==> q = 0`,
MATCH_MP_TAC num_WF THEN
INTRO_TAC "!p; A; !q; B" THEN
SUBGOAL_TAC "" `EVEN(p * p) <=> EVEN(2 * q * q)`
[HYP MESON_TAC "B" []] THEN
SUBGOAL_TAC "" `EVEN(p)` [so (MESON_TAC [ARITH; EVEN_MULT])] THEN
consider "m such that" `p = 2 * m`
[so (MESON_TAC [EVEN_EXISTS])] "C" THEN
cases "qp | pq" `(q:num) < p \/ p <= q` [ARITH_TAC] THENL
[SUBGOAL_TAC "" `q * q = 2 * m * m ==> m = 0` [HYP MESON_TAC "qp A" []] THEN
so (HYP NUM_RING_thmTAC "B C" []);
SUBGOAL_TAC "" `p * p <= (q:num) * q` [so (MESON_TAC [LE_MULT2 ])] THEN
SUBGOAL_TAC "" `q * q = 0` [so (HYP ARITH_thmTAC "B" [])] THEN
so (NUM_RING_thmTAC [])]);;
------------------------------------------------------------------------------
Minimize network downtime and maximize team effectiveness.
Reduce network management and security costs.Learn how to hire
the most talented Cisco Certified professionals. Visit the
Employer Resources Portal
http://www.cisco.com/web/learning/employer_resources/index.html
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
