		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-execution

Exec-when-renamevar

Main theorems of the proof that variable renaming preserves the execution behavior.

We introduce a custom induction schema, which takes into account the recursive structure of all the functions involved in the proof. We introduce it locally.

Then we prove the theorems by mutual induction, using the flag macro from the custom induction schema. These theorems are also necessarily local, because the induction schema is local. Thus, we then restate the theorems non-locally.

We use computed hints to use separate hints for different cases of the induction. This makes the proof and its dependencies more clear.

Definitions and Theorems

Theorem: exec-expression-when-renamevar

(defthm exec-expression-when-renamevar
 (implies
  (and (not (reserrp (expression-renamevar old-expr new-expr ren)))
       (cstate-renamevarp old-cstate new-cstate ren)
       (funenv-renamevarp old-funenv new-funenv))
  (b* ((old-outcome
            (exec-expression old-expr old-cstate old-funenv limit))
       (new-outcome
            (exec-expression new-expr new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (eoutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-expression-list-when-renamevar

(defthm exec-expression-list-when-renamevar
 (implies
  (and
   (not
      (reserrp (expression-list-renamevar old-exprs new-exprs ren)))
   (cstate-renamevarp old-cstate new-cstate ren)
   (funenv-renamevarp old-funenv new-funenv))
  (b*
   ((old-outcome
       (exec-expression-list old-exprs old-cstate old-funenv limit))
    (new-outcome
      (exec-expression-list new-exprs new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (eoutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-funcall-when-renamevar

(defthm exec-funcall-when-renamevar
 (implies
  (and
     (not (reserrp (funcall-renamevar old-funcall new-funcall ren)))
     (cstate-renamevarp old-cstate new-cstate ren)
     (funenv-renamevarp old-funenv new-funenv))
  (b* ((old-outcome (exec-funcall old-funcall
                                  old-cstate old-funenv limit))
       (new-outcome (exec-funcall new-funcall
                                  new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (eoutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-function-when-renamevar

(defthm exec-function-when-renamevar
 (implies
  (and (cstate-renamevarp old-cstate new-cstate ren)
       (funenv-renamevarp old-funenv new-funenv))
  (b* ((old-outcome
            (exec-function fun args old-cstate old-funenv limit))
       (new-outcome
            (exec-function fun args new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (eoutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-statement-when-renamevar

(defthm exec-statement-when-renamevar
 (b* ((ren1 (statement-renamevar old-stmt new-stmt ren)))
  (implies
   (and (not (reserrp ren1))
        (cstate-renamevarp old-cstate new-cstate ren)
        (funenv-renamevarp old-funenv new-funenv))
   (b* ((old-outcome
             (exec-statement old-stmt old-cstate old-funenv limit))
        (new-outcome
             (exec-statement new-stmt new-cstate new-funenv limit)))
    (implies
      (and (not (reserr-nonlimitp old-outcome))
           (not (reserr-nonlimitp new-outcome)))
      (soutcome-result-renamevarp old-outcome new-outcome ren1))))))

Theorem: exec-statement-list-when-renamevar

(defthm exec-statement-list-when-renamevar
 (b* ((ren1 (statement-list-renamevar old-stmts new-stmts ren)))
  (implies
   (and (not (reserrp ren1))
        (cstate-renamevarp old-cstate new-cstate ren)
        (funenv-renamevarp old-funenv new-funenv))
   (b*
    ((old-outcome
        (exec-statement-list old-stmts old-cstate old-funenv limit))
     (new-outcome
       (exec-statement-list new-stmts new-cstate new-funenv limit)))
    (implies
      (and (not (reserr-nonlimitp old-outcome))
           (not (reserr-nonlimitp new-outcome)))
      (soutcome-result-renamevarp old-outcome new-outcome ren1))))))

Theorem: exec-block-when-renamevar

(defthm exec-block-when-renamevar
 (implies
  (and (not (reserrp (block-renamevar old-block new-block ren)))
       (cstate-renamevarp old-cstate new-cstate ren)
       (funenv-renamevarp old-funenv new-funenv))
  (b*
   ((old-outcome (exec-block old-block old-cstate old-funenv limit))
    (new-outcome
         (exec-block new-block new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (soutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-for-iterations-when-renamevar

(defthm exec-for-iterations-when-renamevar
 (implies
  (and (not (reserrp (expression-renamevar old-test new-test ren)))
       (not (reserrp (block-renamevar old-update new-update ren)))
       (not (reserrp (block-renamevar old-body new-body ren)))
       (cstate-renamevarp old-cstate new-cstate ren)
       (funenv-renamevarp old-funenv new-funenv))
  (b*
   ((old-outcome
         (exec-for-iterations old-test old-update
                              old-body old-cstate old-funenv limit))
    (new-outcome
        (exec-for-iterations new-test new-update
                             new-body new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (soutcome-result-renamevarp old-outcome new-outcome ren)))))

Theorem: exec-switch-rest-when-renamevar

(defthm exec-switch-rest-when-renamevar
 (implies
  (and
   (not (reserrp (swcase-list-renamevar old-cases new-cases ren)))
   (not
     (reserrp (block-option-renamevar old-default new-default ren)))
   (cstate-renamevarp old-cstate new-cstate ren)
   (funenv-renamevarp old-funenv new-funenv))
  (b* ((old-outcome
            (exec-switch-rest old-cases old-default
                              target old-cstate old-funenv limit))
       (new-outcome
            (exec-switch-rest new-cases new-default
                              target new-cstate new-funenv limit)))
   (implies
        (and (not (reserr-nonlimitp old-outcome))
             (not (reserr-nonlimitp new-outcome)))
        (soutcome-result-renamevarp old-outcome new-outcome ren)))))