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.