I've been caught out with the same thing for MATCH_MP, I defined
(* MATCH_MP2 delays raising an exception until second argument is seen, *) fun MATCH_MP2 th1 th2 = MATCH_MP th1 th2 ; Jeremy On 23/08/17 17:03, 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