Proof that variable renaming preserves the safety of statements, blocks, and related entities.
This is proved via a custom induction schema that takes into account the recursive structure of the renaming functions and the safety checking functions.
The form of the theorems is as explained in renaming-variables-safety.
Theorem:
(defthm check-safe-statement-when-renamevar (b* ((ren1 (statement-renamevar old new ren)) (varsmodes-old (check-safe-statement old (varset-old ren) funtab)) (varsmodes-new (check-safe-statement new (varset-new ren) funtab))) (implies (and (not (reserrp ren1)) (not (reserrp varsmodes-old))) (and (not (reserrp varsmodes-new)) (equal (vars+modes->vars varsmodes-old) (varset-old ren1)) (equal (vars+modes->vars varsmodes-new) (varset-new ren1)) (equal (vars+modes->modes varsmodes-old) (vars+modes->modes varsmodes-new))))))
Theorem:
(defthm check-safe-statement-list-when-renamevar (b* ((ren1 (statement-list-renamevar old new ren)) (varsmodes-old (check-safe-statement-list old (varset-old ren) funtab)) (varsmodes-new (check-safe-statement-list new (varset-new ren) funtab))) (implies (and (not (reserrp ren1)) (not (reserrp varsmodes-old))) (and (not (reserrp varsmodes-new)) (equal (vars+modes->vars varsmodes-old) (varset-old ren1)) (equal (vars+modes->vars varsmodes-new) (varset-new ren1)) (equal (vars+modes->modes varsmodes-new) (vars+modes->modes varsmodes-old))))))
Theorem:
(defthm check-safe-block-when-renamevar (b* ((ok (block-renamevar old new ren)) (modes-old (check-safe-block old (varset-old ren) funtab)) (modes-new (check-safe-block new (varset-new ren) funtab))) (implies (and (not (reserrp ok)) (not (reserrp modes-old))) (and (not (reserrp modes-new)) (equal modes-new modes-old)))))
Theorem:
(defthm check-safe-block-option-when-renamevar (b* ((ok (block-option-renamevar old new ren)) (modes-old (check-safe-block-option old (varset-old ren) funtab)) (modes-new (check-safe-block-option new (varset-new ren) funtab))) (implies (and (not (reserrp ok)) (not (reserrp modes-old))) (and (not (reserrp modes-new)) (equal modes-new modes-old)))))
Theorem:
(defthm check-safe-swcase-when-renamevar (b* ((ok (swcase-renamevar old new ren)) (modes-old (check-safe-swcase old (varset-old ren) funtab)) (modes-new (check-safe-swcase new (varset-new ren) funtab))) (implies (and (not (reserrp ok)) (not (reserrp modes-old))) (and (not (reserrp modes-new)) (equal modes-new modes-old)))))
Theorem:
(defthm check-swcase-list-when-renamevar (b* ((ok (swcase-list-renamevar old new ren)) (modes-old (check-safe-swcase-list old (varset-old ren) funtab)) (modes-new (check-safe-swcase-list new (varset-new ren) funtab))) (implies (and (not (reserrp ok)) (not (reserrp modes-old))) (and (not (reserrp modes-new)) (equal modes-new modes-old)))))
Theorem:
(defthm check-safe-fundef-when-renamevar (b* ((ok (fundef-renamevar old new)) (ok-old (check-safe-fundef old funtab)) (ok-new (check-safe-fundef new funtab))) (implies (and (not (reserrp ok)) (not (reserrp ok-old))) (not (reserrp ok-new)))))