----------------------------------------------------------------------
drule_all                                                     (Tactic)
----------------------------------------------------------------------
drule_all : thm -> tactic

SYNOPSIS
Attempts to discharge all of a theorem’s antecedents from assumptions

KEYWORDS
tactic, resolution.

DESCRIBE
If {th} is a theorem with a conclusion that is a (possibly universally
quantified) implication (or negation), the theorem-tactic {drule_all}
(implicitly) normalises it have form

    !v1 .. vn. P1 ==> (P2 ==> (P3 ==> ... Q)...)

where each {Pi} is not a conjunction. (In other words, {P /\ Q ==> R}
is normalised to {P ==> (Q ==> R)}.) An application of {drule_all th}
to a goal then attempts to find a consistent instantiation so that all
of the {Pi} antecedents can be discharged by appeal to the goal’s
assumptions. If this repeated instantiation and use of {MP} is
possible, then the (instantiated) conclusion {Q} is added to the goal
with the {MP_TAC} {thm_tactic}.

When finding assumptions, those that have been most recently added to
the assumption list will be preferred.

FAILURE
An invocation of {drule_all th} can only fail when applied to a goal.
It can then fail if {th} is not an implication, or if all of {th}’s
implications cannot be eliminated by matching against the goal’s
assumptions.

EXAMPLE
The {LESS_LESS_EQ_TRANS} theorem states:

   !m n p. m < n /\ n <= p ==> m < p

Then:

   > drule_all arithmeticTheory.LESS_LESS_EQ_TRANS
      ([“x < w”, “1 < x”, “z <= y”, “x <= z”, “y < z”], “P:bool”);
   val it =
      ([([“x < w”, “1 < x”, “z <= y”, “x <= z”, “y < z”],
         “1 < z ==> P”)], fn): goal list * validation

Note how the other possible instance of the theorem (chaining {y < z}
and {z <= y}) is not found.

COMMENTS
The variant {dxrule_all} removes used assumptions from the assumption
list as they resolve against the theorem. The variant {drule_all_then}
allows a continuation other than {MP_TAC} to be used. The variant
{dxrule_all_then} combines both.

SEEALSO
Tactic.drule, Tactic.IMP_RES_TAC.

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