I have a couple of comments/questions on irule:
- I think mp_then is supposed to be better still. Am I right? (Or are they
serving different purposes?)
- I find it annoying that irule produces lots of new subgoals for the
hypotheses. Is there a version that doesn't strip all the conjunctions, so
they can be worked on together?
On 24 August 2017 at 09:22, <michael.norr...@data61.csiro.au> wrote:
> Eta-expanding as you did is nicer, I think.
>
> You might also consider using irule; it is supposed to be an improved
> match_mp_tac (i.e., does more things), and it doesn’t have the particular
> problem with exceptions. Indeed, one of its improvements is that it
> subsumes {MATCH_}ACCEPT_TAC.
>
> Michael
>
> On 23/8/17, 17:28, "Heiko Becker" <heikobecke...@gmail.com> wrote:
>
> Thank you for the fix. With this I could come up with a solution that I
> find ok for the moment:
>
> val my_match_mp_tac = (fn thm => (fn gs => match_mp_tac thm gs))
>
> This allows to at least not have the HOL_ERR handling, but I guess it
> depends what one finds nicer.
>
>
> Heiko
>
> On 08/23/2017 09:03 AM, michael.norr...@data61.csiro.au wrote:
> > You are being caught by the fact that match_mp_tac thm can throw an
> exception before the tactic is ever applied to a goal. In particular, if
> the theorem passed to match_mp_tac is not an implication an exception is
> thrown immediately.
> >
> > You can fix this by handling that possible exception:
> >
> > fun simple_apply thm = ACCEPT_TAC thm ORELSE (match_mp_tac thm
> handle HOL_ERR _ => ALL_TAC)
> >
> > This arguably a poor design for match_mp_tac, and should perhaps be
> changed.
> >
> > Michael
> >
> >
> >
> > On 23/8/17, 16:55, "Heiko Becker" <hbec...@mpi-sws.org> wrote:
> >
> > Hello everyone,
> >
> > while working on some custom tactics, I noticed some strange
> behavior
> > related to combining tactics with match_mp_tac and the ORELSE
> tactical:
> >
> > I am trying to write a tactic takes a theorem and first tries
> out
> > whether it is already a proof of the current goal with
> ACCEPT_TAC.
> > If this does not succeed, the tactic should try matching the
> theorem
> > with match_mp_tac.
> >
> > Here is what I have come up with:
> >
> > fun simple_apply thm = (ACCEPT_TAC thm) ORELSE
> (match_mp_tac thm);
> >
> > I have defined a test tactic, to see whether ACCEPT_TAC works
> as I
> > expect it to work:
> >
> > fun dumb_apply thm = (ACCEPT_TAC thm) ORELSE (FAIL_TAC
> "Unreachable");
> >
> > Strangely the simple_apply tactic does not work in cases, where
> the
> > dumb_apply tactic works:
> >
> > val test_thm = Q.prove (
> > ` !(n:num) (P:num -> bool).
> > P n ==>
> > P n`,
> > rpt gen_tac
> > DISCH_THEN ASSUME_TAC
> > qpat_x_assum `P n` (fn thm => simple_apply thm) (* Fails
> with "No
> > parse of quotation leads to success" *)
> > qpat_x_assum `P n` (fn thm => dumb_apply thm) (* Proves
> the goal *)
> > );
> >
> >
> > Can someone explain to me what I did wrong with the
> simple_apply tactic?
> >
> >
> > Thanks,
> >
> >
> > Heiko
> >
> > ------------------------------------------------------------
> ------------------
> > Check out the vibrant tech community on one of the world's most
> > engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> > _______________________________________________
> > hol-info mailing list
> > hol-info@lists.sourceforge.net
> > https://lists.sourceforge.net/lists/listinfo/hol-info
> >
> >
>
>
>
> ------------------------------------------------------------
> ------------------
> Check out the vibrant tech community on one of the world's most
> engaging tech sites, Slashdot.org! http://sdm.link/slashdot
> _______________________________________________
> hol-info mailing list
> hol-info@lists.sourceforge.net
> https://lists.sourceforge.net/lists/listinfo/hol-info
>
------------------------------------------------------------------------------
Check out the vibrant tech community on one of the world's most
engaging tech sites, Slashdot.org! http://sdm.link/slashdot
_______________________________________________
hol-info mailing list
hol-info@lists.sourceforge.net
https://lists.sourceforge.net/lists/listinfo/hol-info
