Thanks, Petros, but I don't see how SUBGOAL_TAC is any better than SUBGOAL_THEN
at avoiding the one-step-forward-one-step-back awkwardness of MP_TAC/DISCH_THEN
ASSUME_TAC/FIRST_X_ASSUM that John's cases and the modification bcases have.
Below is a tactics script for my proof of the LABEL_TAC exercise in the HOL
Light reference manual, which I should have posted yesterday. BTW how does HOL
and Informatics fit together? Thanks for the feedback on my explanation of
John's cases, which as you say assumes tac will prove t, as does bcases. I
thought of this
you could use replace MP_TAC with (REPEAT_TCL DISJ_CASES_THEN
(LABEL_TAC lab)) [but] DISJ_CASES_THEN will create two new subgoals
(for a total of three).
but as you say that won't work unless I can calculate how my disjuncts I'll
get. There must be a function that calculates that. In the first bcases
below, it's 2, and it's 3 for the second. I need to know because of the THENL
[tac; ALL_TAC], which would be changed to THENL [tac; ALL_TAC; ALL_TAC;
ALL_TAC] for 3 disjuncts. I also don't know how to print a variable number of
ALL_TACs. I thought maybe I could try
SUBGOAL_THEN t ALL_TAC THENL [SUBGOAL_THEN t ALL_TAC; ALL_TAC]
so the top 3 goals in the goalstack would be (for g the original top goal)
t, t, and g
But that won't fly, because
MP_TAC is a thm_tactic, and ALL_TAC is just a tactic. I that the correct
usage? And that's the difference between SUBGOAL_THEN and SUBGOAL_TAC, whether
you use a thm_tactic or a tactic? BTW how do I learn the typed LC or whatever
that explains how tactics and thm_tactics actually work? The HOL Light
tutorial I think is actually a pretty good way to learn how to write tactics
proofs, if you read the whole tutorial from beginning to end, dipping into the
reference manual (and posting here!) when you get stuck, but I don't think it
explains the theory of tactics proofs. Maybe I missed it.
--
Best,
Bill
let soby labs MesonList = FIRST_ASSUM MP_TAC THEN MAP_EVERY
(fun l -> USE_THEN l MP_TAC) labs THEN (MESON_TAC MesonList);;
let consider t lab pf = SUBGOAL_THEN t (CHOOSE_THEN (LABEL_TAC lab)) THENL [pf;
ALL_TAC];;
let state t lab pf = SUBGOAL_THEN t (LABEL_TAC lab) THENL [pf; ALL_TAC];;
let bcases t lab pf =
state t "" pf THEN FIRST_X_ASSUM
(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
let WfAndAntisymImpliesWo = prove
(`(!x y. x <<= y /\ y <<= x ==> x = y) /\
(!s. ~(s = {}) ==> ?a:A. a IN s /\ !x. x IN s ==> a <<= x)
==> (!x y. x <<= y \/ y <<= x) /\
!x y z. x <<= y /\ y <<= z ==> x <<= z`,
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "antisym") (LABEL_TAC "swf"))
THEN STRIP_TAC THEN REPEAT GEN_TAC THENL [ALL_TAC;
DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "xLESSy") (LABEL_TAC "yLESSz"))] THENL
[consider `?s:A->bool. s = {x:A,y:A}` "" (soby [] []);
consider `?s:A->bool. s = {x:A,y:A,z:A}` "C" (soby [] [])] THENL
[state `!p:A. p IN s <=> p = x \/ p = y` "sxy" (soby [] [IN_INSERT;
MEMBER_NOT_EMPTY]);
state `!p:A. p IN s <=> p = x \/ p = y \/ p = z` "sxyz"
(soby [] [IN_INSERT; MEMBER_NOT_EMPTY])] THEN
state `~(s:A->bool = {})` "" (soby [] [MEMBER_NOT_EMPTY]) THEN
consider `?a:A. a IN (s:A->bool) /\ !p:A. p IN s ==> a <<= p` "aExists" (soby
["swf"] []) THENL
[bcases `a:A = x:A \/ a = y:A` "" (soby ["sxy"] []);
bcases `a:A = x:A \/ a = y:A \/ a = z:A` "" (soby ["sxyz"] [])] THENL
[soby ["aExists"; "sxy"] [];
soby ["aExists"; "sxy"] [];
soby ["aExists"; "sxyz"] [];
soby ["aExists"; "sxyz"; "xLESSy"; "antisym"; "yLESSz"] [];
soby ["aExists"; "sxyz"; "yLESSz"; "antisym"; "xLESSy"] []]);;
------------------------------------------------------------------------------
Master Java SE, Java EE, Eclipse, Spring, Hibernate, JavaScript, jQuery
and much more. Keep your Java skills current with LearnJavaNow -
200+ hours of step-by-step video tutorials by Java experts.
SALE $49.99 this month only -- learn more at:
http://p.sf.net/sfu/learnmore_122612
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
