		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-ext-declon-list

Transform a list of external declarations.

Signature
(simpadd0-ext-declon-list extdecls gin) → (mv new-extdecls gout)
Arguments: extdecls — Guard (ext-declon-listp extdecls).; gin — Guard (ginp gin).
Returns: new-extdecls — Type (ext-declon-listp new-extdecls).; gout — Type (goutp gout).

Definitions and Theorems

Function: simpadd0-ext-declon-list

(defun simpadd0-ext-declon-list (extdecls gin)
  (declare (xargs :guard (and (ext-declon-listp extdecls)
                              (ginp gin))))
  (declare (xargs :guard (and (ext-declon-list-unambp extdecls)
                              (ext-declon-list-annop extdecls))))
  (let ((__function__ 'simpadd0-ext-declon-list))
    (declare (ignorable __function__))
    (b* (((gin gin) gin)
         ((when (endp extdecls))
          (mv nil (gout-no-thm gin)))
         ((mv new-edecl (gout gout-edecl))
          (simpadd0-ext-declon (car extdecls)
                               gin))
         (gin (gin-update gin gout-edecl))
         ((mv new-edecls (gout gout-edecls))
          (simpadd0-ext-declon-list
               (cdr extdecls)
               (change-gin gin
                           :vartys gout-edecl.vartys)))
         (gin (gin-update gin gout-edecls)))
      (mv (cons new-edecl new-edecls)
          (change-gout (gout-no-thm gin)
                       :vartys gout-edecls.vartys)))))

Theorem: ext-declon-listp-of-simpadd0-ext-declon-list.new-extdecls

(defthm ext-declon-listp-of-simpadd0-ext-declon-list.new-extdecls
  (b* (((mv ?new-extdecls ?gout)
        (simpadd0-ext-declon-list extdecls gin)))
    (ext-declon-listp new-extdecls))
  :rule-classes :rewrite)

Theorem: goutp-of-simpadd0-ext-declon-list.gout

(defthm goutp-of-simpadd0-ext-declon-list.gout
  (b* (((mv ?new-extdecls ?gout)
        (simpadd0-ext-declon-list extdecls gin)))
    (goutp gout))
  :rule-classes :rewrite)

Theorem: ext-declon-list-unambp-of-simpadd0-ext-declon-list

(defthm ext-declon-list-unambp-of-simpadd0-ext-declon-list
  (b* (((mv ?new-extdecls ?gout)
        (simpadd0-ext-declon-list extdecls gin)))
    (ext-declon-list-unambp new-extdecls)))

Theorem: ext-declon-list-annop-of-simpadd0-ext-declon-list

(defthm ext-declon-list-annop-of-simpadd0-ext-declon-list
  (implies (and (ext-declon-list-unambp extdecls)
                (ext-declon-list-annop extdecls))
           (b* (((mv ?new-extdecls ?gout)
                 (simpadd0-ext-declon-list extdecls gin)))
             (ext-declon-list-annop new-extdecls))))

Theorem: ext-declon-list-aidentp-of-simpadd0-ext-declon-list

(defthm ext-declon-list-aidentp-of-simpadd0-ext-declon-list
  (implies (and (ext-declon-list-unambp extdecls)
                (ext-declon-list-aidentp extdecls gcc))
           (b* (((mv ?new-extdecls ?gout)
                 (simpadd0-ext-declon-list extdecls gin)))
             (ext-declon-list-aidentp new-extdecls gcc))))

Theorem: simpadd0-ext-declon-list-of-ext-declon-list-fix-extdecls

(defthm simpadd0-ext-declon-list-of-ext-declon-list-fix-extdecls
  (equal (simpadd0-ext-declon-list (ext-declon-list-fix extdecls)
                                   gin)
         (simpadd0-ext-declon-list extdecls gin)))

Theorem: simpadd0-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls

(defthm
 simpadd0-ext-declon-list-ext-declon-list-equiv-congruence-on-extdecls
 (implies (c$::ext-declon-list-equiv extdecls extdecls-equiv)
          (equal (simpadd0-ext-declon-list extdecls gin)
                 (simpadd0-ext-declon-list extdecls-equiv gin)))
 :rule-classes :congruence)

Theorem: simpadd0-ext-declon-list-of-gin-fix-gin

(defthm simpadd0-ext-declon-list-of-gin-fix-gin
  (equal (simpadd0-ext-declon-list extdecls (gin-fix gin))
         (simpadd0-ext-declon-list extdecls gin)))

Theorem: simpadd0-ext-declon-list-gin-equiv-congruence-on-gin

(defthm simpadd0-ext-declon-list-gin-equiv-congruence-on-gin
  (implies (gin-equiv gin gin-equiv)
           (equal (simpadd0-ext-declon-list extdecls gin)
                  (simpadd0-ext-declon-list extdecls gin-equiv)))
  :rule-classes :congruence)