Basic substitution operation for 4v-sexprs.
(4v-sexpr-restrict x al) takes a sexpr,
We memoize this function to avoid repeatedly restricting shared
subexpressions, but this only helps when you are restricting with the same
alist. We don't use
Note that this function is "dumb" and does not try in any way to simplify the resulting expressions. The function 4v-sexpr-restrict-with-rw is a "smarter" alternative that is generally slower but can produce simpler sexprs as output.
(defun 4v-sexpr-restrict (x al) (declare (xargs :guard t)) (if (atom x) (and x (let ((look (hons-get x al))) (if look (cdr look) x))) (hons (car x) (4v-sexpr-restrict-list (cdr x) al))))
(defun 4v-sexpr-restrict-list (x al) (declare (xargs :guard t)) (if (atom x) x (hons (4v-sexpr-restrict (car x) al) (4v-sexpr-restrict-list (cdr x) al))))
(defun 4v-sexpr-restrict-memoize-condition (x al) (declare (ignorable x al) (xargs :guard 't)) (and (consp x) (consp (cdr x))))
(defthm 4v-sexpr-eval-4v-sexpr-restrict (equal (4v-sexpr-eval (4v-sexpr-restrict x al1) al2) (4v-sexpr-eval x (append (4v-sexpr-eval-alist al1 al2) al2))))
(defthm 4v-sexpr-eval-list-sexpr-4v-sexpr-restrict-list (equal (4v-sexpr-eval-list (4v-sexpr-restrict-list x al1) al2) (4v-sexpr-eval-list x (append (4v-sexpr-eval-alist al1 al2) al2))))