Quelle  countable_set.pvs   Sprache: PVS

%-------------------------------------------------------------------------
%
%  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 (jamesj@acm.org), 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