Forgive me for not reading in full detail, but I think I can answer your
question:
To use X_CHOOSE_TAC without using DISCH_THEN, you can simply pass it a
theorem.
So, rather than MP_TAC(ASSUME t) followed by DISCH_THEN(CHOOSE_TAC), you
could simply do CHOOSE_TAC(ASSUME t).
On Wed, Dec 12, 2012 at 6:22 PM, Bill Richter <[email protected]
> wrote:
> 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
>
------------------------------------------------------------------------------
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
