Filtering...

outer

books/std/osets/outer
other
(in-package "SET")
other
(include-book "delete")
other
(include-book "union")
other
(include-book "intersect")
other
(include-book "difference")
other
(include-book "cardinality")
other
(set-verify-guards-eagerness 2)
other
(defthm union-delete-x
  (equal (union (delete a x) y)
    (if (in a y)
      (union x y)
      (delete a (union x y)))))
other
(defthm union-delete-y
  (equal (union x (delete a y))
    (if (in a x)
      (union x y)
      (delete a (union x y)))))
other
(defthm intersect-delete-x
  (equal (intersect (delete a x) y)
    (delete a (intersect x y))))
other
(defthm intersect-delete-y
  (equal (intersect x (delete a y))
    (delete a (intersect x y))))
other
(defthm union-over-intersect
  (equal (union x (intersect y z))
    (intersect (union x y) (union x z))))
other
(defthm intersect-over-union
  (equal (intersect x (union y z))
    (union (intersect x y)
      (intersect x z))))
other
(defthm difference-over-union
  (equal (difference x (union y z))
    (intersect (difference x y)
      (difference x z))))
other
(defthm difference-over-intersect
  (equal (difference x (intersect y z))
    (union (difference x y)
      (difference x z))))
other
(defthm difference-delete-x
  (equal (difference (delete a x) y)
    (delete a (difference x y))))
other
(defthm difference-delete-y
  (equal (difference x (delete a y))
    (if (in a x)
      (insert a (difference x y))
      (difference x y))))
other
(defthm difference-insert-y
  (equal (difference x (insert a y))
    (delete a (difference x y))))
other
(defthm intersect-cardinality-x
  (<= (cardinality (intersect x y))
    (cardinality x))
  :rule-classes (:rewrite :linear))
other
(defthm intersect-cardinality-y
  (<= (cardinality (intersect x y))
    (cardinality y))
  :rule-classes (:rewrite :linear))
other
(defthm expand-cardinality-of-union
  (equal (cardinality (union x y))
    (- (+ (cardinality x) (cardinality y))
      (cardinality (intersect x y)))))
other
(defthmd expand-cardinality-of-intersect
  (equal (cardinality (intersect x y))
    (+ (cardinality x)
      (cardinality y)
      (- (cardinality (union x y))))))
other
(theory-invariant (incompatible (:rewrite expand-cardinality-of-union)
    (:rewrite expand-cardinality-of-intersect)))
other
(defthm expand-cardinality-of-difference
  (equal (cardinality (difference x y))
    (- (cardinality x)
      (cardinality (intersect x y)))))
other
(defthmd intersect-cardinality-non-subset
  (implies (not (subset x y))
    (< (cardinality (intersect x y))
      (cardinality x)))
  :rule-classes (:rewrite :linear)
  :hints (("Goal" :in-theory (enable subset))))
other
(defthmd intersect-cardinality-subset-2
  (equal (equal (cardinality (intersect x y))
      (cardinality x))
    (subset x y)))
other
(defthmd intersect-cardinality-non-subset-2
  (equal (< (cardinality (intersect x y))
      (cardinality x))
    (not (subset x y))))