		Search-engine friendly clone of the ACL2 documentation.

Grammar

Abnf-tree-with-root-p

Recognize terminated ABNF trees whose root is the given rule name, for the Java grammar.

Signature
(abnf-tree-with-root-p tree rulename) → yes/no
Arguments: rulename — Guard (stringp rulename).
Returns: yes/no — Type (booleanp yes/no).

This is a useful abbreviation for a more verbose conjunction of ABNF predicates with more verbose arguments.

The tree is terminated, i.e. it has natural numbers at its leaves, not rule names. These natural numbers are Java Unicode characters, because the grammar satisfies abnf::rulelist-in-termset-p for the set (integers-from-to 0 #xffff) as proved here. To prove that the string at the leaves satisfies unicode-listp, we proceed as follows:

We disable integers-from-to and its executable counterpart, so that (integers-from-to 0 #xffff) does not get expanded.
We prove that membership in (integers-from-to 0 #xffff) is equivalent to unicodep (via a library theorem that rewrites the membership assertion into integer inequalities), and then lift that to list-in and unicode-listp.
We prove that abnf-tree-with-root-p implies abnf::string-parsablep, and then abnf::terminal-string-for-rules-p.
We combine the facts from the previous two steps with the abnf::rulelist-in-termset-p theorem about the grammar and with the ABNF library theorem abnf::terminal-strings-in-termset-when-rules-in-termset, which relates the meta-syntactic property abnf::rulelist-in-termset-p with membership in the set of terminals, to obtain the final theorem.

Definitions and Theorems

Function: abnf-tree-with-root-p

(defun abnf-tree-with-root-p (tree rulename)
  (declare (xargs :guard (stringp rulename)))
  (and (abnf::treep tree)
       (abnf::tree-terminatedp tree)
       (abnf::tree-match-element-p
            tree
            (abnf::element-rulename (abnf::rulename rulename))
            *grammar*)))

Theorem: booleanp-of-abnf-tree-with-root-p

(defthm booleanp-of-abnf-tree-with-root-p
  (b* ((yes/no (abnf-tree-with-root-p tree rulename)))
    (booleanp yes/no))
  :rule-classes :rewrite)

Theorem: abnf-treep-when-abnf-tree-with-root-p

(defthm abnf-treep-when-abnf-tree-with-root-p
  (implies (abnf-tree-with-root-p tree rulename)
           (abnf::treep tree)))

Theorem: not-abnf-tree-with-root-p-of-nil

(defthm not-abnf-tree-with-root-p-of-nil
  (not (abnf-tree-with-root-p nil rulename)))

Theorem: unicode-listp-of-string-of-abnf-tree-with-root

(defthm unicode-listp-of-string-of-abnf-tree-with-root
  (implies (abnf-tree-with-root-p tree rulename)
           (unicode-listp (abnf::tree->string tree))))

Theorem: abnf-tree-with-root-p-of-str-fix-rulename

(defthm abnf-tree-with-root-p-of-str-fix-rulename
  (equal (abnf-tree-with-root-p tree (str-fix rulename))
         (abnf-tree-with-root-p tree rulename)))

Theorem: abnf-tree-with-root-p-streqv-congruence-on-rulename

(defthm abnf-tree-with-root-p-streqv-congruence-on-rulename
  (implies (acl2::streqv rulename rulename-equiv)
           (equal (abnf-tree-with-root-p tree rulename)
                  (abnf-tree-with-root-p tree rulename-equiv)))
  :rule-classes :congruence)