RES_CANON

Drule.RES_CANON : (thm -> thm list)

Put an implication into canonical form for resolution.

All the HOL resolution tactics (e.g. IMP_RES_TAC) work by using modus ponens to draw consequences from an implicative theorem and the assumptions of the goal. Some of these tactics derive this implication from a theorem supplied explicitly the user (or otherwise from ‘outside’ the goal) and some obtain it from the assumptions of the goal itself. But in either case, the supplied theorem or assumption is first transformed into a list of implications in ‘canonical’ form by the function RES_CANON.

The theorem argument to RES_CANON should be either be an implication (which can be universally quantified) or a theorem from which an implication can be derived using the transformation rules discussed below. Given such a theorem, RES_CANON returns a list of implications in canonical form. It is the implications in this resulting list that are used by the various resolution tactics to infer consequences from the assumptions of a goal.

The transformations done by RES_CANON th to the theorem th are as follows. First, if th is a negation A |- ~t, this is converted to the implication A |- t ==> F. The following inference rules are then applied repeatedly, until no further rule applies. Conjunctions are split into their components and equivalence (boolean equality) is split into implication in both directions:

      A |- t1 /\ t2                         A |- t1 = t2
   --------------------           ----------------------------------
    A |- t1    A |- t2             A |- t1 ==> t2    A |- t2 ==> t1

Conjunctive antecedents are transformed by:

                A |- (t1 /\ t2) ==> t
   ---------------------------------------------------
    A |- t1 ==> (t2 ==> t)     A |- t2 ==> (t1 ==> t)

and disjunctive antecedents by:

        A |- (t1 \/ t2) ==> t
   --------------------------------
    A |- t1 ==> t    A |- t2 ==> t

The scope of universal quantifiers is restricted, if possible:

    A |- !x. t1 ==> t2
   --------------------         [if x is not free in t1]
    A |- t1 ==> !x. t2

and existentially-quantified antecedents are eliminated by:

      A |- (?x. t1) ==> t2
   ---------------------------  [x' chosen so as not to be free in t2]
    A |- !x'. t1[x'/x] ==> t2

Finally, when no further applications of the above rules are possible, and the theorem is an implication:

   A |- !x1...xn. t1 ==> t2

then the theorem A u {t1} |- t2 is transformed by a recursive application of RES_CANON to get a list of theorems:

   [A u {t1} |- t21 , ... , A u {t1} |- t2n]

and the result of discharging t1 from these theorems:

   [A |- !x1...xn. t1 ==> t21 , ... , A |- !x1...xn. t1 ==> t2n]

is returned. That is, the transformation rules are recursively applied to the conclusions of all implications.

Failure

RES_CANON th fails if no implication(s) can be derived from th using the transformation rules shown above.

Example

The uniqueness of the remainder k MOD n is expressed in HOL by the built-in theorem MOD_UNIQUE:

   |- !n k r. (?q. (k = (q * n) + r) /\ r < n) ==> (k MOD n = r)

For this theorem, the canonical list of implications returned by RES_CANON is as follows:

   - RES_CANON MOD_UNIQUE;
   > val it =
       [|- !r n q k. (k = q * n + r) ==> r < n ==> (k MOD n = r),
        |- !n r. r < n ==> !q k. (k = q * n + r) ==> (k MOD n = r)] : thm list

The existentially-quantified, conjunctive, antecedent has given rise to two implications, and the scope of universal quantifiers has been restricted to the conclusions of the resulting implications wherever possible.

The primary use of RES_CANON is for the (internal) pre-processing phase of the built-in resolution tactics IMP_RES_TAC, IMP_RES_THEN, RES_TAC, and RES_THEN. But the function RES_CANON is also made available at top-level so that users can call it to see the actual form of the implications used for resolution in any particular case.

See also

Tactic.IMP_RES_TAC, Thm_cont.IMP_RES_THEN, Tactic.RES_TAC, Thm_cont.RES_THEN