Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: integer_enumerations.pvs Sprache: PVS

Original von: PVS^©

% every infinite subset of int that is bounded below can be enumerated,
% i.e., there is a strictly monotone surjective function from nat to it.
%
% Author: Alfons Geser ([email protected]), National Institute of Aerospace
% Date: Dec 2004

integer_enumerations[T: TYPE FROM int]: THEORY

BEGIN

  IMPORTING
    infinite_sets_def[T],
    bounded_integers[T]
%    bounded_sets[nat, <=]

  m, n, c: VAR nat
  f: VAR [nat -> T]

  enumerable?(S: set[T]): bool =
    bounded_below?[T](<=)(S) & is_infinite[T](S)

  enumerable_below_bounded: JUDGEMENT
    (enumerable?) SUBTYPE_OF (non_empty_bounded_below?[T])

  enumerable_infinite: JUDGEMENT
    (enumerable?) SUBTYPE_OF (is_infinite[T])

  remove_enumerable: JUDGEMENT
    remove(i: T, S: (enumerable?)) HAS_TYPE (enumerable?)

  S, S1, S2: VAR (enumerable?)

  strictly_monotone?(f): bool = FORALL m, n: m < n => f(m) < f(n)
% same as:
%     preserves(f,
%       restrict[[real, real], [T, T], bool](<),
%       restrict[[real, real], [T, T], bool](<))

  % the enumeration function for S, i.e., the function that enumerates
  % all elements of S in ascending order.
  enum(S)(n): RECURSIVE T =
    IF n = 0 THEN least[T](restrict[[real, real], [T, T], bool](<=))(S)
    ELSE enum(remove(least[T](restrict[[real, real], [T, T], bool](<=))(S), S))(n-1)
    ENDIF
  MEASURE n

  enum_member: JUDGEMENT
    enum(S)(n) HAS_TYPE (S)

%   least_le: LEMMA
%     FORALL (m: (S)):
%       least(restrict[[real, real], [T, T], bool](<=))(S) <= m

  enum_surjective_lem: LEMMA
    FORALL (i: (S)):
      c = i - least(restrict[[real, real], [T, T], bool](<=))(S) =>
        EXISTS n: i = enum(S)(n)

  enum_surjective: LEMMA
    FORALL (i: (S)): EXISTS n: i = enum(S)(n)

  enum_def: THEOREM
    image(enum(S), fullset[nat]) = S

  enum_subset_monotone: LEMMA
    subset?(S1, S2) => enum(S2)(n) <= enum(S1)(n)

  enum_strictly_ascending: LEMMA
    enum(S)(n) < enum(S)(n + 1)

  enum_strictly_monotone: JUDGEMENT
    enum(S) HAS_TYPE (strictly_monotone?)

  enumerable: THEOREM
    EXISTS (f: (strictly_monotone?)): image(f, fullset[nat]) = S

  enum_bijective: LEMMA
    bijective?[nat, (S)](enum(S))

END integer_enumerations

¤ Dauer der Verarbeitung: 0.21 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.