alpha_equiv[alpha: int]: THEORY
 BEGIN

  IMPORTING ieee_import

  x, y: VAR real;

  q: VAR int;

  alpha_eq(x, y): bool =
      (x = y OR
        (EXISTS q:
           q * 2 ^ alpha < x AND
            x < (q + 1) * 2 ^ alpha AND
             q * 2 ^ alpha < y AND y < (q + 1) * 2 ^ alpha));

  alpha_q(x): {i: int | i * 2 ^ alpha <= x AND x < (i + 1) * 2 ^ alpha} =
      floor(x / 2 ^ alpha);

  alpha_q_uniq: LEMMA
    q * 2 ^ alpha <= x AND x < (q + 1) * 2 ^ alpha IMPLIES q = alpha_q(x);

  alpha_rep(x): real =
      LET q = alpha_q(x) IN
        IF q * 2 ^ alpha = x
          THEN x
        ELSE q * 2 ^ alpha + 2 ^ (alpha - 1)
        ENDIF;


  alpha_eq_is_equiv: LEMMA equivalence?(alpha_eq);

  alpha_rep_eq: LEMMA alpha_eq(x, alpha_rep(x));

  alpha_singl_xor_intv: LEMMA
    q * 2 ^ alpha = x AND x /= y IMPLIES NOT alpha_eq(x, y);

  alpha_rep_is_rep_l1: LEMMA alpha_eq(x, y) IMPLIES alpha_q(x) = alpha_q(y);

  alpha_rep_is_rep: LEMMA alpha_eq(x, y) IFF alpha_rep(x) = alpha_rep(y);
 END alpha_equiv

alpha_lemmas: THEORY
 BEGIN

  IMPORTING alpha_equiv

  x, y: VAR real;

  alpha, beta: VAR int;

  alpha_neg: LEMMA alpha_eq[alpha](x, y) IMPLIES alpha_eq[alpha](-x, -y);

  alpha_rep_neg: LEMMA alpha_rep[alpha](x) = -alpha_rep[alpha](-x);

  alpha_stretch: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (k: nat): alpha_eq[alpha + k](2 ^ k * x, 2 ^ k * y));

  alpha_shrink: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (k: nat): alpha_eq[alpha - k](x / 2 ^ k, y / 2 ^ k));

  alpha_shrink_stretch: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (k: int): alpha_eq[alpha + k](2 ^ k * x, 2 ^ k * y));

  alpha_rep_shrink_stretch: LEMMA
    FORALL (k: int):
      alpha_rep[alpha](2 ^ k * x) = 2 ^ k * alpha_rep[alpha - k](x);

  alpha_transl: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (q: int):
        alpha_eq[alpha](x + q * 2 ^ alpha, y + q * 2 ^ alpha));

  alpha_refine_l1: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (k: nat): alpha_eq[alpha + k](x, y));

  alpha_refine: LEMMA
    alpha_eq[alpha](x, y) IMPLIES
     (FORALL (beta: int | beta >= alpha): alpha_eq[beta](x, y));

  alpha_sign: LEMMA x >= 0 IFF alpha_rep[alpha](x) >= 0;

  alpha_ge0: LEMMA x = 0 IFF alpha_rep[alpha](x) = 0;

  alpha_eq0: LEMMA x = 0 IFF alpha_eq[alpha](x, 0);

  alpha_eq_sign: LEMMA
    alpha_eq[alpha](x, y) IMPLIES ((x >= 0 AND y >= 0) OR (x < 0 AND y < 0));

  alpha_abs: LEMMA
    alpha_eq[alpha](x, y) IMPLIES alpha_eq[alpha](abs(x), abs(y));

  alpha_rep_small: Lemma  %% cb
    Forall (alpha: int, x: posreal): x < 2^alpha Implies
      alpha_rep[alpha](x) = 2^(alpha-1);

  alpha_rep_large: LEMMA
    FORALL(alpha: int, x,y: posreal, k: upfrom(alpha)):
      alpha_eq[alpha](x,y) IMPLIES (x<2^k IFF y<2^k);

  alpha_eq_smaller: Lemma
      alpha_eq[alpha](x, y) Implies x < y + 2^alpha;

  alpha_eq_abs: Lemma
      alpha_eq[alpha](x, y) Implies alpha_eq[alpha](abs(x), abs(y));

 END alpha_lemmas

alpha_rd_lem[N: above(1)]: THEORY
 BEGIN

  IMPORTING alpha_lemmas, eta_props[N]

  i: VAR int;

  p: VAR posnat;

  x, x1: VAR nonzero_real;

  y: VAR factoring;

  eta_hat_equiv1: LEMMA
    (y = eta_hat(x) AND alpha_eq[y`e](abs(x), abs(x1))) IMPLIES
     eta_hat(abs(x))`e = eta_hat(abs(x1))`e;

  eta_hat_equiv2: LEMMA
    (y = eta_hat(x) AND alpha_eq[y`e](x, x1)) IMPLIES
     eta_hat(x)`e = eta_hat(x1)`e;

  eta_hat_equiv: LEMMA
    (y = eta_hat(x) AND i <= y`e AND alpha_eq[i](x, x1)) IMPLIES
     eta_hat(x)`e = eta_hat(x1)`e;

  etahat_equiv_commute: LEMMA FORALL(x1,x2: nonzero_real, p: nat):
    alpha_eq[eta_hat(x1)`e-p](x1,x2) IMPLIES
    alpha_eq[eta_hat(x2)`e-p](x2,x1);

  eta_equiv0: LEMMA
    (y = eta(x) AND alpha_eq[y`e](abs(x), abs(x1))) IMPLIES
     (eta_hat(abs(x))`e < emin IFF eta_hat(abs(x1))`e < emin);

  eta_equiv1: LEMMA
    (y = eta(x) AND alpha_eq[y`e](abs(x), abs(x1))) IMPLIES
     eta(abs(x))`e = eta(abs(x1))`e;

  eta_equiv2: LEMMA
    (y = eta(x) AND alpha_eq[y`e](x, x1)) IMPLIES eta(x)`e = eta(x1)`e;

  eta_equiv: LEMMA
    FORALL (x, x1: real):
      (y = eta(x) AND i <= y`e AND alpha_eq[i](x, x1)) IMPLIES
       eta(x)`e = eta(x1)`e;

  alpha_rep_log1: LEMMA
    y = eta(x) IMPLIES
     log2(abs(x)) >= emin IMPLIES
      log2(abs(x)) = log2(abs(alpha_rep[y`e - p](x)));

  alpha_rep_log2: LEMMA
    y = eta(x) IMPLIES
     log2(abs(x)) < emin IMPLIES log2(abs(alpha_rep[y`e - p](x))) < emin;


  alpha_rep_eta: LEMMA
    FORALL (x: real, p: nat):
      y = eta(x) IMPLIES
       eta(alpha_rep[y`e - p](x)) =
        (# s := y`s, e := y`e, f := alpha_rep[-p](y`f) #);

  alpha_rep_ii_fact: LEMMA
    FORALL (y: (ii_i3e_number?), prec: posnat):
      ii_i3e_number?((# s := y`s, e := y`e, f := alpha_rep[-prec](y`f) #));

  alpha_eq_normshift: LEMMA
    FORALL (x: nonneg_real, y: (ii_i3e_number?), prec: posnat):
      (y`s = pos IFF x >= 0) AND
       y`e = eta(x)`e AND alpha_eq[-prec](eta(x)`f, y`f)
       IMPLIES alpha_eq[y`e - prec](x, value(y));
 END alpha_rd_lem