		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-initer-single

Equality lifting transformation of an initializer consisting of a single expression.

Signature
(xeq-initer-single expr expr-new expr-thm-name gin) → (mv initer gout)
Arguments: expr — Guard (exprp expr).; expr-new — Guard (exprp expr-new).; expr-thm-name — Guard (symbolp expr-thm-name).; gin — Guard (ginp gin).
Returns: initer — Type (initerp initer).; gout — Type (goutp gout).

Definitions and Theorems

Function: xeq-initer-single

(defun xeq-initer-single (expr expr-new expr-thm-name gin)
 (declare (xargs :guard (and (exprp expr)
                             (exprp expr-new)
                             (symbolp expr-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp expr)
                             (expr-annop expr)
                             (expr-unambp expr-new)
                             (expr-annop expr-new))))
 (let ((__function__ 'xeq-initer-single))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (initer (initer-single expr))
    (initer-new (initer-single expr-new))
    ((unless expr-thm-name)
     (mv initer-new (gout-no-thm gin)))
    ((mv & old-expr) (ldm-expr expr))
    ((mv & new-expr) (ldm-expr expr-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::initer-kind)
            (:e c::initer-single)
            (:e c::initer-single->get)
            (:e c::expr-kind)
            (:e c::expr-binary->op)
            (:e c::binop-kind)
            (:e c::type-nonchar-integerp)
            initer-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons expr-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'initer-single-congruence
               (cons
                (cons 'old-expr
                      (cons (cons 'quote (cons old-expr 'nil))
                            'nil))
                (cons (cons 'new-expr
                            (cons (cons 'quote (cons new-expr 'nil))
                                  'nil))
                      'nil))))
             (cons
              (cons
               ':instance
               (cons
                'initer-single-errors
                (cons (cons 'expr
                            (cons (cons 'quote (cons old-expr 'nil))
                                  'nil))
                      '((fenv old-fenv)))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-initer-single-thm initer initer-new gin.vartys
                            gin.const-new gin.thm-index hints)))
   (mv initer-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: initerp-of-xeq-initer-single.initer

(defthm initerp-of-xeq-initer-single.initer
  (b* (((mv ?initer ?gout)
        (xeq-initer-single expr expr-new expr-thm-name gin)))
    (initerp initer))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-initer-single.gout

(defthm goutp-of-xeq-initer-single.gout
  (b* (((mv ?initer ?gout)
        (xeq-initer-single expr expr-new expr-thm-name gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: initer-unambp-of-xeq-initer-single

(defthm initer-unambp-of-xeq-initer-single
  (implies
       (expr-unambp expr-new)
       (b* (((mv ?initer ?gout)
             (xeq-initer-single expr expr-new expr-thm-name gin)))
         (initer-unambp initer))))

Theorem: initer-annop-of-xeq-initer-single

(defthm initer-annop-of-xeq-initer-single
  (implies
       (expr-annop expr-new)
       (b* (((mv ?initer ?gout)
             (xeq-initer-single expr expr-new expr-thm-name gin)))
         (initer-annop initer))))

Theorem: initer-aidentp-of-xeq-initer-single

(defthm initer-aidentp-of-xeq-initer-single
  (implies
       (expr-aidentp expr-new gcc)
       (b* (((mv ?initer ?gout)
             (xeq-initer-single expr expr-new expr-thm-name gin)))
         (initer-aidentp initer gcc))))