• Top
  • Documentation
  • Books
  • Recursion-and-induction
  • Boolean-reasoning
  • Debugging
  • Projects
  • Std
    • Std/lists
    • Std/alists
    • Obags
    • Std/util
    • Std/strings
    • Std/io
    • Std/osets
      • Omaps
      • All-by-membership
      • In
      • Defset
      • Primitives
      • Subset
      • Mergesort
      • Intersect
      • Union
      • Pick-a-point-subset-strategy
      • Delete
      • Difference
      • Cardinality
      • Set
      • Double-containment
      • Intersectp
    • 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
  • Testing-utilities
  • Math

• 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 (empty 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-empty

(defthm cardinality-zero-empty
        (equal (equal (cardinality x) 0)
               (empty 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))