		Search-engine friendly clone of the ACL2 documentation.

Abstract-syntax-operations

Negate-expression

Negate an expression.

Signature
(negate-expression expr) → negated-expr
Arguments: expr — Guard (expressionp expr).
Returns: negated-expr — Type (expressionp negated-expr).

The argument expression should be boolean-valued in order for the resulting expression to make sense. We apply the unary boolean negation operator to the expression, but we simplify the resulting expression as follows, when possible:

If the argument expression is a boolean literal, we flip it.
If the argument expression starts with the boolean negation operator, we simply remove the operator (double negation cancels).
If the argument expression starts with an equality or ordering operator, we change the operator to its negation.

Other simplifications could be done, but for now we limit ourselves to the ones above.

Definitions and Theorems

Function: negate-expression

(defun negate-expression (expr)
 (declare (xargs :guard (expressionp expr)))
 (let ((__function__ 'negate-expression))
  (declare (ignorable __function__))
  (expression-case
   expr
   :literal
   (literal-case
    expr.get
    :boolean
    (expression-literal (literal-boolean (not expr.get.value)))
    :character
    (prog2$
     (raise
      "Internal error: ~
                                        applying boolean negation to ~x0."
      expr.get)
     (expression-fix expr))
    :string
    (prog2$
     (raise
      "Internal error: ~
                                     applying boolean negation to ~x0."
      expr.get)
     (expression-fix expr))
    :integer
    (prog2$
     (raise
      "Internal error: ~
                                      applying boolean negation to ~x0."
      expr.get)
     (expression-fix expr)))
   :variable (make-expression-unary :operator (unary-op-not)
                                    :operand expr)
   :unary
   (unary-op-case
    expr.operator
    :not expr.operand
    :minus
    (prog2$
     (raise
      "Internal error: ~
                                  applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr)))
   :binary
   (binary-op-case
    expr.operator
    :eq (make-expression-binary :operator (binary-op-ne)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :ne (make-expression-binary :operator (binary-op-eq)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :lt (make-expression-binary :operator (binary-op-ge)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :le (make-expression-binary :operator (binary-op-gt)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :gt (make-expression-binary :operator (binary-op-le)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :ge (make-expression-binary :operator (binary-op-lt)
                                :left-operand expr.left-operand
                                :right-operand expr.right-operand)
    :and (make-expression-unary :operator (unary-op-not)
                                :operand expr)
    :or (make-expression-unary :operator (unary-op-not)
                               :operand expr)
    :implies (make-expression-unary :operator (unary-op-not)
                                    :operand expr)
    :implied (make-expression-unary :operator (unary-op-not)
                                    :operand expr)
    :iff (make-expression-unary :operator (unary-op-not)
                                :operand expr)
    :add
    (prog2$
     (raise
      "Internal error: ~
                                 applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr))
    :sub
    (prog2$
     (raise
      "Internal error: ~
                                 applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr))
    :mul
    (prog2$
     (raise
      "Internal error: ~
                                 applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr))
    :div
    (prog2$
     (raise
      "Internal error: ~
                                 applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr))
    :rem
    (prog2$
     (raise
      "Internal error: ~
                                 applying boolean negation to ~x0."
      (expression-fix expr))
     (expression-fix expr)))
   :if (make-expression-unary :operator (unary-op-not)
                              :operand expr)
   :when (make-expression-unary :operator (unary-op-not)
                                :operand expr)
   :unless (make-expression-unary :operator (unary-op-not)
                                  :operand expr)
   :cond (make-expression-unary :operator (unary-op-not)
                                :operand expr)
   :call (make-expression-unary :operator (unary-op-not)
                                :operand expr)
   :multi (make-expression-unary :operator (unary-op-not)
                                 :operand expr)
   :component (make-expression-unary :operator (unary-op-not)
                                     :operand expr)
   :bind (make-expression-unary :operator (unary-op-not)
                                :operand expr)
   :product-construct
   (make-expression-unary :operator (unary-op-not)
                          :operand expr)
   :product-field (make-expression-unary :operator (unary-op-not)
                                         :operand expr)
   :product-update (make-expression-unary :operator (unary-op-not)
                                          :operand expr)
   :sum-construct (make-expression-unary :operator (unary-op-not)
                                         :operand expr)
   :sum-field (make-expression-unary :operator (unary-op-not)
                                     :operand expr)
   :sum-update (make-expression-unary :operator (unary-op-not)
                                      :operand expr)
   :sum-test (make-expression-unary :operator (unary-op-not)
                                    :operand expr)
   :bad-expression (make-expression-unary :operator (unary-op-not)
                                          :operand expr))))

Theorem: expressionp-of-negate-expression

(defthm expressionp-of-negate-expression
  (b* ((negated-expr (negate-expression expr)))
    (expressionp negated-expr))
  :rule-classes :rewrite)

Theorem: negate-expression-of-expression-fix-expr

(defthm negate-expression-of-expression-fix-expr
  (equal (negate-expression (expression-fix expr))
         (negate-expression expr)))

Theorem: negate-expression-expression-equiv-congruence-on-expr

(defthm negate-expression-expression-equiv-congruence-on-expr
  (implies (expression-equiv expr expr-equiv)
           (equal (negate-expression expr)
                  (negate-expression expr-equiv)))
  :rule-classes :congruence)