		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Add-var-to-var-renaming

Add a variable to a variable renaming list.

Signature
(add-var-to-var-renaming old new ren) → new-ren
Arguments: old — Guard (identifierp old).; new — Guard (identifierp new).; ren — Guard (renamingp ren).
Returns: new-ren — Type (renaming-resultp new-ren).

We check that the old variable is not already a key in the alist, and that the new variable is not already a value in the alist. This is always the case when processing statically safe code, because variables are added to the renaming list as they get in scope, and the static safety checks ensure that only variables not in scope are added to the scope. In fact, by checking this, we are checking that the code does not shadow variables.

Definitions and Theorems

Function: add-var-to-var-renaming

(defun add-var-to-var-renaming (old new ren)
  (declare (xargs :guard (and (identifierp old)
                              (identifierp new)
                              (renamingp ren))))
  (let ((__function__ 'add-var-to-var-renaming))
    (declare (ignorable __function__))
    (b* ((old (identifier-fix old))
         (new (identifier-fix new))
         (list (renaming->list ren))
         ((when (member-equal old (strip-cars list)))
          (reserrf (list :old-var-already-in-scope
                         old new (renaming-fix ren))))
         ((when (member-equal new (strip-cdrs list)))
          (reserrf (list :new-var-already-in-scope
                         old new (renaming-fix ren)))))
      (renaming (cons (cons old new) list)))))

Theorem: renaming-resultp-of-add-var-to-var-renaming

(defthm renaming-resultp-of-add-var-to-var-renaming
  (b* ((new-ren (add-var-to-var-renaming old new ren)))
    (renaming-resultp new-ren))
  :rule-classes :rewrite)

Theorem: subsetp-equal-of-add-var-to-var-renaming

(defthm subsetp-equal-of-add-var-to-var-renaming
  (b* ((ren1 (add-var-to-var-renaming old new ren)))
    (implies (not (reserrp ren1))
             (subsetp-equal (renaming->list ren)
                            (renaming->list ren1)))))

Theorem: renaming-old/new-of-add-var-to-var-renaming

(defthm renaming-old/new-of-add-var-to-var-renaming
 (implies
    (and (identifierp old-var)
         (identifierp new-var))
    (b* ((ren1 (add-var-to-var-renaming old-var new-var ren)))
      (implies (not (reserrp ren1))
               (and (equal (renaming-old ren1)
                           (insert old-var (renaming-old ren)))
                    (equal (renaming-new ren1)
                           (insert new-var (renaming-new ren))))))))

Theorem: var-renamevar-when-add-var-to-var-renaming

(defthm var-renamevar-when-add-var-to-var-renaming
  (b* ((ren1 (add-var-to-var-renaming old new ren)))
    (implies (not (reserrp ren1))
             (not (reserrp (var-renamevar old new ren1))))))

Theorem: var-renamevar-of-add-var-to-var-renaming-when-var-renamevar

(defthm var-renamevar-of-add-var-to-var-renaming-when-var-renamevar
  (b* ((ren1 (add-var-to-var-renaming old1 new1 ren)))
    (implies (and (not (reserrp ren1))
                  (not (reserrp (var-renamevar old new ren))))
             (not (reserrp (var-renamevar old new ren1))))))

Theorem: add-var-to-var-renaming-of-identifier-fix-old

(defthm add-var-to-var-renaming-of-identifier-fix-old
  (equal (add-var-to-var-renaming (identifier-fix old)
                                  new ren)
         (add-var-to-var-renaming old new ren)))

Theorem: add-var-to-var-renaming-identifier-equiv-congruence-on-old

(defthm add-var-to-var-renaming-identifier-equiv-congruence-on-old
  (implies (identifier-equiv old old-equiv)
           (equal (add-var-to-var-renaming old new ren)
                  (add-var-to-var-renaming old-equiv new ren)))
  :rule-classes :congruence)

Theorem: add-var-to-var-renaming-of-identifier-fix-new

(defthm add-var-to-var-renaming-of-identifier-fix-new
  (equal (add-var-to-var-renaming old (identifier-fix new)
                                  ren)
         (add-var-to-var-renaming old new ren)))

Theorem: add-var-to-var-renaming-identifier-equiv-congruence-on-new

(defthm add-var-to-var-renaming-identifier-equiv-congruence-on-new
  (implies (identifier-equiv new new-equiv)
           (equal (add-var-to-var-renaming old new ren)
                  (add-var-to-var-renaming old new-equiv ren)))
  :rule-classes :congruence)

Theorem: add-var-to-var-renaming-of-renaming-fix-ren

(defthm add-var-to-var-renaming-of-renaming-fix-ren
  (equal (add-var-to-var-renaming old new (renaming-fix ren))
         (add-var-to-var-renaming old new ren)))

Theorem: add-var-to-var-renaming-renaming-equiv-congruence-on-ren

(defthm add-var-to-var-renaming-renaming-equiv-congruence-on-ren
  (implies (renaming-equiv ren ren-equiv)
           (equal (add-var-to-var-renaming old new ren)
                  (add-var-to-var-renaming old new ren-equiv)))
  :rule-classes :congruence)