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
39
|
\DOC bool_EQ_CONV
\TYPE {bool_EQ_CONV : conv}
\SYNOPSIS
Simplifies expressions involving boolean equality.
\KEYWORDS
conversion.
\DESCRIBE
The conversion {bool_EQ_CONV} simplifies equations of the form {"t1 = t2"},
where {t1} and {t2} are of type {:bool}. When applied to a term of the form
{"t = t"}, the conversion {bool_EQ_CONV} returns the theorem
{
|- (t = t) = T
}
\noindent When applied to a term of the form {"t = T"}, the conversion returns
{
|- (t = T) = t
}
\noindent And when applied to a term of the form {"T = t"}, it returns
{
|- (T = t) = t
}
\FAILURE
Fails unless applied to a term of the form {"t1 = t2"}, where {t1} and {t2} are
boolean, and either {t1} and {t2} are syntactically identical terms or one of
{t1} and {t2} is the constant {"T"}.
\EXAMPLE
{
#bool_EQ_CONV "T = F";;
|- (T = F) = F
#bool_EQ_CONV "(0 < n) = T";;
|- (0 < n = T) = 0 < n
}
\ENDDOC
|
