Check if two lists of function definitions are related by variable renaming.
(fundef-list-renamevar old new) → _
This is just a lifting of fundef-renamevar to lists. It does not add anything new to the definition of variable renaming, but it is a useful derived concept.
We prove that if two lists of statements are related by variable renaming, then the lists of function definitions extracted from the statements are also related by variable renaming. We prove this by simultaneous induction on the two lists of statements also involving the renaming and its updating according to the initial statements in the lists.
Function:
(defun fundef-list-renamevar (old new) (declare (xargs :guard (and (fundef-listp old) (fundef-listp new)))) (let ((__function__ 'fundef-list-renamevar)) (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-renamevar (car old) (car new)))) (fundef-list-renamevar (cdr old) (cdr new)))))
Theorem:
(defthm reserr-optionp-of-fundef-list-renamevar (b* ((_ (fundef-list-renamevar old new))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm fundef-list-renamevar-of-statement-to-fundefs (implies (not (reserrp (statement-list-renamevar old new ren))) (not (reserrp (fundef-list-renamevar (statements-to-fundefs old) (statements-to-fundefs new))))))
Theorem:
(defthm fundef-list-renamevar-of-fundef-list-fix-old (equal (fundef-list-renamevar (fundef-list-fix old) new) (fundef-list-renamevar old new)))
Theorem:
(defthm fundef-list-renamevar-fundef-list-equiv-congruence-on-old (implies (fundef-list-equiv old old-equiv) (equal (fundef-list-renamevar old new) (fundef-list-renamevar old-equiv new))) :rule-classes :congruence)
Theorem:
(defthm fundef-list-renamevar-of-fundef-list-fix-new (equal (fundef-list-renamevar old (fundef-list-fix new)) (fundef-list-renamevar old new)))
Theorem:
(defthm fundef-list-renamevar-fundef-list-equiv-congruence-on-new (implies (fundef-list-equiv new new-equiv) (equal (fundef-list-renamevar old new) (fundef-list-renamevar old new-equiv))) :rule-classes :congruence)