Check if all the elements of a set are integer numbers.
Function:
(defun set-all-integerp (set) (declare (xargs :guard (setp set))) (let ((acl2::__function__ 'set-all-integerp)) (declare (ignorable acl2::__function__)) (or (emptyp set) (and (integerp (head set)) (set-all-integerp (tail set))))))
Theorem:
(defthm booleanp-of-set-all-integerp (acl2::b* ((yes/no (set-all-integerp set))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm set-all-integerp-of-insert (equal (set-all-integerp (insert int ints)) (and (integerp int) (set-all-integerp (sfix ints)))))
Theorem:
(defthm set-all-integerp-of-union (equal (set-all-integerp (union ints1 ints2)) (and (set-all-integerp (sfix ints1)) (set-all-integerp (sfix ints2)))))