• Top
    • Documentation
    • Books
    • Boolean-reasoning
    • Debugging
    • Projects
    • Std
      • Std/lists
      • Std/alists
      • Obags
        • Bagp
        • Bag
        • Tail
        • Head
        • Subbag
        • Intersect
        • Empty
          • Union
          • Insert
          • Difference
          • Delete
          • Cardinality
          • Bfix
          • In
          • Occs
        • Std/util
        • Std/strings
        • Std/io
        • Std/osets
        • Std/system
        • Std/basic
        • Std/typed-lists
        • Std/bitsets
        • Std/testing
        • Std/typed-alists
        • Std/stobjs
        • Std-extensions
      • Proof-automation
      • Macro-libraries
      • ACL2
      • Interfacing-tools
      • Hardware-verification
      • Software-verification
      • Math
      • Testing-utilities
    • Obags

    Empty

    Check if an obag is empty.

    Signature
    (empty bag) → yes/no
    Arguments
    bag — Guard (bagp bag).
    Returns
    yes/no — Type (booleanp yes/no).

    This is similar to set::empty for osets.

    Definitions and Theorems

    Function: empty

    (defun empty (bag)
      (declare (xargs :guard (bagp bag)))
      (let ((__function__ 'empty))
        (declare (ignorable __function__))
        (null (bfix bag))))

    Theorem: booleanp-of-empty

    (defthm booleanp-of-empty
      (b* ((yes/no (empty bag)))
        (booleanp yes/no))
      :rule-classes :rewrite)

    Theorem: bagp-when-not-empty

    (defthm bagp-when-not-empty
      (implies (not (empty bag)) (bagp bag)))

    Theorem: bfix-when-empty

    (defthm bfix-when-empty
      (implies (empty x)
               (equal (bfix x) nil)))