1, Canberra City)" <michael.norr...@data61.csiro.au>
Cc: hol-info <hol-info@lists.sourceforge.net>
Subject: Re: [Hol-info] Strange tactics bug when using match_mp_tac
I have a couple of comments/questions on irule:
- I think mp_then is supposed to be better still. Am I right? (Or
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
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 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
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
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:
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.
