Input decomposition 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 input-decomposition-of-parse-alternation (b* (((mv error? tree? rest-input) (parse-alternation input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-concatenation (b* (((mv error? tree? rest-input) (parse-concatenation input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-repetition (b* (((mv error? tree? rest-input) (parse-repetition input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-element (b* (((mv error? tree? rest-input) (parse-element input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-group (b* (((mv error? tree? rest-input) (parse-group input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-option (b* (((mv error? tree? rest-input) (parse-option input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-alt-rest (b* (((mv & trees rest-input) (parse-alt-rest input))) (equal (append (tree-list->string trees) rest-input) (nat-list-fix input))))
Theorem:
(defthm input-decomposition-of-parse-alt-rest-comp (b* (((mv error? tree? rest-input) (parse-alt-rest-comp input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))
Theorem:
(defthm input-decomposition-of-parse-conc-rest (b* (((mv & trees rest-input) (parse-conc-rest input))) (equal (append (tree-list->string trees) rest-input) (nat-list-fix input))))
Theorem:
(defthm input-decomposition-of-parse-conc-rest-comp (b* (((mv error? tree? rest-input) (parse-conc-rest-comp input))) (implies (not error?) (equal (append (tree->string tree?) rest-input) (nat-list-fix input)))))