Quelle integer_enumerations.pvs Sprache: 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 (geser@nianet.org), 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

quality76%

¤ Dauer der Verarbeitung: 0.14 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.