irule
Tactic.irule : thm_tactic
Reduces the goal using a supplied implication, with matching.
When applied to a theorem of the form
A' |- !x1...xn. s ==> !y1...ym. t ==> !z1...zk. u
irule produces a tactic that reduces a goal whose conclusion u' is a
substitution and/or type instance of u to the corresponding instances
of s and of t. Any variables free in s or t but not in u will
be existentially quantified in the resulting subgoal, and a variable
free in both s and t will result in a subgoal which is s /\ t,
existentially quantified
The following diagram is simplified: more implications and quantified variables than shown are allowed.
A ?- u'
========================= irule (A' |- !x. s ==> !y. t ==> u)
A ?- (?z. s') /\ ?w. t'
where z and w are (type instances of) variables among x, y that
do not occur free in s, t. The assumptions A', instantiated, are
added as further new subgoals.
Failure
Fails unless the theorem, when stripped of universal quantification and antecedents of implications, can be instantiated to match the goal.
Comments
The supplied theorem is pre-processed using IRULE_CANON, which removes
the universal quantifiers and antecedents of implications, and
existentially quantifies variables which were instantiated but appeared
only in the antecedents of implications.
Then MATCH_MP_TAC or MATCH_ACCEPT_TAC is applied (depending on
whether or not the result of the preprocessing is an implication). To
avoid preprocessing entirely, one can use prim_irule.
Example
With goal R a (f b) and theorem thm being
|- !x u. P u x ==> !w y. Q w x y ==> R x (f y)
the proof step e (irule thm) gives new goal
(?u. P u a) /\ ?w. Q w a b.
With goal a = b and theorem trans
|- !x y. (x = y) ==> !z. (y = z) ==> (x = z)
the proof step e (irule trans) gives new goal
?y. (a = y) /\ (y = b)
See also
Tactic.irule_at,
Tactic.MATCH_MP_TAC,
Tactic.prim_irule,
Drule.IRULE_CANON