Quellcode-Bibliothek sqrtx.pvs

%------------------------------------------------------------------------------
% 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