|
|
|---|
|
|
|
|---|
Generate the functions and theorems for a concatenation in the alternation that defines a rule name.
(deftreeops-gen-conc-events conc info i conc-equivs-thm
check-conc-fn nonleaf-thm alt-match-thm
alt-singletonp rulename prefix print)
→
(mv matching-thm-events
check-conc-fn-equiv-thm-events
get-tree-list-list-fn-events
rep-matching-thm-events
get-tree-list-fn-events
get-tree-fn-events event-alist)
Function:
(defun deftreeops-gen-conc-events (conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print) (declare (xargs :guard (and (concatenationp conc) (deftreeops-conc-infop info) (posp i) (common-lisp::symbolp conc-equivs-thm) (common-lisp::symbolp check-conc-fn) (common-lisp::symbolp nonleaf-thm) (common-lisp::symbolp alt-match-thm) (booleanp alt-singletonp) (rulenamep rulename) (common-lisp::symbolp prefix) (evmac-input-print-p print)))) (let ((__function__ 'deftreeops-gen-conc-events)) (declare (ignorable __function__)) (b* (((deftreeops-conc-info info) info) (matchp (deftreeops-match-pred prefix)) (alt-matchp (deftreeops-alt-match-pred prefix)) (conc-matchp (deftreeops-conc-match-pred prefix)) (rep-matchp (deftreeops-rep-match-pred prefix)) (rulename-string (rulename->get rulename)) (matching-thm-event? (and info.matching-thm (b* (((unless (consp conc)) (raise "Internal error: empty concatenation.")) (rep (car conc))) (cons (cons 'defruled (cons info.matching-thm (cons (cons 'implies (cons (cons conc-matchp (cons 'cstss (cons (pretty-print-concatenation conc) 'nil))) (cons (cons 'and (cons '(equal (len cstss) 1) (cons (cons rep-matchp (cons '(nth 0 cstss) (cons (pretty-print-repetition rep) 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons conc-matchp (cons rep-matchp '(tree-list-list-match-concatenation-p-when-atom-concatenation tree-list-list-match-concatenation-p-of-cons-concatenation tree-list-terminatedp-of-car-when-tree-list-list-terminatedp nth (:e zp) len))) 'nil)) 'nil))))) 'nil)))) (matching-thm-events (and matching-thm-event? (append matching-thm-event? (and (evmac-input-print->= print :result) (cons (cons 'cw-event (cons '"Theorem ~x0.~%" (cons (cons 'quote (cons info.matching-thm 'nil)) 'nil))) 'nil))))) (check-conc-fn-equiv-thm-event? (and info.check-conc-fn-equiv-thm (cons (cons 'defruled (cons info.check-conc-fn-equiv-thm (cons (cons 'implies (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) (cons (cons 'iff (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) (cons (cons conc-matchp (cons '(tree-nonleaf->branches cst) (cons (pretty-print-concatenation info.conc) 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons (packn-pos (list check-conc-fn '-tree-equiv-congruence-on-cst) check-conc-fn) (cons (packn-pos (list matchp '$-tree-equiv-congruence-on-tree) matchp) '(tree-nonleaf->branches$inline-tree-equiv-congruence-on-x return-type-of-tree-fix.new-x tree-fix-under-tree-equiv))) 'nil)) (cons ':use (cons '(:instance lemma (cst (tree-fix cst))) (cons ':prep-lemmas (cons (cons (cons 'defrule (cons 'lemma (cons (cons 'implies (cons (cons 'and (cons '(treep cst) (cons (cons matchp (cons 'cst (cons rulename-string 'nil))) 'nil))) (cons (cons 'iff (cons (cons 'equal (cons (cons check-conc-fn '(cst)) (cons i 'nil))) (cons (cons conc-matchp (cons '(tree-nonleaf->branches cst) (cons (pretty-print-concatenation info.conc) 'nil))) 'nil))) 'nil))) (cons ':in-theory (cons (cons 'quote (cons (cons check-conc-fn (cons conc-equivs-thm '((:e rulename)))) 'nil)) (cons ':use (cons (cons ':guard-theorem (cons check-conc-fn 'nil)) 'nil))))))) 'nil) 'nil))))))))) 'nil))) (check-conc-fn-equiv-thm-events (and check-conc-fn-equiv-thm-event? (append check-conc-fn-equiv-thm-event? (and (evmac-input-print->= print :result) (cons (cons 'cw-event (cons '"Theorem ~x0.~%" (cons (cons 'quote (cons info.check-conc-fn-equiv-thm 'nil)) 'nil))) 'nil))))) (get-tree-list-list-fn-match-thm (packn-pos (list info.get-tree-list-list-fn '-match) info.get-tree-list-list-fn)) (get-tree-list-list-fn-event? (and (or alt-singletonp check-conc-fn) (cons (cons 'define (cons info.get-tree-list-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 'cstss (cons 'tree-list-listp (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-list-fn '(tree-list-listp-of-tree-nonleaf->branches)) 'nil)) 'nil))) 'nil) 'nil)))) (cons '(tree-nonleaf->branches cst) (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 nonleaf-thm 'nil)) 'nil)) 'nil))) 'nil) (cons '/// (cons (cons 'more-returns (cons (cons 'cstss (cons (cons conc-matchp (cons 'cstss (cons (pretty-print-concatenation info.conc) '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-list-fn-match-thm (cons ':hints (cons (if check-conc-fn (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-list-fn (cons info.check-conc-fn-equiv-thm 'nil)) 'nil)) 'nil))) 'nil) (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-list-fn (cons alt-matchp (cons conc-matchp '(tree-list-list-match-alternation-p-when-atom-alternation tree-list-list-match-alternation-p-of-cons-alternation)))) 'nil)) (cons ':use (cons alt-match-thm 'nil))))) 'nil)) 'nil)))))))) 'nil)) (cons (cons 'fty::deffixequiv (cons info.get-tree-list-list-fn (cons ':hints (cons (cons (cons '"Goal" (cons ':in-theory (cons (cons 'quote (cons (cons info.get-tree-list-list-fn '(tree-nonleaf->branches$inline-tree-equiv-congruence-on-x tree-fix-under-tree-equiv)) 'nil)) 'nil))) 'nil) 'nil)))) 'nil))))))))))))))) 'nil))) (get-tree-list-list-fn-events (and get-tree-list-list-fn-event? (append get-tree-list-list-fn-event? (and (evmac-input-print->= print :result) (cons (cons 'cw-event (cons '"Function ~x0.~%" (cons (cons 'quote (cons info.get-tree-list-list-fn 'nil)) 'nil))) 'nil))))) (conc-singletonp (and (consp conc) (not (consp (cdr conc))))) ((unless (or (not conc-singletonp) (= (len info.rep-infos) (len conc)))) (raise "Internal error: length of ~x0 differs from length of ~x1." info.rep-infos conc) (mv nil nil nil nil nil nil nil)) ((mv rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events event-alist) (if conc-singletonp (deftreeops-gen-rep-list-events conc info.rep-infos i info.get-tree-list-list-fn get-tree-list-list-fn-match-thm info.matching-thm check-conc-fn rulename prefix print) (mv nil nil nil nil)))) (mv matching-thm-events check-conc-fn-equiv-thm-events get-tree-list-list-fn-events rep-matching-thm-events get-tree-list-fn-events get-tree-fn-events (append event-alist (and matching-thm-event? (list (cons info.matching-thm (car matching-thm-event?)))) (and check-conc-fn-equiv-thm-event? (list (cons info.check-conc-fn-equiv-thm (car check-conc-fn-equiv-thm-event?)))) (and get-tree-list-list-fn-event? (list (cons info.get-tree-list-list-fn (car get-tree-list-list-fn-event?)))))))))
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.matching-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.check-conc-fn-equiv-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp check-conc-fn-equiv-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.get-tree-list-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp get-tree-list-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.rep-matching-thm-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp rep-matching-thm-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.get-tree-list-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp get-tree-list-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm pseudo-event-form-listp-of-deftreeops-gen-conc-events.get-tree-fn-events (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (pseudo-event-form-listp get-tree-fn-events)) :rule-classes :rewrite)
Theorem:
(defthm symbol-pseudoeventform-alistp-of-deftreeops-gen-conc-events.event-alist (b* (((mv ?matching-thm-events ?check-conc-fn-equiv-thm-events ?get-tree-list-list-fn-events ?rep-matching-thm-events ?get-tree-list-fn-events ?get-tree-fn-events ?event-alist) (deftreeops-gen-conc-events conc info i conc-equivs-thm check-conc-fn nonleaf-thm alt-match-thm alt-singletonp rulename prefix print))) (symbol-pseudoeventform-alistp event-alist)) :rule-classes :rewrite)