		Search-engine friendly clone of the ACL2 documentation.

Isodata-event-generation

Isodata-gen-new-fn-verify-guards

Generate the event to verify the guards of the new function.

Signature
(isodata-gen-new-fn-verify-guards appcond-thm-names old$ arg-isomaps res-isomaps predicate$ new$ new-to-old$ old-to-new$ old-fn-unnorm-name newp-of-new$ wrld) → new-fn-verify-guards-event
Arguments: appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; old$ — Guard (symbolp old$).; arg-isomaps — Guard (isodata-symbol-isomap-alistp arg-isomaps).; res-isomaps — Guard (isodata-pos-isomap-alistp res-isomaps).; predicate$ — Guard (booleanp predicate$).; new$ — Guard (symbolp new$).; new-to-old$ — Guard (symbolp new-to-old$).; old-to-new$ — Guard (symbolp old-to-new$).; old-fn-unnorm-name — Guard (symbolp old-fn-unnorm-name).; newp-of-new$ — Guard (symbolp newp-of-new$).; wrld — Guard (plist-worldp wrld).
Returns: new-fn-verify-guards-event — A pseudo-event-formp.

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.

Definitions and Theorems

Function: isodata-gen-new-fn-verify-guards

(defun isodata-gen-new-fn-verify-guards
       (appcond-thm-names old$ arg-isomaps res-isomaps
                          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$)
                         (isodata-symbol-isomap-alistp arg-isomaps)
                         (isodata-pos-isomap-alistp res-isomaps)
                         (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__ 'isodata-gen-new-fn-verify-guards))
  (declare (ignorable __function__))
  (b*
   ((hints (isodata-gen-new-fn-verify-guards-hints
                appcond-thm-names
                old$ arg-isomaps res-isomaps
                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)))