Is there any easy HOL 1-line way to state a result t, prove it, then use for
some purpose?
Below I'll give my best shot, and use it to improve the LABEL_TAC entry to the
HOL Light reference manual.
I finally understood, and modified, the HOL Light tutorial (p 78) Mizar-like
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));;
Tell me if this is right: SUBGOAL_THEN is normally used with ASSUME_TAC, but
not always, and here if the first goal is g, then
SUBGOAL_THEN t MP_TAC
makes the first and second goals
t and t ==> g
THENL applies tac to prove t, and does nothing to t ==> g.
Then DISCH_THEN pulls off the antecedent t, and DISJ_CASES_THEN breaks the
disjunction t, and then LABEL_TAC gives each disjunct the same label lab, which
is fine, because the different disjuncts have different goals and so there's no
conflict between the the different copies of the label lab.
That's nice code, but I wondered if we could avoid the MP_TAC/DISCH_THEN
routine, as Ramana, Petros and Michael taught me was sometimes possible.
Here's a substitute bcases, mostly due to my son, which uses my modifications
of the tutorial Mizar-like code
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 pf lab =
state t "" pf THEN FIRST_X_ASSUM
(REPEAT_TCL DISJ_CASES_THEN (LABEL_TAC lab));;
But in a sense, bcases has the same problem as John's code, as it takes a
statement t, pushes it onto the assumption stack via state, proves it with pf,
then pops it off the assumption stack and uses DISJ_CASES_THEN and LABEL_TAC as
John's cases does. Is there a way to avoid one-step-forward-one-step-back
routines like MP_TAC/DISCH_THEN and ASSUME_TAC/FIRST_X_ASSUM here? Anyway, I'm
really happy to understand this, because now I know how to port all my miz3
Hilbert axiomatic geometry results to straight HOL Light tactics. I'll apply
this to the LABEL_TAC entry to the HOL Light reference manual, which has some
typos and a proof that doesn't work.
We'll prove that a binary relation <<= that is antisymmetric and has a strong
wellfoundedness property is a wellorder. The reference manual proves half of
this in one line (if you put the {}s in) with SET_TAC[], but the transitive
part seems harder. My proof below uses the definitions above, and follows my
Hilbert geometry by not using SET_TAC[], but only MESON_TAC and results from
sets.ml.
--
Happy New Year!
Bill
g `(!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`;;
e(DISCH_THEN(CONJUNCTS_THEN2 (LABEL_TAC "antisym") (LABEL_TAC "swf")));;
e(STRIP_TAC THEN STRIP_TAC THEN STRIP_TAC);;
e(consider `?s:A->bool. s = {x:A,y:A}` "" (soby [] []));;
e(state `!p:A. p IN s <=> p = x \/ p = y` "sxy" (soby [] [IN_INSERT;
MEMBER_NOT_EMPTY]));;
e(state `~(s:A->bool = {})` "" (soby [] [MEMBER_NOT_EMPTY]));;
e(consider `?a:A. a IN (s:A->bool) /\ !p:A. p IN s ==> a <<= p` "aExists" (soby
["swf"] []));;
e(bcases `a:A = x:A \/ a = y:A` (soby ["sxy"] []) "xxx");;
e(soby ["aExists"; "sxy"] []);;
e(soby ["aExists"; "sxy"] []);;
e(STRIP_TAC THEN DISCH_THEN(CONJUNCTS_THEN2
(LABEL_TAC "xLESSy") (LABEL_TAC "yLESSz")));;
e(consider `?s:A->bool. s = {x:A,y:A,z:A}` "C" (soby [] []));;
e(state `!p:A. p IN s <=> p = x \/ p = y \/ p = z` "sxyz" (soby [] [IN_INSERT;
MEMBER_NOT_EMPTY]));;
e(state `~(s:A->bool = {})` "" (soby [] [MEMBER_NOT_EMPTY]));;
e(consider `?a:A. a IN (s:A->bool) /\ !p:A. p IN s ==> a <<= p` "aExists" (soby
["swf"] []));;
e(bcases `a:A = x:A \/ a = y:A \/ a = z:A` (soby ["sxyz"] []) "bbb");;
e(soby ["sxyz"] []);;
e(soby ["aExists"; "sxyz"] []);;
e(soby ["aExists"; "sxyz"; "xLESSy"; "antisym"; "yLESSz"] []);;
e(soby ["aExists"; "sxyz"; "yLESSz"; "antisym"; "xLESSy"] []);;
let WfAndAntisymImpliesWo = top_thm();;
------------------------------------------------------------------------------
Master SQL Server Development, Administration, T-SQL, SSAS, SSIS, SSRS
and more. Get SQL Server skills now (including 2012) with LearnDevNow -
200+ hours of step-by-step video tutorials by Microsoft MVPs and experts.
SALE $99.99 this month only - learn more at:
http://p.sf.net/sfu/learnmore_122512
_______________________________________________
hol-info mailing list
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
