		Search-engine friendly clone of the ACL2 documentation.

Abnf-tree-utilities

Check-tree-num-range

Check if an ABNF is a leaf tree with a single natural number in a given range, returning that natural number if successful.

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

Definitions and Theorems

Function: check-tree-num-range

(defun check-tree-num-range (tree min max)
 (declare (xargs :guard (and (abnf::treep tree)
                             (natp min)
                             (natp max))))
 (let ((__function__ 'check-tree-num-range))
   (declare (ignorable __function__))
   (b* ((min (nfix min))
        (max (nfix max))
        (error (reserrf (list :required (list :range (list min max))
                              :found (tree-info-for-error tree))))
        ((okf nats) (check-tree-leafterm tree))
        ((unless (and (consp nats) (endp (cdr nats))))
         error)
        (nat (car nats))
        ((unless (and (<= min nat) (<= nat max)))
         error))
     nat)))

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

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

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

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

Theorem: check-tree-num-range-bounds

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

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

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

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

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

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

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

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

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

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

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

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

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