power_sets [T: TYPE ]: THEORY %------------------------------------------------------------------------ % Power sets, finiteness and cardinality (Version 1.0) 6/28/96 % % by Bruno Dutertre Royal Holloway & Bedford New College % % Defines: % % powerset(S): setof[setof[T]] = { U | subset?(U, S) } % % and establishes fundamental properties % %------------------------------------------------------------------------ % EXPORTING ALL WITH finite_sets_def[nat], finite_sets[nat], % card_def[nat] % % produces "card_B refers to power_sets.S, which must be exported" % THIS IS A BUG. We would like to do this to see if the load time % would be reduced. BEGIN IMPORTING finite_sets@finite_sets, finite_sets@finite_sets_card_eq S, U: VAR set[T] A: VAR finite_set[T] n: VAR nat powerset(S): set[set[T]] = { U | subset?(U, S) } B: finite_set[nat] = { n | n <= 1} card_B: LEMMA card(B) = 2 IMPORTING set_of_functions, 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)) finite_powerset : THEOREM is_finite(powerset(A)) JUDGEMENT powerset(A) HAS_TYPE finite_set[set[T]] 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