		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-nonleaf

Check if an ABNF tree has a given rule name or no rule name as root, returning the list of lists of subtrees if successful.

Signature
(check-tree-nonleaf tree rulename?) → sub
Arguments: tree — Guard (treep tree).; rulename? — Guard (acl2::maybe-stringp rulename?).
Returns: sub — Type (tree-list-list-resultp sub).

Definitions and Theorems

Function: check-tree-nonleaf

(defun check-tree-nonleaf (tree rulename?)
 (declare (xargs :guard (and (treep tree)
                             (acl2::maybe-stringp rulename?))))
 (let ((__function__ 'check-tree-nonleaf))
   (declare (ignorable __function__))
   (if (and (tree-case tree :nonleaf)
            (equal (tree-nonleaf->rulename? tree)
                   (if (acl2::maybe-string-fix rulename?)
                       (rulename (acl2::maybe-string-fix rulename?))
                     nil)))
       (tree-nonleaf->branches tree)
     (reserrf (if (tree-case tree :nonleaf)
                  (list :required (acl2::maybe-string-fix rulename?)
                        :found (tree-nonleaf->rulename? tree))
                (list :required
                      :nonleaf (acl2::maybe-string-fix rulename?)
                      :found (tree-fix tree)))))))

Theorem: tree-list-list-resultp-of-check-tree-nonleaf

(defthm tree-list-list-resultp-of-check-tree-nonleaf
  (b* ((sub (check-tree-nonleaf tree rulename?)))
    (tree-list-list-resultp sub))
  :rule-classes :rewrite)

Theorem: tree-count-of-check-tree-nonleaf

(defthm tree-count-of-check-tree-nonleaf
  (b* ((?sub (check-tree-nonleaf tree rulename?)))
    (implies (not (reserrp sub))
             (< (tree-list-list-count sub)
                (tree-count tree))))
  :rule-classes :linear)

Theorem: check-tree-nonleaf-of-tree-fix-tree

(defthm check-tree-nonleaf-of-tree-fix-tree
  (equal (check-tree-nonleaf (tree-fix tree)
                             rulename?)
         (check-tree-nonleaf tree rulename?)))

Theorem: check-tree-nonleaf-tree-equiv-congruence-on-tree

(defthm check-tree-nonleaf-tree-equiv-congruence-on-tree
  (implies (tree-equiv tree tree-equiv)
           (equal (check-tree-nonleaf tree rulename?)
                  (check-tree-nonleaf tree-equiv rulename?)))
  :rule-classes :congruence)

Theorem: check-tree-nonleaf-of-maybe-string-fix-rulename?

(defthm check-tree-nonleaf-of-maybe-string-fix-rulename?
 (equal (check-tree-nonleaf tree (acl2::maybe-string-fix rulename?))
        (check-tree-nonleaf tree rulename?)))

Theorem: check-tree-nonleaf-maybe-string-equiv-congruence-on-rulename?

(defthm
      check-tree-nonleaf-maybe-string-equiv-congruence-on-rulename?
  (implies (acl2::maybe-string-equiv rulename? rulename?-equiv)
           (equal (check-tree-nonleaf tree rulename?)
                  (check-tree-nonleaf tree rulename?-equiv)))
  :rule-classes :congruence)