Quelle nnreal_expt.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Power function nnx^nny
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%------------------------------------------------------------------------------

nnreal_expt: THEORY

BEGIN

  IMPORTING rational_props_aux,
            nn_root,
            nn_rational_expt

  n:         VAR nat
  pn:        VAR posnat
  a,b,x,y,z: VAR nnreal
  q:         VAR nnrat
  px,py,pa,pb,
  delta,r,
  epsilon:   VAR posreal

  nnreal_expt(x,y):nnreal
   = IF y = 0 OR x = 1 THEN 1
     ELSIF x < 1 THEN glb({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
                 ELSE lub({z | EXISTS q: q <= y AND z = nn_rational_expt(x,q)})
     ENDIF

  nnreal_expt_rat_rew:  LEMMA nnreal_expt(x,q)    = nn_rational_expt(x,q)
  nnreal_expt_nat_rew:  LEMMA nnreal_expt(x,n)    = x^n
  nnreal_expt_root_rew: LEMMA nnreal_expt(x,1/pn) = nn_root(x,pn)

  nnreal_expt_0a:   LEMMA nnreal_expt(0,a) = IF a = 0 THEN 1 ELSE 0 ENDIF
  nnreal_expt_1a:   LEMMA nnreal_expt(1,a) = 1
  nnreal_expt_x1:   LEMMA nnreal_expt(x,1)  = x

  nnreal_expt_pos:  LEMMA nnreal_expt(px,a) > 0
  nnreal_expt_is_0: LEMMA nnreal_expt(x,a) = 0 IFF x = 0 AND a /= 0
  nnreal_expt_gt1:  LEMMA nnreal_expt(x,pa) > 1 IFF x > 1
  nnreal_expt_lt1:  LEMMA nnreal_expt(x,pa) < 1 IFF x < 1

  inv_nnreal_expt:  LEMMA nnreal_expt(1/px,a) = 1/nnreal_expt(px,a)
  mult_nnreal_expt: LEMMA nnreal_expt(x*y,a)
                               = nnreal_expt(x,a)*nnreal_expt(y,a)
  div_nnreal_expt:  LEMMA nnreal_expt(x/py,a)
                               = nnreal_expt(x,a)/nnreal_expt(py,a)

  nnreal_expt_decreasing: LEMMA a < b AND 0 < x AND x < 1 =>
                                nnreal_expt(x,a) > nnreal_expt(x,b)

  nnreal_expt_increasing: LEMMA a < b AND 1 < x =>
                                nnreal_expt(x,a) < nnreal_expt(x,b)

  nnreal_expt_strict_increasing: LEMMA x < y =>
                                       nnreal_expt(x,pa) < nnreal_expt(y,pa)

  continuous_alt_nnreal_expt2: LEMMA
     EXISTS delta: FORALL pb: abs(pa-pb) < delta
                 => abs(nnreal_expt(x,pa)-nnreal_expt(x,pb)) < epsilon

  ne1x: VAR {r | r /= 1}
  gt1x: VAR {r | r > 1}
  lt1x: VAR {r | r < 1}

  nnreal_bijective1: LEMMA
     bijective?[nnreal,{r | r>=1}](lambda y: nnreal_expt(gt1x,y))

  nnreal_bijective2: LEMMA
     bijective?[nnreal,{r | r<=1}](lambda y: nnreal_expt(lt1x,y))

  nnreal_expt_def_gt1: LEMMA
     nnreal_expt(gt1x,py)
          = lub({z | EXISTS q: q < py AND z = nn_rational_expt(gt1x,q)})

  nnreal_expt_plus: LEMMA nnreal_expt(x,a+b)= nnreal_expt(x,a)*nnreal_expt(x,b)
  nnreal_expt_times: LEMMA nnreal_expt(x,a*b) = nnreal_expt(nnreal_expt(x,a),b)

END nnreal_expt

quality91%

¤ Dauer der Verarbeitung: 0.14 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.