Generate the theorem asserting that
the old function always yields values in the domain
(
(tailrec-gen-domain-of-old-thm old$ test nonrec updates variant$ domain$ names-to-avoid appcond-thm-names old-unnorm-name wrld) → (mv event name updated-names-to-avoid)
This is generated only if the variant is
The theorem's formula is
The hints follow the proofs in the design notes.
This theorem event is local, because it is a lemma used to prove the exported main theorem.
Function:
(defun tailrec-gen-domain-of-old-thm (old$ test nonrec updates variant$ domain$ names-to-avoid appcond-thm-names old-unnorm-name wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp test) (pseudo-termp nonrec) (pseudo-term-listp updates) (tailrec-variantp variant$) (pseudo-termfnp domain$) (symbol-listp names-to-avoid) (symbol-symbol-alistp appcond-thm-names) (symbolp old-unnorm-name) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-domain-of-old-thm)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'domain-of-old nil names-to-avoid wrld)) (formula (untranslate (apply-term* domain$ (apply-term old$ (formals old$ wrld))) t wrld)) (hints (case variant$ ((:monoid :assoc) (b* ((domain-of-base-thm (cdr (assoc-eq :domain-of-base appcond-thm-names))) (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))) (domain-of-combine-instance (cons ':instance (cons domain-of-combine-thm (cons ':extra-bindings-ok (cons (cons (tailrec-gen-var-u old$) (cons nonrec 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons (cons old$ updates) 'nil)) 'nil))))))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-unnorm-name (cons (cons ':induction (cons old$ 'nil)) 'nil)) 'nil)) (cons ':induct (cons (cons old$ (formals old$ wrld)) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons domain-of-base-thm (cons domain-of-nonrec-thm (cons domain-of-combine-instance 'nil))) 'nil)) 'nil)) 'nil)))) (:monoid-alt (b* ((domain-of-base-thm (cdr (assoc-eq :domain-of-base appcond-thm-names))) (domain-of-combine-uncond-thm (cdr (assoc-eq :domain-of-combine-uncond 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 nonrec 'nil)) (cons (cons (tailrec-gen-var-v old$) (cons (cons old$ updates) 'nil)) 'nil))))))) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons old-unnorm-name 'nil) 'nil)) (cons ':cases (cons (cons test 'nil) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons domain-of-base-thm (cons domain-of-combine-uncond-instance 'nil)) 'nil)) 'nil)) 'nil)))) (:assoc-alt (raise "Internal error: called when variant is :ASSOC-ALT.")) (t (impossible)))) (event (cons 'local (cons (cons 'defthm (cons name (cons formula (cons ':rule-classes (cons 'nil (cons ':hints (cons hints 'nil))))))) 'nil)))) (mv event name names-to-avoid))))