I fixed my Mizar-like function `consider' (see below) using strings, Marco's
DESTRUCT_TAC ideas and Freek's parse_term ideas, and used it to port the HOL
Light tutorial (p 81) readable proof of the irrationality of sqrt 2. I
realized that John's function (p 78) `using' can be thought of mapping a tactic
to a thm list -> tactic, which we can then apply HYP to! Here's all my
Mizar-like tactics code and my port of John's NSQRT_2. It's readable if you
evaluate the interactive proof, which I'll include because I'm puzzled by my 3
message
"Translating certificate to HOL inferences"
which all come from NUM_RING_thmTAC, built with my new understanding of John's
`using'. Can anyone explain this?
--
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 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 cases sDestruct sDisjlist tac =
let rec list_mk_string_disj sDisjlist =
match sDisjlist with
[] -> "" |
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 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 [])]);;
g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF);;
e(INTRO_TAC "!p; A; !q; B" );;
e(SUBGOAL_TAC "" `EVEN(p * p) <=> EVEN(2 * q * q)`
[HYP MESON_TAC "B" []]);;
e(SUBGOAL_TAC "" `EVEN(p)` [so (MESON_TAC [ARITH; EVEN_MULT])]);;
e(consider "m such that p = 2 * m"
[so (MESON_TAC [EVEN_EXISTS])] "C");;
e(cases "qp | pq" ["(q:num) < p"; "p <= q"] [ARITH_TAC]);;
e(SUBGOAL_TAC "" `q * q = 2 * m * m ==> m = 0` [HYP MESON_TAC "qp A" []]);;
e(so (HYP NUM_RING_thmTAC "B C" []));;
e(SUBGOAL_TAC "" `p * p <= (q:num) * q` [so (MESON_TAC [LE_MULT2 ])]);;
e(SUBGOAL_TAC "" `q * q = 0` [so (HYP ARITH_thmTAC "B" [])]);;
e(so (NUM_RING_thmTAC []));;
let NSQRT_2 = top_thm();;
------------------------------------------------------------------------------
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_d2d_mar
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
