		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-fundef

Transform a function definition.

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

Definitions and Theorems

Function: simpadd0-fundef

(defun simpadd0-fundef (fundef gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (fundefp fundef)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (fundef-unambp fundef)))
 (let ((__function__ 'simpadd0-fundef))
  (declare (ignorable __function__))
  (b*
   (((simpadd0-gin gin) gin)
    ((fundef fundef) fundef)
    ((mv new-spec (simpadd0-gout gout-spec))
     (simpadd0-decl-spec-list fundef.spec gin state))
    (gin
     (change-simpadd0-gin gin
                          :thm-index gout-spec.thm-index
                          :names-to-avoid gout-spec.names-to-avoid))
    ((mv new-declor (simpadd0-gout gout-declor))
     (simpadd0-declor fundef.declor gin state))
    (gin (change-simpadd0-gin
              gin
              :thm-index gout-declor.thm-index
              :names-to-avoid gout-declor.names-to-avoid))
    ((mv new-decls (simpadd0-gout gout-decls))
     (simpadd0-decl-list fundef.decls gin state))
    (gin (change-simpadd0-gin
              gin
              :thm-index gout-decls.thm-index
              :names-to-avoid gout-decls.names-to-avoid))
    ((mv new-body (simpadd0-gout gout-body))
     (simpadd0-stmt fundef.body gin state)))
   (mv (make-fundef :extension fundef.extension
                    :spec new-spec
                    :declor new-declor
                    :asm? fundef.asm?
                    :attribs fundef.attribs
                    :decls new-decls
                    :body new-body)
       (make-simpadd0-gout
            :events (append gout-spec.events gout-declor.events
                            gout-decls.events gout-body.events)
            :thm-name nil
            :thm-index gout-body.thm-index
            :names-to-avoid gout-body.names-to-avoid)))))

Theorem: fundefp-of-simpadd0-fundef.new-fundef

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

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

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

Theorem: fundef-unambp-of-simpadd0-fundef

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

Theorem: simpadd0-fundef-of-fundef-fix-fundef

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

Theorem: simpadd0-fundef-fundef-equiv-congruence-on-fundef

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

Theorem: simpadd0-fundef-of-simpadd0-gin-fix-gin

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

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

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