|
%% interval_bolzano.pvs
%%
%% This theory was originally defined in the reals library in collaboration
%% with J. Fleuriot. It was moved to the interval package by C. Munoz on
%% March 28 2005.
%%----------------------------------------------------------------------------
interval_bolzano : THEORY
BEGIN
IMPORTING interval,reals@log_nat,reals@sqrt
eps : VAR posreal
Prop? : VAR PRED[(Proper?)]
X,Y : VAR (Proper?)
x : VAR nnreal
Continuous?(Prop?): bool =
FORALL(X:(Prop?)): Prop?(HalfLeft(X)) OR Prop?(HalfRight(X))
% Returns a subinterval of X of size less than eps that satisfies Prop?
bolzano_bisect((Prop?:(Continuous?)),(X:(Prop?)),eps) : RECURSIVE
{Y | Y << X AND Prop?(Y) AND size(Y) <= eps} =
if size(X) < eps then X
else
let Y1 = HalfLeft(X) in
let Y2 = HalfRight(X) in
if Prop?(Y1) then
bolzano_bisect(Prop?,Y1,eps)
else
bolzano_bisect(Prop?,Y2,eps)
endif
endif
measure if size(X) < eps then 0 else 1+log_nat(size(X)/eps,2)`1 endif
SqrtProp?(x)(X):bool = sq(lb(X)) <= x AND x <= sq(ub(X))
SqrtProp : JUDGEMENT
SqrtProp?(x) HAS_TYPE (Continuous?)
% Alternative definition of square root using the bisection method
sqrt_bisect(x,eps) : (NonNeg?) =
bolzano_bisect(SqrtProp?(x),[|0,max(1,x)|],eps)
sqrt_bisect_inclusion : LEMMA
sqrt(x) ## sqrt_bisect(x,eps)
END interval_bolzano
¤ Dauer der Verarbeitung: 0.1 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.
|
