Generate the event to verify the guards of the new function.
(expdata-gen-new-fn-verify-guards appcond-thm-names old$ arg-surjmaps res-surjmaps predicate$ new$ new-to-old$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) → new-fn-verify-guards-event
As mentioned elsewhere, the verification of the guards of the new function, when it has to take place, is deferred when the function is introduced. The reason is that, as shown in the design notes, the guard verification proof for the recursive case uses the theorem that relates the old and new functions: thus, the theorem must be proved before guard verification, and the new function must be introduced before proving the theorem. In the non-recursive case, we could avoid deferring guard verification, but we defer it anyhow for uniformity.
The guard verification event is local to the encapsulate generated by the transformation. This keeps the event history after the transformation ``clean'', without implementation-specific proof hints that may refer to local events of the encapsulate that do not exist in the history after the transformation.
Function:
(defun expdata-gen-new-fn-verify-guards (appcond-thm-names old$ arg-surjmaps res-surjmaps predicate$ new$ new-to-old$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) (declare (xargs :guard (and (symbol-symbol-alistp appcond-thm-names) (symbolp old$) (expdata-symbol-surjmap-alistp arg-surjmaps) (expdata-pos-surjmap-alistp res-surjmaps) (booleanp predicate$) (symbolp new$) (symbolp new-to-old$) (symbolp old-to-new$) (symbolp old-fn-unnorm-name) (symbolp newp-of-new$) (plist-worldp wrld)))) (let ((__function__ 'expdata-gen-new-fn-verify-guards)) (declare (ignorable __function__)) (b* ((hints (expdata-gen-new-fn-verify-guards-hints appcond-thm-names old$ arg-surjmaps res-surjmaps predicate$ new-to-old$ new$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld)) (event (cons 'local (cons (cons 'verify-guards (cons new$ (cons ':hints (cons hints '(:guard-simplify :limited))))) 'nil)))) event)))