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
