Generate the theorem asserting that
the guard of the old function is preserved by
(tailrec-gen-old-guard-of-alpha-thm old$ alpha-name names-to-avoid wrld) → (mv event name updated-names-to-avoid)
The theorem's formula is
The hints follow the proof in the design notes.
Since the theorem involves nth applied to cons,
we enable the built-in theorems
This theorem is local, because it is just a lemma used to prove other theorems.
Function:
(defun tailrec-gen-old-guard-of-alpha-thm (old$ alpha-name names-to-avoid wrld) (declare (xargs :guard (and (symbolp old$) (symbolp alpha-name) (symbol-listp names-to-avoid) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-old-guard-of-alpha-thm)) (declare (ignorable __function__)) (b* (((mv name names-to-avoid) (fresh-logical-name-with-$s-suffix 'old-guard-of-alpha nil names-to-avoid wrld)) (formals (formals old$ wrld)) (alpha-component-terms (tailrec-gen-alpha-component-terms alpha-name old$ wrld)) (old-guard (guard old$ nil wrld)) (formula (implicate old-guard (subcor-var formals alpha-component-terms old-guard))) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons alpha-name '(nth-0-cons nth-add1)) 'nil)) (cons ':induct (cons (cons alpha-name formals) 'nil))))) (cons (cons 'quote (cons (cons ':use (cons (cons ':guard-theorem (cons old$ 'nil)) '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))))