Generate the theorem asserting that
the base value of the recursion is in the domain
(
(tailrec-gen-domain-of-ground-base-thm old$ base domain$ appcond-thm-names alpha-name test-of-alpha-name names-to-avoid wrld) → (mv event name updated-names-to-avoid)
The hints follow the proof in the design notes.
This theorem event is local, because it is just a lemma used to prove other theorems.
Function:
(defun tailrec-gen-domain-of-ground-base-thm (old$ base domain$ appcond-thm-names alpha-name test-of-alpha-name names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp base) (pseudo-termfnp domain$) (symbol-symbol-alistp appcond-thm-names) (symbolp alpha-name) (symbolp test-of-alpha-name) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-domain-of-ground-base-thm)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'domain-of-ground-base nil names-to-avoid wrld)) (formula (apply-term* domain$ base)) (domain-of-base-thm (cdr (assoc-eq :domain-of-base appcond-thm-names))) (formals (formals old$ wrld)) (alpha-comps (tailrec-gen-alpha-component-terms alpha-name old$ wrld)) (hints (cons (cons '"Goal" (cons ':in-theory (cons 'nil (cons ':use (cons (cons test-of-alpha-name (cons (cons ':instance (cons domain-of-base-thm (cons ':extra-bindings-ok (alist-to-doublets (pairlis$ formals alpha-comps))))) 'nil)) 'nil))))) 'nil)) (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))))