Tactic.drule

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

COMMENTS

The drule tactic is similar to, but a great deal more controlled than, the IMP_RES_TAC tactic, which will look for a great many more possible instantiations and resolutions to perform. IMP_RES_TAC also puts all of its derived consequences into the assumption list; drule can be sure that there will be just one such consequence, and puts this into the goal directly.

The related dxrule tactic removes the matching assumption from the assumption list. In this example above, the resulting assumption list would just contain 1 < x, having lost the 0 < y which was resolved against the DIV_LESS theorem.

The drule tactic uses the MP_TAC thm_tactic as its fixed continuation; the drule_then variation takes a thm_tactic continuation as its first parameter and applies this to the result of the instantiation and MP call. There is also a dxrule_then, that combines both variations described here.

Finally, note that the implicational theorem may itself have come from the goal’s assumptions, extracted with tools such as FIRST_ASSUM and PAT_ASSUM.

SEEALSO

drule_all, IMP_RES_TAC