src/HOL/Library/Log_Nat.thy
changeset 70349 697450fd25c1
parent 68406 6beb45f6cf67
child 70350 571ae57313a4
     1.1 --- a/src/HOL/Library/Log_Nat.thy	Fri Jun 14 08:34:28 2019 +0000
     1.2 +++ b/src/HOL/Library/Log_Nat.thy	Fri Jun 14 08:34:28 2019 +0000
     1.3 @@ -9,15 +9,37 @@
     1.4  imports Complex_Main
     1.5  begin
     1.6  
     1.7 -definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
     1.8 -"floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
     1.9 +subsection \<open>Preliminaries\<close>
    1.10 +
    1.11 +lemma divide_nat_diff_div_nat_less_one:
    1.12 +  "real x / real b - real (x div b) < 1" for x b :: nat
    1.13 +proof (cases "b = 0")
    1.14 +  case True
    1.15 +  then show ?thesis
    1.16 +    by simp
    1.17 +next
    1.18 +  case False
    1.19 +  then have "real (x div b) + real (x mod b) / real b - real (x div b) < 1"
    1.20 +    by (simp add: field_simps)
    1.21 +  then show ?thesis
    1.22 +    by (simp add: real_of_nat_div_aux [symmetric])
    1.23 +qed
    1.24 +
    1.25 +lemma powr_eq_one_iff [simp]:
    1.26 +  "a powr x = 1 \<longleftrightarrow> x = 0" if "a > 1" for a x :: real
    1.27 +  using that by (auto simp: powr_def split: if_splits)
    1.28 +
    1.29 +
    1.30 +subsection \<open>Floorlog\<close>
    1.31 +
    1.32 +definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat"
    1.33 +  where "floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
    1.34  
    1.35  lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
    1.36 -by(auto simp: floorlog_def floor_mono nat_mono)
    1.37 +  by (auto simp: floorlog_def floor_mono nat_mono)
    1.38  
    1.39  lemma floorlog_bounds:
    1.40 -  assumes "x > 0" "b > 1"
    1.41 -  shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)"
    1.42 +  "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)" if "x > 0" "b > 1"
    1.43  proof
    1.44    show "b ^ (floorlog b x - 1) \<le> x"
    1.45    proof -
    1.46 @@ -35,9 +57,9 @@
    1.47    proof -
    1.48      have "x \<le> b powr (log b x)" using \<open>x > 0\<close> \<open>b > 1\<close> by simp
    1.49      also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
    1.50 -      using assms by (intro powr_less_mono) auto
    1.51 +      using that by (intro powr_less_mono) auto
    1.52      also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
    1.53 -      using assms by (simp flip: powr_realpow)
    1.54 +      using that by (simp flip: powr_realpow)
    1.55      finally
    1.56      have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
    1.57        by (rule of_nat_less_imp_less)
    1.58 @@ -46,124 +68,110 @@
    1.59    qed
    1.60  qed
    1.61  
    1.62 -lemma floorlog_power[simp]:
    1.63 -  assumes "a > 0" "b > 1"
    1.64 -  shows "floorlog b (a * b ^ c) = floorlog b a + c"
    1.65 +lemma floorlog_power [simp]:
    1.66 +  "floorlog b (a * b ^ c) = floorlog b a + c" if "a > 0" "b > 1"
    1.67  proof -
    1.68    have "\<lfloor>log b a + real c\<rfloor> = \<lfloor>log b a\<rfloor> + c" by arith
    1.69 -  then show ?thesis using assms
    1.70 +  then show ?thesis using that
    1.71      by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
    1.72  qed
    1.73  
    1.74  lemma floor_log_add_eqI:
    1.75 -  fixes a::nat and b::nat and r::real
    1.76 -  assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
    1.77 -  shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
    1.78 +  "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>" if "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
    1.79 +    for a b :: nat and r :: real
    1.80  proof (rule floor_eq2)
    1.81 -  have "log b a \<le> log b (a + r)" using assms by force
    1.82 +  have "log b a \<le> log b (a + r)" using that by force
    1.83    then show "\<lfloor>log b a\<rfloor> \<le> log b (a + r)" by arith
    1.84  next
    1.85    define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)"
    1.86    have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)"
    1.87 -    using assms by (simp add: l_def powr_add powr_real_of_int)
    1.88 +    using that by (simp add: l_def powr_add powr_real_of_int)
    1.89    have "a < l"
    1.90    proof -
    1.91 -    have "a = b powr (log b a)" using assms by simp
    1.92 +    have "a = b powr (log b a)" using that by simp
    1.93      also have "\<dots> < b powr floor ((log b a) + 1)"
    1.94 -      using assms(1) by auto
    1.95 +      using that(1) by auto
    1.96      also have "\<dots> = l"
    1.97 -      using assms by (simp add: l_def powr_real_of_int powr_add)
    1.98 +      using that by (simp add: l_def powr_real_of_int powr_add)
    1.99      finally show ?thesis by simp
   1.100    qed
   1.101 -  then have "a + r < l" using assms by simp
   1.102 -  then have "log b (a + r) < log b l" using assms by simp
   1.103 +  then have "a + r < l" using that by simp
   1.104 +  then have "log b (a + r) < log b l" using that by simp
   1.105    also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1"
   1.106 -    using assms by (simp add: l_def_real)
   1.107 +    using that by (simp add: l_def_real)
   1.108    finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
   1.109  qed
   1.110  
   1.111 -lemma divide_nat_diff_div_nat_less_one:
   1.112 -  fixes x b::nat shows "x / b - x div b < 1"
   1.113 -proof -
   1.114 -  have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
   1.115 -  thus ?thesis
   1.116 -    by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
   1.117 -        mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
   1.118 -qed
   1.119 -
   1.120  lemma floor_log_div:
   1.121 -  fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
   1.122 -  shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
   1.123 +  "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1" if "b > 1" "x > 0" "x div b > 0"
   1.124 +    for b x :: nat
   1.125  proof-
   1.126 -  have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using assms by simp
   1.127 +  have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using that by simp
   1.128    also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
   1.129 -    using assms by (subst log_mult) auto
   1.130 -  also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
   1.131 +    using that by (subst log_mult) auto
   1.132 +  also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using that by simp
   1.133    also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>" by simp
   1.134    also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
   1.135 -    using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
   1.136 +    using that real_of_nat_div4 divide_nat_diff_div_nat_less_one
   1.137      by (intro floor_log_add_eqI) auto
   1.138    finally show ?thesis .
   1.139  qed
   1.140  
   1.141 -lemma compute_floorlog[code]:
   1.142 +lemma compute_floorlog [code]:
   1.143    "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
   1.144 -by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
   1.145 +  by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
   1.146      intro!: floor_eq2)
   1.147  
   1.148  lemma floor_log_eq_if:
   1.149 -  fixes b x y :: nat
   1.150 -  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   1.151 -  shows "floor(log b x) = floor(log b y)"
   1.152 +  "\<lfloor>log b x\<rfloor> = \<lfloor>log b y\<rfloor>" if "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   1.153 +    for b x y :: nat
   1.154  proof -
   1.155 -  have "y > 0" using assms by(auto intro: ccontr)
   1.156 -  thus ?thesis using assms by (simp add: floor_log_div)
   1.157 +  have "y > 0" using that by (auto intro: ccontr)
   1.158 +  thus ?thesis using that by (simp add: floor_log_div)
   1.159  qed
   1.160  
   1.161  lemma floorlog_eq_if:
   1.162 -  fixes b x y :: nat
   1.163 -  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   1.164 -  shows "floorlog b x = floorlog b y"
   1.165 +  "floorlog b x = floorlog b y" if "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
   1.166 +    for b x y :: nat
   1.167  proof -
   1.168 -  have "y > 0" using assms by(auto intro: ccontr)
   1.169 -  thus ?thesis using assms
   1.170 -    by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
   1.171 +  have "y > 0" using that by (auto intro: ccontr)
   1.172 +  then show ?thesis using that
   1.173 +    by (auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
   1.174  qed
   1.175  
   1.176 -
   1.177 -lemma powr_eq_one_iff[simp]: "a powr x = 1 \<longleftrightarrow> (x = 0)"
   1.178 -  if "a > 1"
   1.179 -  for a x::real
   1.180 -  using that
   1.181 -  by (auto simp: powr_def split: if_splits)
   1.182 -
   1.183 -lemma floorlog_leD: "floorlog b x \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> x < b ^ w"
   1.184 +lemma floorlog_leD:
   1.185 +  "floorlog b x \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> x < b ^ w"
   1.186    by (metis floorlog_bounds leD linorder_neqE_nat order.strict_trans power_strict_increasing_iff
   1.187        zero_less_one zero_less_power)
   1.188  
   1.189 -lemma floorlog_leI: "x < b ^ w \<Longrightarrow> 0 \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> floorlog b x \<le> w"
   1.190 +lemma floorlog_leI:
   1.191 +  "x < b ^ w \<Longrightarrow> 0 \<le> w \<Longrightarrow> b > 1 \<Longrightarrow> floorlog b x \<le> w"
   1.192    by (drule less_imp_of_nat_less[where 'a=real])
   1.193      (auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less)
   1.194  
   1.195  lemma floorlog_eq_zero_iff:
   1.196 -  "floorlog b x = 0 \<longleftrightarrow> (b \<le> 1 \<or> x \<le> 0)"
   1.197 +  "floorlog b x = 0 \<longleftrightarrow> b \<le> 1 \<or> x \<le> 0"
   1.198    by (auto simp: floorlog_def)
   1.199  
   1.200 -lemma floorlog_le_iff: "floorlog b x \<le> w \<longleftrightarrow> b \<le> 1 \<or> b > 1 \<and> 0 \<le> w \<and> x < b ^ w"
   1.201 +lemma floorlog_le_iff:
   1.202 +  "floorlog b x \<le> w \<longleftrightarrow> b \<le> 1 \<or> b > 1 \<and> 0 \<le> w \<and> x < b ^ w"
   1.203    using floorlog_leD[of b x w] floorlog_leI[of x b w]
   1.204    by (auto simp: floorlog_eq_zero_iff[THEN iffD2])
   1.205  
   1.206 -lemma floorlog_ge_SucI: "Suc w \<le> floorlog b x" if "b ^ w \<le> x" "b > 1"
   1.207 +lemma floorlog_ge_SucI:
   1.208 +  "Suc w \<le> floorlog b x" if "b ^ w \<le> x" "b > 1"
   1.209    using that le_log_of_power[of b w x] power_not_zero
   1.210    by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1
   1.211        zless_nat_eq_int_zless int_add_floor less_floor_iff
   1.212        simp del: floor_add2)
   1.213  
   1.214 -lemma floorlog_geI: "w \<le> floorlog b x" if "b ^ (w - 1) \<le> x" "b > 1"
   1.215 +lemma floorlog_geI:
   1.216 +  "w \<le> floorlog b x" if "b ^ (w - 1) \<le> x" "b > 1"
   1.217    using floorlog_ge_SucI[of b "w - 1" x] that
   1.218    by auto
   1.219  
   1.220 -lemma floorlog_geD: "b ^ (w - 1) \<le> x" if "w \<le> floorlog b x" "w > 0"
   1.221 +lemma floorlog_geD:
   1.222 +  "b ^ (w - 1) \<le> x" if "w \<le> floorlog b x" "w > 0"
   1.223  proof -
   1.224    have "b > 1" "0 < x"
   1.225      using that by (auto simp: floorlog_def split: if_splits)
   1.226 @@ -195,45 +203,48 @@
   1.227  qed
   1.228  
   1.229  
   1.230 -definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
   1.231 +subsection \<open>Bitlen\<close>
   1.232 +
   1.233 +definition bitlen :: "int \<Rightarrow> int"
   1.234 +  where "bitlen a = floorlog 2 (nat a)"
   1.235  
   1.236 -lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   1.237 -by (simp add: bitlen_def floorlog_def)
   1.238 +lemma bitlen_alt_def:
   1.239 +  "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
   1.240 +  by (simp add: bitlen_def floorlog_def)
   1.241  
   1.242 -lemma bitlen_zero[simp]: "bitlen 0 = 0"
   1.243 +lemma bitlen_zero [simp]:
   1.244 +  "bitlen 0 = 0"
   1.245    by (auto simp: bitlen_def floorlog_def)
   1.246  
   1.247 -lemma bitlen_nonneg: "0 \<le> bitlen x"
   1.248 +lemma bitlen_nonneg:
   1.249 +  "0 \<le> bitlen x"
   1.250    by (simp add: bitlen_def)
   1.251  
   1.252  lemma bitlen_bounds:
   1.253 -  assumes "x > 0"
   1.254 -  shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
   1.255 +  "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)" if "x > 0"
   1.256  proof -
   1.257 -  from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
   1.258 -  with assms floorlog_bounds[of "nat x" 2] show ?thesis
   1.259 +  from that have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
   1.260 +  with that floorlog_bounds[of "nat x" 2] show ?thesis
   1.261      by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
   1.262  qed
   1.263  
   1.264 -lemma bitlen_pow2[simp]:
   1.265 -  assumes "b > 0"
   1.266 -  shows "bitlen (b * 2 ^ c) = bitlen b + c"
   1.267 -  using assms
   1.268 -  by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
   1.269 +lemma bitlen_pow2 [simp]:
   1.270 +  "bitlen (b * 2 ^ c) = bitlen b + c" if "b > 0"
   1.271 +  using that by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
   1.272  
   1.273 -lemma compute_bitlen[code]:
   1.274 +lemma compute_bitlen [code]:
   1.275    "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
   1.276 -by (simp add: bitlen_def nat_div_distrib compute_floorlog)
   1.277 +  by (simp add: bitlen_def nat_div_distrib compute_floorlog)
   1.278  
   1.279 -lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
   1.280 -by (auto simp add: bitlen_alt_def)
   1.281 +lemma bitlen_eq_zero_iff:
   1.282 +  "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
   1.283 +  by (auto simp add: bitlen_alt_def)
   1.284     (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
   1.285        not_less zero_less_one)
   1.286  
   1.287  lemma bitlen_div:
   1.288 -  assumes "0 < m"
   1.289 -  shows "1 \<le> real_of_int m / 2^nat (bitlen m - 1)"
   1.290 -    and "real_of_int m / 2^nat (bitlen m - 1) < 2"
   1.291 +  "1 \<le> real_of_int m / 2^nat (bitlen m - 1)"
   1.292 +    and "real_of_int m / 2^nat (bitlen m - 1) < 2" if "0 < m"
   1.293  proof -
   1.294    let ?B = "2^nat (bitlen m - 1)"
   1.295  
   1.296 @@ -242,11 +253,10 @@
   1.297      unfolding of_int_le_iff[symmetric] by auto
   1.298    then show "1 \<le> real_of_int m / ?B" by auto
   1.299  
   1.300 -  from assms have "m \<noteq> 0" by auto
   1.301 -  from assms have "0 \<le> bitlen m - 1" by (auto simp: bitlen_alt_def)
   1.302 +  from that have "0 \<le> bitlen m - 1" by (auto simp: bitlen_alt_def)
   1.303  
   1.304 -  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] ..
   1.305 -  also from assms have "\<dots> = 2^nat(bitlen m - 1 + 1)"
   1.306 +  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF that] ..
   1.307 +  also from that have "\<dots> = 2^nat(bitlen m - 1 + 1)"
   1.308      by (auto simp: bitlen_def)
   1.309    also have "\<dots> = ?B * 2"
   1.310      unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
   1.311 @@ -257,21 +267,26 @@
   1.312    then show "real_of_int m / ?B < 2" by auto
   1.313  qed
   1.314  
   1.315 -lemma bitlen_le_iff_floorlog: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> floorlog 2 (nat x) \<le> nat w"
   1.316 +lemma bitlen_le_iff_floorlog:
   1.317 +  "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> floorlog 2 (nat x) \<le> nat w"
   1.318    by (auto simp: bitlen_def)
   1.319  
   1.320 -lemma bitlen_le_iff_power: "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> x < 2 ^ nat w"
   1.321 +lemma bitlen_le_iff_power:
   1.322 +  "bitlen x \<le> w \<longleftrightarrow> w \<ge> 0 \<and> x < 2 ^ nat w"
   1.323    by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff)
   1.324  
   1.325 -lemma less_power_nat_iff_bitlen: "x < 2 ^ w \<longleftrightarrow> bitlen (int x) \<le> w"
   1.326 +lemma less_power_nat_iff_bitlen:
   1.327 +  "x < 2 ^ w \<longleftrightarrow> bitlen (int x) \<le> w"
   1.328    using bitlen_le_iff_power[of x w]
   1.329    by auto
   1.330  
   1.331 -lemma bitlen_ge_iff_power: "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
   1.332 +lemma bitlen_ge_iff_power:
   1.333 +  "w \<le> bitlen x \<longleftrightarrow> w \<le> 0 \<or> 2 ^ (nat w - 1) \<le> x"
   1.334    unfolding bitlen_def
   1.335    by (auto simp flip: nat_le_iff intro: floorlog_geI dest: floorlog_geD)
   1.336  
   1.337 -lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
   1.338 +lemma bitlen_twopow_add_eq:
   1.339 +  "bitlen (2 ^ w + b) = w + 1" if "0 \<le> b" "b < 2 ^ w"
   1.340    by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym)
   1.341  
   1.342  end