Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: partitions_scaf.pvs Sprache: PVS

Original von: PVS^©

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.1 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.