		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-block-item-stmt

Equality lifting transformation of a block items that consists of a statement.

Signature
(xeq-block-item-stmt stmt stmt-new stmt-thm-name info gin) → (mv item gout)
Arguments: stmt — Guard (stmtp stmt).; stmt-new — Guard (stmtp stmt-new).; stmt-thm-name — Guard (symbolp stmt-thm-name).; gin — Guard (ginp gin).
Returns: item — Type (block-itemp item).; gout — Type (goutp gout).

We put the new statement into a block item.

Definitions and Theorems

Function: xeq-block-item-stmt

(defun xeq-block-item-stmt (stmt stmt-new stmt-thm-name info gin)
 (declare (xargs :guard (and (stmtp stmt)
                             (stmtp stmt-new)
                             (symbolp stmt-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (stmt-unambp stmt)
                             (stmt-annop stmt)
                             (stmt-unambp stmt-new)
                             (stmt-annop stmt-new))))
 (let ((__function__ 'xeq-block-item-stmt))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (item (make-block-item-stmt :stmt stmt
                                :info info))
    (item-new (make-block-item-stmt :stmt stmt-new
                                    :info info))
    ((unless stmt-thm-name)
     (mv item-new (gout-no-thm gin)))
    (types (stmt-types stmt))
    ((mv & old-stmt) (ldm-stmt stmt))
    ((mv & new-stmt) (ldm-stmt stmt-new))
    ((mv & ctypes)
     (ldm-type-option-set types))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::block-item-stmt)
            (:e c::block-item-kind)
            (:e c::block-item-stmt->get)
            c::compustate-frames-number-of-exec-stmt
            c::compustatep-when-compustate-resultp-and-not-errorp
            block-item-stmt-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons stmt-thm-name '((limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'block-item-stmt-congruence
               (cons
                (cons 'old-stmt
                      (cons (cons 'quote (cons old-stmt 'nil))
                            'nil))
                (cons
                  (cons 'new-stmt
                        (cons (cons 'quote (cons new-stmt 'nil))
                              'nil))
                  (cons (cons 'types
                              (cons (cons 'quote (cons ctypes 'nil))
                                    'nil))
                        'nil)))))
             (cons
              (cons
               ':instance
               (cons
                'block-item-stmt-errors
                (cons (cons 'stmt
                            (cons (cons 'quote (cons old-stmt 'nil))
                                  'nil))
                      '((fenv old-fenv)))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-block-item-thm item item-new gin.vartys gin.vartys
                         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 gin.vartys)))))

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

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

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

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

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

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

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

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

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

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