		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-expr-unary

Equality lifting transformation of a unary expression.

Signature
(xeq-expr-unary op arg arg-new arg-thm-name info gin) → (mv expr gout)
Arguments: op — Guard (unopp op).; arg — Guard (exprp arg).; arg-new — Guard (exprp arg-new).; arg-thm-name — Guard (symbolp arg-thm-name).; info — Guard (expr-unary-infop info).; gin — Guard (ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (goutp gout).

The resulting expression is obtained by combining the unary operator with the possibly transformed argument expression.

We generate a theorem iff a theorem was generated for the argument expression and the unary operator is among +, -, ~ and !. The argument expression may be pure or not.

Definitions and Theorems

Function: xeq-expr-unary

(defun xeq-expr-unary (op arg arg-new arg-thm-name info gin)
 (declare (xargs :guard (and (unopp op)
                             (exprp arg)
                             (exprp arg-new)
                             (symbolp arg-thm-name)
                             (expr-unary-infop info)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp arg)
                             (expr-annop arg)
                             (expr-unambp arg-new)
                             (expr-annop arg-new))))
 (let ((__function__ 'xeq-expr-unary))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (expr (make-expr-unary :op op
                           :arg arg
                           :info info))
    (expr-new (make-expr-unary :op op
                               :arg arg-new
                               :info info))
    ((unless (and arg-thm-name
                  (member-eq (unop-kind op)
                             '(:plus :minus :bitnot :lognot))))
     (mv expr-new (gout-no-thm gin)))
    ((mv & old-arg) (ldm-expr arg))
    ((mv & new-arg) (ldm-expr arg-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::unop-nonpointerp)
            (:e c::unop-kind)
            (:e c::expr-unary)
            (:e c::type-kind)
            (:e c::promote-type)
            (:e c::type-nonchar-integerp)
            (:e c::type-sint)
            (:e member-equal)
            expr-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons arg-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'expr-unary-congruence
               (cons
                (cons
                 'op
                 (cons
                     (cons 'quote
                           (cons (unop-case op
                                            :plus (c::unop-plus)
                                            :minus (c::unop-minus)
                                            :bitnot (c::unop-bitnot)
                                            :lognot (c::unop-lognot)
                                            :otherwise (impossible))
                                 'nil))
                     'nil))
                (cons
                 (cons 'old-arg
                       (cons (cons 'quote (cons old-arg 'nil))
                             'nil))
                 (cons (cons 'new-arg
                             (cons (cons 'quote (cons new-arg 'nil))
                                   'nil))
                       'nil)))))
             (cons
              (cons
               ':instance
               (cons
                'expr-unary-errors
                (cons
                 (cons
                  'op
                  (cons
                     (cons 'quote
                           (cons (unop-case op
                                            :plus (c::unop-plus)
                                            :minus (c::unop-minus)
                                            :bitnot (c::unop-bitnot)
                                            :lognot (c::unop-lognot)
                                            :otherwise (impossible))
                                 'nil))
                     'nil))
                 (cons (cons 'arg
                             (cons (cons 'quote (cons old-arg 'nil))
                                   'nil))
                       '((fenv old-fenv))))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-expr-thm expr expr-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: exprp-of-xeq-expr-unary.expr

(defthm exprp-of-xeq-expr-unary.expr
  (b* (((mv ?expr ?gout)
        (xeq-expr-unary op arg arg-new arg-thm-name info gin)))
    (exprp expr))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-expr-unary.gout

(defthm goutp-of-xeq-expr-unary.gout
  (b* (((mv ?expr ?gout)
        (xeq-expr-unary op arg arg-new arg-thm-name info gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: expr-unambp-of-xeq-expr-unary

(defthm expr-unambp-of-xeq-expr-unary
  (implies
       (expr-unambp arg-new)
       (b* (((mv ?expr ?gout)
             (xeq-expr-unary op arg arg-new arg-thm-name info gin)))
         (expr-unambp expr))))

Theorem: expr-annop-of-xeq-expr-unary

(defthm expr-annop-of-xeq-expr-unary
  (implies
       (and (expr-annop arg-new)
            (expr-unary-infop info))
       (b* (((mv ?expr ?gout)
             (xeq-expr-unary op arg arg-new arg-thm-name info gin)))
         (expr-annop expr))))

Theorem: expr-aidentp-of-xeq-expr-unary

(defthm expr-aidentp-of-xeq-expr-unary
  (implies
       (expr-aidentp arg-new gcc)
       (b* (((mv ?expr ?gout)
             (xeq-expr-unary op arg arg-new arg-thm-name info gin)))
         (expr-aidentp expr gcc))))