		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-gen-stmt-thm

Generate a theorem for the transformation of a statement.

Signature
(simpadd0-gen-stmt-thm old new vartys const-new thm-index hints) → (mv thm-event thm-name updated-thm-index)
Arguments: old — Guard (stmtp old).; new — Guard (stmtp new).; vartys — Guard (ident-type-mapp vartys).; const-new — Guard (symbolp const-new).; thm-index — Guard (posp thm-index).; hints — Guard (true-listp hints).
Returns: thm-event — Type (pseudo-event-formp thm-event).; thm-name — Type (symbolp thm-name).; updated-thm-index — Type (posp updated-thm-index).

This is analogous to simpadd0-gen-expr-pure-thm, but for statments instead of pure expressions; see that function's documentation first.

The theorem says that the old statement returns a value of the appropriate type, regardless of whether old and new statements are syntactically equal or not; if the type is void, then the theorem says that execution returns nil, according to our formal dynamic semantics. If old and new statements are not equal, the theorem also says that their execution returns equal values (or both nil) and equal computation states, and that the execution of the new statement does not yield an error.

Definitions and Theorems

Function: simpadd0-gen-stmt-thm

(defun simpadd0-gen-stmt-thm
       (old new vartys const-new thm-index hints)
 (declare (xargs :guard (and (stmtp old)
                             (stmtp new)
                             (ident-type-mapp vartys)
                             (symbolp const-new)
                             (posp thm-index)
                             (true-listp hints))))
 (declare (xargs :guard (and (stmt-unambp old)
                             (stmt-unambp new))))
 (let ((__function__ 'simpadd0-gen-stmt-thm))
  (declare (ignorable __function__))
  (b*
   ((old (stmt-fix old))
    (new (stmt-fix new))
    ((unless (stmt-formalp old))
     (raise "Internal error: ~x0 is not in the formalized subset."
            old)
     (mv '(_) nil 1))
    (equalp (equal old new))
    ((unless (or equalp (stmt-formalp new)))
     (raise "Internal error: ~x0 is not in the formalized subset."
            new)
     (mv '(_) nil 1))
    (type (stmt-type old))
    ((unless (or equalp (equal (stmt-type new) type)))
     (raise
      "Internal error: ~
                the type ~x0 of the new statement ~x1 differs from ~
                the type ~x2 of the old statement ~x3."
      (stmt-type new)
      new type old)
     (mv '(_) nil 1))
    ((unless (type-formalp type))
     (raise "Internal error: statement ~x0 has type ~x1."
            old type)
     (mv '(_) nil 1))
    ((mv & ctype) (ldm-type type))
    (hyps (simpadd0-gen-var-hyps vartys))
    (formula
     (if equalp
      (cons
       'b*
       (cons
        (cons
         (cons
          'stmt
          (cons
           (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-stmt
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil))
                           'nil)))
           'nil))
         '(((mv result &)
            (c::exec-stmt stmt compst fenv limit))))
        (cons
         (cons
          'implies
          (cons
           (cons 'and
                 (append hyps '((not (c::errorp result)))))
           (cons
            (if (type-case type :void)
                '(not result)
             (cons
              'and
              (cons
               'result
               (cons
                   (cons 'equal
                         (cons '(c::type-of-value result)
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil)))
                   'nil))))
            'nil)))
         'nil)))
      (cons
       'b*
       (cons
        (cons
         (cons
          'old-stmt
          (cons
           (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-stmt
                                 (cons (cons 'quote (cons old 'nil))
                                       'nil))
                           'nil)))
           'nil))
         (cons
          (cons
           'new-stmt
           (cons
            (cons
               'mv-nth
               (cons '1
                     (cons (cons 'ldm-stmt
                                 (cons (cons 'quote (cons new 'nil))
                                       'nil))
                           'nil)))
            'nil))
          '(((mv old-result old-compst)
             (c::exec-stmt old-stmt compst old-fenv limit))
            ((mv new-result new-compst)
             (c::exec-stmt new-stmt compst new-fenv limit)))))
        (cons
         (cons
          'implies
          (cons
           (cons 'and
                 (append hyps '((not (c::errorp old-result)))))
           (cons
            (cons
             'and
             (cons
              '(not (c::errorp new-result))
              (cons
               '(equal old-result new-result)
               (cons
                '(equal old-compst new-compst)
                (if (type-case type :void)
                    '((not old-result))
                 (cons
                  'old-result
                  (cons
                   (cons 'equal
                         (cons '(c::type-of-value old-result)
                               (cons (cons 'quote (cons ctype 'nil))
                                     'nil)))
                   'nil)))))))
            'nil)))
         'nil)))))
    (thm-name (packn-pos (list const-new '-thm- thm-index)
                         const-new))
    (thm-index (1+ (pos-fix thm-index)))
    (thm-event
         (cons 'defthmd
               (cons thm-name
                     (cons formula
                           (cons ':hints (cons hints 'nil)))))))
   (mv thm-event thm-name thm-index))))

Theorem: pseudo-event-formp-of-simpadd0-gen-stmt-thm.thm-event

(defthm pseudo-event-formp-of-simpadd0-gen-stmt-thm.thm-event
  (b*
    (((mv ?thm-event ?thm-name ?updated-thm-index)
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)))
    (pseudo-event-formp thm-event))
  :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-gen-stmt-thm.thm-name

(defthm symbolp-of-simpadd0-gen-stmt-thm.thm-name
  (b*
    (((mv ?thm-event ?thm-name ?updated-thm-index)
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)))
    (symbolp thm-name))
  :rule-classes :rewrite)

Theorem: posp-of-simpadd0-gen-stmt-thm.updated-thm-index

(defthm posp-of-simpadd0-gen-stmt-thm.updated-thm-index
  (b*
    (((mv ?thm-event ?thm-name ?updated-thm-index)
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)))
    (posp updated-thm-index))
  :rule-classes :rewrite)

Theorem: simpadd0-gen-stmt-thm-of-stmt-fix-old

(defthm simpadd0-gen-stmt-thm-of-stmt-fix-old
 (equal
      (simpadd0-gen-stmt-thm (stmt-fix old)
                             new vartys const-new thm-index hints)
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)))

Theorem: simpadd0-gen-stmt-thm-stmt-equiv-congruence-on-old

(defthm simpadd0-gen-stmt-thm-stmt-equiv-congruence-on-old
 (implies
  (c$::stmt-equiv old old-equiv)
  (equal
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)
      (simpadd0-gen-stmt-thm old-equiv
                             new vartys const-new thm-index hints)))
 :rule-classes :congruence)

Theorem: simpadd0-gen-stmt-thm-of-stmt-fix-new

(defthm simpadd0-gen-stmt-thm-of-stmt-fix-new
 (equal
      (simpadd0-gen-stmt-thm old (stmt-fix new)
                             vartys const-new thm-index hints)
      (simpadd0-gen-stmt-thm old
                             new vartys const-new thm-index hints)))

Theorem: simpadd0-gen-stmt-thm-stmt-equiv-congruence-on-new

(defthm simpadd0-gen-stmt-thm-stmt-equiv-congruence-on-new
 (implies
   (c$::stmt-equiv new new-equiv)
   (equal
        (simpadd0-gen-stmt-thm old
                               new vartys const-new thm-index hints)
        (simpadd0-gen-stmt-thm old new-equiv
                               vartys const-new thm-index hints)))
 :rule-classes :congruence)