Quelle partitions_scaf.pvs Sprache: 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

quality82%

¤ Dauer der Verarbeitung: 0.12 Sekunden (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.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.