Ziele Untersuchung
mit Columbo Integrität von
Datenbanken Interaktion und
Portierbarkeit Ergonomie der
Schnittstellen

Angebot Produkte Projekt Beratung

Mittel Analytik Modellierung Sprachen Algebra Logik Hardware Denken Kreativität

Zusammenhänge Gesellschaft Wirtschaft Branche Firma


products/Sources/formale Sprachen/PVS/orders/ (Beweissystem der NASA Version 6.0.9^©) Datei vom 28.9.2014 mit Größe 2 kB

Quellcode-Bibliothek 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%

¤ 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.0.12Bemerkung: (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.