Check if the variables in a list are all in a variable table.
(check-var-list vars varset) → yes/no
This lifts check-var to lists.
It is not actually part of the formalization of the static safety checks,
because that formalization uses check-var
to define check-safe-path,
and then lifts the latter to lists.
For the static soundness proof,
it is useful to have this
We prove a theorem that turns check-var-list into the inclusion of the list of variable in the variable table, which is a set.
Function:
(defun check-var-list (vars varset) (declare (xargs :guard (and (identifier-listp vars) (identifier-setp varset)))) (let ((__function__ 'check-var-list)) (declare (ignorable __function__)) (or (endp vars) (and (check-var (car vars) varset) (check-var-list (cdr vars) varset)))))
Theorem:
(defthm booleanp-of-check-var-list (b* ((yes/no (check-var-list vars varset))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm check-var-list-to-set-list-in (implies (and (identifier-listp vars) (identifier-setp varset)) (equal (check-var-list vars varset) (set::list-in vars varset))))
Theorem:
(defthm check-var-list-of-identifier-list-fix-vars (equal (check-var-list (identifier-list-fix vars) varset) (check-var-list vars varset)))
Theorem:
(defthm check-var-list-identifier-list-equiv-congruence-on-vars (implies (identifier-list-equiv vars vars-equiv) (equal (check-var-list vars varset) (check-var-list vars-equiv varset))) :rule-classes :congruence)
Theorem:
(defthm check-var-list-of-identifier-set-fix-varset (equal (check-var-list vars (identifier-set-fix varset)) (check-var-list vars varset)))
Theorem:
(defthm check-var-list-identifier-set-equiv-congruence-on-varset (implies (identifier-set-equiv varset varset-equiv) (equal (check-var-list vars varset) (check-var-list vars varset-equiv))) :rule-classes :congruence)