		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-ext-declon

Transform an external declaration.

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

Definitions and Theorems

Function: simpadd0-ext-declon

(defun simpadd0-ext-declon (extdecl gin)
 (declare (xargs :guard (and (ext-declonp extdecl) (ginp gin))))
 (declare (xargs :guard (and (ext-declon-unambp extdecl)
                             (ext-declon-annop extdecl))))
 (let ((__function__ 'simpadd0-ext-declon))
  (declare (ignorable __function__))
  (b* (((gin gin) gin))
   (ext-declon-case extdecl :fundef
                    (b* (((mv new-fundef (gout gout-fundef))
                          (simpadd0-fundef extdecl.fundef gin))
                         (gin (gin-update gin gout-fundef)))
                      (mv (ext-declon-fundef new-fundef)
                          (change-gout (gout-no-thm gin)
                                       :vartys gout-fundef.vartys)))
                    :declon
                    (b* (((mv new-declon (gout gout-declon))
                          (simpadd0-declon extdecl.declon gin))
                         (gin (gin-update gin gout-declon)))
                      (mv (ext-declon-declon new-declon)
                          (change-gout (gout-no-thm gin)
                                       :vartys gout-declon.vartys)))
                    :empty (mv (ext-declon-empty)
                               (gout-no-thm gin))
                    :asm (mv (ext-declon-fix extdecl)
                             (gout-no-thm gin))))))

Theorem: ext-declonp-of-simpadd0-ext-declon.new-extdecl

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

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

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

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

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

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

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

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

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

Theorem: simpadd0-ext-declon-of-ext-declon-fix-extdecl

(defthm simpadd0-ext-declon-of-ext-declon-fix-extdecl
  (equal (simpadd0-ext-declon (ext-declon-fix extdecl)
                              gin)
         (simpadd0-ext-declon extdecl gin)))

Theorem: simpadd0-ext-declon-ext-declon-equiv-congruence-on-extdecl

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

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

(defthm simpadd0-ext-declon-of-gin-fix-gin
  (equal (simpadd0-ext-declon extdecl (gin-fix gin))
         (simpadd0-ext-declon extdecl gin)))

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

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