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.