• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
    • Std/system
    • Std/basic
    • Std/typed-lists
    • Std/bitsets
      • Bitsets
        • Bitset-members
        • Bitset-insert
        • Bitset-delete
        • Bitset-intersectp
        • Bitset-intersect
        • Bitset-difference
        • Bitset-subsetp
        • Bitset-memberp
        • Bitset-union
        • Bitset-singleton
        • Bitset-list
        • Bitset-cardinality
        • Bitset-list*
        • Utilities
      • Sbitsets
      • Reasoning
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
    • Std-extensions
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Testing-utilities
  • Math

• Bitsets

Bitset-delete

(bitset-delete a x) constructs the set X - {a}.

Signature

(bitset-delete a x) → bitset

Arguments

a — Guard (natp a).

x — Guard (natp x).

Returns

bitset — Type (natp bitset).

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.

Definitions and Theorems

Function: bitset-delete$inline

(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: natp-of-bitset-delete

(defthm acl2::natp-of-bitset-delete
        (b* ((bitset (acl2::bitset-delete$inline a x)))
            (natp bitset))
        :rule-classes :type-prescription)

Theorem: bitset-delete-when-not-natp-left

(defthm bitset-delete-when-not-natp-left
        (implies (not (natp a))
                 (equal (bitset-delete a x)
                        (bitset-delete 0 x))))

Theorem: bitset-delete-when-not-natp-right

(defthm bitset-delete-when-not-natp-right
        (implies (not (natp x))
                 (equal (bitset-delete a x) 0)))

Theorem: bitset-delete-of-nfix-left

(defthm bitset-delete-of-nfix-left
        (equal (bitset-delete (nfix a) x)
               (bitset-delete a x)))

Theorem: bitset-delete-of-nfix-right

(defthm bitset-delete-of-nfix-right
        (equal (bitset-delete a (nfix x))
               (bitset-delete a x)))

Theorem: bitset-members-of-bitset-delete

(defthm bitset-members-of-bitset-delete
        (equal (bitset-members (bitset-delete a x))
               (delete (nfix a) (bitset-members x))))