|
%------------------------------------------------------------------------------
% Various odds & ends for prelude libraries
%
% Author: David Lester, Manchester University, NIA, Université Perpignan
%
% Version 1.0 9/06/06 Initial Version
%------------------------------------------------------------------------------
prelude_sets_aux[T:TYPE]: THEORY
BEGIN
finite_setofsets_is_setofsets:
JUDGEMENT finite_set[set[T]] SUBTYPE_OF setofsets[T]
x: VAR T
A: VAR setofsets[T]
a,b: VAR set[T]
F: VAR finite_set[set[T]]
P: VAR [set[T]->bool]
complement_difference: LEMMA
complement(difference(a,b)) = union(complement(a),b)
Intersection_member:
LEMMA member(x,Intersection(A)) IFF (FORALL (a:(A)): member(x,a))
Intersection_split: LEMMA nonempty?(A) =>
(Intersection(A) = intersection(choose(A),Intersection(rest(A))))
Intersection_finite: LEMMA
P(fullset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND
(FORALL (a,b:set[T]): P(a) AND P(b) => P(intersection(a,b)))
=> P(Intersection(A))
Union_member: LEMMA member(x,Union(A)) IFF (EXISTS (a:(A)): member(x,a))
Union_split: LEMMA nonempty?(A) =>
(Union(A) = union(choose(A),Union(rest(A))))
Union_finite: LEMMA
P(emptyset[T]) AND is_finite(A) AND (FORALL (a:(A)): P(a)) AND
(FORALL (a,b:set[T]): P(a) AND P(b) => P(union(a,b))) => P(Union(A))
finite_Complement: LEMMA is_finite(Complement(F))
END prelude_sets_aux
¤ Dauer der Verarbeitung: 0.16 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
