enumerate

(in-package "ACL2")

(defun enumerate!
  (term i j)
  (declare (xargs :measure (acl2-count (nfix (- (+ 1 (ifix j)) (ifix i))))))
  (cond ((and (integerp i) (integerp j) (<= i j)) (if (equal term i)
        t
        (enumerate! term (+ i 1) j)))
    (t nil)))

(defthm enumerate
  (implies (and (integerp term)
      (integerp i)
      (integerp j)
      (<= i term)
      (<= term j))
    (enumerate! term i j))
  :rule-classes nil)

(defthm enumerate-expander
  (and (implies (and (syntaxp (and (quotep i) (quotep j)))
        (integerp i)
        (integerp j)
        (< j i))
      (equal (enumerate! term i j) nil))
    (implies (and (syntaxp (and (quotep i) (quotep j)))
        (integerp i)
        (integerp j)
        (<= i j))
      (equal (enumerate! term i j)
        (or (equal term i) (enumerate! term (+ i 1) j))))))

(in-theory (disable enumerate!))