		Search-engine friendly clone of the ACL2 documentation.

Atc-function-tables

Atc-symbol-fninfo-alist-to-result-thms

Project the result theorems out of a function information alist, for the functions among a given list.

Signature
(atc-symbol-fninfo-alist-to-result-thms prec-fns among) → thms
Arguments: prec-fns — Guard (atc-symbol-fninfo-alistp prec-fns).; among — Guard (symbol-listp among).
Returns: thms — Type (symbol-listp thms).

The proof of each of these theorems for a function fn makes use of the same theorems for some of the preceding functions in prec-fns, more precisely the ones called in the body of fn. This function serves to collect those theorem names from the alist. The list of symbols given as input consists of the functions called by fn: it is fine if the list contains functions that are not keys of the alist, as it is merely used to filter.

The alist has no duplicate keys. So this function is correct.

Definitions and Theorems

Function: atc-symbol-fninfo-alist-to-result-thms

(defun atc-symbol-fninfo-alist-to-result-thms (prec-fns among)
 (declare (xargs :guard (and (atc-symbol-fninfo-alistp prec-fns)
                             (symbol-listp among))))
 (let ((__function__ 'atc-symbol-fninfo-alist-to-result-thms))
  (declare (ignorable __function__))
  (cond
       ((endp prec-fns) nil)
       ((member-eq (caar prec-fns) among)
        (cons (atc-fn-info->result-thm (cdr (car prec-fns)))
              (atc-symbol-fninfo-alist-to-result-thms (cdr prec-fns)
                                                      among)))
       (t (atc-symbol-fninfo-alist-to-result-thms (cdr prec-fns)
                                                  among)))))

Theorem: symbol-listp-of-atc-symbol-fninfo-alist-to-result-thms

(defthm symbol-listp-of-atc-symbol-fninfo-alist-to-result-thms
  (b*
    ((thms (atc-symbol-fninfo-alist-to-result-thms prec-fns among)))
    (symbol-listp thms))
  :rule-classes :rewrite)