Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: extended_nnreal.pvs Sprache: PVS

Original von: PVS^©

%-------------------------------------------------------------------------
% Extended nnreals
%
%     Author: David Lester, Manchester University
%
%     Version 1.0           20/08/07 Initial (DRL)
%-------------------------------------------------------------------------

extended_nnreal: THEORY

BEGIN

  IMPORTING series@series_aux,
            sigma_set@absconv_series_aux,
            reals@sigma[nat],
            analysis@epsilon_lemmas

  limit: MACRO [(convergent?)->real] = convergence_sequences.limit ;

  extended_nnreal: TYPE+ = [bool,nnreal] CONTAINING (TRUE,0)

  i,j,low,high: VAR nat
  x,y,x1,y1,x2,y2: VAR extended_nnreal
  z:   VAR real
  S,T: VAR [nat->extended_nnreal]
  U:   VAR [nat->nnreal]
  X:   VAR set[extended_nnreal]
  epsilon: VAR posreal
  c:   VAR nnreal

  x_inf(X):extended_nnreal
    = IF (FORALL (x:(X)): NOT x`1)
      THEN (FALSE,0)
      ELSE (TRUE,glb({z | EXISTS x: X(x) AND x`1 AND x`2 = z})) ENDIF

  x_sup(X):extended_nnreal
    = IF empty?(X)
      THEN (TRUE,0)
      ELSIF (EXISTS (x:(X)): NOT x`1) OR
            NOT bounded_above?({z | EXISTS x: X(x) AND x`1 AND x`2 = z})
      THEN (FALSE,0)
      ELSE (TRUE,lub({z | EXISTS x: X(x) AND x`1 AND x`2 = z})) ENDIF

  x_inf(S):extended_nnreal = x_inf(image(S,fullset[nat]))
  x_sup(S):extended_nnreal = x_sup(image(S,fullset[nat]))

  x_sigma(low,high,S):extended_nnreal
    = IF (FORALL i: low <= i AND i <= high => S(i)`1)
      THEN (TRUE,sigma(low,high,lambda i: S(i)`2))
      ELSE (FALSE,0) ENDIF

  x_sum(S):extended_nnreal
    = IF (FORALL i: S(i)`1) AND convergent?(series(lambda i: S(i)`2))
      THEN (TRUE,limit(series(lambda i: S(i)`2)))
      ELSE (FALSE,0) ENDIF

  x_sum(U):extended_nnreal
    = IF convergent?(series(U))
      THEN (TRUE,limit(series(U)))
      ELSE (FALSE,0) ENDIF

  x_converges?(S,x):bool
    = IF (FORALL i: S(i)`1) AND convergent?(lambda i: S(i)`2)
      THEN x`1 AND x`2 = limit(lambda i: S(i)`2)
      ELSE NOT x`1 ENDIF

  x_limit(S):extended_nnreal
    = IF (FORALL i: S(i)`1) AND convergent?(lambda i: S(i)`2)
      THEN (TRUE,limit(lambda i: S(i)`2))
      ELSE (FALSE,0) ENDIF

  x_add(x,y):extended_nnreal
    = IF x`1 AND y`1 THEN (TRUE,x`2+y`2) ELSE (FALSE,0) ENDIF

  x_add(x,c):extended_nnreal = IF x`1 THEN (TRUE,x`2+c) ELSE (FALSE,0) ENDIF

  x_eq(x,y):bool = (x`1 = y`1) AND (x`1 => x`2 = y`2)
  x_le(x,y):bool = (x`1 AND y`1 AND x`2 <= y`2) OR (NOT y`1)
  x_lt(x,y):bool = (x`1 AND y`1 AND x`2 <  y`2) OR (NOT y`1)

  x_eq(x,c):bool = x`1 AND x`2 = c

  x_times(x,y):extended_nnreal
    = IF (x`1 AND y`1) OR x_eq(x,0) OR x_eq(y,0) THEN (TRUE,x`2*y`2)
                                                 ELSE (FALSE,0) ENDIF

  x_times(x,c):extended_nnreal = IF x`1 OR c = 0 THEN (TRUE,x`2*c)
                                                 ELSE (FALSE,0) ENDIF
  x_times(c,x):extended_nnreal = x_times(x,c)

  x_add_commutative:   LEMMA commutative?(x_add)
  x_add_associative:   LEMMA associative?(x_add)
  x_times_commutative: LEMMA commutative?(x_times)
  x_times_associative: LEMMA associative?(x_times)
  x_eq_equivalence:    LEMMA equivalence?(x_eq)
  x_le_preorder:       LEMMA preorder?(x_le)
  x_le_antisymmetric:  LEMMA x_le(x,y) AND x_le(y,x) => x_eq(x,y)

  x_sigma_le: LEMMA (FORALL i: low <= i AND i <= high => x_le(S(i),T(i))) =>
                    x_le(x_sigma(low,high,S),x_sigma(low,high,T))

  x_sigma_lt: LEMMA (FORALL i: low <= i AND i <= high => x_lt(S(i),T(i))) AND
                    low <= high =>
                    x_lt(x_sigma(low,high,S),x_sigma(low,high,T))

  x_sum_le: LEMMA (FORALL i: x_le(S(i),T(i))) => x_le(x_sum(S),x_sum(T))
  x_sum_eq: LEMMA (FORALL i: x_eq(S(i),T(i))) => x_eq(x_sum(S),x_sum(T))
  x_sum_lt: LEMMA (FORALL i: x_lt(S(i),T(i))) => x_lt(x_sum(S),x_sum(T))

  x_inf_le: LEMMA (FORALL i: x_le(S(i),T(i))) => x_le(x_inf(S),x_inf(T))

  x_le_add: LEMMA x_le(x1,y1) AND x_le(x2,y2) =>
                  x_le(x_add(x1,x2),x_add(y1,y2))

  x_add_sum: LEMMA x_eq(x_add(x_sum(S),x_sum(T)),
                        x_sum(lambda i: x_add(S(i),T(i))))

  x_limit_to_sum: LEMMA (FORALL i: x_eq(S(i),x_sigma(0,i,T))) =>
                        x_eq(x_limit(S),x_sum(T))

  x_times_sum: LEMMA (FORALL i: x_eq(x_times(x,S(i)),T(i))) =>
                     x_eq(x_times(x,x_sum(S)),x_sum(T))

  epsilon_x_le: LEMMA
    x_le(x,y) <=> (FORALL epsilon: x_le(x,x_add(y,epsilon)))

  IMPORTING double_index[extended_nnreal],
            double_nn_sequence

  U: VAR [[nat,nat]->extended_nnreal]

  double_x_sum: LEMMA x_eq(x_sum(single_index(U)),
                           x_sum(lambda i: x_sum(lambda j: U(i,j))))

  double_x_sum_eq: LEMMA x_eq(x_sum(lambda i: x_sum(lambda j: U(i,j))),
                              x_sum(lambda j: x_sum(lambda i: U(i,j))))

END extended_nnreal

¤ Dauer der Verarbeitung: 0.18 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.