src/HOL/Library/Log_Nat.thy
 author haftmann Mon Jun 05 15:59:41 2017 +0200 (2017-06-05) changeset 66010 2f7d39285a1a parent 63664 9ddc48a8635e child 66912 a99a7cbf0fb5 permissions -rw-r--r--
executable domain membership checks
 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` nipkow@63663 ` 134` ```definition bitlen :: "int \ int" where "bitlen a = floorlog 2 (nat a)" ``` nipkow@63663 ` 135` nipkow@63663 ` 136` ```lemma bitlen_alt_def: "bitlen a = (if a > 0 then \log 2 a\ + 1 else 0)" ``` nipkow@63663 ` 137` ```by (simp add: bitlen_def floorlog_def) ``` nipkow@63663 ` 138` nipkow@63663 ` 139` ```lemma bitlen_nonneg: "0 \ bitlen x" ``` nipkow@63663 ` 140` ```by (simp add: bitlen_def) ``` nipkow@63663 ` 141` nipkow@63663 ` 142` ```lemma bitlen_bounds: ``` nipkow@63663 ` 143` ``` assumes "x > 0" ``` nipkow@63663 ` 144` ``` shows "2 ^ nat (bitlen x - 1) \ x \ x < 2 ^ nat (bitlen x)" ``` nipkow@63663 ` 145` ```proof - ``` nipkow@63663 ` 146` ``` from assms have "bitlen x \ 1" by (auto simp: bitlen_alt_def) ``` nipkow@63663 ` 147` ``` with assms floorlog_bounds[of "nat x" 2] show ?thesis ``` nipkow@63663 ` 148` ``` by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib) ``` nipkow@63663 ` 149` ```qed ``` nipkow@63663 ` 150` nipkow@63663 ` 151` ```lemma bitlen_pow2[simp]: ``` nipkow@63663 ` 152` ``` assumes "b > 0" ``` nipkow@63663 ` 153` ``` shows "bitlen (b * 2 ^ c) = bitlen b + c" ``` nipkow@63663 ` 154` ``` using assms ``` nipkow@63663 ` 155` ``` by (simp add: bitlen_def nat_mult_distrib nat_power_eq) ``` nipkow@63663 ` 156` nipkow@63663 ` 157` ```lemma compute_bitlen[code]: ``` nipkow@63663 ` 158` ``` "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)" ``` nipkow@63663 ` 159` ```by (simp add: bitlen_def nat_div_distrib compute_floorlog) ``` nipkow@63663 ` 160` nipkow@63664 ` 161` ```lemma bitlen_eq_zero_iff: "bitlen x = 0 \ x \ 0" ``` nipkow@63664 ` 162` ```by (auto simp add: bitlen_alt_def) ``` nipkow@63664 ` 163` ``` (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2 ``` nipkow@63664 ` 164` ``` not_less zero_less_one) ``` nipkow@63664 ` 165` nipkow@63664 ` 166` ```lemma bitlen_div: ``` nipkow@63664 ` 167` ``` assumes "0 < m" ``` nipkow@63664 ` 168` ``` shows "1 \ real_of_int m / 2^nat (bitlen m - 1)" ``` nipkow@63664 ` 169` ``` and "real_of_int m / 2^nat (bitlen m - 1) < 2" ``` nipkow@63664 ` 170` ```proof - ``` nipkow@63664 ` 171` ``` let ?B = "2^nat (bitlen m - 1)" ``` nipkow@63664 ` 172` nipkow@63664 ` 173` ``` have "?B \ m" using bitlen_bounds[OF \0 ] .. ``` nipkow@63664 ` 174` ``` then have "1 * ?B \ real_of_int m" ``` nipkow@63664 ` 175` ``` unfolding of_int_le_iff[symmetric] by auto ``` nipkow@63664 ` 176` ``` then show "1 \ real_of_int m / ?B" by auto ``` nipkow@63664 ` 177` nipkow@63664 ` 178` ``` from assms have "m \ 0" by auto ``` nipkow@63664 ` 179` ``` from assms have "0 \ bitlen m - 1" by (auto simp: bitlen_alt_def) ``` nipkow@63664 ` 180` nipkow@63664 ` 181` ``` have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] .. ``` nipkow@63664 ` 182` ``` also from assms have "\ = 2^nat(bitlen m - 1 + 1)" ``` nipkow@63664 ` 183` ``` by (auto simp: bitlen_def) ``` nipkow@63664 ` 184` ``` also have "\ = ?B * 2" ``` nipkow@63664 ` 185` ``` unfolding nat_add_distrib[OF \0 \ bitlen m - 1\ zero_le_one] by auto ``` nipkow@63664 ` 186` ``` finally have "real_of_int m < 2 * ?B" ``` nipkow@63664 ` 187` ``` by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff) ``` nipkow@63664 ` 188` ``` then have "real_of_int m / ?B < 2 * ?B / ?B" ``` nipkow@63664 ` 189` ``` by (rule divide_strict_right_mono) auto ``` nipkow@63664 ` 190` ``` then show "real_of_int m / ?B < 2" by auto ``` nipkow@63664 ` 191` ```qed ``` nipkow@63664 ` 192` nipkow@63663 ` 193` ```end ```