		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-stmt-compound

Equality lifting transformation of a compound statement.

Signature
(xeq-stmt-compound cstmt cstmt-new cstmt-thm-name gin) → (mv stmt gout)
Arguments: cstmt — Guard (comp-stmtp cstmt).; cstmt-new — Guard (comp-stmtp cstmt-new).; cstmt-thm-name — Guard (symbolp cstmt-thm-name).; gin — Guard (ginp gin).
Returns: stmt — Type (stmtp stmt).; gout — Type (goutp gout).

Definitions and Theorems

Function: xeq-stmt-compound

(defun xeq-stmt-compound (cstmt cstmt-new cstmt-thm-name gin)
 (declare (xargs :guard (and (comp-stmtp cstmt)
                             (comp-stmtp cstmt-new)
                             (symbolp cstmt-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (comp-stmt-unambp cstmt)
                             (comp-stmt-annop cstmt)
                             (comp-stmt-unambp cstmt-new)
                             (comp-stmt-annop cstmt-new))))
 (let ((__function__ 'xeq-stmt-compound))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (stmt-compound cstmt))
    (stmt-new (stmt-compound cstmt-new))
    ((unless cstmt-thm-name)
     (mv stmt-new (gout-no-thm gin)))
    (types (comp-stmt-types cstmt))
    ((mv & old-items) (ldm-comp-stmt cstmt))
    ((mv & new-items)
     (ldm-comp-stmt cstmt-new))
    ((mv & ctypes)
     (ldm-type-option-set types))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::stmt-compound)
            (:e c::stmt-kind)
            c::compustate-frames-number-of-enter-scope
            c::compustate-has-var-with-type-p-of-enter-scope
            stmt-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons ':instance
                  (cons cstmt-thm-name
                        '((compst (c::enter-scope compst))
                          (limit (1- limit)))))
            (cons
             (cons
              ':instance
              (cons
               'stmt-compound-congruence
               (cons
                (cons 'old-items
                      (cons (cons 'quote (cons old-items 'nil))
                            'nil))
                (cons
                  (cons 'new-items
                        (cons (cons 'quote (cons new-items 'nil))
                              'nil))
                  (cons (cons 'types
                              (cons (cons 'quote (cons ctypes 'nil))
                                    'nil))
                        'nil)))))
             (cons
              (cons
               ':instance
               (cons
                'stmt-compound-errors
                (cons
                     (cons 'items
                           (cons (cons 'quote (cons old-items 'nil))
                                 'nil))
                     '((fenv old-fenv)))))
              'nil)))
           'nil)))))
      'nil))
    ((mv thm-event thm-name thm-index)
     (gen-stmt-thm stmt stmt-new gin.vartys
                   gin.const-new gin.thm-index hints)))
   (mv stmt-new
       (make-gout :events (cons thm-event gin.events)
                  :thm-index thm-index
                  :thm-name thm-name
                  :vartys gin.vartys)))))

Theorem: stmtp-of-xeq-stmt-compound.stmt

(defthm stmtp-of-xeq-stmt-compound.stmt
  (b* (((mv ?stmt ?gout)
        (xeq-stmt-compound cstmt cstmt-new cstmt-thm-name gin)))
    (stmtp stmt))
  :rule-classes :rewrite)

Theorem: goutp-of-xeq-stmt-compound.gout

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

Theorem: stmt-unambp-of-xeq-stmt-compound

(defthm stmt-unambp-of-xeq-stmt-compound
 (implies
      (comp-stmt-unambp cstmt-new)
      (b* (((mv ?stmt ?gout)
            (xeq-stmt-compound cstmt cstmt-new cstmt-thm-name gin)))
        (stmt-unambp stmt))))

Theorem: stmt-annop-of-xeq-stmt-compound

(defthm stmt-annop-of-xeq-stmt-compound
 (implies
      (comp-stmt-annop cstmt-new)
      (b* (((mv ?stmt ?gout)
            (xeq-stmt-compound cstmt cstmt-new cstmt-thm-name gin)))
        (stmt-annop stmt))))

Theorem: stmt-aidentp-of-xeq-stmt-compound

(defthm stmt-aidentp-of-xeq-stmt-compound
 (implies
      (comp-stmt-aidentp cstmt-new gcc)
      (b* (((mv ?stmt ?gout)
            (xeq-stmt-compound cstmt cstmt-new cstmt-thm-name gin)))
        (stmt-aidentp stmt gcc))))