% 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
¤ Diese beiden folgenden Angebotsgruppen bietet das Unternehmen0.1Angebot
Wie Sie bei der Firma Beratungs- und Dienstleistungen beauftragen können
¤
|
Lebenszyklus
Die hierunter aufgelisteten Ziele sind für diese Firma wichtig
Ziele
Entwicklung einer Software für die statische Quellcodeanalyse
|
