|
%------------------------------------------------------------------------------
% 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
¤ Dauer der Verarbeitung: 0.0 Sekunden
(vorverarbeitet)
¤
|
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.
|
