		Search-engine friendly clone of the ACL2 documentation.

Renaming-functions

Add-fun-to-fun-renaming

Add a function name to a function renaming list.

Signature
(add-fun-to-fun-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).

This is quite analogous to add-var-to-var-renaming. See its documentation.

Definitions and Theorems

Function: add-fun-to-fun-renaming

(defun add-fun-to-fun-renaming (old new ren)
  (declare (xargs :guard (and (identifierp old)
                              (identifierp new)
                              (renamingp ren))))
  (let ((__function__ 'add-fun-to-fun-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-fun-already-in-scope
                         old new (renaming-fix ren))))
         ((when (member-equal new (strip-cdrs list)))
          (reserrf (list :new-fun-already-in-scope
                         old new (renaming-fix ren)))))
      (renaming (cons (cons old new) list)))))

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

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

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

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

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

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

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

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

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

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

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

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

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

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