		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-extdecl-list

Transform a list of external declarations.

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

Definitions and Theorems

Function: simpadd0-extdecl-list

(defun simpadd0-extdecl-list (extdecls gin state)
  (declare (xargs :stobjs (state)))
  (declare (xargs :guard (and (extdecl-listp extdecls)
                              (simpadd0-ginp gin))))
  (declare (xargs :guard (extdecl-list-unambp extdecls)))
  (let ((__function__ 'simpadd0-extdecl-list))
    (declare (ignorable __function__))
    (b* (((simpadd0-gin gin) gin)
         ((when (endp extdecls))
          (mv nil
              (make-simpadd0-gout :events nil
                                  :thm-name nil
                                  :thm-index gin.thm-index
                                  :names-to-avoid gin.names-to-avoid
                                  :vars nil
                                  :diffp nil)))
         ((mv new-edecl (simpadd0-gout gout-edecl))
          (simpadd0-extdecl (car extdecls)
                            gin state))
         (gin (simpadd0-gin-update gin gout-edecl))
         ((mv new-edecls (simpadd0-gout gout-edecls))
          (simpadd0-extdecl-list (cdr extdecls)
                                 gin state)))
      (mv (cons new-edecl new-edecls)
          (make-simpadd0-gout
               :events (append gout-edecl.events gout-edecls.events)
               :thm-name nil
               :thm-index gout-edecls.thm-index
               :names-to-avoid gout-edecls.names-to-avoid
               :vars (union gout-edecl.vars gout-edecls.vars)
               :diffp (or gout-edecl.diffp gout-edecls.diffp))))))

Theorem: extdecl-listp-of-simpadd0-extdecl-list.new-extdecls

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

Theorem: simpadd0-goutp-of-simpadd0-extdecl-list.gout

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

Theorem: extdecl-list-unambp-of-simpadd0-extdecl-list

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

Theorem: simpadd0-extdecl-list-of-extdecl-list-fix-extdecls

(defthm simpadd0-extdecl-list-of-extdecl-list-fix-extdecls
  (equal (simpadd0-extdecl-list (extdecl-list-fix extdecls)
                                gin state)
         (simpadd0-extdecl-list extdecls gin state)))

Theorem: simpadd0-extdecl-list-extdecl-list-equiv-congruence-on-extdecls

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

Theorem: simpadd0-extdecl-list-of-simpadd0-gin-fix-gin

(defthm simpadd0-extdecl-list-of-simpadd0-gin-fix-gin
  (equal (simpadd0-extdecl-list extdecls (simpadd0-gin-fix gin)
                                state)
         (simpadd0-extdecl-list extdecls gin state)))

Theorem: simpadd0-extdecl-list-simpadd0-gin-equiv-congruence-on-gin

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