		Search-engine friendly clone of the ACL2 documentation.

Defthm-commutative

Introduce a commutativity theorem.

General form:

(defthm-commutative name op :hints ...)

name must be a symbol that names the new theorem.
op must be a symbol that names an existing binary operation, whose (unconditional) commutativity the new theorem asserts.
:hints, if present, must consist of hints of the kind use in defthm. These hints are used to prove the commutative theorem.

More customization options may be added in the future.

The new theorem's variables are `x' and `y', in the same package as op, unless op is the "COMMON-LISP" package, in which case the variables are in the "ACL2" package.

Macro: defthm-commutative

(defmacro
 defthm-commutative (name op &key hints)
 (declare (xargs :guard (and (symbolp name) (symbolp op))))
 (let*
  ((var-pkg (fix-pkg (symbol-package-name op)))
   (x (intern$ "X" var-pkg))
   (y (intern$ "Y" var-pkg)))
  (cons
      'defthm
      (cons name
            (cons (cons 'equal
                        (cons (cons op (cons x (cons y 'nil)))
                              (cons (cons op (cons y (cons x 'nil)))
                                    'nil)))
                  (cons ':hints (cons hints 'nil)))))))