Quelle  partitions.pvs

%------------------------------------------------------------------------------
% Partitions
%
%     Author: David Lester, Manchester University, NIA, Université Perpignan
%
% All references are to SK Berberian "Fundamentals of Real Analysis",
% Springer, 1991
%
% Partitioning a set into a set of sets. Note pleasant combining function
% "join"
%
%     Version 1.0            1/5/07   Initial Version
%------------------------------------------------------------------------------

partitions[T:TYPE]: THEORY

BEGIN

  a,a1,a2: VAR set[T]
  A:       VAR setofsets[T]

  partition?(A,a):bool
    = Union(A) = a AND FORALL (x,y:(A)): x /= y => disjoint?(x,y)

  finite_partition?(A,a):bool = partition?(A,a) AND is_finite(A)

  partition: TYPE+ = (LAMBDA A: partition?(A,fullset[T])) CONTAINING
                                                singleton[set[T]](fullset[T])

  finite_partition: TYPE+ = (LAMBDA A: finite_partition?(A,fullset[T]))
                                CONTAINING singleton[set[T]](fullset[T])

  p1,p2: VAR finite_partition

  IMPORTING finite_sets@finite_cross

  join(p1,p2):finite_partition
    = {a | EXISTS (a1:(p1),a2:(p2)): a = intersection(a1,a2)}

END partitions