%% 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 measureif 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))
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.
