		Search-engine friendly clone of the ACL2 documentation.

Proof-generation

Xeq-stmt-while

Equality lifting transformation of a while loop.

Signature
(xeq-stmt-while test test-new test-thm-name body body-new body-thm-name gin) → (mv stmt gout)
Arguments: test — Guard (exprp test).; test-new — Guard (exprp test-new).; test-thm-name — Guard (symbolp test-thm-name).; body — Guard (stmtp body).; body-new — Guard (stmtp body-new).; body-thm-name — Guard (symbolp body-thm-name).; gin — Guard (ginp gin).
Returns: stmt — Type (stmtp stmt).; gout — Type (goutp gout).

Definitions and Theorems

Function: xeq-stmt-while

(defun xeq-stmt-while (test test-new test-thm-name
                            body body-new body-thm-name gin)
 (declare (xargs :guard (and (exprp test)
                             (exprp test-new)
                             (symbolp test-thm-name)
                             (stmtp body)
                             (stmtp body-new)
                             (symbolp body-thm-name)
                             (ginp gin))))
 (declare (xargs :guard (and (expr-unambp test)
                             (expr-annop test)
                             (expr-unambp test-new)
                             (expr-annop test-new)
                             (stmt-unambp body)
                             (stmt-annop body)
                             (stmt-unambp body-new)
                             (stmt-annop body-new))))
 (let ((__function__ 'xeq-stmt-while))
  (declare (ignorable __function__))
  (b*
   (((gin gin) gin)
    (stmt (make-stmt-while :test test :body body))
    (stmt-new (make-stmt-while :test test-new
                               :body body-new))
    ((unless (and test-thm-name body-thm-name))
     (mv stmt-new (gout-no-thm gin)))
    (types (stmt-types body))
    ((mv & old-test) (ldm-expr test))
    ((mv & new-test) (ldm-expr test-new))
    ((mv & old-body) (ldm-stmt body))
    ((mv & new-body) (ldm-stmt body-new))
    (hints
     (cons
      (cons
       '"Goal"
       (cons
        ':in-theory
        (cons
         ''((:e c::stmt-while)
            (:e c::ident-type-map-fix)
            (:e omap::emptyp)
            (:e omap::head)
            (:e omap::tail)
            (:e insert)
            (:e c::type-nonchar-integerp)
            while-test-hyp while-body-hyp
            c::compustate-has-vars-with-types-p
            stmt-compustate-vars)
         (cons
          ':use
          (cons
           (cons
            (cons
             ':instance
             (cons
              test-thm-name
              (cons
               (cons
                'compst
                (cons
                 (cons
                  'mv-nth
                  (cons
                   '0
                   (cons
                    (cons
                     'while-test-hyp-witness
                     (cons
                      (cons 'quote (cons old-test 'nil))
                      (cons
                       (cons 'quote (cons new-test 'nil))
                       (cons
                        'old-fenv
                        (cons
                          'new-fenv
                          (cons (cons 'quote (cons gin.vartys 'nil))
                                'nil))))))
                    'nil)))
                 'nil))
               (cons
                (cons
                 'limit
                 (cons
                  (cons
                   'mv-nth
                   (cons
                    '1
                    (cons
                     (cons
                      'while-test-hyp-witness
                      (cons
                       (cons 'quote (cons old-test 'nil))
                       (cons
                        (cons 'quote (cons new-test 'nil))
                        (cons
                         'old-fenv
                         (cons
                          'new-fenv
                          (cons (cons 'quote (cons gin.vartys 'nil))
                                'nil))))))
                     'nil)))
                  'nil))
                'nil))))
            (cons
             (cons
              ':instance
              (cons
               body-thm-name
               (cons
                (cons
                 'compst
                 (cons
                  (cons
                   'mv-nth
                   (cons
                    '0
                    (cons
                     (cons
                      'while-body-hyp-witness
                      (cons
                       (cons 'quote (cons old-body 'nil))
                       (cons
                        (cons 'quote (cons new-body 'nil))
                        (cons
                         'old-fenv
                         (cons
                          'new-fenv
                          (cons
                           (cons 'quote (cons types 'nil))
                           (cons
                                (cons 'quote (cons gin.vartys 'nil))
                                'nil)))))))
                     'nil)))
                  'nil))
                (cons
                 (cons
                  'limit
                  (cons
                   (cons
                    'mv-nth
                    (cons
                     '1
                     (cons
                      (cons
                       'while-body-hyp-witness
                       (cons
                        (cons 'quote (cons old-body 'nil))
                        (cons
                         (cons 'quote (cons new-body 'nil))
                         (cons
                          'old-fenv
                          (cons
                           'new-fenv
                           (cons
                            (cons 'quote (cons types 'nil))
                            (cons
                                (cons 'quote (cons gin.vartys 'nil))
                                'nil)))))))
                      'nil)))
                   'nil))
                 'nil))))
             (cons
              (cons
               ':instance
               (cons
                'stmt-while-theorem
                (cons
                 (cons 'old-test
                       (cons (cons 'quote (cons old-test 'nil))
                             'nil))
                 (cons
                  (cons 'new-test
                        (cons (cons 'quote (cons new-test 'nil))
                              'nil))
                  (cons
                   (cons 'old-body
                         (cons (cons 'quote (cons old-body 'nil))
                               'nil))
                   (cons
                    (cons 'new-body
                          (cons (cons 'quote (cons new-body 'nil))
                                'nil))
                    (cons
                     (cons 'types
                           (cons (cons 'quote (cons types 'nil))
                                 'nil))
                     (cons
                      (cons
                          'vartys
                          (cons (cons 'quote (cons gin.vartys 'nil))
                                'nil))
                      'nil))))))))
              '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-while.stmt

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

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

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

Theorem: stmt-unambp-of-xeq-stmt-while

(defthm stmt-unambp-of-xeq-stmt-while
  (implies (and (expr-unambp test-new)
                (stmt-unambp body-new))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-while test test-new test-thm-name
                                 body body-new body-thm-name gin)))
             (stmt-unambp stmt))))

Theorem: stmt-annop-of-xeq-stmt-while

(defthm stmt-annop-of-xeq-stmt-while
  (implies (and (expr-annop test-new)
                (stmt-annop body-new))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-while test test-new test-thm-name
                                 body body-new body-thm-name gin)))
             (stmt-annop stmt))))

Theorem: stmt-aidentp-of-xeq-stmt-while

(defthm stmt-aidentp-of-xeq-stmt-while
  (implies (and (expr-aidentp test-new gcc)
                (stmt-aidentp body-new gcc))
           (b* (((mv ?stmt ?gout)
                 (xeq-stmt-while test test-new test-thm-name
                                 body body-new body-thm-name gin)))
             (stmt-aidentp stmt gcc))))