src/HOL/Library/Log_Nat.thy
 author wenzelm Tue May 15 13:57:39 2018 +0200 (16 months ago) changeset 68189 6163c90694ef parent 67573 ed0a7090167d child 68406 6beb45f6cf67 permissions -rw-r--r--
 nipkow@63663 ` 1` ```(* Title: HOL/Library/Log_Nat.thy ``` nipkow@63663 ` 2` ``` Author: Johannes Hölzl, Fabian Immler ``` nipkow@63663 ` 3` ``` Copyright 2012 TU München ``` nipkow@63663 ` 4` ```*) ``` nipkow@63663 ` 5` nipkow@63663 ` 6` ```section \Logarithm of Natural Numbers\ ``` nipkow@63663 ` 7` nipkow@63663 ` 8` ```theory Log_Nat ``` nipkow@63663 ` 9` ```imports Complex_Main ``` nipkow@63663 ` 10` ```begin ``` nipkow@63663 ` 11` nipkow@63663 ` 12` ```definition floorlog :: "nat \ nat \ nat" where ``` nipkow@63663 ` 13` ```"floorlog b a = (if a > 0 \ b > 1 then nat \log b a\ + 1 else 0)" ``` nipkow@63663 ` 14` nipkow@63663 ` 15` ```lemma floorlog_mono: "x \ y \ floorlog b x \ floorlog b y" ``` nipkow@63663 ` 16` ```by(auto simp: floorlog_def floor_mono nat_mono) ``` nipkow@63663 ` 17` nipkow@63663 ` 18` ```lemma floorlog_bounds: ``` nipkow@63663 ` 19` ``` assumes "x > 0" "b > 1" ``` nipkow@63663 ` 20` ``` shows "b ^ (floorlog b x - 1) \ x \ x < b ^ (floorlog b x)" ``` nipkow@63663 ` 21` ```proof ``` nipkow@63663 ` 22` ``` show "b ^ (floorlog b x - 1) \ x" ``` nipkow@63663 ` 23` ``` proof - ``` nipkow@63663 ` 24` ``` have "b ^ nat \log b x\ = b powr \log b x\" ``` nipkow@63663 ` 25` ``` using powr_realpow[symmetric, of b "nat \log b x\"] \x > 0\ \b > 1\ ``` nipkow@63663 ` 26` ``` by simp ``` nipkow@63663 ` 27` ``` also have "\ \ b powr log b x" using \b > 1\ by simp ``` nipkow@63663 ` 28` ``` also have "\ = real_of_int x" using \0 < x\ \b > 1\ by simp ``` nipkow@63663 ` 29` ``` finally have "b ^ nat \log b x\ \ real_of_int x" by simp ``` nipkow@63663 ` 30` ``` then show ?thesis ``` nipkow@63663 ` 31` ``` using \0 < x\ \b > 1\ of_nat_le_iff ``` nipkow@63663 ` 32` ``` by (fastforce simp add: floorlog_def) ``` nipkow@63663 ` 33` ``` qed ``` nipkow@63663 ` 34` ``` show "x < b ^ (floorlog b x)" ``` nipkow@63663 ` 35` ``` proof - ``` nipkow@63663 ` 36` ``` have "x \ b powr (log b x)" using \x > 0\ \b > 1\ by simp ``` nipkow@63663 ` 37` ``` also have "\ < b powr (\log b x\ + 1)" ``` nipkow@63663 ` 38` ``` using assms by (intro powr_less_mono) auto ``` nipkow@63663 ` 39` ``` also have "\ = b ^ nat (\log b (real_of_int x)\ + 1)" ``` nipkow@63663 ` 40` ``` using assms by (simp add: powr_realpow[symmetric]) ``` nipkow@63663 ` 41` ``` finally ``` nipkow@63663 ` 42` ``` have "x < b ^ nat (\log b (int x)\ + 1)" ``` nipkow@63663 ` 43` ``` by (rule of_nat_less_imp_less) ``` nipkow@63663 ` 44` ``` then show ?thesis ``` nipkow@63663 ` 45` ``` using \x > 0\ \b > 1\ by (simp add: floorlog_def nat_add_distrib) ``` nipkow@63663 ` 46` ``` qed ``` nipkow@63663 ` 47` ```qed ``` nipkow@63663 ` 48` nipkow@63663 ` 49` ```lemma floorlog_power[simp]: ``` nipkow@63663 ` 50` ``` assumes "a > 0" "b > 1" ``` nipkow@63663 ` 51` ``` shows "floorlog b (a * b ^ c) = floorlog b a + c" ``` nipkow@63663 ` 52` ```proof - ``` nipkow@63663 ` 53` ``` have "\log b a + real c\ = \log b a\ + c" by arith ``` nipkow@63663 ` 54` ``` then show ?thesis using assms ``` nipkow@63663 ` 55` ``` by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib) ``` nipkow@63663 ` 56` ```qed ``` nipkow@63663 ` 57` nipkow@63663 ` 58` ```lemma floor_log_add_eqI: ``` nipkow@63663 ` 59` ``` fixes a::nat and b::nat and r::real ``` nipkow@63663 ` 60` ``` assumes "b > 1" "a \ 1" "0 \ r" "r < 1" ``` nipkow@63663 ` 61` ``` shows "\log b (a + r)\ = \log b a\" ``` nipkow@63663 ` 62` ```proof (rule floor_eq2) ``` nipkow@63663 ` 63` ``` have "log b a \ log b (a + r)" using assms by force ``` nipkow@63663 ` 64` ``` then show "\log b a\ \ log b (a + r)" by arith ``` nipkow@63663 ` 65` ```next ``` nipkow@63663 ` 66` ``` define l::int where "l = int b ^ (nat \log b a\ + 1)" ``` nipkow@63663 ` 67` ``` have l_def_real: "l = b powr (\log b a\ + 1)" ``` nipkow@63663 ` 68` ``` using assms by (simp add: l_def powr_add powr_real_of_int) ``` nipkow@63663 ` 69` ``` have "a < l" ``` nipkow@63663 ` 70` ``` proof - ``` nipkow@63663 ` 71` ``` have "a = b powr (log b a)" using assms by simp ``` nipkow@63663 ` 72` ``` also have "\ < b powr floor ((log b a) + 1)" ``` nipkow@63663 ` 73` ``` using assms(1) by auto ``` nipkow@63663 ` 74` ``` also have "\ = l" ``` nipkow@63663 ` 75` ``` using assms by (simp add: l_def powr_real_of_int powr_add) ``` nipkow@63663 ` 76` ``` finally show ?thesis by simp ``` nipkow@63663 ` 77` ``` qed ``` nipkow@63663 ` 78` ``` then have "a + r < l" using assms by simp ``` nipkow@63663 ` 79` ``` then have "log b (a + r) < log b l" using assms by simp ``` nipkow@63663 ` 80` ``` also have "\ = real_of_int \log b a\ + 1" ``` nipkow@63663 ` 81` ``` using assms by (simp add: l_def_real) ``` nipkow@63663 ` 82` ``` finally show "log b (a + r) < real_of_int \log b a\ + 1" . ``` nipkow@63663 ` 83` ```qed ``` nipkow@63663 ` 84` nipkow@63663 ` 85` ```lemma divide_nat_diff_div_nat_less_one: ``` nipkow@63663 ` 86` ``` fixes x b::nat shows "x / b - x div b < 1" ``` nipkow@63663 ` 87` ```proof - ``` nipkow@63663 ` 88` ``` have "int 0 \ \1::real\" by simp ``` nipkow@63663 ` 89` ``` thus ?thesis ``` nipkow@63663 ` 90` ``` by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def ``` nipkow@63663 ` 91` ``` mod_div_trivial real_of_nat_div3 real_of_nat_div_aux) ``` nipkow@63663 ` 92` ```qed ``` nipkow@63663 ` 93` nipkow@63663 ` 94` ```lemma floor_log_div: ``` nipkow@63663 ` 95` ``` fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0" ``` nipkow@63663 ` 96` ``` shows "\log b x\ = \log b (x div b)\ + 1" ``` nipkow@63663 ` 97` ```proof- ``` nipkow@63663 ` 98` ``` have "\log b x\ = \log b (x / b * b)\" using assms by simp ``` nipkow@63663 ` 99` ``` also have "\ = \log b (x / b) + log b b\" ``` nipkow@63663 ` 100` ``` using assms by (subst log_mult) auto ``` nipkow@63663 ` 101` ``` also have "\ = \log b (x / b)\ + 1" using assms by simp ``` nipkow@63663 ` 102` ``` also have "\log b (x / b)\ = \log b (x div b + (x / b - x div b))\" by simp ``` nipkow@63663 ` 103` ``` also have "\ = \log b (x div b)\" ``` nipkow@63663 ` 104` ``` using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one ``` nipkow@63663 ` 105` ``` by (intro floor_log_add_eqI) auto ``` nipkow@63663 ` 106` ``` finally show ?thesis . ``` nipkow@63663 ` 107` ```qed ``` nipkow@63663 ` 108` nipkow@63663 ` 109` ```lemma compute_floorlog[code]: ``` nipkow@63663 ` 110` ``` "floorlog b x = (if x > 0 \ b > 1 then floorlog b (x div b) + 1 else 0)" ``` nipkow@63663 ` 111` ```by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib ``` nipkow@63663 ` 112` ``` intro!: floor_eq2) ``` nipkow@63663 ` 113` nipkow@63663 ` 114` ```lemma floor_log_eq_if: ``` nipkow@63663 ` 115` ``` fixes b x y :: nat ``` nipkow@63663 ` 116` ``` assumes "x div b = y div b" "b > 1" "x > 0" "x div b \ 1" ``` nipkow@63663 ` 117` ``` shows "floor(log b x) = floor(log b y)" ``` nipkow@63663 ` 118` ```proof - ``` nipkow@63663 ` 119` ``` have "y > 0" using assms by(auto intro: ccontr) ``` nipkow@63663 ` 120` ``` thus ?thesis using assms by (simp add: floor_log_div) ``` nipkow@63663 ` 121` ```qed ``` nipkow@63663 ` 122` nipkow@63663 ` 123` ```lemma floorlog_eq_if: ``` nipkow@63663 ` 124` ``` fixes b x y :: nat ``` nipkow@63663 ` 125` ``` assumes "x div b = y div b" "b > 1" "x > 0" "x div b \ 1" ``` nipkow@63663 ` 126` ``` shows "floorlog b x = floorlog b y" ``` nipkow@63663 ` 127` ```proof - ``` nipkow@63663 ` 128` ``` have "y > 0" using assms by(auto intro: ccontr) ``` nipkow@63663 ` 129` ``` thus ?thesis using assms ``` nipkow@63663 ` 130` ``` by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if) ``` nipkow@63663 ` 131` ```qed ``` nipkow@63663 ` 132` nipkow@63663 ` 133` immler@66912 ` 134` ```lemma powr_eq_one_iff[simp]: "a powr x = 1 \ (x = 0)" ``` immler@66912 ` 135` ``` if "a > 1" ``` immler@66912 ` 136` ``` for a x::real ``` immler@66912 ` 137` ``` using that ``` immler@66912 ` 138` ``` by (auto simp: powr_def split: if_splits) ``` immler@66912 ` 139` immler@66912 ` 140` ```lemma floorlog_leD: "floorlog b x \ w \ b > 1 \ x < b ^ w" ``` immler@66912 ` 141` ``` by (metis floorlog_bounds leD linorder_neqE_nat order.strict_trans power_strict_increasing_iff ``` immler@66912 ` 142` ``` zero_less_one zero_less_power) ``` immler@66912 ` 143` immler@66912 ` 144` ```lemma floorlog_leI: "x < b ^ w \ 0 \ w \ b > 1 \ floorlog b x \ w" ``` immler@66912 ` 145` ``` by (drule less_imp_of_nat_less[where 'a=real]) ``` immler@66912 ` 146` ``` (auto simp: floorlog_def Suc_le_eq nat_less_iff floor_less_iff log_of_power_less) ``` immler@66912 ` 147` immler@66912 ` 148` ```lemma floorlog_eq_zero_iff: ``` immler@66912 ` 149` ``` "floorlog b x = 0 \ (b \ 1 \ x \ 0)" ``` immler@66912 ` 150` ``` by (auto simp: floorlog_def) ``` immler@66912 ` 151` immler@66912 ` 152` ```lemma floorlog_le_iff: "floorlog b x \ w \ b \ 1 \ b > 1 \ 0 \ w \ x < b ^ w" ``` immler@66912 ` 153` ``` using floorlog_leD[of b x w] floorlog_leI[of x b w] ``` immler@66912 ` 154` ``` by (auto simp: floorlog_eq_zero_iff[THEN iffD2]) ``` immler@66912 ` 155` immler@66912 ` 156` ```lemma floorlog_ge_SucI: "Suc w \ floorlog b x" if "b ^ w \ x" "b > 1" ``` immler@66912 ` 157` ``` using that le_log_of_power[of b w x] power_not_zero ``` immler@66912 ` 158` ``` by (force simp: floorlog_def Suc_le_eq powr_realpow not_less Suc_nat_eq_nat_zadd1 ``` immler@66912 ` 159` ``` zless_nat_eq_int_zless int_add_floor less_floor_iff ``` immler@66912 ` 160` ``` simp del: floor_add2) ``` immler@66912 ` 161` immler@66912 ` 162` ```lemma floorlog_geI: "w \ floorlog b x" if "b ^ (w - 1) \ x" "b > 1" ``` immler@66912 ` 163` ``` using floorlog_ge_SucI[of b "w - 1" x] that ``` immler@66912 ` 164` ``` by auto ``` immler@66912 ` 165` immler@66912 ` 166` ```lemma floorlog_geD: "b ^ (w - 1) \ x" if "w \ floorlog b x" "w > 0" ``` immler@66912 ` 167` ```proof - ``` immler@66912 ` 168` ``` have "b > 1" "0 < x" ``` immler@66912 ` 169` ``` using that by (auto simp: floorlog_def split: if_splits) ``` immler@66912 ` 170` ``` have "b ^ (w - 1) \ x" if "b ^ w \ x" ``` immler@66912 ` 171` ``` proof - ``` immler@66912 ` 172` ``` have "b ^ (w - 1) \ b ^ w" ``` immler@66912 ` 173` ``` using \b > 1\ ``` immler@66912 ` 174` ``` by (auto intro!: power_increasing) ``` immler@66912 ` 175` ``` also note that ``` immler@66912 ` 176` ``` finally show ?thesis . ``` immler@66912 ` 177` ``` qed ``` immler@66912 ` 178` ``` moreover have "b ^ nat \log (real b) (real x)\ \ x" (is "?l \ _") ``` immler@66912 ` 179` ``` proof - ``` immler@66912 ` 180` ``` have "0 \ log (real b) (real x)" ``` immler@66912 ` 181` ``` using \b > 1\ \0 < x\ ``` immler@66912 ` 182` ``` by (auto simp: ) ``` immler@66912 ` 183` ``` then have "?l \ b powr log (real b) (real x)" ``` immler@66912 ` 184` ``` using \b > 1\ ``` immler@66912 ` 185` ``` by (auto simp add: powr_realpow[symmetric] intro!: powr_mono of_nat_floor) ``` immler@66912 ` 186` ``` also have "\ = x" using \b > 1\ \0 < x\ ``` immler@66912 ` 187` ``` by auto ``` immler@66912 ` 188` ``` finally show ?thesis ``` immler@66912 ` 189` ``` unfolding of_nat_le_iff . ``` immler@66912 ` 190` ``` qed ``` immler@66912 ` 191` ``` ultimately show ?thesis ``` immler@66912 ` 192` ``` using that ``` immler@66912 ` 193` ``` by (auto simp: floorlog_def le_nat_iff le_floor_iff le_log_iff powr_realpow ``` immler@66912 ` 194` ``` split: if_splits elim!: le_SucE) ``` immler@66912 ` 195` ```qed ``` immler@66912 ` 196` immler@66912 ` 197` nipkow@63663 ` 198` ```definition bitlen :: "int \ int" where "bitlen a = floorlog 2 (nat a)" ``` nipkow@63663 ` 199` nipkow@63663 ` 200` ```lemma bitlen_alt_def: "bitlen a = (if a > 0 then \log 2 a\ + 1 else 0)" ``` nipkow@63663 ` 201` ```by (simp add: bitlen_def floorlog_def) ``` nipkow@63663 ` 202` immler@67573 ` 203` ```lemma bitlen_zero[simp]: "bitlen 0 = 0" ``` immler@67573 ` 204` ``` by (auto simp: bitlen_def floorlog_def) ``` immler@67573 ` 205` nipkow@63663 ` 206` ```lemma bitlen_nonneg: "0 \ bitlen x" ``` immler@67573 ` 207` ``` by (simp add: bitlen_def) ``` nipkow@63663 ` 208` nipkow@63663 ` 209` ```lemma bitlen_bounds: ``` nipkow@63663 ` 210` ``` assumes "x > 0" ``` nipkow@63663 ` 211` ``` shows "2 ^ nat (bitlen x - 1) \ x \ x < 2 ^ nat (bitlen x)" ``` nipkow@63663 ` 212` ```proof - ``` nipkow@63663 ` 213` ``` from assms have "bitlen x \ 1" by (auto simp: bitlen_alt_def) ``` nipkow@63663 ` 214` ``` with assms floorlog_bounds[of "nat x" 2] show ?thesis ``` nipkow@63663 ` 215` ``` by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib) ``` nipkow@63663 ` 216` ```qed ``` nipkow@63663 ` 217` nipkow@63663 ` 218` ```lemma bitlen_pow2[simp]: ``` nipkow@63663 ` 219` ``` assumes "b > 0" ``` nipkow@63663 ` 220` ``` shows "bitlen (b * 2 ^ c) = bitlen b + c" ``` nipkow@63663 ` 221` ``` using assms ``` nipkow@63663 ` 222` ``` by (simp add: bitlen_def nat_mult_distrib nat_power_eq) ``` nipkow@63663 ` 223` nipkow@63663 ` 224` ```lemma compute_bitlen[code]: ``` nipkow@63663 ` 225` ``` "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)" ``` nipkow@63663 ` 226` ```by (simp add: bitlen_def nat_div_distrib compute_floorlog) ``` nipkow@63663 ` 227` nipkow@63664 ` 228` ```lemma bitlen_eq_zero_iff: "bitlen x = 0 \ x \ 0" ``` nipkow@63664 ` 229` ```by (auto simp add: bitlen_alt_def) ``` nipkow@63664 ` 230` ``` (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2 ``` nipkow@63664 ` 231` ``` not_less zero_less_one) ``` nipkow@63664 ` 232` nipkow@63664 ` 233` ```lemma bitlen_div: ``` nipkow@63664 ` 234` ``` assumes "0 < m" ``` nipkow@63664 ` 235` ``` shows "1 \ real_of_int m / 2^nat (bitlen m - 1)" ``` nipkow@63664 ` 236` ``` and "real_of_int m / 2^nat (bitlen m - 1) < 2" ``` nipkow@63664 ` 237` ```proof - ``` nipkow@63664 ` 238` ``` let ?B = "2^nat (bitlen m - 1)" ``` nipkow@63664 ` 239` nipkow@63664 ` 240` ``` have "?B \ m" using bitlen_bounds[OF \0 ] .. ``` nipkow@63664 ` 241` ``` then have "1 * ?B \ real_of_int m" ``` nipkow@63664 ` 242` ``` unfolding of_int_le_iff[symmetric] by auto ``` nipkow@63664 ` 243` ``` then show "1 \ real_of_int m / ?B" by auto ``` nipkow@63664 ` 244` nipkow@63664 ` 245` ``` from assms have "m \ 0" by auto ``` nipkow@63664 ` 246` ``` from assms have "0 \ bitlen m - 1" by (auto simp: bitlen_alt_def) ``` nipkow@63664 ` 247` nipkow@63664 ` 248` ``` have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] .. ``` nipkow@63664 ` 249` ``` also from assms have "\ = 2^nat(bitlen m - 1 + 1)" ``` nipkow@63664 ` 250` ``` by (auto simp: bitlen_def) ``` nipkow@63664 ` 251` ``` also have "\ = ?B * 2" ``` nipkow@63664 ` 252` ``` unfolding nat_add_distrib[OF \0 \ bitlen m - 1\ zero_le_one] by auto ``` nipkow@63664 ` 253` ``` finally have "real_of_int m < 2 * ?B" ``` immler@66912 ` 254` ``` by (metis (full_types) mult.commute power.simps(2) of_int_less_numeral_power_cancel_iff) ``` nipkow@63664 ` 255` ``` then have "real_of_int m / ?B < 2 * ?B / ?B" ``` nipkow@63664 ` 256` ``` by (rule divide_strict_right_mono) auto ``` nipkow@63664 ` 257` ``` then show "real_of_int m / ?B < 2" by auto ``` nipkow@63664 ` 258` ```qed ``` nipkow@63664 ` 259` immler@66912 ` 260` ```lemma bitlen_le_iff_floorlog: "bitlen x \ w \ w \ 0 \ floorlog 2 (nat x) \ nat w" ``` immler@66912 ` 261` ``` by (auto simp: bitlen_def) ``` immler@66912 ` 262` immler@66912 ` 263` ```lemma bitlen_le_iff_power: "bitlen x \ w \ w \ 0 \ x < 2 ^ nat w" ``` immler@66912 ` 264` ``` by (auto simp: bitlen_le_iff_floorlog floorlog_le_iff) ``` immler@66912 ` 265` immler@66912 ` 266` ```lemma less_power_nat_iff_bitlen: "x < 2 ^ w \ bitlen (int x) \ w" ``` immler@66912 ` 267` ``` using bitlen_le_iff_power[of x w] ``` immler@66912 ` 268` ``` by auto ``` immler@66912 ` 269` immler@66912 ` 270` ```lemma bitlen_ge_iff_power: "w \ bitlen x \ w \ 0 \ 2 ^ (nat w - 1) \ x" ``` immler@66912 ` 271` ``` unfolding bitlen_def ``` immler@66912 ` 272` ``` by (auto simp: nat_le_iff[symmetric] intro: floorlog_geI dest: floorlog_geD) ``` immler@66912 ` 273` immler@66912 ` 274` ```lemma bitlen_twopow_add_eq: "bitlen (2 ^ w + b) = w + 1" if "0 \ b" "b < 2 ^ w" ``` immler@66912 ` 275` ``` by (auto simp: that nat_add_distrib bitlen_le_iff_power bitlen_ge_iff_power intro!: antisym) ``` immler@66912 ` 276` nipkow@63663 ` 277` ```end ```