|
%------------------------------------------------------------------------------
% Indexed sets over nat
%
% Author: David Lester, Manchester University
%
% Version 1.0 14/06/09 Initial Version
%
% A new operation (along with the recurrence relations) is introduced:
%
% IUnion(n,A) = A_0 u A_1 u ... u A_n
%
% We also show how to turn an indexed set into an increasing one
% with the same IUnion, or a decreasing one, with the same IIntersection.
%
% Finally, we show that there's a disjoint Union available.
%------------------------------------------------------------------------------
nat_indexed_sets[T: TYPE]: THEORY
BEGIN
IMPORTING structures@fun_preds_partial[nat,set[T],reals.<=,subset?[T]],
indexed_sets_aux[nat,T]
n,i: VAR nat
A,B: VAR sequence[set[T]]
IUnion(n,A):set[T] = Union(image[nat,set[T]](A,{i | i <= n}))
IUnion_0_def: LEMMA IUnion(0,A) = A(0)
IUnion_n_def: LEMMA IUnion(n+1,A) = union(IUnion(n,A),A(n+1))
increasing_indexed?(A):bool = IUnion(A) = fullset[T] AND increasing?(A)
increasing_indexed: TYPE+ = (increasing_indexed?) CONTAINING
(lambda n: fullset[T])
increasing_IUnion: LEMMA
EXISTS B: increasing?(B) AND
B(0) = A(0) AND
(FORALL n: B(n+1) = union(B(n),A(n+1))) AND
IUnion(A) = IUnion(B)
decreasing_IIntersection: LEMMA
EXISTS B: decreasing?(B) AND
B(0) = A(0) AND
(FORALL n: B(n+1) = intersection(B(n),A(n+1))) AND
IIntersection(A) = IIntersection(B)
disjoint_IUnion: LEMMA
EXISTS B: disjoint?(B) AND
(FORALL n: IUnion(n,B) = IUnion(n,A)) AND
B(0) = A(0) AND
(FORALL n: B(n+1) = difference(A(n+1),IUnion(n,A))) AND
IUnion(A) = IUnion(B)
END nat_indexed_sets
¤ Dauer der Verarbeitung: 0.16 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.
|
