|
partitions_scaf[T: TYPE+ FROM real]: THEORY
BEGIN
ASSUMING
IMPORTING deriv_domain_def[T]
connected_domain : ASSUMPTION connected?[T]
not_one_element : ASSUMPTION not_one_element?[T]
ENDASSUMING
% <=(x,y:T): bool = x <= y %% hide ugly restrictions
% AUTO_REWRITE+ <=
IMPORTING integral_def,
structures@sort_seq_lems[T,<=],
finite_sets@finite_sets_minmax[T,<=],
ints@max_below
a,b,c,d,x,y,z: VAR T
f,f1,f2,g: VAR [T -> real]
eps, delta: VAR posreal
xv,yv: VAR real
#(t:T): finite_sequence[T] = (# length := 1,
seq := (LAMBDA (x: below[1]): t) #)
gen_seq_lem: LEMMA #(x)(0) = x;
part2set_prep: LEMMA FORALL (a:T, b: {x:T|a<x}, P: partition[T](a, b)):
is_finite[T]({s: T | EXISTS (kk: below(length(P))): seq(P)(kk) = s})
part2set(a:T,b:{x:T|a<x}, P: partition[T](a,b)): finite_set[T]
= {s: T | (EXISTS (kk: below(length(P))): seq(P)(kk) = s)}
part2set_lem: LEMMA FORALL (a:T, b: {x:T|a<x}, P: partition[T](a, b)):
part2set(a,b,P)(a) AND part2set(a,b,P)(b) AND
(FORALL (ii: below(length(P))): part2set(a,b,P)(P(ii)))
AND (FORALL (x: (part2set(a,b,P))): a <= x AND x <= b)
card_part2set: LEMMA FORALL (a:T, b: {x:T|a<x}, P: partition[T](a, b)):
card[T](part2set(a,b,P)) > 1
minmax_part2set: LEMMA FORALL (a:T, b: {x:T|a<x}, P: partition[T](a, b)):
min[T,<=](part2set(a,b,P)) = a AND
max[T,<=](part2set(a,b,P)) = b
JUDGEMENT part2set(a:T,b:{x:T|a<x},P: partition[T](a,b))
HAS_TYPE {s: finite_set[T] | card(s) > 1}
set2seq(S: finite_set[T]): RECURSIVE finite_sequence[T] =
IF empty?[T](S) THEN empty_seq
ELSE #(choose[T](S)) o set2seq(rest[T](S))
ENDIF
MEASURE card[T](S)
S: VAR finite_set[T]
set2seq_length: LEMMA length(set2seq(S)) = card(S)
set2seq_lem: LEMMA LET SP = set2seq(S) IN
FORALL (ii: below(length(SP))): S(SP`seq(ii))
set2seq_exists: LEMMA LET SP = set2seq(S) IN
S(x) IMPLIES
EXISTS (ii: below(length(SP))): SP`seq(ii) = x
AUTO_REWRITE+ set2seq_length
minmax_set2seq: LEMMA card(S) > 0 IMPLIES
min(set2seq(S)) = min[T,<=](S) AND
max(set2seq(S)) = max[T,<=](S)
set2seq_neq : LEMMA LET SP = set2seq(S) IN
FORALL (ii,jj: below(length(sort(SP)))):
ii /= jj IMPLIES SP`seq(ii) /= SP`seq(jj)
sort_set2seq_lem: LEMMA LET SP = set2seq(S) IN
FORALL (ii: below(length(sort(SP)))): S(sort(SP)`seq(ii))
set2part_prep: LEMMA FORALL (S: {s: finite_set[T] | card[T](s) > 1}):
min[T,<=](S) < max[T,<=](S)
sort_set2seq_neq : LEMMA LET SP = sort(set2seq(S)) IN
FORALL (ii,jj: below(length(sort(SP)))):
ii /= jj IMPLIES SP`seq(ii) /= SP`seq(jj)
set2part(S: {s: finite_set[T] | card[T](s) > 1}):
partition[T](min[T,<=](S),max[T,<=](S)) = sort(set2seq(S))
set2part_length: LEMMA card(S) > 1 IMPLIES
length(set2part(S)) = card(S)
AUTO_REWRITE+ set2part_length
set2part_lem: LEMMA FORALL (ii: below(length(set2part(S)))):
card(S) > 1 IMPLIES S(set2part(S)`seq(ii))
set2part_ix: LEMMA S(x) and card(S) > 1 IMPLIES
EXISTS (ii: below(length(set2part(S)))):
x = set2part(S)`seq(ii)
insert(a:T,b:{x:T|a<x},P: partition[T](a,b),
xx: open_interval[T](a,b)): partition[T](a,b) =
set2part(add(xx,part2set(a,b,P)))
END partitions_scaf
¤ Dauer der Verarbeitung: 0.21 Sekunden
(vorverarbeitet)
¤
|
schauen Sie vor die Tür
Fenster
Die Firma ist wie angegeben erreichbar.
Die farbliche Syntaxdarstellung ist noch experimentell.
|
