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

SYNOPSIS
Puts theorem into a ‘canonical’ form.

KEYWORDS
rule, canonical, implication.

DESCRIBE
{IMP_CANON} puts a theorem in ‘canonical’ form by removing quantifiers
and breaking apart conjunctions, as well as disjunctions which form the
antecedent of implications. It applies the following transformation rules:

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

        A |- (t1 \/ t2) ==> t              A |- (?x. t1) ==> t2
   -------------------------------        ----------------------
    A |- t1 ==> t   A |- t2 ==> t          A |- t1[x'/x] ==> t2




FAILURE
Never fails, but if there is no scope for one of the above reductions,
merely gives a list whose only member is the original theorem.

COMMENTS
This is a rather ad-hoc inference rule, and its use is not recommended.

SEEALSO
Thm.CONJUNCT1, Thm.CONJUNCT2, Drule.CONJUNCTS, Thm.DISJ1, Thm.DISJ2,
Thm.EXISTS, Thm.SPEC.

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