| products/Sources/formale Sprachen/Coq/tactics/ |
|
Quellcode-Bibliothek© Kompilation durch diese Firma[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]Datei: int.prf Sprache: PVSOriginal von: PVS© |
|
||||||
|
%------------------------------------------------------------------------------
% Top file for exact_real_arith % % Author: David Lester, Manchester University % % Version 1.0 18/2/09 Initial Release Version %------------------------------------------------------------------------------ mul: THEORY BEGIN IMPORTING prelude_aux, appendix, cauchy x,y,z : VAR real n1,n2,n,m,r : VAR int nnx,nny: VAR nonneg_real npx,npy: VAR nonpos_real nx, ny: VAR negreal px, py: VAR posreal cx, cy: VAR cauchy_real s,s1,s2,p: VAR nat D1: LEMMA n-1 < x AND x < n+1 AND x = 0 => n = 0 D2: LEMMA n-1 < x AND x < n+1 AND x < 0 => n <= 0 D3: LEMMA n-1 < x AND x < n+1 AND 0 < x => 0 <= n negreal_times_posreal_is_negreal: LEMMA nx*py < 0 lt_times_lt_nonneg1: LEMMA nnx < x AND nny < y => nnx*nny < x*y lt_times_lt_nonneg2: LEMMA nnx < x AND y < npy => x*y < nnx*npy D_pp: LEMMA n-1 < px AND px < n+1 AND m-1 < py AND py < m+1 => n*m-abs(n)-abs(m)-1 < px*py AND px*py < n*m+abs(n)+abs(m)+1 D_pn: LEMMA n-1 < px AND px < n+1 AND m-1 < ny AND ny < m+1 => n*m-abs(n)-abs(m)-1 < px*ny AND px*ny < n*m+abs(n)+abs(m)+1 D_nn: LEMMA n-1 < nx AND nx < n+1 AND m-1 < ny AND ny < m+1 => n*m-abs(n)-abs(m)-1 < nx*ny AND nx*ny < n*m+abs(n)+abs(m)+1 D_p0: LEMMA n-1 < px AND px < n+1 AND m-1 < y AND y < m+1 AND y = 0 => n*m-abs(n)-abs(m)-1 < px*y AND px*y < n*m+abs(n) + abs(m)+1 D_n0: LEMMA n-1 < nx AND nx < n+1 AND m-1 < y AND y < m+1 AND y = 0 => n*m-abs(n)-abs(m)-1 < nx*y AND nx*y < n*m+abs(n) + abs(m)+1 D: LEMMA n-1 < x AND x < n+1 AND m-1 < y AND y < m+1 => n*m-abs(n)-abs(m)-1 < x*y AND x*y < n*m+abs(n)+abs(m)+1 mul_p1: LEMMA s = floor(log2(abs(cx(0))+2))+3 => 2^(s-3) <= abs(cx(0))+2 AND abs(cx(0))+2 < 2^(s-2) mul_p2: LEMMA s = floor(log2(abs(cx(0))+2))+3 AND n = cx(p) AND 0 < p => abs(n)+1 <= 2^p*(abs(cx(0))+2) AND 2^p*(abs(cx(0))+2) < 2^(p+s-2) mul_p3: LEMMA s = floor(log2(abs(cx(0))+2))+3 AND 0 < p => abs(cx(p))+1 <= 2^(p+s-2) mul_p4: LEMMA s1 = floor(log2(abs(cx(0))+2))+3 AND s2 = floor(log2(abs(cy(0))+2))+3 => abs(cx(p+s2)) + abs(cy(p+s1)) + 1 < 2^(p+s1+s2-1) mul_p5: LEMMA s1 = floor(log2(abs(cx(0))+2))+3 AND s2 = floor(log2(abs(cy(0))+2))+3 AND n1 = cx(p+s2) AND n2 = cy(p+s1) AND r = round((n1*n2)/2^(p+s1+s2)) => 2^(p+s1+s2)*(r-1) <= n1*n2 - abs(n1) - abs(n2) -1 AND n1*n2 + abs(n1) + abs(n2) +1 <= 2^(p+s1+s2)*(r+1) mul_p6: LEMMA s1 = floor(log2(abs(cx(0))+2))+3 AND s2 = floor(log2(abs(cy(0))+2))+3 AND n1 = cx(p+s2) AND n2 = cy(p+s1) AND r = round((n1*n2)/2^(p+s1+s2)) AND cauchy_prop(x,cx) AND cauchy_prop(y,cy) => r-1 < 2^p*x*y AND 2^p*x*y < r+1 cauchy_mul_type: LEMMA cauchy_real?(LAMBDA p: round( (cx(p + (floor(log2(abs(cy(0)) + 2)) + 3)) * cy(p + (floor(log2(abs(cx(0)) + 2)) + 3))) / 2 ^ (p + (floor(log2(abs(cx(0)) + 2)) + 3) + (floor(log2(abs(cy(0)) + 2)) + 3)))) cauchy_mul(c1, c2:cauchy_real): cauchy_real = (LAMBDA p: LET s1 = floor_log2(abs(c1(0))+2)+3, s2 = floor_log2(abs(c2(0))+2)+3 IN round((c1(p+s2)*c2(p+s1))/2^(p+s1+s2))) mul_lemma: LEMMA cauchy_prop(x,cx) AND cauchy_prop(y,cy) => cauchy_prop(x*y, cauchy_mul(cx,cy)) END mul ¤ Dauer der Verarbeitung: 0.3 Sekunden (vorverarbeitet) ¤ |
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.Bot Zugriff |
