%-------------------------------------------------------------------------
%
% Countable sets of numbers. The countability properties are shown by
% providing bijections between the sets and the natural numbers.
%
% For PVS version 3.2. February 10, 2005
% ---------------------------------------------------------------------
% Author: Jerry James ([email protected]), University of Kansas
%
% EXPORTS
% -------
% prelude: finite_sets[int], finite_sets[nat],
% function_image_aux[int, nat], function_image_aux[nat, int]
% sets_aux: countable_set
%
%-------------------------------------------------------------------------
countable_set: THEORY
BEGIN
IMPORTING function_image_aux[int, nat], function_image_aux[nat, int], bits
IMPORTING orders@set_antisymmetric[[nat, nat], nat]
IMPORTING orders@set_antisymmetric[[int, int], nat]
IMPORTING orders@set_antisymmetric[rat, nat]
% ==========================================================================
% Integers
% ==========================================================================
int_to_nat(i: int): nat = IF i < 0 THEN -2 * i - 1 ELSE 2 * i ENDIF
nat_to_int(n: nat): int = IF even?(n) THEN n / 2 ELSE (n + 1) / -2 ENDIF
int_to_nat_bijective: JUDGEMENT int_to_nat HAS_TYPE (bijective?[int, nat])
nat_to_int_bijective: JUDGEMENT nat_to_int HAS_TYPE (bijective?[nat, int])
% ==========================================================================
% Finite sets of natural numbers
% ==========================================================================
% Use the bit_encoding function
countable_family_nat: THEOREM
EXISTS (f: [finite_set[nat] -> nat]): bijective?(f)
% ==========================================================================
% Finite sets of integers
% ==========================================================================
intset_to_natset(S: finite_set[int]): finite_set[nat] =
image(int_to_nat, S)
intset_to_natset_bijective: JUDGEMENT
intset_to_natset HAS_TYPE (bijective?[finite_set[int], finite_set[nat]])
countable_family_int: THEOREM
EXISTS (f: [finite_set[int] -> nat]): bijective?(f)
% ==========================================================================
% 2-tuples of natural numbers and integers
% ==========================================================================
tuple_to_natset(n: [nat, nat]): finite_set[nat] =
{i: nat | i = n`1 * 2 OR i = n`2 * 2 + 1}
countable_nat_tuple: THEOREM
EXISTS (f: [[nat, nat] -> nat]): bijective?(f)
tuple_to_intset(n: [int, int]): finite_set[int] =
{i: int | i = n`1 * 2 OR i = n`2 * 2 + 1}
countable_int_tuple: THEOREM
EXISTS (f: [[int, int] -> nat]): bijective?(f)
% ==========================================================================
% Rational numbers
% ==========================================================================
countable_rat: THEOREM EXISTS (f: [rat -> nat]): bijective?(f)
END countable_set
¤ Dauer der Verarbeitung: 0.1 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.
|
