		Search-engine friendly clone of the ACL2 documentation.

Binary-digits-grammar-validation

Grammar-bin-digitp

Definition of binary digits based on the grammar.

This defines a binary digit as a string at the leaves of a terminated tree rooted at the binary-digit nonterminal. The string is always a singleton.

This characterizes a (singleton) list of Unicode characters, while bin-digitp characterizes a single Unicode character. Thus, the equivalence theorem has to take this into account.

Definitions and Theorems

Theorem: grammar-bin-digitp-suff

(defthm grammar-bin-digitp-suff
  (implies (and (abnf-tree-with-root-p tree "binary-digit")
                (equal (abnf::tree->string tree) x))
           (grammar-bin-digitp x)))

Theorem: booleanp-of-grammar-bin-digitp

(defthm booleanp-of-grammar-bin-digitp
  (b* ((yes/no (grammar-bin-digitp x)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: singleton-when-grammar-bin-digitp

(defthm singleton-when-grammar-bin-digitp
  (implies (grammar-bin-digitp x)
           (equal (len x) 1)))