Definition of decimal digits based on the grammar.
This defines a decimal digit as a string at the leaves of
a terminated tree rooted at the
This characterizes a (singleton) list of Unicode characters, while dec-digitp characterizes a single Unicode character. Thus, the equivalence theorem has to take this into account.
Theorem:
(defthm grammar-dec-digitp-suff (implies (and (abnf-tree-with-root-p tree "digit") (equal (abnf::tree->string tree) x)) (grammar-dec-digitp x)))
Theorem:
(defthm booleanp-of-grammar-dec-digitp (b* ((yes/no (grammar-dec-digitp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm singleton-when-grammar-dec-digitp (implies (grammar-dec-digitp x) (equal (len x) 1)))