Theory Log_Nat

theory Log_Nat
imports Complex_Main
(*  Title:      HOL/Library/Log_Nat.thy
    Author:     Johannes Hölzl, Fabian Immler
    Copyright   2012  TU München
*)

section ‹Logarithm of Natural Numbers›

theory Log_Nat
imports Complex_Main
begin

definition floorlog :: "nat ⇒ nat ⇒ nat" where
"floorlog b a = (if a > 0 ∧ b > 1 then nat ⌊log b a⌋ + 1 else 0)"

lemma floorlog_mono: "x ≤ y ⟹ floorlog b x ≤ floorlog b y"
by(auto simp: floorlog_def floor_mono nat_mono)

lemma floorlog_bounds:
  assumes "x > 0" "b > 1"
  shows "b ^ (floorlog b x - 1) ≤ x ∧ x < b ^ (floorlog b x)"
proof
  show "b ^ (floorlog b x - 1) ≤ x"
  proof -
    have "b ^ nat ⌊log b x⌋ = b powr ⌊log b x⌋"
      using powr_realpow[symmetric, of b "nat ⌊log b x⌋"] ‹x > 0› ‹b > 1›
      by simp
    also have "… ≤ b powr log b x" using ‹b > 1› by simp
    also have "… = real_of_int x" using ‹0 < x› ‹b > 1› by simp
    finally have "b ^ nat ⌊log b x⌋ ≤ real_of_int x" by simp
    then show ?thesis
      using ‹0 < x› ‹b > 1› of_nat_le_iff
      by (fastforce simp add: floorlog_def)
  qed
  show "x < b ^ (floorlog b x)"
  proof -
    have "x ≤ b powr (log b x)" using ‹x > 0› ‹b > 1› by simp
    also have "… < b powr (⌊log b x⌋ + 1)"
      using assms by (intro powr_less_mono) auto
    also have "… = b ^ nat (⌊log b (real_of_int x)⌋ + 1)"
      using assms by (simp add: powr_realpow[symmetric])
    finally
    have "x < b ^ nat (⌊log b (int x)⌋ + 1)"
      by (rule of_nat_less_imp_less)
    then show ?thesis
      using ‹x > 0› ‹b > 1› by (simp add: floorlog_def nat_add_distrib)
  qed
qed

lemma floorlog_power[simp]:
  assumes "a > 0" "b > 1"
  shows "floorlog b (a * b ^ c) = floorlog b a + c"
proof -
  have "⌊log b a + real c⌋ = ⌊log b a⌋ + c" by arith
  then show ?thesis using assms
    by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
qed

lemma floor_log_add_eqI:
  fixes a::nat and b::nat and r::real
  assumes "b > 1" "a ≥ 1" "0 ≤ r" "r < 1"
  shows "⌊log b (a + r)⌋ = ⌊log b a⌋"
proof (rule floor_eq2)
  have "log b a ≤ log b (a + r)" using assms by force
  then show "⌊log b a⌋ ≤ log b (a + r)" by arith
next
  define l::int where "l = int b ^ (nat ⌊log b a⌋ + 1)"
  have l_def_real: "l = b powr (⌊log b a⌋ + 1)"
    using assms by (simp add: l_def powr_add powr_real_of_int)
  have "a < l"
  proof -
    have "a = b powr (log b a)" using assms by simp
    also have "… < b powr floor ((log b a) + 1)"
      using assms(1) by auto
    also have "… = l"
      using assms by (simp add: l_def powr_real_of_int powr_add)
    finally show ?thesis by simp
  qed
  then have "a + r < l" using assms by simp
  then have "log b (a + r) < log b l" using assms by simp
  also have "… = real_of_int ⌊log b a⌋ + 1"
    using assms by (simp add: l_def_real)
  finally show "log b (a + r) < real_of_int ⌊log b a⌋ + 1" .
qed

lemma divide_nat_diff_div_nat_less_one:
  fixes x b::nat shows "x / b - x div b < 1"
proof -
  have "int 0 ≠ ⌊1::real⌋" by simp
  thus ?thesis
    by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
        mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
qed

