Quellcode-Bibliothek

^© Kompilation durch diese Firma

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

Datei: ExceptionalFinally2.out Sprache: SML

Original von: PVS^©

%------------------------------------------------------------------------------
% Generalized Power function (without ln/exp)
%
%     Author: David Lester, Manchester University & NIA
%
%     Version 1.0            19/08/08   Initial version (DRL)
%
% (Note: we follow the prelude, and define 0^0 = 1)
%
%------------------------------------------------------------------------------

real_expt: THEORY

BEGIN

  IMPORTING nnreal_expt,
            root

  x,y: VAR nnreal
  a,b: VAR real
  i:   VAR int
  pn:  VAR posnat
  na:  VAR negreal
  n0x: VAR nzreal
  pa,pb,px,py,r: VAR posreal
  gt1x: VAR {r | r > 1}
  lt1x: VAR {r | r < 1}

  ^(x:nnreal,a:{a | a >= 0 OR x > 0}):nnreal
     = IF a >= 0 THEN nnreal_expt(x,a) ELSE nnreal_expt(1/x,-a) ENDIF

  real_expt_nnreal_rew: LEMMA x^y = nnreal_expt(x,y)
  real_expt_int_rew:    LEMMA FORALL (i:{i | x /= 0 OR i >= 0}):
                              x^i = exponentiation.^(x,i)
  real_expt_root_rew:   LEMMA x^(1/pn) = root(x,pn)

  real_expt_x0: LEMMA x^0 = 1
  real_expt_1a: LEMMA 1^a = 1
  real_expt_0x: LEMMA 0^x = IF x = 0 THEN 1 ELSE 0 ENDIF
  real_expt_x1: LEMMA x^1 = x

  real_expt_pos:  LEMMA px^a > 0
  real_expt_is_0: LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
                        x^a = 0 IFF x = 0 AND a > 0
  real_expt_gt1:  LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
                        x^a > 1 IFF (x > 1 AND a > 0 OR x < 1 AND a < 0)
  real_expt_lt1:  LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0}):
                        x^a < 1 IFF (x < 1 AND a > 0 OR x > 1 AND a < 0)

  inv_real_expt:  LEMMA (1/px)^a  = 1/(px^a)
  mult_real_expt: LEMMA FORALL (x,y:nnreal,a:{a | a >= 0 OR x > 0 AND y > 0}):
                        (x*y)^a   = x^a * y^a
  div_real_expt:  LEMMA FORALL (x:nnreal,py:posreal,a:{a | a >= 0 OR x > 0}):
                        (x/py)^a = x^a / py^a

  real_expt_neg:  LEMMA px^(-a)  = (1/px)^a
  real_expt_plus: LEMMA FORALL (x:nnreal,a,b:{a | a >= 0 OR x > 0}):
                        x^(a+b) = x^a * x^b
  real_expt_minus:LEMMA px^(a-b) = px^a / px^b
  real_expt_times:LEMMA FORALL (x:nnreal,a:{a | a >= 0 OR x > 0},
                                         b:{b | b >= 0 OR x^a > 0}):
                        x^(a*b) = (x^a)^b

  real_expt_decreasing:        LEMMA a < b => lt1x^a > lt1x^b
  real_expt_increasing:        LEMMA a < b => gt1x^a < gt1x^b
  real_expt_strict_increasing: LEMMA x < y => x^pa < y^pa
  real_expt_strict_decreasing: LEMMA px < y => px^na > y^na

  both_sides_real_expt_lt: LEMMA x^pa <  y^pa IFF x <  y
  both_sides_real_expt_le: LEMMA x^pa <= y^pa IFF x <= y
  both_sides_real_expt_gt: LEMMA x^pa >  y^pa IFF x >  y
  both_sides_real_expt_ge: LEMMA x^pa >= y^pa IFF x >= y
  both_sides_real_expt:    LEMMA x^pa =  y^pa IFF x =  y

  both_sides_real_expt_lt1_lt: LEMMA lt1x^a <  lt1x^b IFF b <  a
  both_sides_real_expt_lt1_le: LEMMA lt1x^a <= lt1x^b IFF b <= a
  both_sides_real_expt_lt1_gt: LEMMA lt1x^a >  lt1x^b IFF b >  a
  both_sides_real_expt_lt1_ge: LEMMA lt1x^a >= lt1x^b IFF b >= a

  both_sides_real_expt_gt1_lt: LEMMA gt1x^a <  gt1x^b IFF a <  b
  both_sides_real_expt_gt1_le: LEMMA gt1x^a <= gt1x^b IFF a <= b
  both_sides_real_expt_gt1_gt: LEMMA gt1x^a >  gt1x^b IFF a >  b
  both_sides_real_expt_gt1_ge: LEMMA gt1x^a >= gt1x^b IFF a >= b

  both_sides_real_expt_eq: LEMMA x^pa = x^pb IFF x = 0 OR x = 1 OR pa = pb

END real_expt

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