		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-event-generation

Simpadd0-transunit

Transform a translation unit.

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

Definitions and Theorems

Function: simpadd0-transunit

(defun simpadd0-transunit (tunit gin state)
 (declare (xargs :stobjs (state)))
 (declare (xargs :guard (and (transunitp tunit)
                             (simpadd0-ginp gin))))
 (declare (xargs :guard (transunit-unambp tunit)))
 (let ((__function__ 'simpadd0-transunit))
  (declare (ignorable __function__))
  (b* (((simpadd0-gin gin) gin)
       ((transunit tunit) tunit)
       ((mv new-decls (simpadd0-gout gout-decls))
        (simpadd0-extdecl-list tunit.decls gin state)))
   (mv (make-transunit :decls new-decls
                       :info tunit.info)
       (make-simpadd0-gout :events gout-decls.events
                           :thm-name nil
                           :thm-index gout-decls.thm-index
                           :names-to-avoid gout-decls.names-to-avoid
                           :vartys gout-decls.vartys
                           :diffp gout-decls.diffp)))))

Theorem: transunitp-of-simpadd0-transunit.new-tunit

(defthm transunitp-of-simpadd0-transunit.new-tunit
  (b* (((mv ?new-tunit ?gout)
        (simpadd0-transunit tunit gin state)))
    (transunitp new-tunit))
  :rule-classes :rewrite)

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

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

Theorem: transunit-unambp-of-simpadd0-transunit

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

Theorem: simpadd0-transunit-of-transunit-fix-tunit

(defthm simpadd0-transunit-of-transunit-fix-tunit
  (equal (simpadd0-transunit (c$::transunit-fix tunit)
                             gin state)
         (simpadd0-transunit tunit gin state)))

Theorem: simpadd0-transunit-transunit-equiv-congruence-on-tunit

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

Theorem: simpadd0-transunit-of-simpadd0-gin-fix-gin

(defthm simpadd0-transunit-of-simpadd0-gin-fix-gin
  (equal (simpadd0-transunit tunit (simpadd0-gin-fix gin)
                             state)
         (simpadd0-transunit tunit gin state)))

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

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