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

quality100%

¤ Dauer der Verarbeitung: 0.12 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.