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
35
36
37
38
|
\DOC AND_CONV
\TYPE {AND_CONV : conv}
\SYNOPSIS
Simplifies certain boolean conjunction expressions.
\LIBRARY reduce
\DESCRIBE
If {tm} corresponds to one of the forms given below, where {t} is an arbitrary
term of type {bool}, then {AND_CONV tm} returns the corresponding theorem. Note
that in the last case the conjuncts need only be alpha-equivalent rather than
strictly identical.
{
AND_CONV "T /\ t" = |- T /\ t = t
AND_CONV "t /\ T" = |- t /\ T = t
AND_CONV "F /\ t" = |- F /\ t = F
AND_CONV "t /\ F" = |- t /\ F = F
AND_CONV "t /\ t" = |- t /\ t = t
}
\FAILURE
{AND_CONV tm} fails unless {tm} has one of the forms indicated above.
\EXAMPLE
{
#AND_CONV "(x = T) /\ F";;
|- (x = T) /\ F = F
#AND_CONV "T /\ (x = T)";;
|- T /\ (x = T) = (x = T)
#AND_CONV "(?x. x=T) /\ (?y. y=T)";;
|- (?x. x = T) /\ (?y. y = T) = (?x. x = T)
}
\ENDDOC
|
