cardinality

(in-package "SET")

(include-book "delete")

(set-verify-guards-eagerness 2)

(defsection cardinality
  :parents (std/osets)
  :short "@(call cardinality) computes the number of elements in @('X')."
  :long "<p>This is like @(see length), but respects the non-set convention and
always returns 0 for ill-formed sets.</p>"
  (defun-inline cardinality
    (x)
    (declare (xargs :guard (setp x) :verify-guards nil))
    (mbe :logic (if (emptyp x)
        0
        (1+ (cardinality (tail x))))
      :exec (length (the list x))))
  (verify-guards cardinality$inline
    :hints (("Goal" :in-theory (enable (:ruleset primitive-rules)))))
  (defthm cardinality-type
    (and (integerp (cardinality x))
      (<= 0 (cardinality x)))
    :rule-classes :type-prescription)
  (defthm cardinality-zero-emptyp
    (equal (equal (cardinality x) 0)
      (emptyp x)))
  (defthm cardinality-sfix-cancel
    (equal (cardinality (sfix x))
      (cardinality x)))
  (encapsulate nil
    (local (defthm cardinality-insert-empty
        (implies (emptyp x)
          (equal (cardinality (insert a x)) 1))
        :hints (("Goal" :use (:instance cardinality$inline
             (x (insert a nil)))))))
    (defthm insert-cardinality
      (equal (cardinality (insert a x))
        (if (in a x)
          (cardinality x)
          (1+ (cardinality x))))))
  (defthm delete-cardinality
    (equal (cardinality (delete a x))
      (if (in a x)
        (1- (cardinality x))
        (cardinality x))))
  (local (defun double-delete-induction
      (x y)
      (declare (xargs :guard (and (setp x) (setp y))))
      (if (or (emptyp x) (emptyp y))
        (list x y)
        (double-delete-induction (delete (head x) x)
          (delete (head x) y)))))
  (local (defthmd subset-double-delete
      (implies (subset x y)
        (subset (delete a x) (delete a y)))
      :hints (("Goal" :in-theory (disable delete-nonmember-cancel
           in-tail-or-head)))))
  (encapsulate nil
    (local (defthm subset-cardinality-lemma
        (implies (and (not (or (emptyp x) (emptyp y)))
            (implies (subset (delete (head x) x)
                (delete (head x) y))
              (<= (cardinality (delete (head x) x))
                (cardinality (delete (head x) y)))))
          (implies (subset x y)
            (<= (cardinality x) (cardinality y))))
        :hints (("goal" :use ((:instance subset-double-delete
              (a (head x))
              (x x)
              (y y)))))))
    (defthm subset-cardinality
      (implies (subset x y)
        (<= (cardinality x) (cardinality y)))
      :hints (("Goal" :induct (double-delete-induction x y)))
      :rule-classes (:rewrite :linear)))
  (defthmd equal-cardinality-subset-is-equality
    (implies (and (setp x)
        (setp y)
        (subset x y)
        (equal (cardinality x) (cardinality y)))
      (equal (equal x y) t))
    :hints (("Goal" :induct (double-delete-induction x y)) ("Subgoal *1/2" :use ((:instance subset-double-delete
           (a (head x))
           (x x)
           (y y)) (:instance (:theorem (implies (equal x y)
                (equal (insert a x)
                  (insert a y))))
            (a (head x))
            (x (tail x))
            (y (delete (head x) y)))))))
  (defthm proper-subset-cardinality
    (implies (and (subset x y)
        (not (subset y x)))
      (< (cardinality x) (cardinality y)))
    :rule-classes (:rewrite :linear)
    :hints (("Goal" :in-theory (disable pick-a-point-subset-strategy)
       :use ((:instance equal-cardinality-subset-is-equality
          (x (sfix x))
          (y (sfix y))))))))