|
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
¤ Dauer der Verarbeitung: 0.15 Sekunden
(vorverarbeitet)
¤
|
Haftungshinweis
Die Informationen auf dieser Webseite wurden
nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit,
noch Qualität der bereit gestellten Informationen zugesichert.
Bemerkung:
Die farbliche Syntaxdarstellung ist noch experimentell.
|
