Mutually recursive ACL2 functions to check if statements, blocks, cases, and function definitions are related by variable renaming.
Function:
(defun statement-renamevar (old new ren) (declare (xargs :guard (and (statementp old) (statementp new) (renamingp ren)))) (let ((__function__ 'statement-renamevar)) (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-renamevar old.get new.get ren))) (renaming-fix ren)) :variable-single (b* (((unless (statement-case new :variable-single)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-variable-single new) new) ((okf &) (expression-option-renamevar old.init new.init ren))) (add-var-to-var-renaming old.name new.name ren)) :variable-multi (b* (((unless (statement-case new :variable-multi)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-variable-multi new) new) ((okf &) (funcall-option-renamevar old.init new.init ren))) (add-vars-to-var-renaming old.names new.names ren)) :assign-single (b* (((unless (statement-case new :assign-single)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-assign-single new) new) ((okf &) (path-renamevar old.target new.target ren)) ((okf &) (expression-renamevar old.value new.value ren))) (renaming-fix ren)) :assign-multi (b* (((unless (statement-case new :assign-multi)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-assign-multi new) new) ((okf &) (path-list-renamevar old.targets new.targets ren)) ((okf &) (funcall-renamevar old.value new.value ren))) (renaming-fix ren)) :funcall (b* (((unless (statement-case new :funcall)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-funcall new) new) ((okf &) (funcall-renamevar old.get new.get ren))) (renaming-fix ren)) :if (b* (((unless (statement-case new :if)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-if new) new) ((okf &) (expression-renamevar old.test new.test ren)) ((okf &) (block-renamevar old.body new.body ren))) (renaming-fix ren)) :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)) ((okf ren1) (statement-list-renamevar old-stmts new-stmts ren)) ((okf &) (expression-renamevar old.test new.test ren1)) ((okf &) (block-renamevar old.update new.update ren1)) ((okf &) (block-renamevar old.body new.body ren1))) (renaming-fix ren)) :switch (b* (((unless (statement-case new :switch)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-switch new) new) ((okf &) (expression-renamevar old.target new.target ren)) ((okf &) (swcase-list-renamevar old.cases new.cases ren)) ((okf &) (block-option-renamevar old.default new.default ren))) (renaming-fix ren)) :leave (b* (((unless (statement-case new :leave)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) (renaming-fix ren)) :break (b* (((unless (statement-case new :break)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) (renaming-fix ren)) :continue (b* (((unless (statement-case new :continue)) (reserrf (list :mismatch (statement-fix old) (statement-fix new))))) (renaming-fix ren)) :fundef (b* (((unless (statement-case new :fundef)) (reserrf (list :mismatch (statement-fix old) (statement-fix new)))) ((statement-fundef new) new) ((okf &) (fundef-renamevar old.get new.get))) (renaming-fix ren)))))
Function:
(defun statement-list-renamevar (old new ren) (declare (xargs :guard (and (statement-listp old) (statement-listp new) (renamingp ren)))) (let ((__function__ 'statement-list-renamevar)) (declare (ignorable __function__)) (b* (((when (endp old)) (if (endp new) (renaming-fix ren) (reserrf (list :mismatch-extra-new (statement-list-fix new))))) ((when (endp new)) (reserrf (list :mismatch-extra-old (statement-list-fix old)))) ((okf ren) (statement-renamevar (car old) (car new) ren))) (statement-list-renamevar (cdr old) (cdr new) ren))))
Function:
(defun block-renamevar (old new ren) (declare (xargs :guard (and (blockp old) (blockp new) (renamingp ren)))) (let ((__function__ 'block-renamevar)) (declare (ignorable __function__)) (b* ((old-stmts (block->statements old)) (new-stmts (block->statements new)) ((okf &) (statement-list-renamevar old-stmts new-stmts ren))) nil)))
Function:
(defun block-option-renamevar (old new ren) (declare (xargs :guard (and (block-optionp old) (block-optionp new) (renamingp ren)))) (let ((__function__ 'block-option-renamevar)) (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-renamevar (block-option-some->val old) (block-option-some->val new) ren)))))
Function:
(defun swcase-renamevar (old new ren) (declare (xargs :guard (and (swcasep old) (swcasep new) (renamingp ren)))) (let ((__function__ 'swcase-renamevar)) (declare (ignorable __function__)) (b* (((unless (equal (swcase->value old) (swcase->value new))) (reserrf (list :mismatch-case-value (swcase->value old) (swcase->value new))))) (block-renamevar (swcase->body old) (swcase->body new) ren))))
Function:
(defun swcase-list-renamevar (old new ren) (declare (xargs :guard (and (swcase-listp old) (swcase-listp new) (renamingp ren)))) (let ((__function__ 'swcase-list-renamevar)) (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-renamevar (car old) (car new) ren))) (swcase-list-renamevar (cdr old) (cdr new) ren))))
Function:
(defun fundef-renamevar (old new) (declare (xargs :guard (and (fundefp old) (fundefp new)))) (let ((__function__ 'fundef-renamevar)) (declare (ignorable __function__)) (b* (((unless (equal (fundef->name old) (fundef->name new))) (reserrf (list :mismatch-function-name (fundef->name old) (fundef->name new)))) ((okf ren) (add-vars-to-var-renaming (fundef->inputs old) (fundef->inputs new) (renaming nil))) ((okf ren) (add-vars-to-var-renaming (fundef->outputs old) (fundef->outputs new) ren))) (block-renamevar (fundef->body old) (fundef->body new) ren))))
Theorem:
(defthm return-type-of-statement-renamevar.new-ren (b* ((?new-ren (statement-renamevar old new ren))) (renaming-resultp new-ren)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-statement-list-renamevar.new-ren (b* ((?new-ren (statement-list-renamevar old new ren))) (renaming-resultp new-ren)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-renamevar._ (b* ((?_ (block-renamevar old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-block-option-renamevar._ (b* ((?_ (block-option-renamevar old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-renamevar._ (b* ((?_ (swcase-renamevar old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-swcase-list-renamevar._ (b* ((?_ (swcase-list-renamevar old new ren))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm return-type-of-fundef-renamevar._ (b* ((?_ (fundef-renamevar old new))) (reserr-optionp _)) :rule-classes :rewrite)
Theorem:
(defthm statement-renamevar-of-statement-fix-old (equal (statement-renamevar (statement-fix old) new ren) (statement-renamevar old new ren)))
Theorem:
(defthm statement-renamevar-of-statement-fix-new (equal (statement-renamevar old (statement-fix new) ren) (statement-renamevar old new ren)))
Theorem:
(defthm statement-renamevar-of-renaming-fix-ren (equal (statement-renamevar old new (renaming-fix ren)) (statement-renamevar old new ren)))
Theorem:
(defthm statement-list-renamevar-of-statement-list-fix-old (equal (statement-list-renamevar (statement-list-fix old) new ren) (statement-list-renamevar old new ren)))
Theorem:
(defthm statement-list-renamevar-of-statement-list-fix-new (equal (statement-list-renamevar old (statement-list-fix new) ren) (statement-list-renamevar old new ren)))
Theorem:
(defthm statement-list-renamevar-of-renaming-fix-ren (equal (statement-list-renamevar old new (renaming-fix ren)) (statement-list-renamevar old new ren)))
Theorem:
(defthm block-renamevar-of-block-fix-old (equal (block-renamevar (block-fix old) new ren) (block-renamevar old new ren)))
Theorem:
(defthm block-renamevar-of-block-fix-new (equal (block-renamevar old (block-fix new) ren) (block-renamevar old new ren)))
Theorem:
(defthm block-renamevar-of-renaming-fix-ren (equal (block-renamevar old new (renaming-fix ren)) (block-renamevar old new ren)))
Theorem:
(defthm block-option-renamevar-of-block-option-fix-old (equal (block-option-renamevar (block-option-fix old) new ren) (block-option-renamevar old new ren)))
Theorem:
(defthm block-option-renamevar-of-block-option-fix-new (equal (block-option-renamevar old (block-option-fix new) ren) (block-option-renamevar old new ren)))
Theorem:
(defthm block-option-renamevar-of-renaming-fix-ren (equal (block-option-renamevar old new (renaming-fix ren)) (block-option-renamevar old new ren)))
Theorem:
(defthm swcase-renamevar-of-swcase-fix-old (equal (swcase-renamevar (swcase-fix old) new ren) (swcase-renamevar old new ren)))
Theorem:
(defthm swcase-renamevar-of-swcase-fix-new (equal (swcase-renamevar old (swcase-fix new) ren) (swcase-renamevar old new ren)))
Theorem:
(defthm swcase-renamevar-of-renaming-fix-ren (equal (swcase-renamevar old new (renaming-fix ren)) (swcase-renamevar old new ren)))
Theorem:
(defthm swcase-list-renamevar-of-swcase-list-fix-old (equal (swcase-list-renamevar (swcase-list-fix old) new ren) (swcase-list-renamevar old new ren)))
Theorem:
(defthm swcase-list-renamevar-of-swcase-list-fix-new (equal (swcase-list-renamevar old (swcase-list-fix new) ren) (swcase-list-renamevar old new ren)))
Theorem:
(defthm swcase-list-renamevar-of-renaming-fix-ren (equal (swcase-list-renamevar old new (renaming-fix ren)) (swcase-list-renamevar old new ren)))
Theorem:
(defthm fundef-renamevar-of-fundef-fix-old (equal (fundef-renamevar (fundef-fix old) new) (fundef-renamevar old new)))
Theorem:
(defthm fundef-renamevar-of-fundef-fix-new (equal (fundef-renamevar old (fundef-fix new)) (fundef-renamevar old new)))
Theorem:
(defthm statement-renamevar-statement-equiv-congruence-on-old (implies (statement-equiv old old-equiv) (equal (statement-renamevar old new ren) (statement-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm statement-renamevar-statement-equiv-congruence-on-new (implies (statement-equiv new new-equiv) (equal (statement-renamevar old new ren) (statement-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm statement-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (statement-renamevar old new ren) (statement-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamevar-statement-list-equiv-congruence-on-old (implies (statement-list-equiv old old-equiv) (equal (statement-list-renamevar old new ren) (statement-list-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamevar-statement-list-equiv-congruence-on-new (implies (statement-list-equiv new new-equiv) (equal (statement-list-renamevar old new ren) (statement-list-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm statement-list-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (statement-list-renamevar old new ren) (statement-list-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-renamevar-block-equiv-congruence-on-old (implies (block-equiv old old-equiv) (equal (block-renamevar old new ren) (block-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm block-renamevar-block-equiv-congruence-on-new (implies (block-equiv new new-equiv) (equal (block-renamevar old new ren) (block-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm block-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (block-renamevar old new ren) (block-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamevar-block-option-equiv-congruence-on-old (implies (block-option-equiv old old-equiv) (equal (block-option-renamevar old new ren) (block-option-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamevar-block-option-equiv-congruence-on-new (implies (block-option-equiv new new-equiv) (equal (block-option-renamevar old new ren) (block-option-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm block-option-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (block-option-renamevar old new ren) (block-option-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamevar-swcase-equiv-congruence-on-old (implies (swcase-equiv old old-equiv) (equal (swcase-renamevar old new ren) (swcase-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamevar-swcase-equiv-congruence-on-new (implies (swcase-equiv new new-equiv) (equal (swcase-renamevar old new ren) (swcase-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (swcase-renamevar old new ren) (swcase-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamevar-swcase-list-equiv-congruence-on-old (implies (swcase-list-equiv old old-equiv) (equal (swcase-list-renamevar old new ren) (swcase-list-renamevar old-equiv new ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamevar-swcase-list-equiv-congruence-on-new (implies (swcase-list-equiv new new-equiv) (equal (swcase-list-renamevar old new ren) (swcase-list-renamevar old new-equiv ren))) :rule-classes :congruence)
Theorem:
(defthm swcase-list-renamevar-renaming-equiv-congruence-on-ren (implies (renaming-equiv ren ren-equiv) (equal (swcase-list-renamevar old new ren) (swcase-list-renamevar old new ren-equiv))) :rule-classes :congruence)
Theorem:
(defthm fundef-renamevar-fundef-equiv-congruence-on-old (implies (fundef-equiv old old-equiv) (equal (fundef-renamevar old new) (fundef-renamevar old-equiv new))) :rule-classes :congruence)
Theorem:
(defthm fundef-renamevar-fundef-equiv-congruence-on-new (implies (fundef-equiv new new-equiv) (equal (fundef-renamevar old new) (fundef-renamevar old new-equiv))) :rule-classes :congruence)
Theorem:
(defthm same-len-when-expression-list-renamevar (implies (not (reserrp (expression-list-renamevar old new ren))) (equal (len old) (len new))))
Theorem:
(defthm expression-list-renamevar-of-append-error (implies (equal (len old) (len new)) (equal (reserrp (expression-list-renamevar (append old old1) (append new new1) ren)) (or (reserrp (expression-list-renamevar old new ren)) (reserrp (expression-list-renamevar old1 new1 ren))))))
Theorem:
(defthm expression-list-renamevar-of-rev-error (implies (equal (len old) (len new)) (equal (reserrp (expression-list-renamevar (rev old) (rev new) ren)) (reserrp (expression-list-renamevar old new ren)))))
Theorem:
(defthm expression-list-renamevar-of-rev-not-error (implies (not (reserrp (expression-list-renamevar old new ren))) (not (reserrp (expression-list-renamevar (rev old) (rev new) ren)))))
Theorem:
(defthm same-statement-kind-when-statement-renamevar (implies (not (reserrp (statement-renamevar old new ren))) (equal (statement-kind new) (statement-kind old))))
Theorem:
(defthm block-option-renamevar-of-nil-1-forward (implies (not (reserrp (block-option-renamevar nil block ren))) (equal block nil)) :rule-classes ((:forward-chaining :trigger-terms ((reserrp (block-option-renamevar nil block ren))))))
Theorem:
(defthm block-option-renamevar-of-nil-2-forward (implies (not (reserrp (block-option-renamevar block nil ren))) (equal block nil)) :rule-classes ((:forward-chaining :trigger-terms ((reserrp (block-option-renamevar block nil ren))))))
Theorem:
(defthm block-option-renamevar-when-nonnil (implies (and x y) (equal (block-option-renamevar x y ren) (block-renamevar x y ren))))
Theorem:
(defthm same-swcase->value-when-swcase-renamevar (implies (not (reserrp (swcase-renamevar old new ren))) (equal (swcase->value new) (swcase->value old))))
Theorem:
(defthm reserrp-of-swcase-renamevar (equal (reserrp (swcase-renamevar x y ren)) (or (not (equal (swcase->value x) (swcase->value y))) (reserrp (block-renamevar (swcase->body x) (swcase->body y) ren)))))
Theorem:
(defthm same-swcase-list->value-list-when-swcase-list-renamevar (implies (not (reserrp (swcase-list-renamevar old new ren))) (equal (swcase-list->value-list new) (swcase-list->value-list old))))
Theorem:
(defthm same-fundef->name-when-fundef-renamevar (implies (not (reserrp (fundef-renamevar old new))) (equal (fundef->name new) (fundef->name old))))
Theorem:
(defthm subsetp-equal-of-statement-renamevar (b* ((ren1 (statement-renamevar old new ren))) (implies (not (reserrp ren1)) (subsetp-equal (renaming->list ren) (renaming->list ren1)))))
Theorem:
(defthm subsetp-equal-of-statement-list-renamevar (b* ((ren1 (statement-list-renamevar old new ren))) (implies (not (reserrp ren1)) (subsetp-equal (renaming->list ren) (renaming->list ren1)))))
Theorem:
(defthm subsetp-equal-of-block-renamevar t :rule-classes nil)
Theorem:
(defthm subsetp-equal-of-block-option-renamevar t :rule-classes nil)
Theorem:
(defthm subsetp-equal-of-swcase-renamevar t :rule-classes nil)
Theorem:
(defthm subsetp-equal-of-swcase-list-renamevar t :rule-classes nil)
Theorem:
(defthm subsetp-equal-of-fundef-renamevar t :rule-classes nil)