AC : thm -> thm -> thm
STRUCTURE
simpLib
SYNOPSIS
Packages associativity and commutativity theorems for use in the simplifier.
DESCRIPTION
The AC function combines an associativity and commutativity theorem. The resulting theorem can be passed to the simplifier as if a rewrite, but will rather be used by the simplifier as the basis for performing AC-normalisation.

The theorems can be combined in either order, can be partly generalised, and need not express associativity in any particular direction from left to right.

FAILURE
AC never fails, but if applied to theorems that are not of the required form, the simplifier will raise an exception when it attempts to use the result.
EXAMPLE
- SIMP_CONV bool_ss [AC ADD_COMM ADD_ASSOC] ``3 + x + y + 1``;
> val it = |- 3 + x + y + 1 = x + (y + (1 + 3)) : thm

- SIMP_CONV bool_ss [AC (GSYM ADD_ASSOC) ADD_COMM] ``x + 1 + y + 3``;
> val it = |- x + 1 + y + 3 = x + (y + (1 + 3)) : thm
SEEALSO
SSFRAG
HOL  Kananaskis-13