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