		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-block-item-declon

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

Signature
(xeq-block-item-declon declon declon-new declon-thm-name info vartys-post gin) → (mv item gout)
Arguments: declon — Guard (declonp declon).; declon-new — Guard (declonp declon-new).; declon-thm-name — Guard (symbolp declon-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-declon

(defun xeq-block-item-declon
       (declon declon-new
               declon-thm-name info vartys-post gin)
 (declare (xargs :guard (and (declonp declon)
                             (declonp declon-new)
                             (symbolp declon-thm-name)
                             (c::ident-type-mapp vartys-post)
                             (ginp gin))))
 (declare (xargs :guard (and (declon-unambp declon)
                             (declon-annop declon)
                             (declon-unambp declon-new)
                             (declon-annop declon-new))))
 (let ((__function__ 'xeq-block-item-declon))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (item (make-block-item-declon :declon declon
                                  :info info))
    (item-new (make-block-item-declon :declon declon-new
                                      :info info))
    (gout-no-thm (change-gout (gout-no-thm gin)
                              :vartys vartys-post))
    ((unless declon-thm-name)
     (mv item-new gout-no-thm))
    ((mv & old-declon)
     (ldm-declon-obj declon))
    ((mv & new-declon)
     (ldm-declon-obj declon-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-declon-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons declon-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'block-item-declon-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-declon-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-declon.item

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

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

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

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

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

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

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

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

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