Validation of the concrete syntax grammar.
We show that rules of the grammar of the ABNF concrete syntax:
These theorems are in a separate file so that the definition of the concrete syntax does not depend on the grammar operations, as also done for core-rules-validation and for concrete-syntax-rules-validation.
(defthm rulelist-wfp-of-*grammar* (rulelist-wfp *grammar*))
(defthm rulelist-closedp-of-*grammar* (rulelist-closedp *grammar*))
(defthm ascii-only-*grammar* (rulelist-in-termset-p *grammar* (integers-from-to 0 127)))
(defthm plugging-yields-*grammar* (set-equiv (plug-rules *concrete-syntax-rules* *core-rules*) *grammar*))