		Search-engine friendly clone of the ACL2 documentation.

Static-safety-checking

Add-vars

Add (a list of) variables to a variable table.

Signature
(add-vars vars varset) → varset?
Arguments: vars — Guard (identifier-listp vars).; varset — Guard (identifier-setp varset).
Returns: varset? — Type (identifier-set-resultp varset?).

The variables are added, one after the other. Duplicates in the list will cause an error.

This lifts add-var to lists.

If this function does not return an error, it is equivalent to set::list-insert.

Definitions and Theorems

Function: add-vars

(defun add-vars (vars varset)
  (declare (xargs :guard (and (identifier-listp vars)
                              (identifier-setp varset))))
  (let ((__function__ 'add-vars))
    (declare (ignorable __function__))
    (b* (((when (endp vars))
          (identifier-set-fix varset))
         ((okf varset)
          (add-var (car vars) varset)))
      (add-vars (cdr vars) varset))))

Theorem: identifier-set-resultp-of-add-vars

(defthm identifier-set-resultp-of-add-vars
  (b* ((varset? (add-vars vars varset)))
    (identifier-set-resultp varset?))
  :rule-classes :rewrite)

Theorem: add-vars-to-set-list-insert

(defthm add-vars-to-set-list-insert
 (b* ((varset1 (add-vars vars varset)))
  (implies (not (reserrp varset1))
           (equal varset1
                  (set::list-insert (identifier-list-fix vars)
                                    (identifier-set-fix varset))))))

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

(defthm add-vars-of-identifier-list-fix-vars
  (equal (add-vars (identifier-list-fix vars)
                   varset)
         (add-vars vars varset)))

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

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

Theorem: add-vars-of-identifier-set-fix-varset

(defthm add-vars-of-identifier-set-fix-varset
  (equal (add-vars vars (identifier-set-fix varset))
         (add-vars vars varset)))

Theorem: add-vars-identifier-set-equiv-congruence-on-varset

(defthm add-vars-identifier-set-equiv-congruence-on-varset
  (implies (identifier-set-equiv varset varset-equiv)
           (equal (add-vars vars varset)
                  (add-vars vars varset-equiv)))
  :rule-classes :congruence)