| products/Sources/formale Sprachen/PVS/sets_aux/ (Beweissystem der NASA Version 6.0.9©) Datei vom 28.9.2014 mit Größe 3 kB |
|
Quelle countability.pvs Sprache: PVS |
|||||||||
|
%-------------------------------------------------------------------------
% % Countable sets, and a recharacterization of infinite sets based on % the definition of countability. % % For PVS version 3.2. March 1, 2005 % --------------------------------------------------------------------- % Author: Jerry James (jamesj@acm.org), University of Kansas % % EXPORTS % ------- % prelude: infinite_sets_def[T] % sets_aux: card_comp_set[nat,T], card_comp_set[T,nat], % card_comp_set_props[T,nat], countability[T] % %------------------------------------------------------------------------- countability[T: TYPE]: THEORY BEGIN IMPORTING infinite_sets_def[T] IMPORTING orders@integer_enumerations[nat] % Proofs only S: VAR set[T] % ========================================================================== % Basic definitions % ========================================================================== is_countable(S): bool = EXISTS (f: (injective?[(S), nat])): TRUE is_countably_infinite(S): bool = EXISTS (f: (bijective?[(S), nat])): TRUE is_uncountable(S): MACRO bool = NOT is_countable(S) countable_set: TYPE+ = (is_countable) CONTAINING emptyset[T] countably_infinite_set: TYPE = (is_countably_infinite) uncountable_set: TYPE = (is_uncountable) countably_infinite_countable: JUDGEMENT countably_infinite_set SUBTYPE_OF countable_set % ========================================================================== % Infinite subsets of a countably infinite set are countably infinite % ========================================================================== countably_infinite_subset: THEOREM FORALL (CountInf: countably_infinite_set), (Inf: infinite_set[T]): subset?(Inf, CountInf) IMPLIES is_countably_infinite(Inf) countable_subset: THEOREM FORALL S, (Count: countable_set): subset?(S, Count) IMPLIES is_countable(S) % ========================================================================== % Countability of the base type % ========================================================================== is_countable_type: bool = EXISTS (f: (injective?[T, nat])): TRUE is_countably_infinite_type: bool = EXISTS (f: (bijective?[T, nat])): TRUE is_uncountable_type: MACRO bool = NOT is_countable_type countable_type_is_countably_infinite: LEMMA is_countably_infinite_type IMPLIES is_countable_type countable_full: LEMMA is_countable_type IFF is_countable(fullset[T]) countably_infinite_full: LEMMA is_countably_infinite_type IFF is_countably_infinite(fullset[T]) uncountable_full: COROLLARY is_uncountable_type IFF is_uncountable(fullset[T]) countable_type_set: LEMMA is_countable_type IMPLIES (FORALL S: is_countable(S)) countably_infinite_type_set: LEMMA is_countably_infinite_type IMPLIES (FORALL S: is_countable(S)) uncountably_infinite_type_set: LEMMA (EXISTS S: is_uncountable(S)) IMPLIES is_uncountable_type countable_complement: LEMMA is_countable_type IMPLIES (FORALL S: is_countable(complement(S))) countably_infinite_complement: LEMMA is_countably_infinite_type IMPLIES (FORALL S: is_countable(complement(S))) END countability ¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤*© Formatika GbR, Deutschland |
|
2026-03-28