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
[email protected]
https://lists.sourceforge.net/lists/listinfo/hol-info
