Replace terms by variables, even inside lambda bodies

WARNING: This utility takes an alist that maps terms to variables.
In that sense it is more restrictive than the corresponding utility that is
built into ACL2,

General Form: (sublis-expr+ alist term)

where `term`. The value is a term that results from replacing
occurrences of terms in the domain of

Consider the following example, which for readability is expressed in terms of untranslated terms.

alist: (((nth '0 (binary-append a b)) . x) ((nth '1 (binary-append a b)) . y)) term (untranslated): (let ((u (cons (nth 0 (append a b)) (nth 1 (append a b))))) (cons (nth 0 (append a b)) u)) result (untranslated): (let ((u (cons x y))) (cons x u))

Note that substitution occurred even inside the body of the input

ACL2 !>(sublis-expr+ '(((nth '0 (binary-append a b)) . x) ((nth '1 (binary-append a b)) . y)) '((lambda (u b a) (cons (nth '0 (binary-append a b)) u)) (cons (nth '0 (binary-append a b)) (nth '1 (binary-append a b))) b a)) ((LAMBDA (U B A) (CONS X U)) (CONS X Y) B A) ACL2 !>

Remark. Notice that a simpler term that is equivalent to the one above is as follows.

((LAMBDA (U) (CONS X U)) (CONS X Y))

Indeed, they both untranslate to:

Finally, we note that variable capture is avoided, as illustrated by the
following example. Consider the (untranslated) input

ACL2 !>(sublis-expr+ '((x . u)) '((lambda (u x) (cons x u)) (cons x y) x)) ((LAMBDA (U X) (CONS X U)) (CONS U Y) U) ACL2 !>(untranslate ; input '((lambda (u x) (cons x u)) (cons x y) x) nil (w state)) (LET ((U (CONS X Y))) (CONS X U)) ACL2 !>(untranslate ; result '((LAMBDA (U X) (CONS X U)) (CONS U Y) U) nil (w state)) (LET ((U (CONS U Y)) (X U)) (CONS X U)) ACL2 !>

It would also be an error to replace

ACL2 !>(sublis-expr+ '((u . x)) '((lambda (u x) (cons x u)) (cons x y) x)) ((LAMBDA (U X) (CONS X U)) (CONS X Y) X) ACL2 !>(untranslate ; new result '((LAMBDA (U X) (CONS X U)) (CONS X Y) X) nil (w state)) (LET ((U (CONS X Y))) (CONS X U)) ACL2 !>

It would also have been correct to rename the bound variable, to produce the
result