irule is an “improved” version of match_mp_tac; mp_then is an improved version
of imp_res_tac (strictly, imp_res_then).
Alternatively, irule applies an introduction rule to the goal (“backwards”);
mp_then applies an elimination rule to assumptions.
I agree about the stripping of conjunctions.
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
(We apologize if you receive multiple copies of this announcement)
===
SAFECOMP 2017 Last call for participation
The 36th International Conference on Computer Safety, Reliability and Security
12 - 15 September 2017
Trento, Italy
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
-- CALL FOR PARTICIPATION --
15th ACM/IEEE
International Conference
on
Formal Methods and Models for System Design
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.
