Thank, Ramana and Petros! Your code looks very helpful, and I'll study it, but
first I want to explain something I did with miz3's `consider' but could not
port to HOL Light, even using the tutorial p 78 Mizar-like `consider'. Here's
a simpler version of the tutorial p 65 `reachable'
let addN = new_definition
`!p p' n.
addN p p' n <=> ?s.
s 0 = p /\ s n = p' /\
(!m. m < n ==> s (SUC m) = SUC (s m))`;;
Here's a very simple result I proved with mi3z, related to the tutorial p 67
REACHABLE_INVARIANT:
addfour_THM : thm =
|- !p p'. addN p p' 4 ==> (?q. addN p q 3 /\ p' = SUC q)
#load "unix.cma";;
loadt "miz3/miz3.ml";;
horizon := 0;;
let addfour_THM = thm `;
thus !p p'. addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q
proof
let p p' be num;
assume addN p p' 4;
consider s such that
s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m)) [sDef] by
-, addN;
consider q such that
q = s 3 [qDef];
SUC 3 = 4;
s 0 = p /\ s 3 = q /\ (!m. m < 3 ==> s (SUC m) = SUC (s m)) /\ p' = SUC q
by -, qDef, LT, sDef;
qed by -, addN;
`;;
Let's try to port this proof to HOL Light up to qDef:
g `addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q`;;
e(SIMP_TAC[addN]);;
e(DISCH_THEN(X_CHOOSE_TAC `s: num->num`));;
e(SUBGOAL_THEN `s 0 = p` ASSUME_TAC);;
e(ASM_MESON_TAC[]);;
It's OK to the last line, but MESON times out with Exception: Failure
"solve_goal: Too deep". I get the same problem using John's Mizar-like
`consider':
g `addN p p' 4 ==> ?q. addN p q 3 /\ p' = SUC q`;;
e(SIMP_TAC[addN]);;
e(assume("A") `?s. s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s
m))`);;
e(so consider (`s:num->num`,"B",
`s 0 = p /\ s 4 = p' /\ (!m. m < 4 ==> s (SUC m) = SUC (s m))`) (using []
trivial));;
e(so have `s 0 = p` (by ["B"] trivial));;
To run this, you need the tutorial Mizar-like code included below. I think I'm
using John's code correctly, because it's similar to his p 81 Mizar-like proof
of NSQRT_2. The moral of the story must be that HOL uses different idioms
(e.g. Petros's) to accomplish the same things I know how to do easily in miz3.
This example of course is quite simple, but it illustrates a problem: how to do
we bind a variable to a function with a label so that we can use it repeatedly?
With John's Mizar-like consider we can bind variables to numbers, e.g.
so consider (‘m:num‘,"C",‘p = 2 * m‘) (using [EVEN_EXISTS] trivial) THEN
I studied the HOL Light sources and a number of places that X_CHOOSE_TAC was
applied to a function. But it seemed to me that EXISTS_TAC was usually applied
right afterward, and that's not saving the function for later use.
--
Best,
Bill
let fix ts = MAP_EVERY X_GEN_TAC ts;;
let assume lab t =
DISCH_THEN(fun th -> if concl th = t then LABEL_TAC lab th
else failwith "assume");;
let we’re finished tac = tac;;
let suffices_to_prove q tac = SUBGOAL_THEN q (fun th -> MP_TAC th THEN tac);;
let note(lab,t) tac =
SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
DISCH_THEN(fun th -> LABEL_TAC lab th);;
let have t = note("",t);;
let cases (lab,t) tac =
SUBGOAL_THEN t MP_TAC THENL [tac; ALL_TAC] THEN
DISCH_THEN(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
let consider (x,lab,t) tac =
let tm = mk_exists(x,t) in
SUBGOAL_THEN tm (X_CHOOSE_THEN x (LABEL_TAC lab)) THENL [tac; ALL_TAC];;
let trivial = MESON_TAC[];;
let algebra = CONV_TAC NUM_RING;;
let arithmetic = ARITH_TAC;;
let by labs tac = MAP_EVERY (fun l -> USE_THEN l MP_TAC) labs THEN tac;;
let using ths tac = MAP_EVERY MP_TAC ths THEN tac;;
let so constr arg tac = constr arg (FIRST_ASSUM MP_TAC THEN tac);;
------------------------------------------------------------------------------
LogMeIn Rescue: Anywhere, Anytime Remote support for IT. Free Trial
Remotely access PCs and mobile devices and provide instant support
Improve your efficiency, and focus on delivering more value-add services
Discover what IT Professionals Know. Rescue delivers
http://p.sf.net/sfu/logmein_12329d2d
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
