		Search-engine friendly clone of the ACL2 documentation.

Kestrel-utilities

Integers-from-to

Ordered list of all the integers in a range.

Signature
(integers-from-to min max) → ints
Arguments: min — Guard (integerp min).; max — Guard (integerp max).
Returns: ints — Type (integer-listp ints).

The range goes from min to max, inclusive. If min exceeds max, the result is nil.

Definitions and Theorems

Function: integers-from-to-aux

(defun integers-from-to-aux (min max ints)
       (declare (xargs :guard (and (integerp min)
                                   (integerp max)
                                   (integer-listp ints))))
       (let ((__function__ 'integers-from-to-aux))
            (declare (ignorable __function__))
            (b* ((min (mbe :logic (ifix min) :exec min))
                 (max (mbe :logic (ifix max) :exec max)))
                (cond ((> min max) ints)
                      (t (integers-from-to-aux min (1- max)
                                               (cons max ints)))))))

Function: integers-from-to

(defun
 integers-from-to (min max)
 (declare (xargs :guard (and (integerp min) (integerp max))))
 (let
  ((__function__ 'integers-from-to))
  (declare (ignorable __function__))
  (mbe
   :logic (b* ((min (ifix min)) (max (ifix max)))
              (cond ((> min max) nil)
                    (t (cons min (integers-from-to (1+ min) max)))))
   :exec (integers-from-to-aux min max nil))))

Theorem: integer-listp-of-integers-from-to

(defthm integer-listp-of-integers-from-to
        (b* ((ints (integers-from-to min max)))
            (integer-listp ints))
        :rule-classes :rewrite)

Theorem: true-listp-of-integers-from-to

(defthm true-listp-of-integers-from-to
        (b* ((ints (integers-from-to min max)))
            (true-listp ints))
        :rule-classes :type-prescription)

Theorem: nat-listp-of-integers-from-to

(defthm nat-listp-of-integers-from-to
        (equal (nat-listp (integers-from-to min max))
               (or (> (ifix min) (ifix max))
                   (natp (ifix min)))))

Theorem: pos-listp-of-integers-from-to

(defthm pos-listp-of-integers-from-to
        (equal (pos-listp (integers-from-to min max))
               (or (> (ifix min) (ifix max))
                   (posp (ifix min)))))

Theorem: int-equiv-implies-equal-integers-from-to-1

(defthm int-equiv-implies-equal-integers-from-to-1
        (implies (int-equiv min min-equiv)
                 (equal (integers-from-to min max)
                        (integers-from-to min-equiv max)))
        :rule-classes (:congruence))

Theorem: int-equiv-implies-equal-integers-from-to-2

(defthm int-equiv-implies-equal-integers-from-to-2
        (implies (int-equiv max max-equiv)
                 (equal (integers-from-to min max)
                        (integers-from-to min max-equiv)))
        :rule-classes (:congruence))

Theorem: integers-from-to-nil-when-min>max

(defthm integers-from-to-nil-when-min>max
        (implies (> (ifix min) (ifix max))
                 (equal (integers-from-to min max) nil)))

Theorem: integers-from-to-iff-min<=max

(defthm integers-from-to-iff-min<=max
        (iff (integers-from-to min max)
             (<= (ifix min) (ifix max))))

Theorem: member-of-integers-from-to

(defthm member-of-integers-from-to
        (iff (member x (integers-from-to min max))
             (and (integerp x)
                  (<= (ifix min) x)
                  (<= x (ifix max)))))

Subtopics

Integers-from-to-as-set: Theorems about integers-from-to as a finite set.