1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
|
\DOC PRESIMP_CONV
\TYPE {PRESIMP_CONV : conv}
\SYNOPSIS
Applies basic propositional simplifications and some miniscoping.
\DESCRIBE
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
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.
\SEEALSO
CNF_CONV, DNF_CONV, NNF_CONV, PRENEX_CONV, SKOLEM_CONV.
\ENDDOC
|
