		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-fundef

Transform a function definition.

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

Definitions and Theorems

Function: simpadd0-fundef

(defun simpadd0-fundef (fundef)
  (declare (xargs :guard (fundefp fundef)))
  (declare (xargs :guard (fundef-unambp fundef)))
  (let ((__function__ 'simpadd0-fundef))
    (declare (ignorable __function__))
    (b* (((fundef fundef) fundef)
         ((mv new-spec events-spec)
          (simpadd0-decl-spec-list fundef.spec))
         ((mv new-declor events-declor)
          (simpadd0-declor fundef.declor))
         ((mv new-decls events-decls)
          (simpadd0-decl-list fundef.decls))
         ((mv new-body events-body)
          (simpadd0-stmt fundef.body)))
      (mv (make-fundef :extension fundef.extension
                       :spec new-spec
                       :declor new-declor
                       :asm? fundef.asm?
                       :attribs fundef.attribs
                       :decls new-decls
                       :body new-body)
          (append events-spec events-declor
                  events-decls events-body)))))

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

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

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

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

Theorem: fundef-unambp-of-simpadd0-fundef

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

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

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

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