I have a question about X_CHOOSE_TAC and another vote for miz3.
In miz3 you can easily define variables with `consider'. The HOL Light
tutorial only explains two ways to define variables, both in proofs (p 73--81)
of the irrationality of sqrt{2}. John's p 78 Mizar-like `consider' is close to
miz3's, but I do not understand the code and I've found no HOL Light source
code that seems to be using the idea. I believe the only other variable
definition in the tutorial is on p 74:
e(DISCH_THEN(X_CHOOSE_THEN 'm:num' SUBST_ALL_TAC));;
In the HOL Light source code I see variants of this, but always with DISCH. I
use DISCH_THEN(CHOOSE_TAC) below. How can I use X_CHOOSE_TAC without DISCH?
John has a nice Mizar-like proof of the irrationality of sqrt{2} using his
consider on p 81. I turned it into a normal tactics proof, but my code below
looks clumsy. It looks odd the way I add assumptions by SUBGOAL_THEN and then
in one line prove the sub-goal. I bet this can be done in one line. I think
my use of X_CHOOSE_TAC and DISCH is odd. It's fine to only define variables
through a "existentially quantified conclusion" like ?x.alpha, because when we
define x, it no doubt satisfies some property alpha, thus ?x.alpha must be
true. So I made my ?x.alpha a sub-goal, proved it, and then used
MP_TAC(ASSUME `?x.alpha`)
to make ?x.alpha the antecedent of the goal, and then used
DISCH_THEN(CHOOSE_TAC)
to define the variable x and make alpha an assumption. Then we go back to the
original goal. Can someone tell me a better way?
--
Best,
Bill
g `!p q. p * p = 2 * q * q ==> q = 0`;;
e(MATCH_MP_TAC num_WF);;
e(REPEAT STRIP_TAC);;
e(SUBGOAL_THEN `EVEN p` ASSUME_TAC);;
e(ASM_MESON_TAC[EVEN_EXISTS; EVEN_MULT]);;
e(SUBGOAL_THEN `?m. p = 2 * m` ASSUME_TAC);;
e(ASM_MESON_TAC[EVEN_EXISTS]);;
e(MP_TAC(ASSUME `?m. p = 2 * m`));;
e(DISCH_THEN(CHOOSE_TAC));;
e(DISJ_CASES_TAC(ARITH_RULE `q < p \/ p <= q`));;
e(SUBGOAL_THEN `q * q = 2 * m * m ==> m = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[]);;
e(SUBGOAL_THEN `q * q = 2 * m * m` ASSUME_TAC);;
e(SUBGOAL_THEN `p = 2 * m /\ p * p = 2 * q * q ==> q * q = 2 * m * m`
ASSUME_TAC);;
e(CONV_TAC NUM_RING);;
e(ASM_MESON_TAC[]);;
e(SUBGOAL_THEN `m = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[]);;
e(ASM_MESON_TAC[MULT_EQ_0]);;
e(SUBGOAL_THEN `p * p <= q * q` ASSUME_TAC);;
e(ASM_MESON_TAC[LE_MULT2]);;
e(SUBGOAL_THEN `p * p = 2 * q * q /\ p * p <= q * q ==> q * q = 0` ASSUME_TAC);;
e(ARITH_TAC);;
e(SUBGOAL_THEN `q * q = 0` ASSUME_TAC);;
e(ASM_MESON_TAC[MULT_EQ_0]);;
e(ASM_MESON_TAC[MULT_EQ_0]);;
------------------------------------------------------------------------------
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
