SSL lagrange_scaf.pvs

lagrange_scaf[T:TYPE]: THEORY
%------------------------------------------------------------------------------
% Unions of Partitions (disjoint covering sets)
%
%     Author: Rick Butler, NASA Langley
%             Adapted from equivalence_classes (David Lester)
%
%     Version 1.0           12/12/07     
%
%  THIS IS NOW OBSOLETE -- see lagrange_scaf 
%------------------------------------------------------------------------------
BEGIN


  SS:  VAR setofsets[T]
  a,b: VAR set[T]
  n:   VAR nat
  x,y: VAR T

% We define a "partition" as a set of nonempty, disjoint sets.

  partition?(SS): bool = (FORALL (a,b:(SS)): a = b OR disjoint?(a,b))

  partition: TYPE = (partition?) CONTAINING emptyset[(nonempty?[T])]

  P: VAR partition

% We now define "finite_partitions" as a finite set of finite nonempty sets.
 
  finite_partition?(SS): bool
    = partition?(SS) AND is_finite(SS) AND every(is_finite[T])(SS)

  finite_partition: TYPE = (finite_partition?) CONTAINING
                                                  emptyset[(nonempty?[T])]
  FP: VAR finite_partition

  finite_partition_is_partition:JUDGEMENT finite_partition SUBTYPE_OF partition


  IMPORTING finite_sets@finite_sets_inductions


  AUTO_REWRITE+ member

  m: VAR nat
  PP: VAR finite_partition

  card_Union_rest: LEMMA nonempty?(PP) IMPLIES Union(PP) = union(Union(rest(PP)),choose(PP))

  card_equal_partition: LEMMA card(PP) = n AND
                              (FORALL (A: (PP)): card(A) = m) AND
                              (FORALL (A,B: (PP)): A = B OR disjoint?(A,B))
                              IMPLIES
                                  card(Union(PP)) = n*m


  H: VAR set[T]
  card_eq_part: LEMMA (FORALL (A,B: (PP)): card(A) = card(B)) AND
                      (FORALL (A,B: (PP)): A = B OR disjoint?(A,B)) AND
                      PP(H)
                    IMPLIES
                       card(Union(PP)) = card(PP)*card(H)

END lagrange_scaf