Quelle  mul.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