Tree matching theorems for parse-alternation, parse-concatenation, parse-repetition, parse-element, parse-group, parse-option, parse-alt-rest, parse-alt-rest-comp, parse-conc-rest, and parse-conc-rest-comp.
Theorem:
(defthm tree-match-of-parse-alternation-lemma (b* (((mv error? tree? &) (parse-alternation input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *alternation*) *grammar*))))
Theorem:
(defthm tree-match-of-parse-concatenation-lemma (b* (((mv error? tree? &) (parse-concatenation input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *concatenation*) *grammar*))))
Theorem:
(defthm tree-match-of-parse-repetition-lemma (b* (((mv error? tree? &) (parse-repetition input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *repetition*) *grammar*))))
Theorem:
(defthm tree-match-of-parse-element-lemma (b* (((mv error? tree? &) (parse-element input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *element*) *grammar*))))
Theorem:
(defthm tree-match-of-parse-group-lemma (b* (((mv error? tree? &) (parse-group input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *group*) *grammar*))))
Theorem:
(defthm tree-match-of-parse-option-lemma (b* (((mv error? tree? &) (parse-option input))) (implies (not error?) (tree-match-element-p tree? (element-rulename *option*) *grammar*))))
Theorem:
(defthm tree-list-match-of-parse-alt-rest-lemma (b* (((mv & trees &) (parse-alt-rest input))) (tree-list-match-repetition-p trees (*_ (!_ (/_ (*_ *c-wsp*) "/" (*_ *c-wsp*) *concatenation*))) *grammar*)))
Theorem:
(defthm tree-match-of-parse-alt-rest-comp-lemma (b* (((mv error? tree? &) (parse-alt-rest-comp input))) (implies (not error?) (tree-match-element-p tree? (!_ (/_ (*_ *c-wsp*) "/" (*_ *c-wsp*) *concatenation*)) *grammar*))))
Theorem:
(defthm tree-list-match-of-parse-conc-rest-lemma (b* (((mv & trees &) (parse-conc-rest input))) (tree-list-match-repetition-p trees (*_ (!_ (/_ (1*_ *c-wsp*) *repetition*))) *grammar*)))
Theorem:
(defthm tree-match-of-parse-conc-rest-comp-lemma (b* (((mv error? tree? &) (parse-conc-rest-comp input))) (implies (not error?) (tree-match-element-p tree? (!_ (/_ (1*_ *c-wsp*) *repetition*)) *grammar*))))
Theorem:
(defthm tree-match-of-parse-alternation (b* (((mv error? tree? &) (parse-alternation input))) (implies (and (not error?) (equal element (element-rulename *alternation*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-match-of-parse-concatenation (b* (((mv error? tree? &) (parse-concatenation input))) (implies (and (not error?) (equal element (element-rulename *concatenation*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-match-of-parse-repetition (b* (((mv error? tree? &) (parse-repetition input))) (implies (and (not error?) (equal element (element-rulename *repetition*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-match-of-parse-element (b* (((mv error? tree? &) (parse-element input))) (implies (and (not error?) (equal element (element-rulename *element*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-match-of-parse-group (b* (((mv error? tree? &) (parse-group input))) (implies (and (not error?) (equal element (element-rulename *group*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-match-of-parse-option (b* (((mv error? tree? &) (parse-option input))) (implies (and (not error?) (equal element (element-rulename *option*))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-list-match-of-parse-alt-rest (b* (((mv & trees &) (parse-alt-rest input))) (implies (equal repetition (*_ (!_ (/_ (*_ *c-wsp*) "/" (*_ *c-wsp*) *concatenation*)))) (tree-list-match-repetition-p trees repetition *grammar*))))
Theorem:
(defthm tree-match-of-parse-alt-rest-comp (b* (((mv error? tree? &) (parse-alt-rest-comp input))) (implies (and (not error?) (equal element (!_ (/_ (*_ *c-wsp*) "/" (*_ *c-wsp*) *concatenation*)))) (tree-match-element-p tree? element *grammar*))))
Theorem:
(defthm tree-list-match-of-parse-conc-rest (b* (((mv & trees &) (parse-conc-rest input))) (implies (equal repetition (*_ (!_ (/_ (1*_ *c-wsp*) *repetition*)))) (tree-list-match-repetition-p trees repetition *grammar*))))
Theorem:
(defthm tree-match-of-parse-conc-rest-comp (b* (((mv error? tree? &) (parse-conc-rest-comp input))) (implies (and (not error?) (equal element (!_ (/_ (1*_ *c-wsp*) *repetition*)))) (tree-match-element-p tree? element *grammar*))))