log2: THEORY
 BEGIN
 IMPORTING int_induction

  x: VAR posreal;

  plog2_rec(x: {x: real | x >= 1}): RECURSIVE nat =
    IF x >= 2 THEN 1 + plog2_rec(x / 2) ELSE 0 ENDIF
     MEASURE ceiling(x);

  nlog2_rec(x: {x: real | x > 0 AND x < 2}): RECURSIVE nat =
    IF x < 1 THEN 1 + nlog2_rec(x * 2) ELSE 0 ENDIF
     MEASURE plog2_rec((1 / x) * 2) + 1;

  log2(x): int = IF (x >= 1) THEN plog2_rec(x) ELSE -nlog2_rec(x) ENDIF;

  log2_mul2expt: LEMMA
    FORALL (x: posreal, k: int): log2(x * 2 ^ k) = log2(x) + k;


  log2_exp2: THEOREM FORALL (k: int): log2(2 ^ k) = k;

  log2_val: THEOREM
    FORALL (k: int, x: {x | 2 ^ k <= x & x < 2 ^ (k + 1)}): log2(x) = k;

  exp2_log2: THEOREM
    FORALL (x: posreal): 2 ^ log2(x) <= x AND x < 2 ^ (1 + log2(x));

  log2_ge: THEOREM
    FORALL (k: int, x: {x: posreal | x >= 2 ^ k}): log2(x) >= k;

  log2_lt: THEOREM
    FORALL (k: int, x: {x: posreal | x < 2 ^ k}): log2(x) < k;

  log2_ineq: THEOREM
    FORALL (x, y: posreal):
      (x >= y IMPLIES log2(x) >= log2(y)) AND
       (log2(x) > log2(y) IMPLIES x > y);

  log2_ineq2: THEOREM
    FORALL (x: posreal, i: int): log2(x) >= i IMPLIES x >= 2 ^ i;

  log2_ineq3: THEOREM FORALL (x: posreal, i: int): x < 2 ^ i IFF log2(x) < i;

 END log2