Generate the theorem
that relates the old function to the wrapper function
(
(tailrec-gen-old-to-wrapper-thm old$ wrapper-name$ old-to-wrapper-name$ old-to-wrapper-enable$ old-to-new-name$ wrapper-unnorm-name wrld) → (mv local-event exported-event)
The macro used to introduce the theorem is determined by whether the theorem must be enabled or not.
The theorem's formula
has the form
The theorem is proved by expanding the (non-normalized) definition of the wrapper function and using the theorem that relates the old function to the new function.
This function is called only if the
Function:
(defun tailrec-gen-old-to-wrapper-thm (old$ wrapper-name$ old-to-wrapper-name$ old-to-wrapper-enable$ old-to-new-name$ wrapper-unnorm-name wrld) (declare (xargs :guard (and (symbolp old$) (symbolp wrapper-name$) (symbolp old-to-wrapper-name$) (booleanp old-to-wrapper-enable$) (symbolp old-to-new-name$) (symbolp wrapper-unnorm-name) (plist-worldp wrld)))) (let ((__function__ 'tailrec-gen-old-to-wrapper-thm)) (declare (ignorable __function__)) (b* ((formals (formals old$ wrld)) (formula (untranslate (cons 'equal (cons (apply-term old$ formals) (cons (apply-term wrapper-name$ formals) 'nil))) t wrld)) (hints (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons wrapper-unnorm-name 'nil) 'nil)) (cons ':use (cons old-to-new-name$ 'nil))))) 'nil))) (evmac-generate-defthm old-to-wrapper-name$ :formula formula :hints hints :enable old-to-wrapper-enable$))))