		Search-engine friendly clone of the ACL2 documentation.

Semantics

Theorems-about-terminated-trees-matching-elements

Some theorems about terminated trees matching certain elements.

Definitions and Theorems

Theorem: tree-nonleaf-when-match-rulename/group/option

(defthm tree-nonleaf-when-match-rulename/group/option
  (implies (and (tree-match-element-p tree element rules)
                (member-eq (element-kind element)
                           '(:rulename :group :option))
                (tree-terminatedp tree))
           (equal (tree-kind tree) :nonleaf)))

Theorem: tree-leafterm-when-match-numval/charval

(defthm tree-leafterm-when-match-numval/charval
  (implies (and (tree-match-element-p tree element rules)
                (member-eq (element-kind element)
                           '(:num-val :char-val)))
           (equal (tree-kind tree) :leafterm)))

Theorem: tree-rulename-when-match-rulename

(defthm tree-rulename-when-match-rulename
  (implies (and (tree-match-element-p tree element rules)
                (element-case element :rulename)
                (tree-terminatedp tree))
           (equal (tree-nonleaf->rulename? tree)
                  (element-rulename->get element))))

Theorem: tree-branches-match-alt-when-match-rulename

(defthm tree-branches-match-alt-when-match-rulename
 (implies
   (and (tree-match-element-p tree element rules)
        (element-case element :rulename)
        (equal alt
               (lookup-rulename (element-rulename->get element)
                                rules))
        (tree-terminatedp tree))
   (tree-list-list-match-alternation-p (tree-nonleaf->branches tree)
                                       alt rules)))

Theorem: tree-nats-match-sensitive-when-match-char-val-sensitive

(defthm tree-nats-match-sensitive-when-match-char-val-sensitive
 (implies
  (and
   (tree-match-element-p tree element rules)
   (element-case element :char-val)
   (char-val-case (element-char-val->get element)
                  :sensitive)
   (equal
    chars
    (explode
        (char-val-sensitive->get (element-char-val->get element)))))
  (nats-match-sensitive-chars-p (tree-leafterm->get tree)
                                chars)))

Theorem: tree-nats-match-insensitive-when-match-char-val-insensitive

(defthm tree-nats-match-insensitive-when-match-char-val-insensitive
 (implies
  (and
   (tree-match-element-p tree element rules)
   (element-case element :char-val)
   (char-val-case (element-char-val->get element)
                  :insensitive)
   (equal
    chars
    (explode
      (char-val-insensitive->get (element-char-val->get element)))))
  (nats-match-insensitive-chars-p (tree-leafterm->get tree)
                                  chars)))