round_props[N: above(1), P:posnat]: THEORY
%%%% misc lemmas on the rounding function 
BEGIN

  IMPORTING round_fact2[N,P]

  mode: VAR rounding_mode;
  x,y: VAR real;
  i: VAR int;

  round_inx: LEMMA round(x, mode, P)=x IFF
    round(alpha_rep[eta(x)`e - P](x), mode, P)=alpha_rep[eta(x)`e - P](x);

  round_inx_eq: LEMMA (i<=eta(x)`e-P AND alpha_eq[i](x,y)) 
    IMPLIES (round(x, mode, P)=x IFF round(y, mode, P)=y);

  round_denormal: LEMMA denormal?(eta(x)) IMPLIES eta(round(x, mode, P))`e = emin;

END round_props


round_monoton [ N:above(1), P: posnat ] : Theory
Begin

  Importing xmin[N,P], round_correct[N,P];

  x: Var real;
  y: Var (if_i3e_number?[N,P]);
  mode: Var rounding_mode;

  round_neg_over_representable: Lemma
    x >= value(y) Implies
      round(x, to_neg, P) >= value(y);

  round_nearest_over_representable: Lemma
    x >= value(y) Implies
      round(x, to_nearest, P) >= value(y);

  round_over_representable: Lemma
    x >= value(y) Implies
      round(x, mode, P) >= value(y);

  round_under_representable: Lemma
    x <= value(y) Implies
      round(x, mode, P) <= value(y);

  round_Xmin: Lemma
    x >= Xmin[N,P] Implies
      round(x, mode, P) >= Xmin[N,P];

  round_minus_Xmin: Lemma
    x <= -Xmin[N,P] Implies
      round(x, mode, P) <= -Xmin[N,P];

  % unfinished
  %round_ge: LEMMA
  %  FORALL (x, y: real, mode: rounding_mode):
  %    x >= y IMPLIES round[N, P](x, mode, P) >= round[N, P](y, mode, P);

End round_monoton