		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Add-funs-to-fun-renaming

Add the function names in a list to a function renaming list.

Signature
(add-funs-to-fun-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-funs-to-fun-renaming

(defun add-funs-to-fun-renaming (old new ren)
 (declare (xargs :guard (and (identifier-listp old)
                             (identifier-listp new)
                             (renamingp ren))))
 (let ((__function__ 'add-funs-to-fun-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-fun-to-fun-renaming (car old)
                              (car new)
                              ren)))
   (add-funs-to-fun-renaming (cdr old)
                             (cdr new)
                             ren))))

Theorem: renaming-resultp-of-add-funs-to-fun-renaming

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

Theorem: same-len-when-add-funs-to-fun-renaming

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

Theorem: add-funs-to-fun-renaming-of-identifier-list-fix-old

(defthm add-funs-to-fun-renaming-of-identifier-list-fix-old
  (equal (add-funs-to-fun-renaming (identifier-list-fix old)
                                   new ren)
         (add-funs-to-fun-renaming old new ren)))

Theorem: add-funs-to-fun-renaming-identifier-list-equiv-congruence-on-old

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

Theorem: add-funs-to-fun-renaming-of-identifier-list-fix-new

(defthm add-funs-to-fun-renaming-of-identifier-list-fix-new
  (equal (add-funs-to-fun-renaming old (identifier-list-fix new)
                                   ren)
         (add-funs-to-fun-renaming old new ren)))

Theorem: add-funs-to-fun-renaming-identifier-list-equiv-congruence-on-new

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

Theorem: add-funs-to-fun-renaming-of-renaming-fix-ren

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

Theorem: add-funs-to-fun-renaming-renaming-equiv-congruence-on-ren

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