		Search-engine friendly clone of the ACL2 documentation.

Simpadd0-input-processing

Simpadd0-process-inputs

Process all the inputs.

Signature
(simpadd0-process-inputs const-old const-new proofs wrld) → (mv erp tunits-old const-old$ const-new$ proofs$)
Arguments: wrld — Guard (plist-worldp wrld).
Returns: tunits-old — Type (transunit-ensemblep tunits-old).; const-old$ — Type (symbolp const-old$).; const-new$ — Type (symbolp const-new$).; proofs$ — Type (booleanp proofs$).

Definitions and Theorems

Function: simpadd0-process-inputs

(defun simpadd0-process-inputs (const-old const-new proofs wrld)
 (declare (xargs :guard (plist-worldp wrld)))
 (let ((__function__ 'simpadd0-process-inputs))
  (declare (ignorable __function__))
  (b*
   (((reterr)
     (c$::irr-transunit-ensemble)
     nil nil nil)
    ((unless (symbolp const-old))
     (reterr
      (msg
       "The first input must be a symbol, ~
                      but it is ~x0 instead."
       const-old)))
    ((unless (symbolp const-new))
     (reterr
      (msg
       "The second input must be a symbol, ~
                      but it is ~x0 instead."
       const-new)))
    ((unless (booleanp proofs))
     (reterr
      (msg
       "The :PROOFS input must be a boolean, ~
                      but it is ~x0 instead."
       proofs)))
    ((unless (acl2::constant-symbolp const-old wrld))
     (reterr
      (msg
       "The first input, ~x0, must be a named constant, ~
                      but it is not."
       const-old)))
    (tunits-old (acl2::constant-value const-old wrld))
    ((unless (transunit-ensemblep tunits-old))
     (reterr
      (msg
       "The value of the constant ~x0 ~
                      must be a translation unit ensemble, ~
                      but it is ~x1 instead."
       const-old tunits-old)))
    ((unless (transunit-ensemble-unambp tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must be unambiguous, ~
                      but it is not."
       tunits-old const-old)))
    ((unless (transunit-ensemble-annop tunits-old))
     (reterr
      (msg
       "The translation unit ensemble ~x0 ~
                      that is the value of the constant ~x1 ~
                      must contains validation information, ~
                      but it does not."
       tunits-old const-old))))
   (retok tunits-old
          const-old const-new proofs))))

Theorem: transunit-ensemblep-of-simpadd0-process-inputs.tunits-old

(defthm transunit-ensemblep-of-simpadd0-process-inputs.tunits-old
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (transunit-ensemblep tunits-old))
  :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-process-inputs.const-old$

(defthm symbolp-of-simpadd0-process-inputs.const-old$
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (symbolp const-old$))
  :rule-classes :rewrite)

Theorem: symbolp-of-simpadd0-process-inputs.const-new$

(defthm symbolp-of-simpadd0-process-inputs.const-new$
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (symbolp const-new$))
  :rule-classes :rewrite)

Theorem: booleanp-of-simpadd0-process-inputs.proofs$

(defthm booleanp-of-simpadd0-process-inputs.proofs$
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (booleanp proofs$))
  :rule-classes :rewrite)

Theorem: transunit-ensemble-unambp-of-simpadd0-process-inputs

(defthm transunit-ensemble-unambp-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (implies (not erp)
             (transunit-ensemble-unambp tunits-old))))

Theorem: transunit-ensemble-annop-of-simpadd0-process-inputs

(defthm transunit-ensemble-annop-of-simpadd0-process-inputs
  (b* (((mv acl2::?erp ?tunits-old
            ?const-old$ ?const-new$ ?proofs$)
        (simpadd0-process-inputs const-old const-new proofs wrld)))
    (implies (not erp)
             (transunit-ensemble-annop tunits-old))))