(bitset-delete a x) constructs the set
This looks pretty efficient, but keep in mind that it still has to construct a new set and hence is linear in the size of the set. You should probably avoid calling this in a loop if possible; instead, consider functions like bitset-intersect and bitset-difference.
Function:
(defun acl2::bitset-delete$inline (a x) (declare (type unsigned-byte a) (type unsigned-byte x)) (declare (xargs :guard (and (natp a) (natp x)))) (declare (xargs :split-types t)) (let ((__function__ 'bitset-delete)) (declare (ignorable __function__)) (the unsigned-byte (logandc1 (the unsigned-byte (ash 1 (the unsigned-byte (lnfix a)))) (the unsigned-byte (lnfix x))))))
Theorem:
(defthm acl2::natp-of-bitset-delete (b* ((bitset (acl2::bitset-delete$inline a x))) (natp bitset)) :rule-classes :type-prescription)
Theorem:
(defthm bitset-delete-when-not-natp-left (implies (not (natp a)) (equal (bitset-delete a x) (bitset-delete 0 x))))
Theorem:
(defthm bitset-delete-when-not-natp-right (implies (not (natp x)) (equal (bitset-delete a x) 0)))
Theorem:
(defthm bitset-delete-of-nfix-left (equal (bitset-delete (nfix a) x) (bitset-delete a x)))
Theorem:
(defthm bitset-delete-of-nfix-right (equal (bitset-delete a (nfix x)) (bitset-delete a x)))
Theorem:
(defthm bitset-members-of-bitset-delete (equal (bitset-members (bitset-delete a x)) (delete (nfix a) (bitset-members x))))