		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-block-item-decl

Equality lifting transformation of a block item that consists of a declaration.

Signature
(xeq-block-item-decl decl decl-new decl-thm-name info vartys-post gin) → (mv item gout)
Arguments: decl — Guard (declp decl).; decl-new — Guard (declp decl-new).; decl-thm-name — Guard (symbolp decl-thm-name).; vartys-post — Guard (c::ident-type-mapp vartys-post).; gin — Guard (ginp gin).
Returns: item — Type (block-itemp item).; gout — Type (goutp gout).

We put the new declaration into a block item.

Definitions and Theorems

Function: xeq-block-item-decl

(defun xeq-block-item-decl (decl decl-new
                                 decl-thm-name info vartys-post gin)
 (declare (xargs :guard (and (declp decl)
                             (declp decl-new)
                             (symbolp decl-thm-name)
                             (c::ident-type-mapp vartys-post)
                             (ginp gin))))
 (declare (xargs :guard (and (decl-unambp decl)
                             (decl-annop decl)
                             (decl-unambp decl-new)
                             (decl-annop decl-new))))
 (let ((__function__ 'xeq-block-item-decl))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (item (make-block-item-decl :decl decl
                                :info info))
    (item-new (make-block-item-decl :decl decl-new
                                    :info info))
    (gout-no-thm (change-gout (gout-no-thm gin)
                              :vartys vartys-post))
    ((unless decl-thm-name)
     (mv item-new gout-no-thm))
    ((mv & old-declon) (ldm-decl-obj decl))
    ((mv & new-declon)
     (ldm-decl-obj decl-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::block-item-declon)
            (:e c::block-item-kind)
            (:e c::block-item-declon->get)
            (:e insert)
            c::compustate-frames-number-of-exec-obj-declon
            c::compustatep-when-compustate-resultp-and-not-errorp
            block-item-decl-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons decl-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'block-item-decl-congruence
               (cons
                (cons 'old-declon
                      (cons (cons 'quote (cons old-declon 'nil))
                            'nil))
                (cons
                    (cons 'new-declon
                          (cons (cons 'quote (cons new-declon 'nil))
                                'nil))
                    'nil))))
             (cons
              (cons
               ':instance
               (cons
                'block-item-decl-errors
                (cons
                    (cons 'declon
                          (cons (cons 'quote (cons old-declon 'nil))
                                'nil))
                    '((fenv old-fenv)))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-block-item-thm item item-new gin.vartys vartys-post
                         gin.const-new gin.thm-index hints)))
   (mv item-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys vartys-post)))))

Theorem: block-itemp-of-xeq-block-item-decl.item

(defthm block-itemp-of-xeq-block-item-decl.item
  (b* (((mv ?item ?gout)
        (xeq-block-item-decl decl decl-new
                             decl-thm-name info vartys-post gin)))
    (block-itemp item))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-block-item-decl.gout

(defthm goutp-of-xeq-block-item-decl.gout
  (b* (((mv ?item ?gout)
        (xeq-block-item-decl decl decl-new
                             decl-thm-name info vartys-post gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: block-item-unambp-of-xeq-block-item-decl

(defthm block-item-unambp-of-xeq-block-item-decl
 (implies
    (decl-unambp decl-new)
    (b* (((mv ?item ?gout)
          (xeq-block-item-decl decl decl-new
                               decl-thm-name info vartys-post gin)))
      (block-item-unambp item))))

Theorem: block-item-annop-of-xeq-block-item-decl

(defthm block-item-annop-of-xeq-block-item-decl
 (implies
    (decl-annop decl-new)
    (b* (((mv ?item ?gout)
          (xeq-block-item-decl decl decl-new
                               decl-thm-name info vartys-post gin)))
      (block-item-annop item))))

Theorem: block-item-aidentp-of-xeq-block-item-decl

(defthm block-item-aidentp-of-xeq-block-item-decl
 (implies
    (decl-aidentp decl-new gcc)
    (b* (((mv ?item ?gout)
          (xeq-block-item-decl decl decl-new
                               decl-thm-name info vartys-post gin)))
      (block-item-aidentp item gcc))))