		Search-engine friendly clone of the ACL2 documentation.

Bitsets

Bitset-members

(bitset-members x) converts a bitset into an ordinary, ordered set.

Signature
(bitset-members x) → *
Arguments: x — Guard (natp x).

Reasoning note: bitset-members is fundamental to reasoning about bitsets; see Reasoning with Bitsets in bitsets. Its definition and the theorem in-of-bitset-members should generally be left disabled since they expose the underlying representation of bitsets.

Performance note: bitset-members is inherently expensive: no matter how it is implemented, it must create at least |X| conses. You may sometimes be able to avoid this cost using functions like bitset-memberp, bitset-intersectp, or bitset-subsetp instead.

It is simple enough to convert a bitset into an ordered set: since the integer-length of x gives us an upper bound on its elements, we just need to walk up to this bound and collect all i such that (logbitp i x).

The definition below uses bits-between to do just this. However, note that when the bignum-extract-opt book is loaded (which requires a ttag), a more efficient implementation is used; see ttag-bitset-members and bignum-extract for details.

Definitions and Theorems

Function: bitset-members

(defun bitset-members (x)
       (declare (xargs :guard (natp x)))
       (let ((__function__ 'bitset-members))
            (declare (ignorable __function__))
            (mbe :logic (let ((x (nfix x)))
                             (bits-between 0 (integer-length x) x))
                 :exec (bits-between 0 (integer-length x) x))))

Theorem: bitset-members-default

(defthm bitset-members-default
        (implies (not (natp a))
                 (equal (bitset-members a) nil)))

Theorem: bitset-members-of-nfix

(defthm bitset-members-of-nfix
        (equal (bitset-members (nfix b))
               (bitset-members b)))

Theorem: true-listp-of-bitset-members

(defthm true-listp-of-bitset-members
        (true-listp (bitset-members x))
        :rule-classes :type-prescription)

Theorem: nat-listp-of-bitset-members

(defthm nat-listp-of-bitset-members
        (nat-listp (bitset-members x)))

Theorem: no-duplicatesp-equal-of-bitset-members

(defthm no-duplicatesp-equal-of-bitset-members
        (no-duplicatesp-equal (bitset-members x)))

Theorem: setp-of-bitset-members

(defthm setp-of-bitset-members
        (setp (bitset-members x)))

Theorem: in-of-bitset-members

(defthm in-of-bitset-members
        (equal (in a (bitset-members x))
               (and (natp a) (logbitp a (nfix x)))))

Theorem: bitset-members-under-iff

(defthm bitset-members-under-iff
        (iff (bitset-members x) (posp x)))

Subtopics

Ttag-bitset-members: Notes about the optimization of bitset-members.