Extension of 4v-sexpr-restrict to alists.
(4v-sexpr-restrict-alist x al) is given an alist
It is beneficial for
Function:
(defun 4v-sexpr-restrict-alist1 (x al) "Assumes AL is fast" (declare (xargs :guard t)) (cond ((atom x) nil) ((atom (car x)) (4v-sexpr-restrict-alist1 (cdr x) al)) (t (cons (cons (caar x) (4v-sexpr-restrict (cdar x) al)) (4v-sexpr-restrict-alist1 (cdr x) al)))))
Function:
(defun 4v-sexpr-restrict-alist (x al) "Makes AL fast if necessary" (declare (xargs :guard t)) (mbe :logic (cond ((atom x) nil) ((atom (car x)) (4v-sexpr-restrict-alist (cdr x) al)) (t (cons (cons (caar x) (4v-sexpr-restrict (cdar x) al)) (4v-sexpr-restrict-alist (cdr x) al)))) :exec (with-fast-alist al (4v-sexpr-restrict-alist1 x al))))
Theorem:
(defthm 4v-sexpr-restrict-alist1-removal (equal (4v-sexpr-restrict-alist1 x al) (4v-sexpr-restrict-alist x al)))
Theorem:
(defthm 4v-sexpr-eval-alist-4v-sexpr-restrict-alist (equal (4v-sexpr-eval-alist (4v-sexpr-restrict-alist x al) env) (4v-sexpr-eval-alist x (append (4v-sexpr-eval-alist al env) env))))
Theorem:
(defthm hons-assoc-equal-4v-sexpr-restrict-alist (equal (hons-assoc-equal x (4v-sexpr-restrict-alist al env)) (and (hons-assoc-equal x al) (cons x (4v-sexpr-restrict (cdr (hons-assoc-equal x al)) env)))))
Theorem:
(defthm alist-keys-4v-sexpr-restrict-alist (equal (alist-keys (4v-sexpr-restrict-alist al env)) (alist-keys al)))
Theorem:
(defthm alist-equiv-implies-alist-equiv-4v-sexpr-restrict-alist-1 (implies (alist-equiv a a-equiv) (alist-equiv (4v-sexpr-restrict-alist a b) (4v-sexpr-restrict-alist a-equiv b))) :rule-classes (:congruence))