1\DOC AC_CONV
2
3\TYPE {AC_CONV : (thm * thm) -> conv}
4
5\SYNOPSIS
6Proves equality of terms using associative and commutative laws.
7
8\KEYWORDS
9conversion,associative, commutative.
10
11\DESCRIBE
12Suppose {_} is a function, which is assumed to be infix in the following
13syntax, and {ath} and {cth} are theorems expressing its associativity and
14commutativity; they must be of the following form, except that any free
15variables may have arbitrary names and may be universally quantified:
16{
17   ath = |- m _ (n _ p) = (m _ n) _ p
18   cth = |- m _ n = n _ m
19}
20Then the conversion {AC_CONV(ath,cth)} will prove equations whose
21left and right sides can be made identical using these associative and
22commutative laws.
23
24\FAILURE
25Fails if the associative or commutative law has an invalid form, or if the
26term is not an equation between AC-equivalent terms.
27
28\EXAMPLE
29Consider the terms {x + SUC t + ((3 + y) + z)} and {3 + SUC t + x + y + z}.
30{AC_CONV} proves them equal.
31{
32   - AC_CONV(ADD_ASSOC,ADD_SYM)
33       (Term `x + (SUC t) + ((3 + y) + z) = 3 + (SUC t) + x + y + z`);
34
35   > val it =
36     |- (x + ((SUC t) + ((3 + y) + z)) = 3 + ((SUC t) + (x + (y + z)))) = T
37}
38
39
40\COMMENTS
41Note that the preproved associative and commutative laws for the operators {+},
42{*}, {/\} and {\/} are already in the right form to give to {AC_CONV}.
43
44\SEEALSO
45Conv.SYM_CONV.
46\ENDDOC
47