		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-nonleaf-num-range

Check if an ABNF tree is a non-leaf tree with a given optional rule name or no rule name as root and a list of one list of one subtree, where the subtree is a leaf tree with a single natural number in a range, returning that natural number if successful.

Signature
(check-tree-nonleaf-num-range tree rulename? min max) → nat
Arguments: tree — Guard (abnf::treep tree).; rulename? — Guard (maybe-stringp rulename?).; min — Guard (natp min).; max — Guard (natp max).
Returns: nat — Type (nat-resultp nat).

Definitions and Theorems

Function: check-tree-nonleaf-num-range

(defun check-tree-nonleaf-num-range (tree rulename? min max)
  (declare (xargs :guard (and (abnf::treep tree)
                              (maybe-stringp rulename?)
                              (natp min)
                              (natp max))))
  (let ((__function__ 'check-tree-nonleaf-num-range))
    (declare (ignorable __function__))
    (b* (((okf tree)
          (check-tree-nonleaf-1-1 tree rulename?)))
      (check-tree-num-range tree min max))))

Theorem: nat-resultp-of-check-tree-nonleaf-num-range

(defthm nat-resultp-of-check-tree-nonleaf-num-range
  (b* ((nat (check-tree-nonleaf-num-range tree rulename? min max)))
    (nat-resultp nat))
  :rule-classes :rewrite)

Theorem: natp-of-check-tree-nonleaf-num-range

(defthm natp-of-check-tree-nonleaf-num-range
  (b* ((acl2::?nat
            (check-tree-nonleaf-num-range tree rulename? min max)))
    (implies (not (reserrp nat))
             (natp nat)))
  :rule-classes :forward-chaining)

Theorem: check-tree-nonleaf-num-range-bounds

(defthm check-tree-nonleaf-num-range-bounds
  (b* ((acl2::?nat
            (check-tree-nonleaf-num-range tree rulename? min max)))
    (implies (not (reserrp nat))
             (and (<= (nfix min) nat)
                  (<= nat (nfix max)))))
  :rule-classes :linear)

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

(defthm check-tree-nonleaf-num-range-of-tree-fix-tree
  (equal (check-tree-nonleaf-num-range (abnf::tree-fix tree)
                                       rulename? min max)
         (check-tree-nonleaf-num-range tree rulename? min max)))

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

(defthm check-tree-nonleaf-num-range-tree-equiv-congruence-on-tree
 (implies
  (abnf::tree-equiv tree tree-equiv)
  (equal
       (check-tree-nonleaf-num-range tree rulename? min max)
       (check-tree-nonleaf-num-range tree-equiv rulename? min max)))
 :rule-classes :congruence)

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

(defthm check-tree-nonleaf-num-range-of-maybe-string-fix-rulename?
 (equal
     (check-tree-nonleaf-num-range tree (maybe-string-fix rulename?)
                                   min max)
     (check-tree-nonleaf-num-range tree rulename? min max)))

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

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

Theorem: check-tree-nonleaf-num-range-of-nfix-min

(defthm check-tree-nonleaf-num-range-of-nfix-min
  (equal (check-tree-nonleaf-num-range tree rulename? (nfix min)
                                       max)
         (check-tree-nonleaf-num-range tree rulename? min max)))

Theorem: check-tree-nonleaf-num-range-nat-equiv-congruence-on-min

(defthm check-tree-nonleaf-num-range-nat-equiv-congruence-on-min
 (implies
  (acl2::nat-equiv min min-equiv)
  (equal
       (check-tree-nonleaf-num-range tree rulename? min max)
       (check-tree-nonleaf-num-range tree rulename? min-equiv max)))
 :rule-classes :congruence)

Theorem: check-tree-nonleaf-num-range-of-nfix-max

(defthm check-tree-nonleaf-num-range-of-nfix-max
 (equal (check-tree-nonleaf-num-range tree rulename? min (nfix max))
        (check-tree-nonleaf-num-range tree rulename? min max)))

Theorem: check-tree-nonleaf-num-range-nat-equiv-congruence-on-max

(defthm check-tree-nonleaf-num-range-nat-equiv-congruence-on-max
 (implies
  (acl2::nat-equiv max max-equiv)
  (equal
       (check-tree-nonleaf-num-range tree rulename? min max)
       (check-tree-nonleaf-num-range tree rulename? min max-equiv)))
 :rule-classes :congruence)