Rename all the occurrences of a rule name to a new rule name, in all the rules in a list of rules.
Function:
(defun rulelist-rename-rule (rules oldname newname) (declare (xargs :guard (and (rulelistp rules) (rulenamep oldname) (rulenamep newname)))) (cond ((endp rules) nil) (t (cons (rule-rename-rule (car rules) oldname newname) (rulelist-rename-rule (cdr rules) oldname newname)))))
Theorem:
(defthm rulelistp-of-rulelist-rename-rule (b* ((new-rules (rulelist-rename-rule rules oldname newname))) (rulelistp new-rules)) :rule-classes :rewrite)