lemma floor_log_div:
  fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
  shows "⌊log b x⌋ = ⌊log b (x div b)⌋ + 1"
proof-
  have "⌊log b x⌋ = ⌊log b (x / b * b)⌋" using assms by simp
  also have "… = ⌊log b (x / b) + log b b⌋"
    using assms by (subst log_mult) auto
  also have "… = ⌊log b (x / b)⌋ + 1" using assms by simp
  also have "⌊log b (x / b)⌋ = ⌊log b (x div b + (x / b - x div b))⌋" by simp
  also have "… = ⌊log b (x div b)⌋"
    using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
    by (intro floor_log_add_eqI) auto
  finally show ?thesis .
qed

lemma compute_floorlog[code]:
  "floorlog b x = (if x > 0 ∧ b > 1 then floorlog b (x div b) + 1 else 0)"
by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
    intro!: floor_eq2)

lemma floor_log_eq_if:
  fixes b x y :: nat
  assumes "x div b = y div b" "b > 1" "x > 0" "x div b ≥ 1"
  shows "floor(log b x) = floor(log b y)"
proof -
  have "y > 0" using assms by(auto intro: ccontr)
  thus ?thesis using assms by (simp add: floor_log_div)
qed

lemma floorlog_eq_if:
  fixes b x y :: nat
  assumes "x div b = y div b" "b > 1" "x > 0" "x div b ≥ 1"
  shows "floorlog b x = floorlog b y"
proof -
  have "y > 0" using assms by(auto intro: ccontr)
  thus ?thesis using assms
    by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
qed


definition bitlen :: "int ⇒ int" where "bitlen a = floorlog 2 (nat a)"

lemma bitlen_alt_def: "bitlen a = (if a > 0 then ⌊log 2 a⌋ + 1 else 0)"
by (simp add: bitlen_def floorlog_def)

lemma bitlen_nonneg: "0 ≤ bitlen x"
by (simp add: bitlen_def)

lemma bitlen_bounds:
  assumes "x > 0"
  shows "2 ^ nat (bitlen x - 1) ≤ x ∧ x < 2 ^ nat (bitlen x)"
proof -
  from assms have "bitlen x ≥ 1" by (auto simp: bitlen_alt_def)
  with assms floorlog_bounds[of "nat x" 2] show ?thesis
    by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
qed

lemma bitlen_pow2[simp]:
  assumes "b > 0"
  shows "bitlen (b * 2 ^ c) = bitlen b + c"
  using assms
  by (simp add: bitlen_def nat_mult_distrib nat_power_eq)

lemma compute_bitlen[code]:
  "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
by (simp add: bitlen_def nat_div_distrib compute_floorlog)

lemma bitlen_eq_zero_iff: "bitlen x = 0 ⟷ x ≤ 0"
by (auto simp add: bitlen_alt_def)
   (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
      not_less zero_less_one)

lemma bitlen_div:
  assumes "0 < m"
  shows "1 ≤ real_of_int m / 2^nat (bitlen m - 1)"
    and "real_of_int m / 2^nat (bitlen m - 1) < 2"
proof -
  let ?B = "2^nat (bitlen m - 1)"

  have "?B ≤ m" using bitlen_bounds[OF ‹0 <m›] ..
  then have "1 * ?B ≤ real_of_int m"
    unfolding of_int_le_iff[symmetric] by auto
  then show "1 ≤ real_of_int m / ?B" by auto

  from assms have "m ≠ 0" by auto
  from assms have "0 ≤ bitlen m - 1" by (auto simp: bitlen_alt_def)

  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] ..
  also from assms have "… = 2^nat(bitlen m - 1 + 1)"
    by (auto simp: bitlen_def)
  also have "… = ?B * 2"
    unfolding nat_add_distrib[OF ‹0 ≤ bitlen m - 1› zero_le_one] by auto
  finally have "real_of_int m < 2 * ?B"
    by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff)
  then have "real_of_int m / ?B < 2 * ?B / ?B"
    by (rule divide_strict_right_mono) auto
  then show "real_of_int m / ?B < 2" by auto
qed

end