----------------------------------------------------------------------
RES_CANON                                                      (Drule)
----------------------------------------------------------------------
RES_CANON : (thm -> thm list)

SYNOPSIS
Put an implication into canonical form for resolution.

KEYWORDS
rule, resolution, implication, canonical.

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

USES
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.

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

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