|
%------------------------------------------------------------------------------
% sqrt
%
% Author: David Lester, Manchester University
%
% Version 1.0 18/2/09 Initial Release Version
%------------------------------------------------------------------------------
sqrtx: THEORY
BEGIN
IMPORTING prelude_aux, appendix, cauchy, unique, reals@sqrt,
bisection_nat_sqrt
cx: VAR cauchy_real
x: VAR real
p,n,r: VAR nat
nncx: VAR cauchy_nnreal
nnx,nny: VAR nnreal
nnsqrt(x):nnreal = IF 0 <= x THEN sqrt(x) ELSE 0 ENDIF
sqrt_p1: LEMMA 0 < n AND r = floor(sqrt(n))
=> (r-1)^2 <= n-1 AND n+1 <= (r+1)^2
sqrt_p2: LEMMA 0 < n AND r = floor(sqrt(n)) AND
n-1 < nnx * 2 ^ (2 * p) AND nnx * 2 ^ (2 * p) < n+1
=> (r-1)^2 < nnx*2 ^ (2 * p) AND nnx*2 ^ (2 * p) < (r+1)^2
sqrt_p3: LEMMA 0 <= nncx(p)
cauchy_nnsqrt(nncx): cauchy_nnreal = (LAMBDA p: bisection_sqrt(nncx(2*p)))
sqrt_nn_lemma: LEMMA cauchy_prop(nnx,nncx)
=> cauchy_prop(sqrt(nnx), cauchy_nnsqrt(nncx))
cauchy_sqrt(nncx):cauchy_nnreal = cauchy_nnsqrt(nncx)
sqrt_lemma: LEMMA cauchy_prop(nnx,nncx) =>
cauchy_prop(sqrt(nnx),cauchy_sqrt(nncx))
END sqrtx
¤ 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.
|
