		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Equate-expressions

Construct an equality between two expressions.

Signature
(equate-expressions left right) → equality
Arguments: left — Guard (expressionp left).; right — Guard (expressionp right).
Returns: equality — Type (expressionp equality).

Definitions and Theorems

Function: equate-expressions

(defun equate-expressions (left right)
  (declare (xargs :guard (and (expressionp left)
                              (expressionp right))))
  (let ((__function__ 'equate-expressions))
    (declare (ignorable __function__))
    (make-expression-binary :operator (binary-op-eq)
                            :left-operand left
                            :right-operand right)))

Theorem: expressionp-of-equate-expressions

(defthm expressionp-of-equate-expressions
  (b* ((equality (equate-expressions left right)))
    (expressionp equality))
  :rule-classes :rewrite)

Theorem: equate-expressions-of-expression-fix-left

(defthm equate-expressions-of-expression-fix-left
  (equal (equate-expressions (expression-fix left)
                             right)
         (equate-expressions left right)))

Theorem: equate-expressions-expression-equiv-congruence-on-left

(defthm equate-expressions-expression-equiv-congruence-on-left
  (implies (expression-equiv left left-equiv)
           (equal (equate-expressions left right)
                  (equate-expressions left-equiv right)))
  :rule-classes :congruence)

Theorem: equate-expressions-of-expression-fix-right

(defthm equate-expressions-of-expression-fix-right
  (equal (equate-expressions left (expression-fix right))
         (equate-expressions left right)))

Theorem: equate-expressions-expression-equiv-congruence-on-right

(defthm equate-expressions-expression-equiv-congruence-on-right
  (implies (expression-equiv right right-equiv)
           (equal (equate-expressions left right)
                  (equate-expressions left right-equiv)))
  :rule-classes :congruence)