Quelle root.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Generalized Root function
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% (We can take nth-roots of negative numbers provided n is odd.
%  I could believe that the type-constraints make this unusable;
%  feedback appreciated.)
%------------------------------------------------------------------------------

root: THEORY

BEGIN

  IMPORTING reals@sign,
            nn_root

  x,y,z: VAR real
  epsilon,
    delta: VAR posreal
  pm,pn:   VAR posnat
  nx: VAR nnreal

  root(x:real,pn:{pm | x >= 0 OR odd?(pm)}):real = nn_root(abs(x),pn)*sign(x)

  root_0n: LEMMA root(0,pn) = 0
  root_1n: LEMMA root(1,pn) = 1
  root_x1: LEMMA root(x,1)  = x

  root_nn_root_rew: LEMMA root(nx,pn) = nn_root(nx,pn)

  root_expt: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x^pn,pn) = x
  expt_root: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn)^pn = x

  root_is_0: LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn) = 0 IFF x = 0
  root_pos:  LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn) > 0 IFF x > 0
  root_neg:  LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn) < 0 IFF x < 0
  root_gt1:  LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn) > 1 IFF x > 1
  root_lt1:  LEMMA FORALL (x:real,pn:{pm | x >= 0 OR odd?(pm)}):
                   root(x,pn) < 1 IFF x < 1

  neg_root:  LEMMA odd?(pn) => root(-x,pn) = -root(x,pn)

  mult_root: LEMMA FORALL (x,y:real,pn:{pm | x >= 0 AND y >= 0 OR odd?(pm)}):
                   root(x*y,pn)  = root(x,pn)*root(y,pn)
  inv_root:  LEMMA FORALL (n0x:nzreal,pn:{pm | n0x >= 0 OR odd?(pm)}):
                   root(1/n0x,pn) = 1/root(n0x,pn)
  div_root:  LEMMA FORALL (x:real,n0y:nzreal,
                           pn:{pm | x >= 0 AND n0y >= 0 OR odd?(pm)}):
                   root(x/n0y,pn) = root(x,pn)/root(n0y,pn)

  root_mult: LEMMA FORALL (x:real,pm,pn:{i:posnat | x >= 0 OR odd?(i)}):
                   root(x,pn*pm)  = root(root(x,pn),pm)

  root_increasing: LEMMA ((0 < x AND x < 1) OR
                          (odd?(pn) AND odd?(pm) AND x < -1)) AND
                         pn < pm => root(x,pn) < root(x,pm)

  root_decreasing: LEMMA (1 < x OR
                          (odd?(pn) AND odd?(pm) AND -1 < x AND x < 0)) AND
                         pn < pm => root(x,pn) > root(x,pm)

  continuous_alt_root:
             LEMMA FORALL (x:real,epsilon:posreal,
                           pn:{pm | x >= 0 AND y >= 0 OR odd?(pm)}):
                   EXISTS delta: FORALL (y:{z | z >= 0 OR odd?(pn)}):
                                abs(x-y) < delta
                                 => abs(root(x,pn)-root(y,pn)) < epsilon

END root

quality94%

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

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.