		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-extdecl

Transform an external declaration.

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

Definitions and Theorems

Function: simpadd0-extdecl

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

Theorem: extdeclp-of-simpadd0-extdecl.new-extdecl

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

Theorem: goutp-of-simpadd0-extdecl.gout

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

Theorem: extdecl-unambp-of-simpadd0-extdecl

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

Theorem: extdecl-annop-of-simpadd0-extdecl

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

Theorem: extdecl-aidentp-of-simpadd0-extdecl

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

Theorem: simpadd0-extdecl-of-extdecl-fix-extdecl

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

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

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

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

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

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

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