Recognize finite sets of natural numbers.
(nat-setp x) → yes/no
Function:
(defun nat-setp (x) (declare (xargs :guard t)) (let ((acl2::__function__ 'nat-setp)) (declare (ignorable acl2::__function__)) (and (setp x) (set-all-natp x))))
Theorem:
(defthm booleanp-of-nat-setp (acl2::b* ((yes/no (nat-setp x))) (booleanp yes/no)) :rule-classes :rewrite)
Theorem:
(defthm setp-when-nat-setp (implies (nat-setp nats) (setp nats)))
Theorem:
(defthm nat-setp-of-insert (equal (nat-setp (insert nat nats)) (and (natp nat) (nat-setp (sfix nats)))))
Theorem:
(defthm nat-setp-of-union (equal (nat-setp (union nats1 nats2)) (and (nat-setp (sfix nats1)) (nat-setp (sfix nats2)))))