I guess you've found a bug in the documentation. Thanks, Michael! I think you're right, because the ref manual makes the same apparent error:
http://www.cl.cam.ac.uk/~jrh13/hol-light/reference.html Given a goal (A,t), STRIP_TAC removes one outermost occurrence of one of the connectives !, ==>, ~ or /\ from the conclusion of the goal t. But the important point is that you taught me about about STRIP_ASSUME_TAC, about which the ref manual says Given a theorem th and a goal (A,t), STRIP_ASSUME_TAC th splits th into a list of theorems. This is done by recursively breaking conjunctions into separate conjuncts, cases-splitting disjunctions, and eliminating existential quantifiers by choosing arbitrary variables. That looks extremely useful. You're also explaining DISCH_THEN. The ref manual says DISCH_THEN removes the antecedent and then creates a theorem by ASSUMEing it. This new theorem is passed to the theorem-tactic given as DISCH_THEN's argument. The consequent tactic is then applied. I can't figure out what ASSUMEing means, I think I can skip that and say DISCH_THEN removes the antecedent and [passes it] to the theorem-tactic given as DISCH_THEN's argument. DISCH_TAC [...] is more or less equivalent to DISCH_THEN ASSUME_TAC The tutorial say that's exactly true on page 50! I should have realized that. My minimal objective here is to understand miz3 well enough in terms of HOL Light tactics to be able to explain miz3. Freek's explanation of miz3 only uses the obscure Mizar concept of the thesis, and it seems clear to me that we need the HOL concepts of goalstack and assumption list. My maximal objective is to understand tactics well enough to get these fast Intel chips to prove theorems for me that I don't already know how to prove. In my simple AddFour miz3 proof I posted, I did something that you & Petros didn't explain to me how to do, as my miz3 consider q such that q = s 3 [qDef]; isn't quite replaced by your e (EXISTS_TAC `(s:num->num) 3`);; which plugs s 3 in for q in the existential statement ?q. ..... Also the miz3 behavior of MESON looks the same as the tactic ASM_MESON_TAC. It looks like in miz3, my qDef was EXISTS_TAC-ed, but that doesn't easily happen in tactics. In fact, I thought that in my tactics proof that ASM_MESON_TAC ignored my assumption value of q 3 [`q = s 3`] so I tried running your proof without EXISTS_TAC, and it worked, although I got a MESON solved at number of 17,212,792: 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))`;; g `!p p'. addN p p' 4 ==> (?q. addN p q 3 /\ p' = SUC q)`;; e (REPEAT GEN_TAC);; e (SIMP_TAC[addN]);; e(STRIP_TAC);; e (ASM_MESON_TAC[LT;ARITH_RULE `SUC 3 = 4`]);; let addfour_THM = top_thm();; -- Best, Bill ------------------------------------------------------------------------------ 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
