`drule : thm -> tactic`
STRUCTURE
SYNOPSIS
Performs one step of resolution (or modus ponens) against implication theorem.
DESCRIPTION
If theorem th is of the form A |- t, where t is of the form !x1..xn. P .. /\ ... ==> Q or !x1..xn. P .. ==> Q, then a call to drule th (asl,g) looks for an assumption in asl that matches the pattern P .. in t. It then performs instantiation of th’s universally quantified and free variables, transforms any conjunctions on the left into a minimal number of chained implications, and calls MP once to generate a consequent theorem A |- t'. This theorem is then passed to MP_TAC, turning the goal into (asl, t' ==> g). (We assume that A is a subset of asl; otherwise the tactic is invalid.)
FAILURE
A call to drule th (asl,g) will fail if th is not a (possibly universally quantified) implication (or negation), or if there are no assumptions in asl matching the “first” hypothesis of th.
EXAMPLE
The DIV_LESS theorem states:
```   !n d. 0 < n /\ 1 < d ==> (n DIV d < n)
```
Then:
```   > drule arithmeticTheory.DIV_LESS ([“1 < x”, “0 < y”], “P:bool”);
val it =
([([“1 < x”, “0 < y”], “(!d. 1 < d ==> y DIV d < y) ==> P”)], fn):
goal list * validation
```