• Top
  • Documentation
  • Books
  • Boolean-reasoning
  • Projects
  • Debugging
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • Defset
      • In
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Double-containment
      • Difference
      • Cardinality
      • Set
      • Intersectp
    • Std/basic
    • Std/system
    • Std/typed-lists
    • Std/bitsets
    • Std/testing
    • Std/typed-alists
    • Std/stobjs
  • Proof-automation
  • Macro-libraries
  • ACL2
  • Interfacing-tools
  • Hardware-verification
  • Software-verification
  • Math
  • Testing-utilities

• Std/osets

Cardinality

(cardinality x) computes the number of elements in X.

This is like length, but respects the non-set convention and always returns 0 for ill-formed sets.

Definitions and Theorems

Function: cardinality

(defun cardinality (x)
  (declare (xargs :guard (setp x)))
  (mbe :logic
       (if (emptyp x)
           0
         (1+ (cardinality (tail x))))
       :exec (length (the list x))))

Theorem: cardinality-type

(defthm cardinality-type
  (and (integerp (cardinality x))
       (<= 0 (cardinality x)))
  :rule-classes :type-prescription)

Theorem: cardinality-zero-emptyp

(defthm cardinality-zero-emptyp
  (equal (equal (cardinality x) 0)
         (emptyp x)))

Theorem: cardinality-sfix-cancel

(defthm cardinality-sfix-cancel
  (equal (cardinality (sfix x))
         (cardinality x)))

Theorem: insert-cardinality

(defthm insert-cardinality
  (equal (cardinality (insert a x))
         (if (in a x)
             (cardinality x)
           (1+ (cardinality x)))))

Theorem: delete-cardinality

(defthm delete-cardinality
  (equal (cardinality (delete a x))
         (if (in a x)
             (1- (cardinality x))
           (cardinality x))))

Theorem: subset-cardinality

(defthm subset-cardinality
  (implies (subset x y)
           (<= (cardinality x) (cardinality y)))
  :rule-classes (:rewrite :linear))

Theorem: equal-cardinality-subset-is-equality

(defthm equal-cardinality-subset-is-equality
  (implies (and (setp x)
                (setp y)
                (subset x y)
                (equal (cardinality x) (cardinality y)))
           (equal (equal x y) t)))

Theorem: proper-subset-cardinality

(defthm proper-subset-cardinality
  (implies (and (subset x y) (not (subset y x)))
           (< (cardinality x) (cardinality y)))
  :rule-classes (:rewrite :linear))