rd2int[N: above(2), P: posnat]: THEORY
BEGIN

  IMPORTING fact_mul2[N,P], round_props[N,P]

  x: VAR (ii_i3e_number?);
  mode: VAR rounding_mode;
  i: VAR int;

  Ngt1: JUDGEMENT N HAS_TYPE above(1);

  %%%%% rd2int is defined fact->fact in order to allow the reuse
  %%%%% for the operation "round to integer in fl.pt. format

  %%% First we define the rounding function
   rd2int(x, mode):  (ii_i3e_number?)
    = eta(round_frac(value(x), mode, 0));

  %%rd2int_lem1: LEMMA 0<=x`e AND x`e<P-1 IMPLIES eta(value(x) * 2 ^ (1 - P + emin))`e = emin;
  rd2int_lem2: LEMMA 0<=x`e AND x`e<P-1 IMPLIES denormal?(eta(value(x) * 2 ^ (1 - P + emin)));

  rd2int_rewr: LEMMA
     0<=x`e AND x`e<P-1 IMPLIES
     value(rd2int(x, mode)) =
        2 ^ (P - 1 - emin) * round(value(x) * 2 ^ (emin + 1 - P), mode, P);

  %%% Now we prove the cortectness of the rounding-function
  rd2int_is_int: LEMMA integer?(value(rd2int(x, mode)));

  rd2int_pos_correct: LEMMA value(rd2int(x, to_pos)) >= value(x) 
    AND (i >= value(x) IMPLIES abs(value(x)-i)>=abs(value(x)-value(rd2int(x, to_pos))));

  rd2int_neg_correct: LEMMA value(rd2int(x, to_neg)) <= value(x) 
    AND (i <= value(x) IMPLIES abs(value(x)-i)>=abs(value(x)-value(rd2int(x, to_neg))));

  rd2int_zero_correct: LEMMA
     abs(value(rd2int(x, to_zero))) <= abs(value(x)) AND
      (abs(i) <= abs(value(x)) IMPLIES
        abs(value(x) - i) >= abs(value(x) - value(rd2int(x, to_zero))));

  rd2int_nearest_correct: LEMMA
    abs(value(x) - i) >= abs(value(x) - value(rd2int(x, to_nearest))); 

  rd2int_tie: LEMMA
    abs(value(x) - value(rd2int(x, to_nearest))) = 1/2 IMPLIES
      even?(value(rd2int(x, to_nearest)));


  %%% Now we prove, that rd2int is trivial, if 0>e OR e>P-1
  rd2int_large: LEMMA P>=2 AND if_i3e_number?[N,P](x) AND x`e>=P-1 IMPLIES rd2int(x,mode) = x;
  rd2int_small: LEMMA x`e<0 IMPLIES rd2int(x,mode) =
    IF x`f=0 THEN (# s:=pos, e:=emin, f:=0 #) ELSE
    COND
      mode = to_zero -> (# s:=pos, e:=emin, f:=0 #),

      mode = to_pos AND x`s=neg -> (# s:=pos, e:=emin, f:=0 #),
      mode = to_pos AND x`s=pos -> (# s:=pos, e:=0, f:=1 #),

      mode = to_neg AND x`s=neg -> (# s:=neg, e:=0, f:=1 #),
      mode = to_neg AND x`s=pos -> (# s:=pos, e:=emin, f:=0 #),

      mode = to_nearest AND x`e<-1 -> (# s:=pos, e:=emin, f:=0 #),
      mode = to_nearest AND x`e=-1 AND x`f=1 -> (# s:=pos, e:=emin, f:=0 #),
      mode = to_nearest AND x`e=-1 AND x`f/=1 -> (# s:=x`s, e:=0, f:= 1 #)
    ENDCOND ENDIF;

  %%% Now comes the algorithm: round 2 times, see also lemma round_denormal
  rd2int_alg1: LEMMA
     if_i3e_number?[N, P]
         (eta(2 ^ (P - 1 - emin) *
               round(value(x) * 2 ^ (emin + 1 - P), mode, P)));

  rd2int_alg2: LEMMA
    0<=x`e AND x`e<P-1 IMPLIES
     rd2int(x, mode) =
      eta(round(2 ^ (P - 1 - emin) *
               round(value(x) * 2 ^ (emin + 1 - P), mode, P), mode, P));


  %%% This is the central lemma for rounding to integer format
  rd2int_format: LEMMA
    0<=x`e AND x`e<P-1 IMPLIES
      LET E=eta(round(value(x) * 2 ^ (emin + 1 - P), mode, P)) IN
      value(rd2int(x, mode)) = sign(E`s) * E`f * 2^(P-1);
END rd2int