AC_CONV
Conv.AC_CONV : (thm * thm) -> conv
Proves equality of terms using associative and commutative laws.
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.