Generate the functions and theorems for a repetition in a concatenation in the alternation that defines a rule name.
(deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix) → (mv matching-thm-event? get-tree-list-fn-event? get-tree-fn-event? event-alist)
Function:
(defun deftreeops-gen-rep-events (rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix) (declare (xargs :guard (and (repetitionp rep) (deftreeops-rep-infop info) (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)))) (let ((__function__ 'deftreeops-gen-rep-events)) (declare (ignorable __function__)) (b* (((deftreeops-rep-info info) info) (matchp (deftreeops-match-pred prefix)) (rep-matchp (deftreeops-rep-match-pred prefix)) (rulename-string (rulename->get rulename)) (elem (repetition->element rep)) (matching-thm-event? (and info.matching-thm (cons (cons 'defruled (cons info.matching-thm (cons (cons 'implies (cons (cons rep-matchp (cons 'csts (cons (pretty-print-repetition rep) 'nil))) (cons (cons 'and (cons '(equal (len csts) 1) (cons (cons matchp (cons '(nth 0 csts) (cons (pretty-print-element elem) 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons rep-matchp (cons matchp '(tree-list-match-repetition-p-of-1-repetition tree-terminatedp-of-car-when-tree-list-terminatedp (:e nati-finite) (:e repeat-range) (:e repetition->element) (:e repetition->range) nth (:e zp) len))) 'nil)) 'nil))))) 'nil))) (get-tree-list-fn-match-thm (packn-pos (list info.get-tree-list-fn '-match) info.get-tree-list-fn)) (get-tree-list-fn-event? (and info.get-tree-list-fn (cons (cons 'define (cons info.get-tree-list-fn (cons '((cst treep)) (cons ':guard (cons (if check-conc-fn (cons 'and (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) 'nil))) (cons matchp (cons 'cst (cons rulename-string 'nil)))) (cons ':returns (cons (cons 'csts (cons 'tree-listp (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-fn '(return-type-of-tree-list-fix.newx)) 'nil)) 'nil))) 'nil) 'nil)))) (cons (cons 'tree-list-fix (cons (cons 'nth (cons '0 (cons (cons get-tree-list-list-fn '(cst)) 'nil))) 'nil)) (cons ':prepwork (cons '((local (in-theory nil))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons '(:e elementp) (cons (cons ':t (cons get-tree-list-list-fn 'nil)) (cons 'tree-listp-of-nth-when-tree-list-listp (cons (packn-pos (list 'tree-list-listp-of- get-tree-list-list-fn) get-tree-list-list-fn) '((:e nfix)))))) 'nil)) (cons ':use (cons (cons get-tree-list-list-fn-match-thm (cons (cons ':instance (cons conc-matching-thm (cons (cons 'cstss (cons (cons get-tree-list-list-fn '(cst)) 'nil)) 'nil))) 'nil)) 'nil))))) 'nil) (cons '/// (cons (cons 'more-returns (cons (cons 'csts (cons (cons rep-matchp (cons 'csts (cons (pretty-print-repetition rep) 'nil))) (cons ':hyp (cons (if check-conc-fn (cons 'and (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) 'nil))) (cons matchp (cons 'cst (cons rulename-string 'nil)))) (cons ':name (cons get-tree-list-fn-match-thm (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-fn (cons 'tree-list-fix-when-tree-listp (cons 'tree-listp-of-nth-when-tree-list-listp (cons '(:e nfix) (cons (packn-pos (list 'tree-list-listp-of- get-tree-list-list-fn) get-tree-list-list-fn) 'nil))))) 'nil)) (cons ':use (cons (cons (cons ':instance (cons get-tree-list-list-fn-match-thm '((cst cst)))) (cons (cons ':instance (cons conc-matching-thm (cons (cons 'cstss (cons (cons get-tree-list-list-fn '(cst)) 'nil)) 'nil))) 'nil)) 'nil))))) 'nil) 'nil)))))))) 'nil)) (cons (cons 'fty::deffixequiv (cons info.get-tree-list-fn (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-fn (cons (packn-pos (list get-tree-list-list-fn '-of-tree-fix-cst) get-tree-list-list-fn) 'nil)) 'nil)) 'nil))) 'nil) 'nil)))) 'nil))))))))))))))) 'nil))) (get-tree-fn-event? (and info.get-tree-fn (cons (cons 'define (cons info.get-tree-fn (cons '((cst treep)) (cons ':guard (cons (if check-conc-fn (cons 'and (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) 'nil))) (cons matchp (cons 'cst (cons rulename-string 'nil)))) (cons ':returns (cons (cons 'cst1 (cons 'treep (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-fn '(return-type-of-tree-fix.new-x)) 'nil)) 'nil))) 'nil) 'nil)))) (cons (cons 'tree-fix (cons (cons 'nth (cons '0 (cons (cons info.get-tree-list-fn '(cst)) 'nil))) 'nil)) (cons ':prepwork (cons '((local (in-theory nil))) (cons ':guard-hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons '(:e elementp) (cons (cons ':t (cons info.get-tree-list-fn 'nil)) (cons 'treep-of-nth-when-tree-listp (cons (packn-pos (list 'tree-listp-of- info.get-tree-list-fn) info.get-tree-list-fn) '((:e nfix)))))) 'nil)) (cons ':use (cons (cons get-tree-list-fn-match-thm (cons (cons ':instance (cons info.matching-thm (cons (cons 'csts (cons (cons info.get-tree-list-fn '(cst)) 'nil)) 'nil))) 'nil)) 'nil))))) 'nil) (cons '/// (cons (cons 'more-returns (cons (cons 'cst1 (cons (cons matchp (cons 'cst1 (cons (pretty-print-element elem) 'nil))) (cons ':hyp (cons (if check-conc-fn (cons 'and (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) 'nil))) (cons matchp (cons 'cst (cons rulename-string 'nil)))) (cons ':name (cons (packn-pos (list info.get-tree-fn '-match) info.get-tree-fn) (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-fn (cons 'tree-fix-when-treep (cons 'treep-of-nth-when-tree-listp (cons '(:e nfix) (cons (packn-pos (list 'tree-listp-of- info.get-tree-list-fn) info.get-tree-list-fn) 'nil))))) 'nil)) (cons ':use (cons (cons get-tree-list-fn-match-thm (cons (cons ':instance (cons info.matching-thm (cons (cons 'csts (cons (cons info.get-tree-list-fn '(cst)) 'nil)) 'nil))) 'nil)) 'nil))))) 'nil) 'nil)))))))) 'nil)) (cons (cons 'fty::deffixequiv (cons info.get-tree-fn (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-fn (cons (packn-pos (list info.get-tree-list-fn '-of-tree-fix-cst) info.get-tree-list-fn) 'nil)) 'nil)) 'nil))) 'nil) 'nil)))) 'nil))))))))))))))) 'nil)))) (mv matching-thm-event? get-tree-list-fn-event? get-tree-fn-event? (append (and matching-thm-event? (list (cons info.matching-thm (car matching-thm-event?)))) (and get-tree-list-fn-event? (list (cons info.get-tree-list-fn (car get-tree-list-fn-event?)))) (and get-tree-fn-event? (list (cons info.get-tree-fn (car get-tree-fn-event?)))))))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-events.matching-thm-event? (b* (((mv ?matching-thm-event? ?get-tree-list-fn-event? ?get-tree-fn-event? ?event-alist) (deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp matching-thm-event?)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-list-fn-event? (b* (((mv ?matching-thm-event? ?get-tree-list-fn-event? ?get-tree-fn-event? ?event-alist) (deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp get-tree-list-fn-event?)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-rep-events.get-tree-fn-event? (b* (((mv ?matching-thm-event? ?get-tree-list-fn-event? ?get-tree-fn-event? ?event-alist) (deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (pseudo-event-form-listp get-tree-fn-event?)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-rep-events.event-alist (b* (((mv ?matching-thm-event? ?get-tree-list-fn-event? ?get-tree-fn-event? ?event-alist) (deftreeops-gen-rep-events rep info i get-tree-list-list-fn get-tree-list-list-fn-match-thm conc-matching-thm check-conc-fn rulename prefix))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)