		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-new-fn-verify-guards

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

Signature
(parteval-gen-new-fn-verify-guards old$ static$ new-name$ thm-name$ case wrld) → local-event
Arguments: old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; new-name$ — Guard (symbolp new-name$).; thm-name$ — Guard (symbolp thm-name$).; case — Guard (member case '(1 2 3)).; wrld — Guard (plist-worldp wrld).
Returns: local-event — A pseudo-event-formp.

We instruct ACL2 not to simplify the guard conjecture, and accordingly to use the unsimplified guard theorem of old. This increases the robustness of the generated proof.

Definitions and Theorems

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

(defun parteval-gen-new-fn-verify-guards
       (old$ static$ new-name$ thm-name$ case wrld)
 (declare (xargs :guard (and (symbolp old$)
                             (symbol-alistp static$)
                             (symbolp new-name$)
                             (symbolp thm-name$)
                             (member case '(1 2 3))
                             (plist-worldp wrld))))
 (let ((__function__ 'parteval-gen-new-fn-verify-guards))
  (declare (ignorable __function__))
  (b*
   ((guard-thm-instance
         (cons ':instance
               (cons (cons ':guard-theorem
                           (cons old$ '(nil)))
                     (cons ':extra-bindings-ok
                           (alist-to-doublets static$)))))
    (old-to-new-instances? (and (= case 2)
                                (parteval-gen-old-to-new-thm-instances
                                     (recursive-calls old$ wrld)
                                     old$ static$ thm-name$ wrld)))
    (hints
     (cons
          (cons '"Goal"
                (cons ':in-theory
                      (cons 'nil
                            (cons ':use
                                  (cons (cons guard-thm-instance
                                              old-to-new-instances?)
                                        'nil)))))
          'nil)))
   (cons
    'local
    (cons
       (cons 'verify-guards
             (cons new-name$
                   (cons ':hints
                         (cons hints '(:guard-simplify :limited)))))
       'nil)))))