Add a function name to a function renaming list.
(add-fun-to-fun-renaming old new ren) → new-ren
This is quite analogous to add-var-to-var-renaming. See its documentation.
Function:
(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:
(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:
(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:
(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:
(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:
(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:
(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:
(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)