power_sets [T: TYPE ]: THEORY
%------------------------------------------------------------------------
%  Power sets, finiteness and cardinality    (Version 1.0) 6/28/96
%
%      by Bruno Dutertre    Royal Holloway & Bedford New College
% 
%   Establishes fundamental properties.  The definition and finiteness
%   proof have moved to the prelude.
%  
%------------------------------------------------------------------------

EXPORTING ALL WITH finite_sets[nat], finite_sets[T], sets[T],
                   finite_sets_of_sets[T], set_of_functions[T, nat]

BEGIN

  IMPORTING finite_sets@finite_sets_card_eq, finite_sets_of_sets[T], sets[T]

  S, U: VAR set[T]
  A: VAR finite_set[T]
  n: VAR nat

  B: finite_set[nat] = { n | n <= 1} 

  card_B: LEMMA  card(B) = 2

  IMPORTING set_of_functions[T, nat], finite_sets@finite_sets_eq

  powerset_bijection       : LEMMA (EXISTS (f: [(powerset(S)) -> [(S)->(B)]]):
                                                 bijective?(f))

  finite_powerset_bijection: LEMMA (EXISTS (f: [(powerset(A))->(funset(A,B))]):
                                                 bijective?(f))

  card_powerset            : THEOREM card(powerset(A)) = 2 ^ card(A)

  elem_finite_powerset     : THEOREM (FORALL (X: (powerset(A))): is_finite(X))

  SS: VAR set[set[T]]
  finite_subset_of_powerset: THEOREM subset?(SS,powerset(A)) 
                                        IMPLIES is_finite(SS)

END power_sets