		Search-engine friendly clone of the ACL2 documentation.

Parteval-event-generation

Parteval-gen-old-to-new-thm-instances

Generate an instance of the old-to-new theorem for each recursive call of old.

Signature
(parteval-gen-old-to-new-thm-instances rec-calls-with-tests old$ static$ thm-name$ wrld) → lemma-instances
Arguments: rec-calls-with-tests — Recursive calls of old.
Guard (pseudo-tests-and-call-listp rec-calls-with-tests).; old$ — Guard (symbolp old$).; static$ — Guard (symbol-alistp static$).; thm-name$ — Guard (symbolp thm-name$).; wrld — Guard (plist-worldp wrld).
Returns: lemma-instances — Type (pseudo-event-form-listp lemma-instances).

This is used in the guard verification proof of new in case 2. The design notes and parteval-template.lisp show that, in case 2, the old-to-new theorem must be instantiated by replacing the dynamic formal arguments with the corresponding actual arguments in the recursive call. This must be done for all recursive calls. In addition, the static parameters yj, which in case 2 are unchanged in all the recursive calls, must be replaced with the constant terms cj.

This code goes through the recursive calls of old and generates the lemma instances as just described. For each such call, first we create an alist from all the formal parameters of old to the arguments in the recursive calls with each yj replaced with cj; then we remove the static parameters from that alist (which that alist maps all to themselves), and we join the result with static$, obtaining the whole instantiation, in alist form.

Definitions and Theorems

Function: parteval-gen-old-to-new-thm-instances

(defun parteval-gen-old-to-new-thm-instances
       (rec-calls-with-tests old$ static$ thm-name$ wrld)
 (declare
  (xargs
      :guard (and (pseudo-tests-and-call-listp rec-calls-with-tests)
                  (symbolp old$)
                  (symbol-alistp static$)
                  (symbolp thm-name$)
                  (plist-worldp wrld))))
 (let ((__function__ 'parteval-gen-old-to-new-thm-instances))
   (declare (ignorable __function__))
   (b* (((when (endp rec-calls-with-tests)) nil)
        (rec-call-with-tests (car rec-calls-with-tests))
        (rec-call (access tests-and-call
                          rec-call-with-tests :call))
        (rec-args (fargs rec-call))
        (rec-args (fsublis-var static$ rec-args))
        (all-alist (pairlis$ (formals old$ wrld) rec-args))
        (dynamic-alist (remove-assocs-eq (strip-cars static$)
                                         all-alist))
        (final-alist (append dynamic-alist static$))
        (lemma-instance
             (cons ':instance
                   (cons thm-name$
                         (cons ':extra-bindings-ok
                               (alist-to-doublets final-alist)))))
        (lemma-instances (parteval-gen-old-to-new-thm-instances
                              (cdr rec-calls-with-tests)
                              old$ static$ thm-name$ wrld)))
     (cons lemma-instance lemma-instances))))

Theorem: pseudo-event-form-listp-of-parteval-gen-old-to-new-thm-instances

(defthm
   pseudo-event-form-listp-of-parteval-gen-old-to-new-thm-instances
  (b* ((lemma-instances (parteval-gen-old-to-new-thm-instances
                             rec-calls-with-tests
                             old$ static$ thm-name$ wrld)))
    (pseudo-event-form-listp lemma-instances))
  :rule-classes :rewrite)