CHeck if all the variables in a file scope are defined.
(var-table-all-definedp vartab) → yes/no
We only use this ACL2 function when the variable table has one scope, which must therefore be the file scope.
Function:
(defun var-table-all-definedp (vartab) (declare (xargs :guard (var-tablep vartab))) (let ((__function__ 'var-table-all-definedp)) (declare (ignorable __function__)) (var-scope-all-definedp (car vartab))))
Theorem:
(defthm booleanp-of-var-table-all-definedp (b* ((yes/no (var-table-all-definedp vartab))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm var-table-all-definedp-of-var-table-fix-vartab (equal (var-table-all-definedp (var-table-fix vartab)) (var-table-all-definedp vartab)))
Theorem:
(defthm var-table-all-definedp-var-table-equiv-congruence-on-vartab (implies (var-table-equiv vartab vartab-equiv) (equal (var-table-all-definedp vartab) (var-table-all-definedp vartab-equiv))) :rule-classes :congruence)