Quelle  root.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