----------------------------------------------------------------------
irule                                                         (Tactic)
----------------------------------------------------------------------
irule : thm_tactic

SYNOPSIS
Reduces the goal using a supplied implication, with matching.

KEYWORDS
tactic, modus ponens, implication.

DESCRIBE
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)


SEEALSO
Tactic.MATCH_MP_TAC, Tactic.prim_irule, Drule.IRULE_CANON.

----------------------------------------------------------------------