%-------------------------------------------------------------------------
%
% Properties of countable (and uncountable) sets.
%
% For PVS version 3.2. February 9, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
% David Lester, Manchester University
%
% 1.1: Modified for PVS 4.2 (EXPORTs removed, IMPORTS restricted)
%-------------------------------------------------------------------------
countable_props[T: TYPE]: THEORY
BEGIN
IMPORTING countability[T], finite_sets[T]
% These imports are just for the proofs
IMPORTING infinite_nat_def[T]
t: VAR T
S, R, Q: VAR set[T]
Fin: VAR finite_set[T]
Inf: VAR infinite_set[T]
A,Count, Count1, Count2: VAR countable_set[T]
CountInf, CountInf1, CountInf2: VAR countably_infinite_set[T]
Uncount: VAR uncountable_set[T]
% Countably infinite sets are infinite
infinite_countably_infinite: JUDGEMENT
countably_infinite_set[T] SUBTYPE_OF infinite_set[T]
countably_infinite_is_nonempty: JUDGEMENT
countably_infinite_set SUBTYPE_OF (nonempty?[T])
%%% Set operations on countable sets
countably_infinite_add: JUDGEMENT
add(t, CountInf) HAS_TYPE countably_infinite_set[T]
countable_add: JUDGEMENT add(t, Count) HAS_TYPE countable_set[T]
countably_infinite_remove: JUDGEMENT
remove(t, CountInf) HAS_TYPE countably_infinite_set[T]
countable_remove: JUDGEMENT remove(t, Count) HAS_TYPE countable_set[T]
countably_infinite_rest: JUDGEMENT
rest(CountInf) HAS_TYPE countably_infinite_set[T]
countable_rest: JUDGEMENT rest(Count) HAS_TYPE countable_set[T]
countable_intersection1: JUDGEMENT
intersection(Count, S) HAS_TYPE countable_set[T]
countable_intersection2: JUDGEMENT
intersection(S, Count) HAS_TYPE countable_set[T]
countably_infinite_difference: JUDGEMENT
difference(CountInf, Fin) HAS_TYPE countably_infinite_set[T]
countable_difference: JUDGEMENT
difference(Count, S) HAS_TYPE countable_set[T]
finite_countable: JUDGEMENT finite_set[T] SUBTYPE_OF countable_set[T]
%%% Uncountable sets
% Uncountable sets are infinite
infinite_uncountable: JUDGEMENT
uncountable_set[T] SUBTYPE_OF infinite_set[T]
% Every infinite set has a countably infinite subset
countably_infinite_subset_exists: THEOREM
FORALL Inf: EXISTS CountInf: subset?(CountInf, Inf)
% Every infinite set has a countably infinite proper subset
countably_infinite_strict_subset_exists: THEOREM
FORALL Inf: EXISTS CountInf: strict_subset?(CountInf, Inf)
%%% Countable sets
% Countable sets are finite or countably infinite
countable_card: COROLLARY
is_countable(S) IFF is_finite(S) OR is_countably_infinite(S)
countably_infinite_union1: JUDGEMENT
union(CountInf, Count) HAS_TYPE countably_infinite_set[T]
countably_infinite_union2: JUDGEMENT
union(Count, CountInf) HAS_TYPE countably_infinite_set[T]
countable_union: JUDGEMENT union(Count1, Count2) HAS_TYPE countable_set[T]
countably_infinite_def: LEMMA
is_countably_infinite(S) IFF is_countable(S) AND is_infinite(S)
countable_emptyset: LEMMA is_countable(emptyset[T])
countable_singleton: LEMMA is_countable(singleton(t))
% --------------- The following added back by Rick Butler ---------------
IMPORTING card_comp_set_props[T, T], card_comp_set_props[T, nat]
%%% Uncountable sets
% Uncountable sets are infinite
infinite_uncountable: JUDGEMENT
uncountable_set[T] SUBTYPE_OF infinite_set[T]
%%% cardinality properties of finite/countable/uncountable sets
card_le_finite: THEOREM
FORALL S, Fin: card_le(S, Fin) IMPLIES is_finite(S)
card_ge_infinite: THEOREM
FORALL S, Inf: card_ge(S, Inf) IMPLIES is_infinite(S)
card_eq_countably_infinite: THEOREM
FORALL S, CountInf:
card_eq(S, CountInf) IMPLIES is_countably_infinite(S)
card_le_countable: COROLLARY
FORALL S, Count: card_le(S, Count) IMPLIES is_countable(S)
card_ge_uncountable: COROLLARY
FORALL S, Uncount: card_ge(S, Uncount) IMPLIES is_uncountable(S)
%%% Adding and removing countable pieces from infinite sets
countably_infinite_subset_union: LEMMA
FORALL Q, R, S:
subset?(Q, S) AND
disjoint?(S, R) AND
is_countably_infinite(R) AND is_countably_infinite(Q)
IMPLIES card_eq(S, union(S, R))
countable_finite_subset_union: LEMMA
FORALL Q, R, S:
subset?(Q, S) AND
disjoint?(S, R) AND is_finite(R) AND is_countably_infinite(Q)
IMPLIES card_eq(S, union(S, R))
infinite_countable_union: THEOREM
FORALL Inf, Count: card_eq(Inf, union(Inf, Count))
infinite_countable_difference: THEOREM
FORALL S, Count:
is_finite(difference(S, Count)) OR card_eq(S, difference(S, Count))
END countable_props
¤ Dauer der Verarbeitung: 0.13 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.
|
