PRESIMP_CONV : conv

SYNOPSIS
Applies basic propositional simplifications and some miniscoping.

DESCRIPTION
The conversion PRESIMP_CONV applies various routine simplifications to Boolean terms involving constants, e.g. p /\ T <=> p. It also tries to push universal quantifiers through conjunctions and existential quantifiers through disjunctions, e.g. (?x. p[x] \/ q[x]) <=> (?x. p[x]) \/ (?x. q[x]) (``miniscoping'') but does not transform away other connectives like implication that would allow it do do this more completely.

FAILURE CONDITIONS
Never fails.

EXAMPLE
  # PRESIMP_CONV `?x. x = 1 /\ y = 1 \/ F \/ T /\ y = 2`;;
  val it : thm =
    |- (?x. x = 1 /\ y = 1 \/ F \/ T /\ y = 2) <=>
       (?x. x = 1) /\ y = 1 \/ y = 2

USES
Useful as an initial simplification before more substantial normal form conversions.

SEE ALSO
CNF_CONV, DNF_CONV, MINISCOPE_CONV, NNF_CONV, PRENEX_CONV, SKOLEM_CONV.