Quelle cauchy.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Cauchy property
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

cauchy  : THEORY

  BEGIN
  IMPORTING prelude_aux,
            appendix

  x: VAR real
  p: VAR nat
  c: VAR [nat->int]

  cauchy_prop(x, c): bool  = (FORALL p: c(p)-1 < x*2^p AND x*2^p < c(p)+1)

  cauchy_real?(c):     bool = EXISTS (x:real):       cauchy_prop(x,c)
  cauchy_nzreal?(c):   bool = EXISTS (x:nzreal):     cauchy_prop(x,c)
  cauchy_nnreal?(c):   bool = EXISTS (x:nnreal):     cauchy_prop(x,c)
  cauchy_npreal?(c):   bool = EXISTS (x:npreal):     cauchy_prop(x,c)
  cauchy_posreal?(c):  bool = EXISTS (x:posreal):    cauchy_prop(x,c)
  cauchy_negreal?(c):  bool = EXISTS (x:negreal):    cauchy_prop(x,c)
  cauchy_smallreal?(c):bool = EXISTS (sx:smallreal): cauchy_prop(sx,c)

  cauchy_real:     NONEMPTY_TYPE = (cauchy_real?)   CONTAINING (LAMBDA p:0)
  cauchy_nzreal:   NONEMPTY_TYPE = (cauchy_nzreal?) CONTAINING (LAMBDA p:2^p)
  cauchy_nnreal:   NONEMPTY_TYPE = (cauchy_nnreal?) CONTAINING (LAMBDA p:2^p)
  cauchy_npreal:   NONEMPTY_TYPE = (cauchy_npreal?) CONTAINING (LAMBDA p:0)
  cauchy_posreal:  NONEMPTY_TYPE = (cauchy_posreal?) CONTAINING (LAMBDA p:2^p)
  cauchy_negreal:  NONEMPTY_TYPE = (cauchy_negreal?) CONTAINING (LAMBDA p:-2^p)
  cauchy_smallreal:
                   NONEMPTY_TYPE = (cauchy_smallreal?) CONTAINING (LAMBDA p:0)

  JUDGEMENT cauchy_nzreal    SUBTYPE_OF cauchy_real
  JUDGEMENT cauchy_nnreal    SUBTYPE_OF cauchy_real
  JUDGEMENT cauchy_npreal    SUBTYPE_OF cauchy_real
  JUDGEMENT cauchy_posreal   SUBTYPE_OF cauchy_nnreal
  JUDGEMENT cauchy_posreal   SUBTYPE_OF cauchy_nzreal
  JUDGEMENT cauchy_negreal   SUBTYPE_OF cauchy_nzreal
  JUDGEMENT cauchy_negreal   SUBTYPE_OF cauchy_npreal
  JUDGEMENT cauchy_smallreal SUBTYPE_OF cauchy_real

  cx: VAR cauchy_real

  cauchy_zero:cauchy_nnreal = (LAMBDA p:0)

  unique_cauchy_zero:  LEMMA cauchy_prop(x,cauchy_zero) <=> x = 0
  unique_cauchy_zero2: LEMMA cauchy_prop(0,cx) <=>
                             (FORALL p: cx(p) = cauchy_zero(p))
  unique_cauchy_zero3: LEMMA cauchy_prop(0,cx) <=> cx = cauchy_zero

END cauchy

quality98%

¤ Dauer der Verarbeitung: 0.1 Sekunden (vorverarbeitet) ¤

Versionsinformation zu Columbo

Bemerkung:

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

Anfrage:

Dauer der Verarbeitung:

Sekunden

sprechenden Kalenders