Hello Bill, Without being as much of an expert as other people on this list, it is my understanding that traditionally HOL systems are rather inflexible when it comes to manipulating assumptions.
If you need to apply further rules/tactics, it is preferable to deal with antecedents rather than assumptions. For example, instead of this: e(SUBGOAL_THEN `EVEN p` ASSUME_TAC);; it would be easier to do this: e(SUBGOAL_THEN `EVEN p` MP_TAC);; and then manipulate the antecedent further using DISCH_THEN (ie. without the need for your extra MP_TAC (ASSUME t) step). In the spirit of Ramana's reply, you can avoid using DISCH_THEN as follows: e(SUBGOAL_THEN `EVEN p` (CHOOSE_TAC o REWRITE_RULE[EVEN_EXISTS]));; (You are actually using ASM_MESON_TAC to prove `?m. p = 2 * m` from `EVEN p` but rewriting is sufficient.) This, of course, requires some planning ahead of what you need to do with `EVEN p`, but I am just demonstrating how one would manage not to use DISCH_THEN with CHOOSE_TAC. Note that this would actually be less complicated if you didn't use `EVEN p` as an intermediate subgoal but went straight for `?m. p = 2 * m` (realising this would mean skipping a step from the original proof). You are using EVEN_EXISTS to prove your subgoal anyway! You can simply: e(SUBGOAL_THEN `?m. p = 2 * m` CHOOSE_TAC);; To sum up, the first part of your proof: 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));; can be "simplified" as follows: g `!p q. p * p = 2 * q * q ==> q = 0`;; e(MATCH_MP_TAC num_WF);; e(REPEAT STRIP_TAC);; e(SUBGOAL_THEN `?m. p = 2 * m` CHOOSE_TAC);; e(ASM_MESON_TAC[EVEN_EXISTS;EVEN_MULT]);; Hope this helps. Regards, Petros On 12/12/2012 07:22, Bill Richter wrote: > 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? > -- Petros Papapanagiotou CISA, School of Informatics The University of Edinburgh Email: [email protected] --- The University of Edinburgh is a charitable body, registered in Scotland, with registration number SC005336. ------------------------------------------------------------------------------ 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
