Vince, I solved your parser/preterm/retypecheck exercise to fix my cases, using
this below:
(term_of_preterm o (retypecheck [])) (end_itlist
(fun pt1 pt2 -> (Combp (Combp (`;\/`, pt1), pt2))) pretermDisjlist)
But I think it's much simpler to get the parser to produce strings instead of
preterms. So modify quotexpander in system.ml to be
let quotexpander s =
if s = "" then failwith "Empty quotation" else
let c = String.sub s 0 1 in
if c = "\"" then
"\""^(String.escaped (String.sub s 1 (String.length s - 1)))^"\"" else
if c = ":" then
"parse_type \""^
(String.escaped (String.sub s 1 (String.length s - 1)))^"\""
else if c = ";" then "parse_qproof \""^(String.escaped s)^"\""
else "parse_term \""^(String.escaped s)^"\"";;
You can see that I profited from your version of quotexpander, so thanks! So
if the first character of a back-quoted expression is a doublequote, it will be
treated exactly as a string minus the doublequote:
# `"X Y such that
move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y)`;;
val it : string =
"X Y such that\n move (B,A,C) (B,A,X) /\\ move (B,A,X) (B',A,X) /\\\n
move (B',A,X) (B',A,Y) /\\ move (B',A,Y) (B',A',Y)"
Now I can define consider and case_split (Thanks, Petros) just as I did before
using strings, but now I don't get problems of backslashes and newlines I had
using strings:
# "X Y such that
move (B,A,C) (B,A,X) /\ move (B,A,X) (B',A,X) /\
move (B',A,X) (B',A,Y) /\ move (B',A,Y) (B',A',Y)";;
val it : string =
"X Y such that\n move (B,A,C) (B,A,X) /\\ move (B,A,X) (B',A,X) /move
(B',A,X) (B',A,Y) /\\ move (B',A,Y) (B',A',Y)"
The whole purpose of parsing is to deal with the /move error above. I'm
including an example below based on the HOL Light tutorial readable proof of
the irrationality of sqrt 2. My code also contains my solution of your
parser/preterm/retypecheck exercise, which for simplicity borrows Freek's c =
";" branch of quotexpander.
--
Best,
Bill
(* first modify quotexpander in system.ml as above, and then run
ocaml
#use "hol.ml";;
*)
let consider vars_t prfs lab =
let len = String.length vars_t in
let rec findSuchThat = function
n -> if String.sub vars_t n 9 = "such that" then n
else findSuchThat (n + 1) in
let n = findSuchThat 1 in
let vars = String.sub vars_t 0 (n - 1) and
t = String.sub vars_t (n + 9) (len - n - 9) in
let tm = parse_term ("?" ^ vars ^ ". " ^ 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 case_split sDestruct sDisjlist tac =
let rec list_mk_string_disj = function
[] -> ""
| s::[] -> "(" ^ s ^ ")"
| s::ls -> "(" ^ s ^ ") \\/ " ^ list_mk_string_disj ls in
let disjthm = parse_term (list_mk_string_disj sDisjlist) in
SUBGOAL_TAC "" disjthm tac THEN FIRST_X_ASSUM
(DESTRUCT_TAC sDestruct);;
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 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
case_split "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 [])]);;
(* now a version using a solution of Vince's parser/preterm/retypecheck
exercise *)
let parse_qproof s = (fst o parse_preterm o lex o explode)
(String.sub s 1 (String.length s - 1));;
let case_split sDestruct pretermDisjlist tac =
let disjthm = (term_of_preterm o (retypecheck [])) (end_itlist
(fun pt1 pt2 -> (Combp (Combp (`;\/`, pt1), pt2))) pretermDisjlist) in
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
case_split "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 [])]);;
------------------------------------------------------------------------------
Try New Relic Now & We'll Send You this Cool Shirt
New Relic is the only SaaS-based application performance monitoring service
that delivers powerful full stack analytics. Optimize and monitor your
browser, app, & servers with just a few lines of code. Try New Relic
and get this awesome Nerd Life shirt! http://p.sf.net/sfu/newrelic_d2d_apr
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
