		Search-engine friendly clone of the ACL2 documentation.

Tree-utilities

Check-tree-num-range-4

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

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

Definitions and Theorems

Function: check-tree-num-range-4

(defun check-tree-num-range-4
       (tree min1 max1 min2 max2 min3 max3 min4 max4)
 (declare (xargs :guard (and (treep tree)
                             (natp min1)
                             (natp max1)
                             (natp min2)
                             (natp max2)
                             (natp min3)
                             (natp max3)
                             (natp min4)
                             (natp max4))))
 (let ((__function__ 'check-tree-num-range-4))
   (declare (ignorable __function__))
   (b*
     ((min1 (nfix min1))
      (max1 (nfix max1))
      (min2 (nfix min2))
      (max2 (nfix max2))
      (min3 (nfix min3))
      (max3 (nfix max3))
      (min4 (nfix min4))
      (max4 (nfix max4))
      (error (reserrf (list :required (list :ranges (list min1 max1)
                                            (list min2 max2)
                                            (list min3 max3)
                                            (list min4 max4))
                            :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))
                   (and (<= min3 nat) (<= nat max3))
                   (and (<= min4 nat) (<= nat max4))))
       error))
     nat)))

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

(defthm nat-resultp-of-check-tree-num-range-4
 (b*
  ((nat
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))
  (nat-resultp nat))
 :rule-classes :rewrite)

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

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

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

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

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

(defthm check-tree-num-range-4-of-tree-fix-tree
 (equal
    (check-tree-num-range-4 (tree-fix tree)
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1
                            max1 min2 max2 min3 max3 min4 max4)))

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

(defthm check-tree-num-range-4-tree-equiv-congruence-on-tree
 (implies
  (tree-equiv tree tree-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree-equiv min1
                            max1 min2 max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

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

(defthm check-tree-num-range-4-of-nfix-min1
  (equal
       (check-tree-num-range-4 tree (nfix min1)
                               max1 min2 max2 min3 max3 min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

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

(defthm check-tree-num-range-4-nat-equiv-congruence-on-min1
 (implies
  (acl2::nat-equiv min1 min1-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1-equiv
                            max1 min2 max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

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

(defthm check-tree-num-range-4-of-nfix-max1
  (equal
       (check-tree-num-range-4 tree min1 (nfix max1)
                               min2 max2 min3 max3 min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

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

(defthm check-tree-num-range-4-nat-equiv-congruence-on-max1
 (implies
  (acl2::nat-equiv max1 max1-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1-equiv
                            min2 max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

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

(defthm check-tree-num-range-4-of-nfix-min2
  (equal
       (check-tree-num-range-4 tree min1 max1 (nfix min2)
                               max2 min3 max3 min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

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

(defthm check-tree-num-range-4-nat-equiv-congruence-on-min2
 (implies
  (acl2::nat-equiv min2 min2-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2-equiv max2 min3 max3 min4 max4)))
 :rule-classes :congruence)

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

(defthm check-tree-num-range-4-of-nfix-max2
  (equal
       (check-tree-num-range-4 tree min1 max1 min2 (nfix max2)
                               min3 max3 min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

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

(defthm check-tree-num-range-4-nat-equiv-congruence-on-max2
 (implies
  (acl2::nat-equiv max2 max2-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2 max2-equiv min3 max3 min4 max4)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-4-of-nfix-min3

(defthm check-tree-num-range-4-of-nfix-min3
  (equal
       (check-tree-num-range-4 tree min1 max1 min2 max2 (nfix min3)
                               max3 min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-num-range-4-nat-equiv-congruence-on-min3

(defthm check-tree-num-range-4-nat-equiv-congruence-on-min3
 (implies
  (acl2::nat-equiv min3 min3-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2 max2 min3-equiv max3 min4 max4)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-4-of-nfix-max3

(defthm check-tree-num-range-4-of-nfix-max3
  (equal
       (check-tree-num-range-4 tree
                               min1 max1 min2 max2 min3 (nfix max3)
                               min4 max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-num-range-4-nat-equiv-congruence-on-max3

(defthm check-tree-num-range-4-nat-equiv-congruence-on-max3
 (implies
  (acl2::nat-equiv max3 max3-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2 max2 min3 max3-equiv min4 max4)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-4-of-nfix-min4

(defthm check-tree-num-range-4-of-nfix-min4
  (equal
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 (nfix min4)
                               max4)
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-num-range-4-nat-equiv-congruence-on-min4

(defthm check-tree-num-range-4-nat-equiv-congruence-on-min4
 (implies
  (acl2::nat-equiv min4 min4-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2 max2 min3 max3 min4-equiv max4)))
 :rule-classes :congruence)

Theorem: check-tree-num-range-4-of-nfix-max4

(defthm check-tree-num-range-4-of-nfix-max4
  (equal
       (check-tree-num-range-4 tree min1 max1
                               min2 max2 min3 max3 min4 (nfix max4))
       (check-tree-num-range-4 tree min1
                               max1 min2 max2 min3 max3 min4 max4)))

Theorem: check-tree-num-range-4-nat-equiv-congruence-on-max4

(defthm check-tree-num-range-4-nat-equiv-congruence-on-max4
 (implies
  (acl2::nat-equiv max4 max4-equiv)
  (equal
    (check-tree-num-range-4 tree
                            min1 max1 min2 max2 min3 max3 min4 max4)
    (check-tree-num-range-4 tree min1 max1
                            min2 max2 min3 max3 min4 max4-equiv)))
 :rule-classes :congruence)