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
40
41
42
|
\DOC AC_CONV
\TYPE {AC_CONV : ((thm # thm) -> conv)}
\SYNOPSIS
Proves equality of terms using associative and commutative laws.
\KEYWORDS
conversion,associative, commutative.
\DESCRIBE
Suppose {_} is a function, which is assumed to be infix in the following syntax,
and {ath} and {cth} are theorems expressing its associativity and
commutativity; they must be of the following form, except that any free
variables may have arbitrary names and may be universally quantified:
{
ath = |- m _ (n _ p) = (m _ n) _ p
cth = |- m _ n = n _ m
}
\noindent Then the conversion {AC_CONV(ath,cth)} will prove equations whose
left and right sides can be made identical using these associative and
commutative laws.
\FAILURE
Fails if the associative or commutative law has an invalid form, or if the
term is not an equation between AC-equivalent terms.
\EXAMPLE
{
#AC_CONV(ADD_ASSOC,ADD_SYM)
# "x + (SUC t) + ((3 + y) + z) = 3 + (SUC t) + x + y + z";;
|- (x + ((SUC t) + ((3 + y) + z)) = 3 + ((SUC t) + (x + (y + z)))) = T
}
\COMMENTS
Note that the preproved associative and commutative laws for the operators {+},
{*}, {/\} and {\/} are already in the right form to give to {AC_CONV}.
\SEEALSO
SYM_CONV.
\ENDDOC
|
