		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-expr-binary

Transform a binary expression.

Signature
(simpadd0-expr-binary op arg1 arg1-new arg1-thm-name arg2 arg2-new arg2-thm-name info gin) → (mv expr gout)
Arguments: op — Guard (binopp op).; arg1 — Guard (exprp arg1).; arg1-new — Guard (exprp arg1-new).; arg1-thm-name — Guard (symbolp arg1-thm-name).; arg2 — Guard (exprp arg2).; arg2-new — Guard (exprp arg2-new).; arg2-thm-name — Guard (symbolp arg2-thm-name).; info — Guard (expr-binary-infop info).; gin — Guard (ginp gin).
Returns: expr — Type (exprp expr).; gout — Type (goutp gout).

First, we lift the equalities of the sub-expressions to an equality for the binary expression. Then we check whether the resulting binary expression has the form E + 0, with E of type int and 0 the int octal 0 without leading zeros, in which case the resulting expression is just E; the theorem that lifts equality is used to prove the equality of the original expression to E.

The proof for the original-to-simplified theorem makes use of the supporting theorem simpadd0-expr+zero-to-expr, which says that E + 0, with E of type int, is semantically equivalent to E. The hypothesis that E has type int is discharged via the theorem arg1-thm-name; we only need the type part of it in the proof; to discharge that theorem's hypothesis that E does not error, we also need an instance of expr-binary-pure-strict-errors (of which we only really need the part for the first argument). To apply simpadd0-expr+zero-to-expr, which includes the hypothesis that E does not yield an error with limit, we use c::exec-expr-limit-monotone from c::exec-monotone to derive that hypothesis from the fact that E does not yield an error with (1- limit), which in turn is obtained from the hypothesis that E + 0 does not yield an error with limit. We also need the theorem for the lifted equality, i.e. gout.thm-name. We enable the executable counterparts of various functions so that things match up in the proof; in particular, we need to reduce the (c::expr-const ...) in the theorem simpadd0-expr+zero-to-expr to a quoted constant.

Definitions and Theorems

Function: simpadd0-expr-binary

