Check if two lists of function definitions are related by function renaming.
(fundef-list-renamefun old new ren) → _
This is just a lifting of fundef-renamefun to lists. It does not add anything new to the definition of function renaming, but it is a useful derived concept.
We prove that if two lists of statements are related by function renaming, then the lists of function definitions extracted from the statements are also related by function renaming. We prove this by simultaneous induction on the two lists of statements.
Function:
(defun fundef-list-renamefun (old new ren) (declare (xargs :guard (and (fundef-listp old) (fundef-listp new) (renamingp ren)))) (let ((__function__ 'fundef-list-renamefun)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) nil (reserrf (list :mismatch-extra-new (fundef-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (fundef-list-fix old)))) ((okf &) (fundef-renamefun (car old) (car new) ren))) (fundef-list-renamefun (cdr old) (cdr new) ren))))
Theorem:
(defthm reserr-optionp-of-fundef-list-renamefun (b* ((_ (fundef-list-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm fundef-list-renamefun-of-statement-to-fundefs (implies (not (reserrp (statement-list-renamefun old new ren))) (not (reserrp (fundef-list-renamefun (statements-to-fundefs old) (statements-to-fundefs new) ren)))))
Theorem:
(defthm fundef-list-renamefun-of-fundef-list-fix-old (equal (fundef-list-renamefun (fundef-list-fix old) new ren) (fundef-list-renamefun old new ren)))
Theorem:
(defthm fundef-list-renamefun-fundef-list-equiv-congruence-on-old (implies (fundef-list-equiv old old-equiv) (equal (fundef-list-renamefun old new ren) (fundef-list-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm fundef-list-renamefun-of-fundef-list-fix-new (equal (fundef-list-renamefun old (fundef-list-fix new) ren) (fundef-list-renamefun old new ren)))
Theorem:
(defthm fundef-list-renamefun-fundef-list-equiv-congruence-on-new (implies (fundef-list-equiv new new-equiv) (equal (fundef-list-renamefun old new ren) (fundef-list-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm fundef-list-renamefun-of-renaming-fix-ren (equal (fundef-list-renamefun old new (renaming-fix ren)) (fundef-list-renamefun old new ren)))
Theorem:
(defthm fundef-list-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (fundef-list-renamefun old new ren) (fundef-list-renamefun old new ren-equiv))) :rule-classes :congruence)