		Search-engine friendly clone of the ACL2 documentation.

Restrict-event-generation

Restrict-gen-verify-guards

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

Signature
(restrict-gen-verify-guards old new old-to-new appcond-thm-names stub? wrld) → local-event
Arguments: old — Guard (symbolp old).; new — Guard (symbolp new).; old-to-new — Guard (symbolp old-to-new).; appcond-thm-names — Guard (symbol-symbol-alistp appcond-thm-names).; stub? — Guard (symbolp stub?).; wrld — Guard (plist-worldp wrld).
Returns: local-event — Type (pseudo-event-formp local-event).

As mentioned in restrict-gen-new, 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.

Following the design notes, the guards are verified using the guard theorem of the old function and the :restriction-guard applicability condition. This suffices for the non-recursive case (in the empty theory). For the recursive case, we also use the :restriction-of-rec-calls applicability condition, and we carry out the proof in the theory consisting of the theorem that relates the old and new functions: this theorem rewrites all the recursive calls of the old function, in the old function's guard theorem, to corresponding recursive calls of the new function (the design notes cover the representative case of a single recursive call, but the transformation covers functions with multiple recursive calls). If the old and new functions are reflexive, we functionally instantiate the stub in the :restriction-of-rec-calls applicability condition.

The guard verification event is local; the exported function definition has :verify-guards set to t (when it must be guard-verified).

We use the limited simplification option to prevent the dropping of guard hypotheses, which we have otherwise observed in at least one case. As this may involve additional obligations, we make sure to use the guard theorem with limited simplification (which is actually the default, but we make it explicit for clarity), and, in restrict-gen-appconds, as discussed there, we retrieve the guard obligations of the restricting predicate with limited simplification as well, so that we have a possibly stronger theorem as that applicability condition.

We also enable not in the quoted theory. We have seen at least one example fail without this, due to some special treatment by ACL2 in clausification. It is not clear whether enabling not may cause problems elsewhere: the proofs in the design notes, upon which the generated ACL2 proofs are based, assume that certain parts of the terms are ``atomic''; those parts might start with not, in which case enabling not may disrupt the proofs. As we have not yet observed such cases though, for now we add not to the theory, but with the caveat that we may need something more general and robust at some point in the future.

Definitions and Theorems

Function: restrict-gen-verify-guards

(defun restrict-gen-verify-guards
       (old new
            old-to-new appcond-thm-names stub? wrld)
 (declare
      (xargs :guard (and (symbolp old)
                         (symbolp new)
                         (symbolp old-to-new)
                         (symbol-symbol-alistp appcond-thm-names)
                         (symbolp stub?)
                         (plist-worldp wrld))))
 (let ((__function__ 'restrict-gen-verify-guards))
  (declare (ignorable __function__))
  (b*
   ((recursive (recursivep old nil wrld))
    (hints
     (if recursive
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          (cons 'quote
                (cons (cons old-to-new '(not)) 'nil))
          (cons
           ':use
           (cons
            (cons
             (cons ':guard-theorem (cons old 'nil))
             (cons
              (cdr (assoc-eq :restriction-guard appcond-thm-names))
              (cons
               (if stub?
                (cons
                 ':functional-instance
                 (cons
                  (cdr
                   (assoc-eq
                       :restriction-of-rec-calls appcond-thm-names))
                  (cons (cons stub? (cons new 'nil))
                        'nil)))
                (cdr
                 (assoc-eq
                      :restriction-of-rec-calls appcond-thm-names)))
               'nil)))
            'nil)))))
       'nil)
      (cons
       (cons
        '"Goal"
        (cons
         ':in-theory
         (cons
          ''(not)
          (cons
           ':use
           (cons
            (cons
             (cons ':guard-theorem (cons old 'nil))
             (cons
               (cdr (assoc-eq :restriction-guard appcond-thm-names))
               'nil))
            'nil)))))
       'nil)))
    (event
     (cons
      'local
      (cons
        (cons 'verify-guards
              (cons new
                    (cons ':guard-simplify
                          (cons ':limited
                                (cons ':hints (cons hints 'nil))))))
        'nil))))
   event)))

Theorem: pseudo-event-formp-of-restrict-gen-verify-guards

(defthm pseudo-event-formp-of-restrict-gen-verify-guards
  (b*
   ((local-event
         (restrict-gen-verify-guards old new old-to-new
                                     appcond-thm-names stub? wrld)))
   (pseudo-event-formp local-event))
  :rule-classes :rewrite)