Recognize finite sets of integer numbers.
(integer-setp x) → yes/no
Function:
(defun integer-setp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'integer-setp)) (declare (ignorable acl2::__function__)) (and (setp x) (set-all-integerp x))))
Theorem:
(defthm booleanp-of-integer-setp (acl2::b* ((yes/no (integer-setp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm setp-when-integer-setp (implies (integer-setp ints) (setp ints)))
Theorem:
(defthm integer-setp-of-insert (equal (integer-setp (insert int ints)) (and (integerp int) (integer-setp (sfix ints)))))
Theorem:
(defthm integer-setp-of-union (equal (integer-setp (union ints1 ints2)) (and (integer-setp (sfix ints1)) (integer-setp (sfix ints2)))))