| Quellcodebibliothek Statistik Leitseite products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 4 kB |
|
Quelle countable_props.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Properties of countable (and uncountable) sets. % % For PVS version 3.2. February 9, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), 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.1 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28