Generate an instance of the
(parteval-gen-old-to-new-thm-instances rec-calls-with-tests old$ static$ thm-name$ wrld) → lemma-instances
This is used in the guard verification proof of
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
Function:
(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:
(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)