Theorems about function environments and variable renaming.
If two function definitions are related by variable renaming, their corresponding function information is as well.
If two lists of function definitions are related, so are the corresponding scopes. This is proved via an intermediate theorem saying that adding related function information to related function scopes yields related function scopes.
Adding related function definitions to related function environments yields related function environments. This concerns add-funs.
Retrieving the same function from related function scopes yields related function information.
Related function scopes have the same keys. This is stated in two slightly different theorems.
If two function environments are related, so are their cdrs.
Finding a function from related function environments yields related information and remaining environments.
If two lists of function definitions are related, their corresponding scopes are either both errors or none.
Two related function scopes and two related function environments have the same disjointness status.
Adding related function definitions to related function environments yields either two errors or no errors.
Theorem:
(defthm funinfo-renamevarp-of-funinfo-for-fundef (implies (not (reserrp (fundef-renamevar old new))) (funinfo-renamevarp (funinfo-for-fundef old) (funinfo-for-fundef new))))
Theorem:
(defthm funscope-renamevarp-of-update (implies (and (funscopep old-scope) (funscopep new-scope) (funinfop old-info) (funinfop new-info) (identifierp fun) (funscope-renamevarp old-scope new-scope) (funinfo-renamevarp old-info new-info)) (funscope-renamevarp (omap::update fun old-info old-scope) (omap::update fun new-info new-scope))))
Theorem:
(defthm funscope-renamevarp-of-funscope-for-fundefs (implies (not (reserrp (fundef-list-renamevar old-funs new-funs))) (b* ((old-scope1 (funscope-for-fundefs old-funs)) (new-scope1 (funscope-for-fundefs new-funs))) (implies (and (not (reserrp old-scope1)) (not (reserrp new-scope1))) (funscope-renamevarp old-scope1 new-scope1)))))
Theorem:
(defthm funenv-renamevarp-of-add-funs (implies (and (funenv-renamevarp old-env new-env) (not (reserrp (fundef-list-renamevar old-funs new-funs)))) (b* ((old-env1 (add-funs old-funs old-env)) (new-env1 (add-funs new-funs new-env))) (implies (and (not (reserrp old-env1)) (not (reserrp new-env1))) (funenv-renamevarp old-env1 new-env1)))))
Theorem:
(defthm funinfo-renamevarp-when-funscope-renamevarp (implies (and (funscopep old-scope) (funscopep new-scope) (funscope-renamevarp old-scope new-scope)) (b* ((old-fun+info (omap::assoc fun old-scope)) (new-fun+info (omap::assoc fun new-scope))) (implies (and (consp old-fun+info) (consp new-fun+info)) (funinfo-renamevarp (cdr old-fun+info) (cdr new-fun+info))))))
Theorem:
(defthm same-in-when-funscope-renamevarp (implies (and (funscopep old-scope) (funscopep new-scope) (funscope-renamevarp old-scope new-scope)) (equal (consp (omap::assoc fun old-scope)) (consp (omap::assoc fun new-scope)))))
Theorem:
(defthm same-funscope-keys-when-renamevar (implies (and (funscopep old) (funscopep new) (funscope-renamevarp old new)) (equal (omap::keys old) (omap::keys new))))
Theorem:
(defthm funenv-renamevarp-of-cdr (implies (funenv-renamevarp old-env new-env) (funenv-renamevarp (cdr old-env) (cdr new-env))))
Theorem:
(defthm funinfo+funenv-renamevarp-of-find-fun (implies (funenv-renamevarp old-env new-env) (b* ((old-info+env (find-fun fun old-env)) (new-info+env (find-fun fun new-env)) (old-info (funinfo+funenv->info old-info+env)) (new-info (funinfo+funenv->info new-info+env)) (old-env1 (funinfo+funenv->env old-info+env)) (new-env1 (funinfo+funenv->env new-info+env))) (implies (and (not (reserrp old-info+env)) (not (reserrp new-info+env))) (and (funinfo-renamevarp old-info new-info) (funenv-renamevarp old-env1 new-env1))))))
Theorem:
(defthm same-funscope-for-fundefs-error-when-renamevar (implies (not (reserrp (fundef-list-renamevar old-funs new-funs))) (b* ((old-scope1 (funscope-for-fundefs old-funs)) (new-scope1 (funscope-for-fundefs new-funs))) (equal (reserrp old-scope1) (reserrp new-scope1)))))
Theorem:
(defthm same-ensure-funscope-disjoint-when-renamevar (implies (and (funscope-renamevarp old-funscope new-funscope) (funenv-renamevarp old-funenv new-funenv)) (equal (ensure-funscope-disjoint old-funscope old-funenv) (ensure-funscope-disjoint new-funscope new-funenv))))
Theorem:
(defthm same-add-funs-error-when-renamevar (implies (and (funenv-renamevarp old-funenv new-funenv) (not (reserrp (fundef-list-renamevar old-funs new-funs)))) (b* ((old-funenv1 (add-funs old-funs old-funenv)) (new-funenv1 (add-funs new-funs new-funenv))) (equal (reserrp old-funenv1) (reserrp new-funenv1)))))