(defun simpadd0-expr-binary
       (op arg1 arg1-new arg1-thm-name
           arg2 arg2-new arg2-thm-name info gin)
 (declare (xargs :guard (and (binopp op)
                             (exprp arg1)
                             (exprp arg1-new)
                             (symbolp arg1-thm-name)
                             (exprp arg2)
                             (exprp arg2-new)
                             (symbolp arg2-thm-name)
                             (expr-binary-infop info)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp arg1)
                             (expr-annop arg1)
                             (expr-unambp arg1-new)
                             (expr-annop arg1-new)
                             (expr-unambp arg2)
                             (expr-annop arg2)
                             (expr-unambp arg2-new)
                             (expr-annop arg2-new))))
 (let ((__function__ 'simpadd0-expr-binary))
  (declare (ignorable __function__))
  (b*
   (((mv expr-new (gout gout))
     (xeq-expr-binary op arg1 arg1-new arg1-thm-name
                      arg2 arg2-new arg2-thm-name info gin))
    (simpp (and (binop-case op :add)
                (type-case (expr-type arg1-new) :sint)
                (expr-zerop arg2-new)))
    ((when (not simpp)) (mv expr-new gout))
    (expr-new-simp (expr-fix arg1-new))
    ((unless gout.thm-name)
     (mv expr-new-simp gout))
    ((gin gin) (gin-update gin gout))
    (expr (make-expr-binary :op op
                            :arg1 arg1
                            :arg2 arg2
                            :info info))
    ((mv & cexpr-new-simp)
     (ldm-expr expr-new-simp))
    ((mv & czero) (ldm-expr arg2-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::iconst-length-none)
            (:e c::iconst-base-oct)
            (:e c::iconst)
            (:e c::const-int)
            (:e c::expr-const)
            (:e c::binop-add)
            (:e c::expr-binary)
            (:e c::type-sint)
            (:e c::binop-strictp)
            (:e c::expr-purep)
            (:e c::binop-purep)
            expr-compustate-vars nfix)
         (cons
          ':use
          (cons
           (cons
            gout.thm-name
            (cons
             (cons
              ':instance
              (cons
               'simpadd0-expr+zero-to-expr
               (cons
                (cons 'expr
                      (cons (cons 'quote (cons cexpr-new-simp 'nil))
                            'nil))
                '((fenv old-fenv)))))
             (cons
              arg1-thm-name
              (cons
               (cons
                ':instance
                (cons
                 'expr-binary-pure-strict-errors
                 (cons
                  (cons
                      'op
                      (cons (cons 'quote (cons (c::binop-add) 'nil))
                            'nil))
                  (cons
                   (cons
                      'arg1
                      (cons (cons 'quote (cons cexpr-new-simp 'nil))
                            'nil))
                   (cons (cons 'arg2
                               (cons (cons 'quote (cons czero 'nil))
                                     'nil))
                         '((fenv old-fenv)))))))
               (cons
                (cons
                 ':instance
                 (cons
                  'c::exec-expr-limit-monotone
                  (cons
                   (cons
                      'e
                      (cons (cons 'quote (cons cexpr-new-simp 'nil))
                            'nil))
                   '((compst compst)
                     (fenv old-fenv)
                     (limit (1- limit))
                     (limit1 limit)))))
                'nil)))))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-expr-thm expr expr-new-simp gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv expr-new-simp
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: exprp-of-simpadd0-expr-binary.expr

(defthm exprp-of-simpadd0-expr-binary.expr
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
   (exprp expr))
 :rule-classes :rewrite)

Theorem: goutp-of-simpadd0-expr-binary.gout

(defthm goutp-of-simpadd0-expr-binary.gout
 (b* (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
   (goutp gout))
 :rule-classes :rewrite)

Theorem: expr-unambp-of-simpadd0-expr-binary

(defthm expr-unambp-of-simpadd0-expr-binary
 (implies
   (and (expr-unambp arg1-new)
        (expr-unambp arg2-new))
   (b*
     (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
     (expr-unambp expr))))

Theorem: expr-annop-of-simpadd0-expr-binary

(defthm expr-annop-of-simpadd0-expr-binary
 (implies
   (and (expr-annop arg1-new)
        (expr-annop arg2-new)
        (expr-binary-infop info))
   (b*
     (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
     (expr-annop expr))))

Theorem: expr-aidentp-of-simpadd0-expr-binary

(defthm expr-aidentp-of-simpadd0-expr-binary
 (implies
   (and (expr-aidentp arg1-new gcc)
        (expr-aidentp arg2-new gcc))
   (b*
     (((mv ?expr ?gout)
       (simpadd0-expr-binary op arg1 arg1-new arg1-thm-name
                             arg2 arg2-new arg2-thm-name info gin)))
     (expr-aidentp expr gcc))))

Theorem: simpadd0-expr+zero-to-expr

(defthm simpadd0-expr+zero-to-expr
 (b*
  ((zero
       (c::expr-const
            (c::const-int
                 (c::make-iconst :value 0
                                 :base (c::iconst-base-oct)
                                 :unsignedp nil
                                 :length (c::iconst-length-none)))))
   (expr+zero (c::expr-binary (c::binop-add)
                              expr zero))
   ((mv expr-eval expr-compst)
    (c::exec-expr expr compst fenv (1- limit)))
   (expr-val (c::expr-value->value expr-eval))
   ((mv expr+zero-eval expr+zero-compst)
    (c::exec-expr expr+zero compst fenv limit))
   (expr+zero-val (c::expr-value->value expr+zero-eval)))
  (implies (and (c::expr-purep expr)
                (not (c::errorp expr-eval))
                expr-eval
                (equal (c::type-of-value expr-val)
                       (c::type-sint)))
           (and (not (c::errorp expr+zero-eval))
                expr+zero-eval
                (equal expr+zero-val expr-val)
                (equal expr+zero-compst expr-compst)))))