Quelle power.pvs Sprache: PVS

%------------------------------------------------------------------------------
% Power
%
%     Author: David Lester, Manchester University
%
%     Version 1.0            18/2/09   Initial Release Version
%------------------------------------------------------------------------------

power: THEORY

BEGIN

  IMPORTING prelude_aux, prelude_A4, appendix, cauchy, unique

  w,x,y,z,a,b: VAR real
  pn,q0,q1: VAR posnat
  p,q,p1,n: VAR nat
  cx: VAR cauchy_real
  scx: VAR cauchy_smallreal
  sx: VAR smallreal
  r,X,Y,X0: VAR int
  rx: VAR rat
  e1: VAR posreal

  abs_ge0:       LEMMA 0 <= abs(x)
  abs_neg:       LEMMA abs(-x) = abs(x)
  abs_interval:  LEMMA abs(x-y) < a <=> x-a < y AND y < x+a
  abs_interval1: LEMMA abs(x) < a <=> -a < x AND x < a
  abs_interval2: LEMMA abs(x) <= a <=> -a <= x AND x <= a
  triangle_open: LEMMA abs(x-y) < a AND abs(y-z) < b => abs(x-z) < a+b
  abs_error:     LEMMA abs(x-y) < a AND abs(w-z) < b => abs(x+w-(y+z)) < a+b

  lemma_A2_generalized: LEMMA r = round(x) => r-1/2 <= x AND x < r+1/2

  cauchy_power_lt1_n_odd: LEMMA
     odd?(pn) AND sx+e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_n_even: LEMMA
     even?(pn) AND sx+e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_snz_odd: LEMMA
     odd?(pn) AND sx < 0 AND sx+e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_snz_even: LEMMA
     even?(pn) AND sx < 0 AND sx+e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_sn_odd: LEMMA
     odd?(pn) AND sx < 0 AND 0 < sx+e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_sn_even: LEMMA
     even?(pn) AND sx < 0 AND 0 < sx+e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_z: LEMMA
     sx = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_sp_odd: LEMMA
     odd?(pn) AND 0 < sx AND sx-e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_sp_even: LEMMA
     even?(pn) AND 0 < sx AND sx-e1 < 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_pz: LEMMA
     sx-e1 = 0 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_p: LEMMA
     0 < sx-e1 AND e1 = 2^-(p+floor(log2(pn))+3) AND
     Y = round ((rx*e1)^pn*2^p) AND rx-1 < sx / e1 AND sx / e1 < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_main_generalized: LEMMA
     Y = round ((rx*2^-(p+floor(log2(pn))+3))^pn*2^p) AND
     rx-1 < sx * 2^(p+floor(log2(pn))+3) AND
     sx * 2^(p+floor(log2(pn))+3) < rx+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_main: LEMMA
     Y = round ((X*2^-(p+floor(log2(pn))+3))^pn*2^p) AND
     X-1 < sx * 2^(p+floor(log2(pn))+3) AND
     sx * 2^(p+floor(log2(pn))+3) < X+1 =>
     Y-1 < sx^pn * 2^p AND sx^pn * 2^p < 1+Y

  cauchy_power_lt1_isreal: LEMMA cauchy_real?
       (LAMBDA p: round ((scx(p+floor(log2(pn))+3) *
                                             2^-(p+floor(log2(pn))+3))^pn*2^p))

  cauchy_power_lt1(scx:cauchy_smallreal, pn:posnat):cauchy_real
     = (LAMBDA p: round ((scx(p+floor(log2(pn))+3) *
                                             2^-(p+floor(log2(pn))+3))^pn*2^p))

  power_lemma_lt1: LEMMA cauchy_prop(sx,scx)
                       => cauchy_prop(sx^pn, cauchy_power_lt1(scx,pn))

  cauchy_power_div1: LEMMA X0-1 < x AND x < X0+1 AND
                     p = floor(log2(abs(X0)+1))+1 =>
                     -(2^p) < x AND x < 2^p

  cauchy_power_main: LEMMA
     X0-1 < x AND x < X0+1 AND q = 1+floor(log2(abs(X0)+1)) AND
     p1 = p+floor(log2(pn))+3+pn*q AND Y = round ((X/2^p1)^pn*2^p) AND
     X-1 < x * 2^p1 AND x * 2^p1 < X+1 =>
     Y-1 < x^pn * 2^p AND x^pn * 2^p < 1+Y

  cauchy_power_isreal: LEMMA cauchy_real?
   (LAMBDA p:
      LET p1 = p+floor_log2(pn)+3+pn*(1+floor_log2(abs(cx(0))+1))
      IN  round((cx(p1)*2^-(p1))^pn*2^p))

  cauchy_power(cx:cauchy_real, pn:posnat):cauchy_real
     = (LAMBDA p: LET p1 = p+floor_log2(pn)+3+pn*(1+floor_log2(abs(cx(0))+1))
                  IN  round((cx(p1)*2^-(p1))^pn*2^p))

  power_lemma: LEMMA cauchy_prop(x,cx) => cauchy_prop(x^pn,cauchy_power(cx,pn))

END power

quality95%

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