Generate the theorem that relates
the old function to the new function
(
(tailrec-gen-old-to-new-thm old$ test base nonrec updates a variant$ new-name$ old-to-new-name$ old-to-new-enable$ appcond-thm-names domain-of-old-name domain-of-ground-base-name combine-left-identity-ground-name new-formals new-to-old-name$ wrld) → (mv local-event exported-event)
The theorem is
The hints follow the proof in the design notes,
for the case in which left identity holds
when the variant is
For the
Function:
(defun tailrec-gen-old-to-new-thm (old$ test base nonrec updates a variant$ new-name$ old-to-new-name$ old-to-new-enable$ appcond-thm-names domain-of-old-name domain-of-ground-base-name combine-left-identity-ground-name new-formals new-to-old-name$ wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp test) (pseudo-termp base) (pseudo-termp nonrec) (pseudo-term-listp updates) (symbolp a) (tailrec-variantp variant$) (symbolp new-name$) (symbolp old-to-new-name$) (booleanp old-to-new-enable$) (symbol-symbol-alistp appcond-thm-names) (symbolp domain-of-old-name) (symbolp domain-of-ground-base-name) (symbolp combine-left-identity-ground-name) (symbol-listp new-formals) (symbolp new-to-old-name$) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-old-to-new-thm)) (declare (ignorable __function__)) (b* ((formula (cons 'equal (cons (apply-term old$ (formals old$ wrld)) (cons (tailrec-gen-old-as-new-term old$ test base nonrec updates a variant$ new-name$ new-formals wrld) 'nil)))) (hints (case variant$ ((:monoid :monoid-alt) (b* ((combine-left-identity-ground-instance (cons ':instance (cons combine-left-identity-ground-name (cons ':extra-bindings-ok (cons (cons (tailrec-gen-id-var-u old$ wrld) (cons (apply-term old$ (formals old$ wrld)) 'nil)) 'nil))))) (new-to-old-instance (cons ':instance (cons new-to-old-name$ (cons ':extra-bindings-ok (cons (cons a (cons base 'nil)) 'nil)))))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons domain-of-ground-base-name (cons domain-of-old-name (cons new-to-old-instance (cons combine-left-identity-ground-instance 'nil)))) 'nil))))) 'nil))) (:assoc (b* ((formals (formals old$ wrld)) (domain-of-nonrec-thm (cdr (assoc-eq :domain-of-nonrec appcond-thm-names))) (new-to-old-instance (cons ':instance (cons new-to-old-name$ (cons ':extra-bindings-ok (cons (cons a (cons nonrec 'nil)) (alist-to-doublets (pairlis$ formals updates)))))))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':expand (cons (cons (cons old$ formals) 'nil) (cons ':use (cons (cons domain-of-nonrec-thm (cons new-to-old-instance 'nil)) 'nil))))))) 'nil))) (:assoc-alt (b* ((formals (formals old$ wrld)) (new-to-old-instance (cons ':instance (cons new-to-old-name$ (cons ':extra-bindings-ok (cons (cons a (cons nonrec 'nil)) (alist-to-doublets (pairlis$ formals updates)))))))) (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':expand (cons (cons (cons old$ formals) 'nil) (cons ':use (cons (cons new-to-old-instance 'nil) 'nil))))))) 'nil))) (t (impossible))))) (evmac-generate-defthm old-to-new-name$ :formula formula :hints hints :enable old-to-new-enable$))))