Mutually recursive ACL2 functions to check if statements, blocks, cases, and function definitions are related by function renaming.
Function:
(defun statement-renamefun (old new ren) (declare (xargs :guard (and (statementp old) (statementp new) (renamingp ren)))) (let ((__function__ 'statement-renamefun)) (declare (ignorable __function__)) (statement-case old :block (b* (((unless (statement-case new :block)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-block new) new) ((okf &) (block-renamefun old.get new.get ren))) nil) :variable-single (b* (((unless (statement-case new :variable-single)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-variable-single new) new) ((unless (equal old.name new.name)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((okf &) (expression-option-renamefun old.init new.init ren))) nil) :variable-multi (b* (((unless (statement-case new :variable-multi)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-variable-multi new) new) ((unless (equal old.names new.names)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((okf &) (funcall-option-renamefun old.init new.init ren))) nil) :assign-single (b* (((unless (statement-case new :assign-single)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-assign-single new) new) ((unless (equal old.target new.target)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((okf &) (expression-renamefun old.value new.value ren))) nil) :assign-multi (b* (((unless (statement-case new :assign-multi)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-assign-multi new) new) ((unless (equal old.targets new.targets)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((okf &) (funcall-renamefun old.value new.value ren))) nil) :funcall (b* (((unless (statement-case new :funcall)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-funcall new) new) ((okf &) (funcall-renamefun old.get new.get ren))) nil) :if (b* (((unless (statement-case new :if)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-if new) new) ((okf &) (expression-renamefun old.test new.test ren)) ((okf &) (block-renamefun old.body new.body ren))) nil) :for (b* (((unless (statement-case new :for)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-for new) new) (old-stmts (block->statements old.init)) (new-stmts (block->statements new.init)) (old-funs (fundef-list->name-list (statements-to-fundefs old-stmts))) (new-funs (fundef-list->name-list (statements-to-fundefs new-stmts))) ((okf ren) (add-funs-to-fun-renaming old-funs new-funs ren)) ((okf &) (statement-list-renamefun old-stmts new-stmts ren)) ((okf &) (expression-renamefun old.test new.test ren)) ((okf &) (block-renamefun old.update new.update ren)) ((okf &) (block-renamefun old.body new.body ren))) nil) :switch (b* (((unless (statement-case new :switch)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-switch new) new) ((okf &) (expression-renamefun old.target new.target ren)) ((okf &) (swcase-list-renamefun old.cases new.cases ren)) ((okf &) (block-option-renamefun old.default new.default ren))) nil) :leave (b* (((unless (statement-case new :leave)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) nil) :break (b* (((unless (statement-case new :break)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) nil) :continue (b* (((unless (statement-case new :continue)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) nil) :fundef (b* (((unless (statement-case new :fundef)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-fundef new) new) ((okf &) (fundef-renamefun old.get new.get ren))) nil))))
Function:
(defun statement-list-renamefun (old new ren) (declare (xargs :guard (and (statement-listp old) (statement-listp new) (renamingp ren)))) (let ((__function__ 'statement-list-renamefun)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) nil (reserrf (list :mismatch-extra-new (statement-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (statement-list-fix old)))) ((okf &) (statement-renamefun (car old) (car new) ren))) (statement-list-renamefun (cdr old) (cdr new) ren))))
Function:
(defun block-renamefun (old new ren) (declare (xargs :guard (and (blockp old) (blockp new) (renamingp ren)))) (let ((__function__ 'block-renamefun)) (declare (ignorable __function__)) (b* ((old-stmts (block->statements old)) (new-stmts (block->statements new)) (old-fns (fundef-list->name-list (statements-to-fundefs old-stmts))) (new-fns (fundef-list->name-list (statements-to-fundefs new-stmts))) ((okf ren) (add-funs-to-fun-renaming old-fns new-fns ren)) ((okf &) (statement-list-renamefun old-stmts new-stmts ren))) nil)))
Function:
(defun block-option-renamefun (old new ren) (declare (xargs :guard (and (block-optionp old) (block-optionp new) (renamingp ren)))) (let ((__function__ 'block-option-renamefun)) (declare (ignorable __function__)) (block-option-case old :none (if (block-option-case new :none) nil (reserrf (list :mismatch (block-option-fix old) (block-option-fix new)))) :some (block-option-case new :none (reserrf (list :mismatch (block-option-fix old) (block-option-fix new))) :some (block-renamefun (block-option-some->val old) (block-option-some->val new) ren)))))
Function:
(defun swcase-renamefun (old new ren) (declare (xargs :guard (and (swcasep old) (swcasep new) (renamingp ren)))) (let ((__function__ 'swcase-renamefun)) (declare (ignorable __function__)) (b* (((unless (equal (swcase->value old) (swcase->value new))) (reserrf (list :mismatch-case-value (swcase->value old) (swcase->value new))))) (block-renamefun (swcase->body old) (swcase->body new) ren))))
Function:
(defun swcase-list-renamefun (old new ren) (declare (xargs :guard (and (swcase-listp old) (swcase-listp new) (renamingp ren)))) (let ((__function__ 'swcase-list-renamefun)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) nil (reserrf (list :mismatch-extra-new (swcase-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (swcase-list-fix old)))) ((okf &) (swcase-renamefun (car old) (car new) ren))) (swcase-list-renamefun (cdr old) (cdr new) ren))))
Function:
(defun fundef-renamefun (old new ren) (declare (xargs :guard (and (fundefp old) (fundefp new) (renamingp ren)))) (let ((__function__ 'fundef-renamefun)) (declare (ignorable __function__)) (b* (((okf &) (fun-renamefun (fundef->name old) (fundef->name new) ren)) ((unless (equal (fundef->inputs old) (fundef->inputs new))) (reserrf (list :mismatch (fundef-fix old) (fundef-fix new)))) ((unless (equal (fundef->outputs old) (fundef->outputs new))) (reserrf (list :mismatch (fundef-fix old) (fundef-fix new))))) (block-renamefun (fundef->body old) (fundef->body new) ren))))
Theorem:
(defthm return-type-of-statement-renamefun._ (b* ((?_ (statement-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-statement-list-renamefun._ (b* ((?_ (statement-list-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-renamefun._ (b* ((?_ (block-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-option-renamefun._ (b* ((?_ (block-option-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-renamefun._ (b* ((?_ (swcase-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-list-renamefun._ (b* ((?_ (swcase-list-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-fundef-renamefun._ (b* ((?_ (fundef-renamefun old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm statement-renamefun-of-statement-fix-old (equal (statement-renamefun (statement-fix old) new ren) (statement-renamefun old new ren)))
Theorem:
(defthm statement-renamefun-of-statement-fix-new (equal (statement-renamefun old (statement-fix new) ren) (statement-renamefun old new ren)))
Theorem:
(defthm statement-renamefun-of-renaming-fix-ren (equal (statement-renamefun old new (renaming-fix ren)) (statement-renamefun old new ren)))
Theorem:
(defthm statement-list-renamefun-of-statement-list-fix-old (equal (statement-list-renamefun (statement-list-fix old) new ren) (statement-list-renamefun old new ren)))
Theorem:
(defthm statement-list-renamefun-of-statement-list-fix-new (equal (statement-list-renamefun old (statement-list-fix new) ren) (statement-list-renamefun old new ren)))
Theorem:
(defthm statement-list-renamefun-of-renaming-fix-ren (equal (statement-list-renamefun old new (renaming-fix ren)) (statement-list-renamefun old new ren)))
Theorem:
(defthm block-renamefun-of-block-fix-old (equal (block-renamefun (block-fix old) new ren) (block-renamefun old new ren)))
Theorem:
(defthm block-renamefun-of-block-fix-new (equal (block-renamefun old (block-fix new) ren) (block-renamefun old new ren)))
Theorem:
(defthm block-renamefun-of-renaming-fix-ren (equal (block-renamefun old new (renaming-fix ren)) (block-renamefun old new ren)))
Theorem:
(defthm block-option-renamefun-of-block-option-fix-old (equal (block-option-renamefun (block-option-fix old) new ren) (block-option-renamefun old new ren)))
Theorem:
(defthm block-option-renamefun-of-block-option-fix-new (equal (block-option-renamefun old (block-option-fix new) ren) (block-option-renamefun old new ren)))
Theorem:
(defthm block-option-renamefun-of-renaming-fix-ren (equal (block-option-renamefun old new (renaming-fix ren)) (block-option-renamefun old new ren)))
Theorem:
(defthm swcase-renamefun-of-swcase-fix-old (equal (swcase-renamefun (swcase-fix old) new ren) (swcase-renamefun old new ren)))
Theorem:
(defthm swcase-renamefun-of-swcase-fix-new (equal (swcase-renamefun old (swcase-fix new) ren) (swcase-renamefun old new ren)))
Theorem:
(defthm swcase-renamefun-of-renaming-fix-ren (equal (swcase-renamefun old new (renaming-fix ren)) (swcase-renamefun old new ren)))
Theorem:
(defthm swcase-list-renamefun-of-swcase-list-fix-old (equal (swcase-list-renamefun (swcase-list-fix old) new ren) (swcase-list-renamefun old new ren)))
Theorem:
(defthm swcase-list-renamefun-of-swcase-list-fix-new (equal (swcase-list-renamefun old (swcase-list-fix new) ren) (swcase-list-renamefun old new ren)))
Theorem:
(defthm swcase-list-renamefun-of-renaming-fix-ren (equal (swcase-list-renamefun old new (renaming-fix ren)) (swcase-list-renamefun old new ren)))
Theorem:
(defthm fundef-renamefun-of-fundef-fix-old (equal (fundef-renamefun (fundef-fix old) new ren) (fundef-renamefun old new ren)))
Theorem:
(defthm fundef-renamefun-of-fundef-fix-new (equal (fundef-renamefun old (fundef-fix new) ren) (fundef-renamefun old new ren)))
Theorem:
(defthm fundef-renamefun-of-renaming-fix-ren (equal (fundef-renamefun old new (renaming-fix ren)) (fundef-renamefun old new ren)))
Theorem:
(defthm statement-renamefun-statement-equiv-congruence-on-old (implies (statement-equiv old old-equiv) (equal (statement-renamefun old new ren) (statement-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm statement-renamefun-statement-equiv-congruence-on-new (implies (statement-equiv new new-equiv) (equal (statement-renamefun old new ren) (statement-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm statement-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (statement-renamefun old new ren) (statement-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamefun-statement-list-equiv-congruence-on-old (implies (statement-list-equiv old old-equiv) (equal (statement-list-renamefun old new ren) (statement-list-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamefun-statement-list-equiv-congruence-on-new (implies (statement-list-equiv new new-equiv) (equal (statement-list-renamefun old new ren) (statement-list-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (statement-list-renamefun old new ren) (statement-list-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-renamefun-block-equiv-congruence-on-old (implies (block-equiv old old-equiv) (equal (block-renamefun old new ren) (block-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm block-renamefun-block-equiv-congruence-on-new (implies (block-equiv new new-equiv) (equal (block-renamefun old new ren) (block-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm block-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (block-renamefun old new ren) (block-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamefun-block-option-equiv-congruence-on-old (implies (block-option-equiv old old-equiv) (equal (block-option-renamefun old new ren) (block-option-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamefun-block-option-equiv-congruence-on-new (implies (block-option-equiv new new-equiv) (equal (block-option-renamefun old new ren) (block-option-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (block-option-renamefun old new ren) (block-option-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamefun-swcase-equiv-congruence-on-old (implies (swcase-equiv old old-equiv) (equal (swcase-renamefun old new ren) (swcase-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamefun-swcase-equiv-congruence-on-new (implies (swcase-equiv new new-equiv) (equal (swcase-renamefun old new ren) (swcase-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (swcase-renamefun old new ren) (swcase-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamefun-swcase-list-equiv-congruence-on-old (implies (swcase-list-equiv old old-equiv) (equal (swcase-list-renamefun old new ren) (swcase-list-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamefun-swcase-list-equiv-congruence-on-new (implies (swcase-list-equiv new new-equiv) (equal (swcase-list-renamefun old new ren) (swcase-list-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (swcase-list-renamefun old new ren) (swcase-list-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm fundef-renamefun-fundef-equiv-congruence-on-old (implies (fundef-equiv old old-equiv) (equal (fundef-renamefun old new ren) (fundef-renamefun old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm fundef-renamefun-fundef-equiv-congruence-on-new (implies (fundef-equiv new new-equiv) (equal (fundef-renamefun old new ren) (fundef-renamefun old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm fundef-renamefun-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (fundef-renamefun old new ren) (fundef-renamefun old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm same-statement-kind-when-statement-renamefun (implies (not (reserrp (statement-renamefun old new ren))) (equal (statement-kind new) (statement-kind old))))