		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-extdecl

Transform an external declaration.

Signature
(simpadd0-extdecl extdecl) → (mv new-extdecl events)
Arguments: extdecl — Guard (extdeclp extdecl).
Returns: new-extdecl — Type (extdeclp new-extdecl).; events — Type (pseudo-event-form-listp events).

Definitions and Theorems

Function: simpadd0-extdecl

(defun simpadd0-extdecl (extdecl)
  (declare (xargs :guard (extdeclp extdecl)))
  (declare (xargs :guard (extdecl-unambp extdecl)))
  (let ((__function__ 'simpadd0-extdecl))
    (declare (ignorable __function__))
    (extdecl-case extdecl :fundef
                  (b* (((mv new-fundef events-fundef)
                        (simpadd0-fundef extdecl.unwrap)))
                    (mv (extdecl-fundef new-fundef)
                        events-fundef))
                  :decl
                  (b* (((mv new-decl events-decl)
                        (simpadd0-decl extdecl.unwrap)))
                    (mv (extdecl-decl new-decl)
                        events-decl))
                  :empty (mv (extdecl-empty) nil)
                  :asm (mv (extdecl-fix extdecl) nil))))

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

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

Theorem: pseudo-event-form-listp-of-simpadd0-extdecl.events

(defthm pseudo-event-form-listp-of-simpadd0-extdecl.events
  (b* (((mv ?new-extdecl ?events)
        (simpadd0-extdecl extdecl)))
    (pseudo-event-form-listp events))
  :rule-classes :rewrite)

Theorem: extdecl-unambp-of-simpadd0-extdecl

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

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

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

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