Generate the theorem asserting that
the base value of the recursion
is left identity of the combination operator
(
(tailrec-gen-combine-left-identity-ground-thm old$ base combine q r 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 is local, because it is just a lemma used to prove other theorems.
Function:
(defun tailrec-gen-combine-left-identity-ground-thm (old$ base combine q r domain$ appcond-thm-names alpha-name test-of-alpha-name names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (pseudo-termp base) (pseudo-termp combine) (symbolp q) (symbolp r) (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-combine-left-identity-ground-thm)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'combine-left-identity-ground nil names-to-avoid wrld)) (u (tailrec-gen-var-u old$)) (combine-op (tailrec-gen-combine-op combine q r)) (formula (implicate (apply-term* domain$ u) (cons 'equal (cons (apply-term* combine-op base u) (cons u 'nil))))) (combine-left-identity-thm (cdr (assoc-eq :combine-left-identity 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 combine-left-identity-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))))