|
ordered_finite_sequences[T: TYPE+, <=:(total_order?[T])]: THEORY
BEGIN
IMPORTING structures@sort_seq_lems[T, <=], relations_extra[T], finite_seqs[T]
s, s1, s2: VAR ne_seqs
consensus_function: TYPE = [s: ne_seqs -> {t: T | min(s) <= t AND t <= max(s)}]
cf: VAR consensus_function
k: VAR posnat
i,j,l: VAR nat
extract_one: LEMMA
i<=j AND i<s`length AND j<s`length AND l<=j-i
IMPLIES (s^(i,j))`seq(l) = s`seq(i+l)
extract_upper: LEMMA
i<=j AND i<s`length AND j<s`length
IMPLIES (s^(i,j))`seq(length(s^(i,j))-1) = s`seq(j)
min_extract: LEMMA
i<=j AND i<s`length IMPLIES min(sort(s)^(i,j)) = sort(s)`seq(i)
max_extract: LEMMA
i<=j AND i<s`length AND j<s`length
IMPLIES max(sort(s)^(i,j)) = sort(s)`seq(j)
minmax(s): ne_seqs = (: min(s), max(s) :) % uses conversion list2finseq
min_le_max: LEMMA min(s) <= max(s)
min_minmax: LEMMA min(minmax(s)) = min(s)
max_minmax: LEMMA max(minmax(s)) = max(s)
min_in_consensus: JUDGEMENT min HAS_TYPE in_consensus_function
max_in_consensus: JUDGEMENT max HAS_TYPE in_consensus_function
in_consensus: JUDGEMENT in_consensus_function SUBTYPE_OF consensus_function
min_consensus: JUDGEMENT min HAS_TYPE consensus_function
max_consensus: JUDGEMENT max HAS_TYPE consensus_function
choose_consensus: JUDGEMENT choose(i) HAS_TYPE consensus_function
IMPORTING pigeonhole,
finite_sets@finite_sets_below,
finite_sets@finite_sets_card_eq
% Set of indexes from the unsorted seq whose value is equal or
% lower than the value of given index in the sorted sequence
lower(s, k, (i: below(k))): finite_set[below(k)] =
{j: below(k) | s`length = k AND s`seq(j) <= sort(s)`seq(i)}
upper(s, k, (i: below(k))): finite_set[below(k)] =
{j: below(k) | s`length = k AND sort(s)`seq(i) <= s`seq(j)}
% Map a set of indexes from the sorted sequence into a set of indexes
% in the unsorted seq
map_set(s, k, (a: finite_set[below(k)])): finite_set[below(k)] =
{i: below(k) | s`length = k AND a(sort_map(s)(i))}
map_subset_lower: LEMMA
i<k AND s`length = k
IMPLIES
subset?(map_set(s, k, {m:below(k) | m <= i}), lower(s, k, i))
map_subset_upper: LEMMA
i<k AND s`length = k
IMPLIES
subset?(map_set(s, k, {m:below(k) | i <= m}), upper(s, k, i))
% a bijective mapping function for a subset of below(k)
mapper(s, k, (a: finite_set[below(k)]))(i:(map_set(s,k,a))): (a) = sort_map(s)(i)
map_card_eq: LEMMA
FORALL (a:finite_set[below(k)]):
s`length = k
IMPLIES
card(map_set(s, k, a)) = card(a)
card_below_set: LEMMA i < k IMPLIES i+1 <= card({m:below(k) | m <= i})
card_above_set: LEMMA i < k IMPLIES k-i <= card({m:below(k) | i <= m})
card_lower: LEMMA i < k AND s`length = k IMPLIES i + 1 <= card[below(k)](lower(s, k, i))
card_upper: LEMMA i < k AND s`length = k IMPLIES k - i <= card[below(k)](upper(s, k, i))
sort_overlap: LEMMA
s1`length = k AND
s2`length = k
IMPLIES
FORALL (i: below(k)):
EXISTS (j: below(k)):
s2`seq(j) <= sort(s2)`seq(i) AND
sort(s1)`seq(i) <= s1`seq(j)
leq_validity: COROLLARY
s`length = k
IMPLIES
FORALL (i: below(k)):
EXISTS (j: below(k)):
s`seq(j) <= sort(s)`seq(i)
END ordered_finite_sequences
¤ Dauer der Verarbeitung: 0.9 Sekunden
(vorverarbeitet)
¤
|
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.
|
