Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: nnreal_expt.pvs Sprache: PVS

Original von: 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

¤ Dauer der Verarbeitung: 0.15 Sekunden (vorverarbeitet) ¤

Download des Quellennavigators
Download des sprechenden Kalenders
in der Quellcodebibliothek suchen

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.