Rick,

In collaboration with Jacques and Alfons, we have finished a theory
sqrt_approx that contains definitions of sqrt_newton and sqrt_bisect
(newton and bisection methods for computing square roots). They come
with their respective boundary properties, i.e.,

  sqrt_newton_gt : LEMMA 
    sqrt_newton(a,n) > sqrt(a)

  sqrt_bisect_boundaries : LEMMA
    sqrt_bisect_lb(a,n) <= sqrt(a) AND
    sqrt(a) <= sqrt_bisect_ub(a,n) 

We have also included a general theory of the bisection method
(Bolzano's theory) that can instantiated accordingly to compute other
roots.

I include the dump file in case you want to add it to our reals library.
However, notice that in the proofs I have used FIELD, CANCEL-BY, and
some of the Ben's strategies. 

Aside from that, you may also add comments "%% Proved in Isabelle-HOL by
Jacques Fleuriot" to the following axioms in the trig library.

  sin_bound : AXIOM 0 <= a AND a <= PI IMPLIES
                       sin_approx(a,2*n) <= sin(a) AND
                       sin(a) <= sin_approx(a,2*n+1)  

  cos_bound : AXIOM -PI/2 <= a AND a <= PI/2 IMPLIES
                       cos_approx(a,2*n+1) <= cos(a) AND
                       cos(a) <= cos_approx(a,2*(n+1))  
 
--
Cesar A. Munoz H.       | munoz@icase.edu, C.A.Munoz@larc.nasa.gov
Staff Scientist         | http://www.icase.edu/~munoz
ICASE - NASA Langley    | Phone +1 757 864-8018  Fax +1 757 864-6134
Mail Stop 132C,  3 West Reid Street, NASA LaRC, Hampton, VA 23681-2199,
USA.%Patch files loaded: patch2 version 1.2.2.36

$$$pvs-strategies
(load "~munoz/manip-package/manip-strategies")
(load "~munoz/Xtrategies/Field/extra-tegies")
(load "~munoz/Xtrategies/Field/field-strategies")
(load "~munoz/manip-package/collect-rule-sigs")

$$$sqrt_approx.pvs
sqrt_approx : THEORY
%-----------------------------------------------------------------------------
%  Includes sqrt_newton, sqrt_bisect, sqrt_lb, sqrt_up
%
%  Cesar   Munoz    (munoz@icase.edu)
%
%  In collaboration with
%    Jacques Fleuriot (j.d.f@icase.edu)
%    Alfons  Geser    (geser@icase.edu)
%
%  ICASE - NASA Langley 
%  July 2001
%-----------------------------------------------------------------------------
BEGIN

  IMPORTING reals@sqrt,bolzano

  n  : VAR nat
  a  : VAR nonneg_real
  ab : VAR Boundaries

  sqrt_newton(a,n) : RECURSIVE posreal =
    IF n = 0 THEN a+1
    ELSE (1/2) * (sqrt_newton(a,n-1) + (a / sqrt_newton(a,n-1)))
    ENDIF
    MEASURE (n+1)

  sq_sqrt_newton : LEMMA
    sq(sqrt_newton(a,n)) > a

  sqrt_newton_gt : LEMMA 
    sqrt_newton(a,n) > sqrt(a)

  sqrt_newton_decreasing : LEMMA
    sqrt_newton(a,n+1) < sqrt_newton(a,n)

  sqrt_bisect(a,ab,n) : Boundaries =
    bolzano_bisect(LAMBDA(ab):sq(ab`2) < a,ab,n)

  sqrt_bisect_lem : LEMMA
    ab`1 >= 0 AND ab`1 <= sqrt(a) AND sqrt(a) <= ab`2 =>
    sqrt_bisect(a,ab,n)`1 <= sqrt(a) AND
    sqrt(a) <= sqrt_bisect(a,ab,n)`2

  sqrt_bisect_lb(a,n) : nonneg_real =
    sqrt_bisect(a,(0,max(1,a)),n)`1

  sqrt_bisect_ub(a,n) : nonneg_real =
    sqrt_bisect(a,(0,max(1,a)),n)`2

  sqrt_bisect_boundaries : LEMMA
    sqrt_bisect_lb(a,n) <= sqrt(a) AND
    sqrt(a) <= sqrt_bisect_ub(a,n) 

  sqrt_lb(a) : nonneg_real = sqrt_bisect_lb(a,10)

  sqrt_ub(a) : nonneg_real = sqrt_bisect_ub(a,10)

  SQRT : LEMMA
    sqrt_lb(a) <= sqrt(a) AND
    sqrt(a) <= sqrt_ub(a)

END sqrt_approx

$$$sqrt_approx.prf
(|sqrt_approx| (|sqrt_newton_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|sqrt_newton_TCC2| "" (TERMINATION-TCC) NIL NIL)
 (|sq_sqrt_newton| "" (SKOLEM 1 ("a" _))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (EXPAND "sqrt_newton" 1)
          (("2" (SQ-SIMP)
            (("2" (EXPAND "sq")
              (("2" (FIELD 1)
                (("2" (CANCEL-BY 1 "2*sqrt_newton(a, J)")
                  (("2" (NAME-REPLACE "SQRT" "sqrt_newton(a,J)")
                    (("2" (BOTH-SIDES "-" "4 * (SQRT * SQRT * a)")
                      (("2" (GROUND)
                        (("2" (LEMMA "sq_minus")
                          (("2" (INST -1 "SQRT * SQRT" "a")
                            (("2" (CASE "sq(SQRT * SQRT - a) > 0")
                              (("1" (GRIND) NIL NIL)
                               ("2"
                                (HIDE -1 3)
                                (("2"
                                  (LEMMA "sq_gt")
                                  (("2"
                                    (INST -1 "SQRT*SQRT - a" "0")
                                    (("2"
                                      (REWRITE "sq_0")
                                      (("2" (GROUND) NIL NIL))
                                      NIL))
                                    NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_newton_gt| "" (SKOSIMP)
  (("" (LEMMA "sq_sqrt_newton")
    (("" (INST?)
      (("" (LEMMA "sqrt_gt")
        (("" (INST -1 "sq(sqrt_newton(a!1, n!1))" "a!1")
          (("" (REWRITE "sqrt_sq") (("" (GROUND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_newton_decreasing| "" (SKOLEM 1 ("a" "n"))
  (("" (EXPAND "sqrt_newton" 1 1)
    (("" (FIELD 1)
      (("" (LEMMA "sq_sqrt_newton")
        (("" (INST?) (("" (EXPAND "sq") (("" (GROUND) NIL NIL)) NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_bisect_lem| "" (SKOLEM 1 ("a" _ _))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (SKOLEM 1 "ab")
          (("2" (EXPAND "sqrt_bisect")
            (("2" (EXPAND "bolzano_bisect" 1)
              (("2" (FLATTEN)
                (("2" (SPLIT)
                  (("1" (LIFT-IF)
                    (("1" (GROUND)
                      (("1" (INST -2 "((ab`1 + ab`2) / 2,ab`2)")
                        (("1" (GROUND)
                          (("1" (LEMMA "sq_le")
                            (("1" (INST?)
                              (("1"
                                (REWRITE "sq_sqrt")
                                (("1" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (INST -1 "(ab`1,(ab`1+ab`2)/2)")
                        (("2" (GROUND)
                          (("2" (HIDE 3)
                            (("2" (LEMMA "sqrt_lt")
                              (("2"
                                (INST?)
                                (("2"
                                  (REWRITE "sqrt_sq")
                                  (("2" (GROUND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (LIFT-IF)
                    (("2" (GROUND)
                      (("1" (INST -2 "((ab`1 + ab`2) / 2,ab`2)")
                        (("1" (GROUND)
                          (("1" (LEMMA "sq_le")
                            (("1" (INST?)
                              (("1"
                                (REWRITE "sq_sqrt")
                                (("1" (GROUND) NIL NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("2" (INST -1 "(ab`1,(ab`1+ab`2)/2)")
                        (("2" (GROUND)
                          (("2" (HIDE 3)
                            (("2" (LEMMA "sqrt_lt")
                              (("2"
                                (INST?)
                                (("2"
                                  (REWRITE "sqrt_sq")
                                  (("2" (GROUND) NIL NIL))
                                  NIL))
                                NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_bisect_lb_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|sqrt_bisect_lb_TCC2| "" (SKOLEM 1 ("a" "n"))
  (("" (LEMMA "bolzano_bisect_min")
    (("" (EXPAND "sqrt_bisect")
      (("" (INST?) (("1" (GRIND) NIL NIL) ("2" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_bisect_ub_TCC1| "" (SKOLEM 1 ("a" "n"))
  (("" (EXPAND "sqrt_bisect")
    ((""
      (CASE "bolzano_bisect(LAMBDA (ab): sq(ab`2) < a, (0, max(1, a)),n)`1 >= 0")
      (("1" (GROUND) NIL NIL)
       ("2" (HIDE 2)
        (("2" (LEMMA "bolzano_bisect_min")
          (("2" (INST?)
            (("1" (GROUND) NIL NIL)
             ("2" (HIDE 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL))
          NIL))
        NIL)
       ("3" (HIDE 2) (("3" (GRIND) NIL NIL)) NIL))
      NIL))
    NIL))
  NIL)
 (|sqrt_bisect_boundaries| "" (SKOLEM 1 ("a" "n"))
  (("" (EXPAND "sqrt_bisect_lb")
    (("" (EXPAND "sqrt_bisect_ub")
      (("" (LEMMA "sqrt_bisect_lem")
        (("" (CASE "sqrt(a) <= max(1,a)")
          (("1" (INST?)
            (("1" (GROUND) NIL NIL)
             ("2" (HIDE -1 2) (("2" (GRIND) NIL NIL)) NIL))
            NIL)
           ("2" (HIDE -1 2)
            (("2" (EXPAND "max")
              (("2" (LIFT-IF)
                (("2" (GROUND)
                  (("1" (LEMMA "sq_le")
                    (("1" (INST?)
                      (("1" (REWRITE "sq_sqrt")
                        (("1" (GROUND)
                          (("1" (EXPAND "sq")
                            (("1" (CANCEL-BY 2 "a") NIL NIL)) NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL)
                   ("2" (LEMMA "sq_le")
                    (("2" (INST?)
                      (("2" (REWRITE "sq_sqrt")
                        (("2" (GROUND)
                          (("2" (EXPAND "sq") (("2" (GROUND) NIL NIL))
                            NIL))
                          NIL))
                        NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (SQRT "" (SKOLEM 1 "a")
       (("" (EXPAND "sqrt_lb")
         (("" (EXPAND "sqrt_ub")
           (("" (LEMMA "sqrt_bisect_boundaries") (("" (INST?) NIL NIL))
             NIL))
           NIL))
         NIL))
       NIL))


$$$bolzano.pvs
bolzano : THEORY
%----------------------------------------------------------------------------
%  Bolzano's Bisection Method
%
%  Cesar Munoz      (munoz@icase.edu)
%
%  In collaboration with
%    Jacques Fleuriot (j.d.f@icase.edu)
% 
%  ICASE - NASA Langley 
%  July 2001
%----------------------------------------------------------------------------
BEGIN

  n     : VAR nat
  a,b   : VAR real

  Boundaries : TYPE = {a,b| a <= b} 

  P     : VAR PRED[Boundaries]
  ab,bc : VAR Boundaries

  bolzano_bisect(P,ab,n) : RECURSIVE Boundaries =
    IF n=0 THEN ab
    ELSE LET mid = (ab`1 + ab`2)/2 IN
      IF P((ab`1,mid)) THEN bolzano_bisect(P,(mid,ab`2),n-1)
      ELSE bolzano_bisect(P,(ab`1,mid),n-1)
      ENDIF
    ENDIF
  MEASURE n+1

  bolzano_bisect_increasing : LEMMA
    bolzano_bisect(P,ab,n)`1 <= bolzano_bisect(P,ab,n+1)`1

  bolzano_bisect_min : LEMMA
    ab`1 <= bolzano_bisect(P,ab,n)`1 

  bolzano_bisect_decreasing : LEMMA
    bolzano_bisect(P,ab,n+1)`2 <= bolzano_bisect(P,ab,n)`2

  bolzano_bisect_max : LEMMA
    bolzano_bisect(P,ab,n)`2 <= ab`2

  bolzano_bisect_interval : LEMMA
    bolzano_bisect(P,ab,n)`2 - bolzano_bisect(P,ab,n)`1 = 
    (ab`2 - ab`1)/2^n

END bolzano

$$$bolzano.prf
(|bolzano| (|bolzano_bisect_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|bolzano_bisect_TCC2| "" (SUBTYPE-TCC) NIL NIL)
 (|bolzano_bisect_TCC3| "" (SUBTYPE-TCC) NIL NIL)
 (|bolzano_bisect_TCC4| "" (TERMINATION-TCC) NIL NIL)
 (|bolzano_bisect_TCC5| "" (SUBTYPE-TCC) NIL NIL)
 (|bolzano_bisect_TCC6| "" (SUBTYPE-TCC) NIL NIL)
 (|bolzano_bisect_TCC7| "" (TERMINATION-TCC) NIL NIL)
 (|bolzano_bisect_increasing| "" (SKOLEM 1 ("P" "_" "_"))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (SKOLEM 1 "ab")
          (("2" (EXPAND "bolzano_bisect" 1)
            (("2" (LIFT-IF)
              (("2" (GROUND)
                (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bolzano_bisect_min| "" (SKOLEM 1 ("P" "ab" _))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (LEMMA "bolzano_bisect_increasing")
          (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bolzano_bisect_decreasing| "" (SKOLEM 1 ("P" "_" "_"))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (SKOLEM 1 "ab")
          (("2" (EXPAND "bolzano_bisect" 1)
            (("2" (LIFT-IF)
              (("2" (GROUND)
                (("1" (INST?) NIL NIL) ("2" (INST?) NIL NIL)) NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bolzano_bisect_max| "" (SKOLEM 1 ("P" "ab" _))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (LEMMA "bolzano_bisect_decreasing")
          (("2" (INST?) (("2" (GROUND) NIL NIL)) NIL)) NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|bolzano_bisect_interval| "" (SKOLEM 1 ("P" "_" "_"))
  (("" (INDUCT "n")
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (FLATTEN)
        (("2" (SKOLEM 1 "ab")
          (("2" (EXPAND "bolzano_bisect" 1)
            (("2" (LIFT-IF)
              (("2" (GROUND)
                (("1" (INST?)
                  (("1" (REPLACE -2 :HIDE? T)
                    (("1" (HIDE -1) (("1" (GRIND) NIL NIL)) NIL)) NIL))
                  NIL)
                 ("2" (INST?)
                  (("2" (REPLACE -1 :HIDE? T)
                    (("2" (HIDE 1) (("2" (GRIND) NIL NIL)) NIL)) NIL))
                  NIL))
                NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL))
    NIL))
  NIL)
 (|not_P_bolzano_TCC1| "" (SUBTYPE-TCC) NIL NIL)
 (|not_P_bolzano| "" (SKOLEM 1 ("P" "ab" _))
  (("" (INDUCT "n" 1)
    (("1" (GRIND) NIL NIL)
     ("2" (SKOLEM 1 "J")
      (("2" (GROUND)
        (("2" (EXPAND "bolzano_bisect" -2)
          (("2" (NAME-REPLACE "A" "bolzano_bisect(P, ab, J)")
            (("2" (INST -1 "(A`1,(A`1+A`2)/2)" "((A`1+A`2)/2,A`2)")
              (("1" (BETA)
                (("1" (ETA "Boundaries")
                  (("1" (INST?)
                    (("1" (SPLIT -2)
                      (("1" (GRIND) NIL NIL) ("2" (PROPAX) NIL NIL)
                       ("3" (HIDE -1)
                        (("3" (REVEAL -4)
                          (("3" (REPLACE -1 :HIDE? T :DIR RL)
                            (("3" (GROUND)
                              (("1" (POSTPONE) NIL NIL)
                               ("2" (POSTPONE) NIL NIL))
                              NIL))
                            NIL))
                          NIL))
                        NIL)
                       ("4" (POSTPONE) NIL NIL))
                      NIL))
                    NIL))
                  NIL))
                NIL)
               ("2" (GRIND) NIL NIL) ("3" (GRIND) NIL NIL))
              NIL))
            NIL))
          NIL))
        NIL))
      NIL)
     ("3" (GRIND) NIL NIL))
    NIL))
  NIL))