Sets : THEORY

BEGIN

  X   : TYPE
  SET : TYPE = pred[X]

  x,y   : VAR X
  R,S,T : VAR SET


  % ---------- membership

  member(x, S): bool = S(x);


  % ---------- equality on sets

  ==(S,T) : bool =
    FORALL x: member(x,S) IFF member(x,T)


  % ---------- empty sets

% 4-2 a)

  emptyset : SET = [... hier ausfuellen! ...]

  empty_no_members: LEMMA 
    NOT member(x, emptyset)


  % ---------- fullset

% 4-2 a)

  fullset : SET = [... hier ausfuellen! ...]

  fullset_member : LEMMA 
    member(x, fullset)
  

  % ---------- add an element to a set

% 4-2 b)

  add(x, S): SET = [... hier ausfuellen! ...]

  member_add : LEMMA 
    member(x, add(x, S)) 

  add_idempotent : LEMMA
    add(x, add(x,S)) == add(x,S)

  % ---------- remove an element from a set

% 4-2 b)

  remove(x, S) : SET = [... hier ausfuellen! ...]

  member_remove : LEMMA
    NOT member(x,remove(x,S))

  % ---------- subset relationship

% 4-2 c)

  subset?(S, T): bool = [... hier ausfuellen! ...]

  subset_emptyset : LEMMA 
    subset?(emptyset, S)

  subset_fullset : LEMMA 
    subset?(S, fullset)

  subset_antisymmetric : LEMMA 
    subset?(S, T) AND subset?(T, S) IMPLIES S == T

  % ---------- union of sets

% 4-2 d)

  union(S, T): SET = [... hier ausfuellen! ...]

  union_commutative : LEMMA 
    union(S, T) == union(T, S)

  union_subset : LEMMA 
    subset?(S, T) IMPLIES union(S, T) == T


  % ---------- set intersection

% 4-2 d)

  intersection(S, T) : SET = [... hier ausfuellen! ...]

  distribute_union_intersection : LEMMA
    union(S, intersection(T, R)) == intersection(union(S, T), union(S, R))


  % ---------- complement of sets

% 4-2 e)

  complement(S) : SET = [... hier ausfuellen! ...]

  complement_emptyset : LEMMA 
    complement(emptyset) == fullset

  demorgan : LEMMA
    complement(intersection(S, T)) == union(complement(S), complement(T))


  % ---------- difference

% 4-2 e)

  difference(S, T) : SET = [... hier ausfuellen! ...]

  difference_fullset : LEMMA 
    difference(S, fullset) == emptyset

  difference_intersection : LEMMA
    difference(S, T) == intersection(S, complement(T))

END Sets