		Search-engine friendly clone of the ACL2 documentation.

Simpadd0

Simpadd0-fn

Event expansion of the transformation.

Signature
(simpadd0-fn const-old const-new proofs wrld) → event
Arguments: wrld — Guard (plist-worldp wrld).
Returns: event — Type (pseudo-event-formp event).

Definitions and Theorems

Function: simpadd0-fn

(defun simpadd0-fn (const-old const-new proofs wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'simpadd0-fn))
  (declare (ignorable __function__))
  (b*
   (((unless (symbolp const-old))
     (raise "~x0 must be a symbol." const-old)
     '(_))
    ((unless (symbolp const-new))
     (raise "~x0 must be a symbol." const-new)
     '(_))
    ((unless (symbolp proofs))
     (raise "~x0 must be a boolean." proofs)
     '(_))
    (tunits-old (acl2::constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits-old))
     (raise "~x0 must be a translation unit ensemble.")
     '(_))
    ((unless (transunit-ensemble-unambp tunits-old))
     (raise "~x0 must be an unambiguous translation unit ensemble.")
     '(_))
    (tunits-new (simpadd0-transunit-ensemble tunits-old))
    ((unless (or (not proofs)
                 (b* (((mv erp &)
                       (c$::ldm-transunit-ensemble tunits-old)))
                   (not erp))))
     (raise
      "The old translation unit ~x0 is not within ~
                the subset of C covered by our formal semantics."
      tunits-old)
     '(_))
    ((unless (or (not proofs)
                 (b* (((mv erp &)
                       (c$::ldm-transunit-ensemble tunits-new)))
                   (not erp))))
     (raise
      "The new translation unit ~x0 is not within ~
                the subset of C covered by our formal semantics."
      tunits-new)
     '(_))
    (thm-events (and proofs
                     (simpadd0-gen-proofs-for-transunit-ensemble
                          const-old
                          const-new tunits-old tunits-new)))
    (const-event
         (cons 'defconst
               (cons const-new
                     (cons (cons 'quote (cons tunits-new 'nil))
                           'nil)))))
   (cons 'progn
         (cons const-event thm-events)))))

Theorem: pseudo-event-formp-of-simpadd0-fn

(defthm pseudo-event-formp-of-simpadd0-fn
  (b* ((event (simpadd0-fn const-old const-new proofs wrld)))
    (pseudo-event-formp event))
  :rule-classes :rewrite)