Page 54 of the HOL Light tutorial answers my dumb question of yesterday:
Note a subtle point here. When we split a goal into two or more
subgoals, the goalstack presents them to us one at a time. However,
in the tactic script, using THEN will apply the same tactics to all
the goals.
That's why my interactive proof required two e(COND_CASES_TAC)s, but my tactic
script only used one COND_CASES_TAC. I can simplify now that I understand
this:
let NSUM_CLAUS_NUMSEG = prove
(`(!m. nsum (m..0) f = if m = 0 then f 0 else 0) /\
!m n. nsum (m..SUC n) f = if m <= SUC n then nsum (m..n) f + f (SUC n) else
0`,
REWRITE_TAC[NUMSEG_CLAUS] THEN REPEAT STRIP_TAC THEN
COND_CASES_TAC THEN
SIMP_TAC[NSUM_SING; FINITE_NUMSEG; NSUM_CLAUSES] THEN
SIMP_TAC[ARITH_RULE `~(SUC n <= n)`; IN_NUMSEG; ADD_SYM]);;
This uses my simple modification of NUMSEG_CLAUSES
NUMSEG_CLAUS;;
|- (!m. m..0 = (if m = 0 then {0} else {})) /\
(!m n. m..SUC n = (if m <= SUC n then SUC n INSERT (m..n) else {}))
My main purpose here is to understand the semantics of miz3, which Freek
describes in terms of the changing thesis. But it seems to me that the
goalstack explains miz3 better than the poorly documented Mizar concept of the
thesis. It seems to me that the thesis is just the bottom goal in the
goalstack, but that we need the entire goalstack to understand a miz3 proof.
And it seems to me that a miz3 proof should be easily translated into a HOL
Light interactive proof. For instance, if the thesi thesis at some point in
the proof is α ⇒ β, and you write
assume α;
then the thesis is now β. But that's just MATCH_MP_TAC. If inside a miz3 proof
you write
α
proof
[...]
qed;
there is still a thesis after the qed, the thesis we had when we wrote α.
Which is to say, we added α to the goalstack, but after proving α, we remove α
from the goalstack, and we're back to the previous bottom element of the
goalstack. And so forth. It will take me a while to straighten this out. But
I think that's the sensible way to understand miz3 semantics: in terms of HOL
Light interactive proofs, and not Mizar.
--
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
