% various extras for the standard prelude

sets_lemmas_aux[T:TYPE]: THEORY

BEGIN

  x, y: VAR T
  a, b, c: VAR set[T]
  A, B : Var setofsets[T]

  IMPORTING sets_lemmas[T]

  union_complement:        LEMMA union(a,complement(a))        = fullset
  intersection_complement: LEMMA intersection(a,complement(a)) = emptyset
  disjoint_complement:     LEMMA disjoint?(a,complement(a))
  disjoint_commutative:    LEMMA disjoint?(a,b) = disjoint?(b,a)
  disjoint_empty:          LEMMA disjoint?(a,emptyset)
  powerset_fullset:        LEMMA member(a, powerset(a))
  union_diff_inter:        LEMMA union(difference(a,b),intersection(a,b)) = a
  disjoint_diff_inter:     LEMMA disjoint?(difference(a,b),intersection(a,b))
  disjoint_member:         LEMMA disjoint?(a,b) AND member(x,a) IMPLIES
                                                               NOT member(x,b)

END sets_lemmas_aux