Generate the theorem equating the new function
to a combination of the old function with
(tailrec-gen-new-to-old-thm old$ nonrec updates combine q r variant$ domain$ new-name$ a new-to-old-name$ new-to-old-enable$ appcond-thm-names old-unnorm-name domain-of-old-name new-formals new-unnorm-name wrld) → (mv local-event exported-event)
The theorem's formula is
(implies (domain a) (equal (new x1 ... xn a) combine<a,(old x1 ... xn)>))
if the variant is
(equal (new x1 ... xn a) combine<a,(old x1 ... xn)>)
if the variant is
The hints follow the proofs in the design notes.
Note that
Function:
(defun tailrec-gen-new-to-old-thm (old$ nonrec updates combine q r variant$ domain$ new-name$ a new-to-old-name$ new-to-old-enable$ appcond-thm-names old-unnorm-name domain-of-old-name new-formals new-unnorm-name wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp nonrec) (pseudo-term-listp updates) (pseudo-termp combine) (symbolp q) (symbolp r) (tailrec-variantp variant$) (pseudo-termfnp domain$) (symbolp new-name$) (symbolp a) (symbolp new-to-old-name$) (booleanp new-to-old-enable$) (symbol-symbol-alistp appcond-thm-names) (symbolp old-unnorm-name) (symbolp domain-of-old-name) (symbol-listp new-formals) (symbolp new-unnorm-name) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-new-to-old-thm)) (declare (ignorable __function__)) (b* ((formula (cons 'equal (cons (apply-term new-name$ new-formals) (cons (apply-term* (tailrec-gen-combine-op combine q r) a (apply-term old$ (formals old$ wrld))) 'nil)))) (formula (if (eq variant$ :assoc-alt) formula (implicate (apply-term* domain$ a) formula))) (formula (untranslate formula t wrld)) (hints (case variant$ ((:monoid :assoc) (b* ((domain-of-nonrec-thm (cdr (assoc-eq :domain-of-nonrec appcond-thm-names))) (domain-of-combine-thm (cdr (assoc-eq :domain-of-combine appcond-thm-names))) (combine-associativity-thm (cdr (assoc-eq :combine-associativity appcond-thm-names))) (combine-right-identity-thm? (cdr (assoc-eq :combine-right-identity appcond-thm-names))) (domain-of-combine-instance (cons ':instance (cons domain-of-combine-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons a 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons nonrec 'nil)) 'nil)))))) (combine-associativity-instance (cons ':instance (cons combine-associativity-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons a 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons nonrec 'nil)) (cons (cons (tailrec-gen-var-w old$) (cons (apply-term old$ updates) 'nil)) 'nil))))))) (combine-right-identity-instance? (and combine-right-identity-thm? (cons ':instance (cons combine-right-identity-thm? (cons ':extra-bindings-ok (cons (cons (tailrec-gen-id-var-u old$ wrld) (cons a 'nil)) 'nil)))))) (domain-of-old-instance (cons ':instance (cons domain-of-old-name (cons ':extra-bindings-ok (alist-to-doublets (pairlis$ (formals old$ wrld) updates))))))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-unnorm-name (cons new-unnorm-name (cons (cons ':induction (cons new-name$ 'nil)) 'nil))) 'nil)) (cons ':induct (cons (cons new-name$ new-formals) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (append (and combine-right-identity-thm? (list combine-right-identity-instance?)) (cons domain-of-nonrec-thm (cons domain-of-combine-instance (cons domain-of-old-instance (cons combine-associativity-instance 'nil))))) 'nil)) 'nil)) 'nil)))) (:monoid-alt (b* ((domain-of-combine-uncond-thm (cdr (assoc-eq :domain-of-combine-uncond appcond-thm-names))) (combine-associativity-uncond-thm (cdr (assoc-eq :combine-associativity-uncond appcond-thm-names))) (combine-right-identity-thm (cdr (assoc-eq :combine-right-identity appcond-thm-names))) (domain-of-combine-uncond-instance (cons ':instance (cons domain-of-combine-uncond-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons a 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons nonrec 'nil)) 'nil)))))) (combine-associativity-uncond-instance (cons ':instance (cons combine-associativity-uncond-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons a 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons nonrec 'nil)) (cons (cons (tailrec-gen-var-w old$) (cons (apply-term old$ updates) 'nil)) 'nil))))))) (combine-right-identity-instance (cons ':instance (cons combine-right-identity-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-id-var-u old$ wrld) (cons a 'nil)) 'nil)))))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-unnorm-name (cons new-unnorm-name (cons (cons ':induction (cons new-name$ 'nil)) 'nil))) 'nil)) (cons ':induct (cons (cons new-name$ new-formals) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons combine-right-identity-instance (cons domain-of-combine-uncond-instance (cons combine-associativity-uncond-instance 'nil))) 'nil)) 'nil)) 'nil)))) (:assoc-alt (b* ((combine-associativity-uncond-thm (cdr (assoc-eq :combine-associativity-uncond appcond-thm-names))) (combine-associativity-uncond-instance (cons ':instance (cons combine-associativity-uncond-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons a 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons nonrec 'nil)) (cons (cons (tailrec-gen-var-w old$) (cons (apply-term old$ updates) 'nil)) 'nil)))))))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-unnorm-name (cons new-unnorm-name (cons (cons ':induction (cons new-name$ 'nil)) 'nil))) 'nil)) (cons ':induct (cons (cons new-name$ new-formals) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons combine-associativity-uncond-instance 'nil) 'nil)) 'nil)) 'nil)))) (t (impossible))))) (evmac-generate-defthm new-to-old-name$ :formula formula :hints hints :enable new-to-old-enable$))))