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

quality68%

¤ 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.