		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-extdecl

Transform an external declaration.

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

Definitions and Theorems

Function: simpadd0-extdecl

(defun simpadd0-extdecl (extdecl gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (extdeclp extdecl)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (extdecl-unambp extdecl)))
 (let ((__function__ 'simpadd0-extdecl))
  (declare (ignorable __function__))
  (b* (((simpadd0-gin gin) gin))
   (extdecl-case
    extdecl :fundef
    (b* (((mv new-fundef (simpadd0-gout gout-fundef))
          (simpadd0-fundef extdecl.unwrap gin state)))
      (mv (extdecl-fundef new-fundef)
          (make-simpadd0-gout
               :events gout-fundef.events
               :thm-name nil
               :thm-index gout-fundef.thm-index
               :names-to-avoid gout-fundef.names-to-avoid)))
    :decl
    (b* (((mv new-decl (simpadd0-gout gout-decl))
          (simpadd0-decl extdecl.unwrap gin state)))
      (mv (extdecl-decl new-decl)
          (make-simpadd0-gout
               :events gout-decl.events
               :thm-name nil
               :thm-index gout-decl.thm-index
               :names-to-avoid gout-decl.names-to-avoid)))
    :empty
    (mv (extdecl-empty)
        (make-simpadd0-gout :events nil
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid))
    :asm
    (mv (extdecl-fix extdecl)
        (make-simpadd0-gout :events nil
                            :thm-name nil
                            :thm-index gin.thm-index
                            :names-to-avoid gin.names-to-avoid))))))

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

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

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

(defthm simpadd0-goutp-of-simpadd0-extdecl.gout
  (b* (((mv ?new-extdecl ?gout)
        (simpadd0-extdecl extdecl gin state)))
    (simpadd0-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 state)))
    (extdecl-unambp new-extdecl)))

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

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

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 state)
                  (simpadd0-extdecl extdecl-equiv gin state)))
  :rule-classes :congruence)

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

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

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

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