		Search-engine friendly clone of the ACL2 documentation.

Deftreeops-event-generation

Deftreeops-gen-rep-list-events

Lift deftreeops-gen-rep-events to lists.

Signature
(deftreeops-gen-rep-list-events conc infos i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix print) → (mv matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist)
Arguments: conc — Guard (concatenationp conc).; infos — Guard (deftreeops-rep-info-listp infos).; i — Index of the concatenation that this repetition is part of.
Guard (posp i).; get-tree-list-list-fn — The function <prefix>-<rulename>-conc or <prefix>-<rulename>-conc<i> described in deftreeops.
Guard (common-lisp::symbolp get-tree-list-list-fn).; get-tree-list-list-fn-match-thm — The theorem saying that get-tree-list-list-fn) matches the concatenation.
Guard (common-lisp::symbolp get-tree-list-list-fn-match-thm).; conc-matching-thm — Guard (common-lisp::symbolp conc-matching-thm).; check-conc-fn — Guard (common-lisp::symbolp check-conc-fn).; rulename — Guard (rulenamep rulename).; prefix — Guard (common-lisp::symbolp prefix).; print — Guard (evmac-input-print-p print).
Returns: matching-thm-events — Type (pseudo-event-form-listp matching-thm-events).; get-tree-list-fn-events — Type (pseudo-event-form-listp get-tree-list-fn-events).; get-tree-fn-events — Type (pseudo-event-form-listp get-tree-fn-events).; event-alist — Type (symbol-pseudoeventform-alistp event-alist).

Definitions and Theorems

Function: deftreeops-gen-rep-list-events

(defun deftreeops-gen-rep-list-events
       (conc infos i get-tree-list-list-fn
             get-tree-list-list-fn-match-thm
             conc-matching-thm
             check-conc-fn rulename prefix print)
 (declare
  (xargs :guard
         (and (concatenationp conc)
              (deftreeops-rep-info-listp infos)
              (posp i)
              (common-lisp::symbolp get-tree-list-list-fn)
              (common-lisp::symbolp get-tree-list-list-fn-match-thm)
              (common-lisp::symbolp conc-matching-thm)
              (common-lisp::symbolp check-conc-fn)
              (rulenamep rulename)
              (common-lisp::symbolp prefix)
              (evmac-input-print-p print))))
 (declare (xargs :guard (equal (len infos) (len conc))))
 (let ((__function__ 'deftreeops-gen-rep-list-events))
   (declare (ignorable __function__))
   (b* (((when (endp conc))
         (mv nil nil nil nil))
        ((mv matching-thm-events
             get-tree-list-fn-events
             get-tree-fn-events event-alist)
         (deftreeops-gen-rep-events
              (car conc)
              (car infos)
              i get-tree-list-list-fn
              get-tree-list-list-fn-match-thm
              conc-matching-thm
              check-conc-fn rulename prefix print))
        ((mv more-matching-thm-events
             more-get-tree-list-fn-events
             more-get-tree-fn-events
             more-event-alist)
         (deftreeops-gen-rep-list-events
              (cdr conc)
              (cdr infos)
              i get-tree-list-list-fn
              get-tree-list-list-fn-match-thm
              conc-matching-thm
              check-conc-fn rulename prefix print)))
     (mv (append matching-thm-events
                 more-matching-thm-events)
         (append get-tree-list-fn-events
                 more-get-tree-list-fn-events)
         (append get-tree-fn-events
                 more-get-tree-fn-events)
         (append event-alist more-event-alist)))))

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.matching-thm-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.matching-thm-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-list-events
            conc infos i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp matching-thm-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-list-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-list-fn-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-list-events
            conc infos i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp get-tree-list-fn-events))
 :rule-classes :rewrite)

Theorem: pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-fn-events

(defthm
 pseudo-event-form-listp-of-deftreeops-gen-rep-list-events.get-tree-fn-events
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-list-events
            conc infos i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (pseudo-event-form-listp get-tree-fn-events))
 :rule-classes :rewrite)

Theorem: symbol-pseudoeventform-alistp-of-deftreeops-gen-rep-list-events.event-alist

(defthm
 symbol-pseudoeventform-alistp-of-deftreeops-gen-rep-list-events.event-alist
 (b* (((mv ?matching-thm-events
           ?get-tree-list-fn-events
           ?get-tree-fn-events ?event-alist)
       (deftreeops-gen-rep-list-events
            conc infos i get-tree-list-list-fn
            get-tree-list-list-fn-match-thm
            conc-matching-thm
            check-conc-fn rulename prefix print)))
   (symbol-pseudoeventform-alistp event-alist))
 :rule-classes :rewrite)