# Theory Log_Nat

(*  Title:      HOL/Library/Log_Nat.thy
Author:     Johannes Hölzl, Fabian Immler
*)

section ‹Logarithm of Natural Numbers›

theory Log_Nat
imports Complex_Main
begin

subsection ‹Preliminaries›

lemma divide_nat_diff_div_nat_less_one:
"real x / real b - real (x div b) < 1" for x b :: nat
proof (cases "b = 0")
case True
then show ?thesis
by simp
next
case False
then have "real (x div b) + real (x mod b) / real b - real (x div b) < 1"
then show ?thesis
qed

subsection ‹Floorlog›

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:
"b ^ (floorlog b x - 1)  x  x < b ^ (floorlog b x)" if "x > 0" "b > 1"
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
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 that by (intro powr_less_mono) auto
also have " = b ^ nat (log b (real_of_int x) + 1)"
using that by (simp flip: powr_realpow)
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]:
"floorlog b (a * b ^ c) = floorlog b a + c" if "a > 0" "b > 1"
proof -
have "log b a + real c = log b a + c" by arith
then show ?thesis using that
by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
qed

"log b (a + r) = log b a" if "b > 1" "a  1" "0  r" "r < 1"
for a b :: nat and r :: real
proof (rule floor_eq2)
have "log b a  log b (a + r)" using that 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)"
have "a < l"
proof -
have "a = b powr (log b a)" using that by simp
also have " < b powr floor ((log b a) + 1)"
using that(1) by auto
also have " = l"
finally show ?thesis by simp
qed
then have "a + r < l" using that by simp
then have "log b (a + r) < log b l" using that by simp
also have " = real_of_int log b a + 1"
using that by (simp add: l_def_real)
finally show "log b (a + r) < real_of_int log b a + 1" .
qed

lemma floor_log_div:
"log b x = log b (x div b) + 1" if "b > 1" "x > 0" "x div b > 0"
for b x :: nat
proof-
have "log b x = log b (x / b * b)" using that by simp
also have " = log b (x / b) + log b b"
using that by (subst log_mult) auto
also have " = log b (x / b) + 1" using that 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 that real_of_nat_div4 divide_nat_diff_div_nat_less_one
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:
"log b x = log b y" if "x div b = y div b" "b > 1" "x > 0" "x div b  1"
for b x y :: nat
proof -
have "y > 0" using that by (auto intro: ccontr)
thus ?thesis using that by (simp add: floor_log_div)
qed

lemma floorlog_eq_if:
"floorlog b x = floorlog b y" if "x div b = y div b" "b > 1" "x > 0" "x div b  1"
for b x y :: nat
proof -
have "y > 0" using that by (auto intro: ccontr)
then show ?thesis using that
by (auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
qed

lemma floorlog_leD:
"floorlog b x  w  b > 1  x < b ^ w"
by (metis floorlog_bounds leD linorder_neqE_nat order.strict_trans power_strict_increasing_iff
zero_less_one zero_less_power)

lemma floorlog_leI:
"x < b ^ w  0  w  b > 1  floorlog b x  w"
by (drule less_imp_of_nat_less[where 'a=])
(auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less)

lemma floorlog_eq_zero_iff:
"floorlog b x = 0  b  1  x  0"
by (auto simp: floorlog_def)

lemma floorlog_le_iff:
"floorlog b x  w  b  1  b > 1  0  w  x < b ^ w"
using floorlog_leD[of b x w] floorlog_leI[of x b w]
by (auto simp: floorlog_eq_zero_iff[THEN iffD2])

lemma floorlog_ge_SucI:
"Suc w  floorlog b x" if "b ^ w  x" "b > 1"
using that le_log_of_power[of b w x] power_not_zero
by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1

lemma floorlog_geI:
"w  floorlog b x" if "b ^ (w - 1)  x" "b > 1"
using floorlog_ge_SucI[of b "w - 1" x] that
by auto

lemma floorlog_geD:
"b ^ (w - 1)  x" if "w  floorlog b x" "w > 0"
proof -
have "b > 1" "0 < x"
using that by (auto simp: floorlog_def split: if_splits)
have "b ^ (w - 1)  x" if "b ^ w  x"
proof -
have "b ^ (w - 1)  b ^ w"
using b > 1
by (auto intro!: power_increasing)
also note that
finally show ?thesis .
qed
moreover have "b ^ nat log (real b) (real x)  x" (is "?l  _")
proof -
have "0  log (real b) (real x)"
using b > 1 0 < x
by auto
then have "?l  b powr log (real b) (real x)"
using b > 1
by (auto simp flip: powr_realpow intro!: powr_mono of_nat_floor)
also have " = x" using b > 1 0 < x
by auto
finally show ?thesis
unfolding of_nat_le_iff .
qed
ultimately show ?thesis
using that
by (auto simp: floorlog_def le_nat_iff le_floor_iff le_log_iff powr_realpow
split: if_splits elim!: le_SucE)
qed

subsection ‹Bitlen›

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)"

lemma bitlen_zero [simp]:

by (auto simp: bitlen_def floorlog_def)

lemma bitlen_nonneg:
"0  bitlen x"

lemma bitlen_bounds:
"2 ^ nat (bitlen x - 1)  x  x < 2 ^ nat (bitlen x)" if "x > 0"
proof -
from that have "bitlen x  1" by (auto simp: bitlen_alt_def)
with that 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]:
"bitlen (b * 2 ^ c) = bitlen b + c" if "b > 0"
using that 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"
not_less zero_less_one)

lemma bitlen_div:
"1  real_of_int m / 2^nat (bitlen m - 1)"
and "real_of_int m / 2^nat (bitlen m - 1) < 2" if "0 < m"
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 that have "0  bitlen m - 1" by (auto simp: bitlen_alt_def)

have "m < 2^nat(bitlen m)" using bitlen_bounds[OF that] ..
also from that 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) 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

lemma bitlen_le_iff_floorlog:
"bitlen x  w  w  0  floorlog 2 (nat x)  nat w"
by (auto simp: bitlen_def)

lemma bitlen_le_iff_power:
"bitlen x  w  w  0  x < 2 ^ nat w"
by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff)

lemma less_power_nat_iff_bitlen:
"x < 2 ^ w  bitlen (int x)  w"
using bitlen_le_iff_power[of x w]
by auto

lemma bitlen_ge_iff_power:
"w  bitlen x  w  0  2 ^ (nat w - 1)  x"
unfolding bitlen_def
by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)