Mark, thanks for explaining my irregular syntax (how do I learn I can't mix symbolic and alpha-numeric characters?), and that HOL Zero precedence is similar to HOL Light's. I have a SWAP_FORALL_THM question an a vote for miz3. I got this tactics proof to work, but I don't know why it does:
let ReachableInvariant = prove (`!p p'. reachable p p' ==> oriented_area p = oriented_area p'`, ASM_SIMP_TAC[ReachLemma] THEN SIMP_TAC[LEFT_IMP_EXISTS_THM] THEN SIMP_TAC[SWAP_FORALL_THM] THEN INDUCT_TAC THEN ASM_MESON_TAC[reachableN_CLAUSES; MOVE_INVARIANT]);; This tactics script requires other things to run, but my problem doesn't involve them, I think. Writing this interactively I see that SIMP_TAC[SWAP_FORALL_THM] performed the goal reduction `!p p' n. reachableN p p' n ==> oriented_area p = oriented_area p'` `!n p p'. reachableN p p' n ==> oriented_area p = oriented_area p'` That's what I wanted, because now INDUCT_TAC gives me induction on the variable n. But I don't know why that happened. I would have thought that SWAP_FORALL_THM would take switch the variables p and p' instead: SWAP_FORALL_THM;; val it : thm = |- !P. (!x y. P x y) <=> (!y x. P x y) This tactics script I think shows the value of miz3. I was only able to write this, I think, after having already written the following miz3 proof, which is much longer but was much easier to write. I've only read up to page 68 of the HOL Light tutorial, and I don't quite understand what these tactics do, or how to set up a tactics proof. But I knew it could be done, and "in spirit" how the proof would go, so I was able to hunt through theorems.ml to find what I needed. -- Best, Bill let ReachableInvariant = thm `; let p p' be (real#real)#(real#real)#(real#real); assume reachable p p' [H1]; thus oriented_area p = oriented_area p' proof consider P such that P = \n. ! p p'. reachableN p p' n ==> oriented_area p = oriented_area p' [Pdef]; P 0 [P0] by Pdef, reachableN_CLAUSES; ! n. P n ==> P (SUC n) proof let n be num; assume P n; ! p p'. reachableN p p' n ==> oriented_area p = oriented_area p' [nStep] by -, Pdef; ! r r'. reachableN r r' (SUC n) ==> oriented_area r = oriented_area r' proof let r r' be (real#real)#(real#real)#(real#real); assume reachableN r r' (SUC n); consider q such that reachableN r q n /\ move q r' [qExists] by -, reachableN_CLAUSES; oriented_area r = oriented_area q /\ oriented_area q = oriented_area r' by -, nStep, MOVE_INVARIANT; qed by -; qed by -, Pdef; ! n. P n [allPn] by -, P0, Pdef, num_INDUCTION; consider n such that reachableN p p' n by H1, ReachLemma; qed by -, Pdef, allPn; `;; ------------------------------------------------------------------------------ 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 hol-info@lists.sourceforge.net https://lists.sourceforge.net/lists/listinfo/hol-info