		Search-engine friendly clone of the ACL2 documentation.

Dynamic-semantics

Add-vars-values

Lift add-var-value to lists.

Signature
(add-vars-values vars vals cstate) → new-cstate
Arguments: vars — Guard (identifier-listp vars).; vals — Guard (value-listp vals).; cstate — Guard (cstatep cstate).
Returns: new-cstate — Type (cstate-resultp new-cstate).

It is an error if there are extra values or extra variables. Their number must be the same. We make this a run-time check because it is part of the conditions to be checked by the defensive dynamic semantics.

Definitions and Theorems

Function: add-vars-values

(defun add-vars-values (vars vals cstate)
 (declare (xargs :guard (and (identifier-listp vars)
                             (value-listp vals)
                             (cstatep cstate))))
 (let ((__function__ 'add-vars-values))
   (declare (ignorable __function__))
   (b*
     (((when (endp vars))
       (if (endp vals)
           (cstate-fix cstate)
         (reserrf (list :extra-values (value-list-fix vals)))))
      ((when (endp vals))
       (reserrf (list :extra-variables (identifier-list-fix vars))))
      ((okf cstate)
       (add-var-value (car vars)
                      (car vals)
                      cstate)))
     (add-vars-values (cdr vars)
                      (cdr vals)
                      cstate))))

Theorem: cstate-resultp-of-add-vars-values

(defthm cstate-resultp-of-add-vars-values
  (b* ((new-cstate (add-vars-values vars vals cstate)))
    (cstate-resultp new-cstate))
  :rule-classes :rewrite)

Theorem: error-info-wfp-of-add-vars-values

(defthm error-info-wfp-of-add-vars-values
  (b* ((?new-cstate (add-vars-values vars vals cstate)))
    (implies (reserrp new-cstate)
             (error-info-wfp new-cstate))))

Theorem: add-vars-values-of-identifier-list-fix-vars

(defthm add-vars-values-of-identifier-list-fix-vars
  (equal (add-vars-values (identifier-list-fix vars)
                          vals cstate)
         (add-vars-values vars vals cstate)))

Theorem: add-vars-values-identifier-list-equiv-congruence-on-vars

(defthm add-vars-values-identifier-list-equiv-congruence-on-vars
  (implies (identifier-list-equiv vars vars-equiv)
           (equal (add-vars-values vars vals cstate)
                  (add-vars-values vars-equiv vals cstate)))
  :rule-classes :congruence)

Theorem: add-vars-values-of-value-list-fix-vals

(defthm add-vars-values-of-value-list-fix-vals
  (equal (add-vars-values vars (value-list-fix vals)
                          cstate)
         (add-vars-values vars vals cstate)))

Theorem: add-vars-values-value-list-equiv-congruence-on-vals

(defthm add-vars-values-value-list-equiv-congruence-on-vals
  (implies (value-list-equiv vals vals-equiv)
           (equal (add-vars-values vars vals cstate)
                  (add-vars-values vars vals-equiv cstate)))
  :rule-classes :congruence)

Theorem: add-vars-values-of-cstate-fix-cstate

(defthm add-vars-values-of-cstate-fix-cstate
  (equal (add-vars-values vars vals (cstate-fix cstate))
         (add-vars-values vars vals cstate)))

Theorem: add-vars-values-cstate-equiv-congruence-on-cstate

(defthm add-vars-values-cstate-equiv-congruence-on-cstate
  (implies (cstate-equiv cstate cstate-equiv)
           (equal (add-vars-values vars vals cstate)
                  (add-vars-values vars vals cstate-equiv)))
  :rule-classes :congruence)