Proof that variable renaming preserves the safety of expressions.
If two expressions are related by variable renaming, and the old expression is safe, then the new expression is also safe, and it returns the same number of values as the old one. This is proved via the induction schema on two expressions simultaneously; it also involves lists of expressions and function calls. The renaming map is not updated here, because expressions do not introduce new variables.
Theorem:
(defthm check-safe-expression-when-renamevar (implies (not (reserrp (expression-renamevar old new ren))) (b* ((n-old (check-safe-expression old (varset-old ren) funtab)) (n-new (check-safe-expression new (varset-new ren) funtab))) (implies (not (reserrp n-old)) (and (not (reserrp n-new)) (equal n-new n-old))))))
Theorem:
(defthm check-safe-expression-list-when-renamevar (implies (not (reserrp (expression-list-renamevar old new ren))) (b* ((n-old (check-safe-expression-list old (varset-old ren) funtab)) (n-new (check-safe-expression-list new (varset-new ren) funtab))) (implies (not (reserrp n-old)) (and (not (reserrp n-new)) (equal n-new n-old))))))
Theorem:
(defthm check-safe-funcall-when-renamevar (implies (not (reserrp (funcall-renamevar old new ren))) (b* ((n-old (check-safe-funcall old (varset-old ren) funtab)) (n-new (check-safe-funcall new (varset-new ren) funtab))) (implies (not (reserrp n-old)) (and (not (reserrp n-new)) (equal n-new n-old))))))