Impressum interval_bolzano.pvs Sprache: PVS

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

quality88%

¤ 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.0.1Bemerkung: (vorverarbeitet) ¤

*Bot Zugriff

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.