Theorems about restricting variables in parallel executions related by variable renaming.
See restrict-vars-when-renamevar for background and motivation. The following two lemmas are make use of the theorems there to show that, during the execution of certain constructs, the variable renaming relation between computation states is preserved. These lemmas are directly used in the main theorems.
Theorem:
(defthm exec-when-renamevar-restrict-vars-lemma-1 (implies (and (not (reserrp (statement-list-renamevar old-stmts new-stmts ren))) (not (reserrp (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit)))) (not (reserrp (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit)))) (cstate-renamevarp old-cstate new-cstate ren) (cstate-renamevarp (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (statement-list-renamevar old-stmts new-stmts ren))) (cstate-renamevarp (restrict-vars (omap::keys (cstate->local old-cstate)) (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit)))) (restrict-vars (omap::keys (cstate->local new-cstate)) (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit)))) ren)))
Theorem:
(defthm exec-when-renamevar-restrict-vars-lemma-2 (implies (and (not (reserrp (statement-list-renamevar old-stmts new-stmts ren))) (not (reserrp (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit)))) (not (reserrp (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit)))) (cstate-renamevarp old-cstate new-cstate ren) (cstate-renamevarp (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (statement-list-renamevar old-stmts new-stmts ren)) (not (reserrp (exec-for-iterations old-test old-update old-body (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit)))) (not (reserrp (exec-for-iterations new-test new-update new-body (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit)))) (cstate-renamevarp (soutcome->cstate (exec-for-iterations old-test old-update old-body (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (soutcome->cstate (exec-for-iterations new-test new-update new-body (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (statement-list-renamevar old-stmts new-stmts ren))) (cstate-renamevarp (restrict-vars (omap::keys (cstate->local old-cstate)) (soutcome->cstate (exec-for-iterations old-test old-update old-body (soutcome->cstate (exec-statement-list old-stmts old-cstate (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs old-stmts) old-funenv) (+ -1 limit)))) (restrict-vars (omap::keys (cstate->local new-cstate)) (soutcome->cstate (exec-for-iterations new-test new-update new-body (soutcome->cstate (exec-statement-list new-stmts new-cstate (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit))) (add-funs (statements-to-fundefs new-stmts) new-funenv) (+ -1 limit)))) ren)))