defthm-commutative

(in-package "ACL2")

(defmacro+ defthm-commutative
  (name op &key hints)
  (declare (xargs :guard (and (symbolp name) (symbolp op))))
  :parents (std/util)
  :short "Introduce a commutativity theorem."
  :long (topstring (p "General form:")
    (codeblock "(defthm-commutative name op :hints ...)")
    (ul (li "@('name') must be a symbol that names the new theorem.")
      (li "@('op') must be a symbol that names an existing binary operation,
      whose (unconditional) commutativity the new theorem asserts.")
      (li "@(':hints'), if present, must consist of hints
      of the kind use in @(tsee defthm).
      These hints are used to prove the commutative theorem."))
    (p "More customization options may be added in the future.")
    (p "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."))
  (let* ((var-pkg (fix-pkg (symbol-package-name op))) (x (intern$ "X" var-pkg))
      (y (intern$ "Y" var-pkg)))
    `(defthm ,NAME (equal (,OP ,X ,Y) (,OP ,Y ,X)) :hints ,HINTS)))