		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables-safety

Renaming-variables-statements/blocks/cases/fundefs-safety

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.

Definitions and Theorems

Theorem: check-safe-statement-when-renamevar

(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: check-safe-statement-list-when-renamevar

(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: check-safe-block-when-renamevar

(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: check-safe-block-option-when-renamevar

(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: check-safe-swcase-when-renamevar

(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: check-swcase-list-when-renamevar

(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: check-safe-fundef-when-renamevar

(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)))))