Drule.IMP

STRUCTURE

SYNOPSIS

Puts theorem into a ‘canonical’ form.

DESCRIPTION

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

CONJUNCT1, CONJUNCT2, CONJUNCTS, DISJ1, DISJ2, EXISTS, SPEC