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