Check if all the elements of a set are natural numbers.
Function:
(defun set-all-natp (set) (declare (xargs :guard (setp set))) (let ((acl2::__function__ 'set-all-natp)) (declare (ignorable acl2::__function__)) (or (emptyp set) (and (natp (head set)) (set-all-natp (tail set))))))
Theorem:
(defthm booleanp-of-set-all-natp (acl2::b* ((yes/no (set-all-natp set))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm set-all-natp-of-insert (equal (set-all-natp (insert nat nats)) (and (natp nat) (set-all-natp (sfix nats)))))
Theorem:
(defthm set-all-natp-of-union (equal (set-all-natp (union nats1 nats2)) (and (set-all-natp (sfix nats1)) (set-all-natp (sfix nats2)))))