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