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