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
