AC_CONV : (thm * thm) -> conv
STRUCTURE
Conv
SYNOPSIS
Proves equality of terms using associative and commutative laws.
DESCRIPTION
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
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
Consider the terms x + SUC t + ((3 + y) + z) and 3 + SUC t + x + y + z. AC_CONV proves them equal. 
   - AC_CONV(ADD_ASSOC,ADD_SYM)
       (Term `x + (SUC t) + ((3 + y) + z) = 3 + (SUC t) + x + y + z`);

   > val it =
     |- (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
HOL  Kananaskis-13