		Search-engine friendly clone of the ACL2 documentation.

Renaming-variables

Add-vars-to-var-renaming

Add the variables in a list to a variable renaming list.

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

Definitions and Theorems

Function: add-vars-to-var-renaming

(defun add-vars-to-var-renaming (old new ren)
 (declare (xargs :guard (and (identifier-listp old)
                             (identifier-listp new)
                             (renamingp ren))))
 (let ((__function__ 'add-vars-to-var-renaming))
  (declare (ignorable __function__))
  (b*
   (((when (endp old))
     (if (endp new)
         (renaming-fix ren)
       (reserrf
            (list :mismatch-extra-new (identifier-list-fix new)))))
    ((when (endp new))
     (reserrf (list :mismatch-extra-old (identifier-list-fix old))))
    ((okf ren)
     (add-var-to-var-renaming (car old)
                              (car new)
                              ren)))
   (add-vars-to-var-renaming (cdr old)
                             (cdr new)
                             ren))))

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

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

Theorem: same-len-when-add-vars-to-var-renaming

(defthm same-len-when-add-vars-to-var-renaming
  (implies (not (reserrp (add-vars-to-var-renaming old new ren)))
           (equal (len new) (len old))))

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

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

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

(defthm var-renamevar-of-add-vars-to-var-renaming-when-var-renamevar
  (b* ((ren1 (add-vars-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: var-list-renamevar-when-add-vars-to-var-renaming

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

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

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

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

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

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

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

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

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

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

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

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

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