%------------------------------------------------------------------------------ % 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_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
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.
