		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-num-range-2

Check if an ABNF is a leaf tree with a single natural number in one of two given ranges, returning that natural number if successful.

Signature
(check-tree-num-range-2 tree min1 max1 min2 max2) → nat
Arguments: tree — Guard (treep tree).; min1 — Guard (natp min1).; max1 — Guard (natp max1).; min2 — Guard (natp min2).; max2 — Guard (natp max2).
Returns: nat — Type (nat-resultp nat).

Definitions and Theorems

Function: check-tree-num-range-2

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

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

(defthm nat-resultp-of-check-tree-num-range-2
  (b* ((nat (check-tree-num-range-2 tree min1 max1 min2 max2)))
    (nat-resultp nat))
  :rule-classes :rewrite)

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

(defthm natp-of-check-tree-num-range-2
  (b*
    ((acl2::?nat (check-tree-num-range-2 tree min1 max1 min2 max2)))
    (implies (not (reserrp nat))
             (natp nat)))
  :rule-classes :forward-chaining)

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

(defthm check-tree-num-range-2-bounds
  (b*
    ((acl2::?nat (check-tree-num-range-2 tree min1 max1 min2 max2)))
    (implies (not (reserrp nat))
             (or (and (<= (nfix min1) nat)
                      (<= nat (nfix max1)))
                 (and (<= (nfix min2) nat)
                      (<= nat (nfix max2))))))
  :rule-classes nil)

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

(defthm check-tree-num-range-2-of-tree-fix-tree
  (equal (check-tree-num-range-2 (tree-fix tree)
                                 min1 max1 min2 max2)
         (check-tree-num-range-2 tree min1 max1 min2 max2)))

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

(defthm check-tree-num-range-2-tree-equiv-congruence-on-tree
 (implies
    (tree-equiv tree tree-equiv)
    (equal (check-tree-num-range-2 tree min1 max1 min2 max2)
           (check-tree-num-range-2 tree-equiv min1 max1 min2 max2)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-2-of-nfix-min1

(defthm check-tree-num-range-2-of-nfix-min1
  (equal (check-tree-num-range-2 tree (nfix min1)
                                 max1 min2 max2)
         (check-tree-num-range-2 tree min1 max1 min2 max2)))

Theorem: check-tree-num-range-2-nat-equiv-congruence-on-min1

(defthm check-tree-num-range-2-nat-equiv-congruence-on-min1
 (implies
    (acl2::nat-equiv min1 min1-equiv)
    (equal (check-tree-num-range-2 tree min1 max1 min2 max2)
           (check-tree-num-range-2 tree min1-equiv max1 min2 max2)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-2-of-nfix-max1

(defthm check-tree-num-range-2-of-nfix-max1
  (equal (check-tree-num-range-2 tree min1 (nfix max1)
                                 min2 max2)
         (check-tree-num-range-2 tree min1 max1 min2 max2)))

Theorem: check-tree-num-range-2-nat-equiv-congruence-on-max1

(defthm check-tree-num-range-2-nat-equiv-congruence-on-max1
 (implies
    (acl2::nat-equiv max1 max1-equiv)
    (equal (check-tree-num-range-2 tree min1 max1 min2 max2)
           (check-tree-num-range-2 tree min1 max1-equiv min2 max2)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-2-of-nfix-min2

(defthm check-tree-num-range-2-of-nfix-min2
  (equal (check-tree-num-range-2 tree min1 max1 (nfix min2)
                                 max2)
         (check-tree-num-range-2 tree min1 max1 min2 max2)))

Theorem: check-tree-num-range-2-nat-equiv-congruence-on-min2

(defthm check-tree-num-range-2-nat-equiv-congruence-on-min2
 (implies
    (acl2::nat-equiv min2 min2-equiv)
    (equal (check-tree-num-range-2 tree min1 max1 min2 max2)
           (check-tree-num-range-2 tree min1 max1 min2-equiv max2)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-2-of-nfix-max2

(defthm check-tree-num-range-2-of-nfix-max2
  (equal (check-tree-num-range-2 tree min1 max1 min2 (nfix max2))
         (check-tree-num-range-2 tree min1 max1 min2 max2)))

Theorem: check-tree-num-range-2-nat-equiv-congruence-on-max2

(defthm check-tree-num-range-2-nat-equiv-congruence-on-max2
 (implies
    (acl2::nat-equiv max2 max2-equiv)
    (equal (check-tree-num-range-2 tree min1 max1 min2 max2)
           (check-tree-num-range-2 tree min1 max1 min2 max2-equiv)))
 :rule-classes :congruence)