src/HOL/Library/Log_Nat.thy
author nipkow
Fri, 12 Aug 2016 09:57:09 +0200
changeset 63664 9ddc48a8635e
parent 63663 28d1deca302e
child 66912 a99a7cbf0fb5
permissions -rw-r--r--
tuned
Ignore whitespace changes - Everywhere: Within whitespace: At end of lines:
63663
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     1
(*  Title:      HOL/Library/Log_Nat.thy
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     2
    Author:     Johannes Hölzl, Fabian Immler
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     3
    Copyright   2012  TU München
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     4
*)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     5
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     6
section \<open>Logarithm of Natural Numbers\<close>
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     7
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     8
theory Log_Nat
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
     9
imports Complex_Main
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    10
begin
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    11
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    12
definition floorlog :: "nat \<Rightarrow> nat \<Rightarrow> nat" where
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    13
"floorlog b a = (if a > 0 \<and> b > 1 then nat \<lfloor>log b a\<rfloor> + 1 else 0)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    14
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    15
lemma floorlog_mono: "x \<le> y \<Longrightarrow> floorlog b x \<le> floorlog b y"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    16
by(auto simp: floorlog_def floor_mono nat_mono)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    17
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    18
lemma floorlog_bounds:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    19
  assumes "x > 0" "b > 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    20
  shows "b ^ (floorlog b x - 1) \<le> x \<and> x < b ^ (floorlog b x)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    21
proof
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    22
  show "b ^ (floorlog b x - 1) \<le> x"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    23
  proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    24
    have "b ^ nat \<lfloor>log b x\<rfloor> = b powr \<lfloor>log b x\<rfloor>"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    25
      using powr_realpow[symmetric, of b "nat \<lfloor>log b x\<rfloor>"] \<open>x > 0\<close> \<open>b > 1\<close>
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    26
      by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    27
    also have "\<dots> \<le> b powr log b x" using \<open>b > 1\<close> by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    28
    also have "\<dots> = real_of_int x" using \<open>0 < x\<close> \<open>b > 1\<close> by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    29
    finally have "b ^ nat \<lfloor>log b x\<rfloor> \<le> real_of_int x" by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    30
    then show ?thesis
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    31
      using \<open>0 < x\<close> \<open>b > 1\<close> of_nat_le_iff
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    32
      by (fastforce simp add: floorlog_def)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    33
  qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    34
  show "x < b ^ (floorlog b x)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    35
  proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    36
    have "x \<le> b powr (log b x)" using \<open>x > 0\<close> \<open>b > 1\<close> by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    37
    also have "\<dots> < b powr (\<lfloor>log b x\<rfloor> + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    38
      using assms by (intro powr_less_mono) auto
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    39
    also have "\<dots> = b ^ nat (\<lfloor>log b (real_of_int x)\<rfloor> + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    40
      using assms by (simp add: powr_realpow[symmetric])
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    41
    finally
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    42
    have "x < b ^ nat (\<lfloor>log b (int x)\<rfloor> + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    43
      by (rule of_nat_less_imp_less)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    44
    then show ?thesis
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    45
      using \<open>x > 0\<close> \<open>b > 1\<close> by (simp add: floorlog_def nat_add_distrib)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    46
  qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    47
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    48
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    49
lemma floorlog_power[simp]:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    50
  assumes "a > 0" "b > 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    51
  shows "floorlog b (a * b ^ c) = floorlog b a + c"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    52
proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    53
  have "\<lfloor>log b a + real c\<rfloor> = \<lfloor>log b a\<rfloor> + c" by arith
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    54
  then show ?thesis using assms
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    55
    by (auto simp: floorlog_def log_mult powr_realpow[symmetric] nat_add_distrib)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    56
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    57
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    58
lemma floor_log_add_eqI:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    59
  fixes a::nat and b::nat and r::real
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    60
  assumes "b > 1" "a \<ge> 1" "0 \<le> r" "r < 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    61
  shows "\<lfloor>log b (a + r)\<rfloor> = \<lfloor>log b a\<rfloor>"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    62
proof (rule floor_eq2)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    63
  have "log b a \<le> log b (a + r)" using assms by force
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    64
  then show "\<lfloor>log b a\<rfloor> \<le> log b (a + r)" by arith
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    65
next
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    66
  define l::int where "l = int b ^ (nat \<lfloor>log b a\<rfloor> + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    67
  have l_def_real: "l = b powr (\<lfloor>log b a\<rfloor> + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    68
    using assms by (simp add: l_def powr_add powr_real_of_int)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    69
  have "a < l"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    70
  proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    71
    have "a = b powr (log b a)" using assms by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    72
    also have "\<dots> < b powr floor ((log b a) + 1)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    73
      using assms(1) by auto
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    74
    also have "\<dots> = l"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    75
      using assms by (simp add: l_def powr_real_of_int powr_add)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    76
    finally show ?thesis by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    77
  qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    78
  then have "a + r < l" using assms by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    79
  then have "log b (a + r) < log b l" using assms by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    80
  also have "\<dots> = real_of_int \<lfloor>log b a\<rfloor> + 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    81
    using assms by (simp add: l_def_real)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    82
  finally show "log b (a + r) < real_of_int \<lfloor>log b a\<rfloor> + 1" .
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    83
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    84
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    85
lemma divide_nat_diff_div_nat_less_one:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    86
  fixes x b::nat shows "x / b - x div b < 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    87
proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    88
  have "int 0 \<noteq> \<lfloor>1::real\<rfloor>" by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    89
  thus ?thesis
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    90
    by (metis add_diff_cancel_left' floor_divide_of_nat_eq less_eq_real_def
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    91
        mod_div_trivial real_of_nat_div3 real_of_nat_div_aux)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    92
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    93
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    94
lemma floor_log_div:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    95
  fixes b x :: nat assumes "b > 1" "x > 0" "x div b > 0"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    96
  shows "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x div b)\<rfloor> + 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    97
proof-
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    98
  have "\<lfloor>log b x\<rfloor> = \<lfloor>log b (x / b * b)\<rfloor>" using assms by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
    99
  also have "\<dots> = \<lfloor>log b (x / b) + log b b\<rfloor>"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   100
    using assms by (subst log_mult) auto
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   101
  also have "\<dots> = \<lfloor>log b (x / b)\<rfloor> + 1" using assms by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   102
  also have "\<lfloor>log b (x / b)\<rfloor> = \<lfloor>log b (x div b + (x / b - x div b))\<rfloor>" by simp
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   103
  also have "\<dots> = \<lfloor>log b (x div b)\<rfloor>"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   104
    using assms real_of_nat_div4 divide_nat_diff_div_nat_less_one
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   105
    by (intro floor_log_add_eqI) auto
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   106
  finally show ?thesis .
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   107
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   108
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   109
lemma compute_floorlog[code]:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   110
  "floorlog b x = (if x > 0 \<and> b > 1 then floorlog b (x div b) + 1 else 0)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   111
by (auto simp: floorlog_def floor_log_div[of b x] div_eq_0_iff nat_add_distrib
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   112
    intro!: floor_eq2)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   113
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   114
lemma floor_log_eq_if:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   115
  fixes b x y :: nat
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   116
  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   117
  shows "floor(log b x) = floor(log b y)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   118
proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   119
  have "y > 0" using assms by(auto intro: ccontr)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   120
  thus ?thesis using assms by (simp add: floor_log_div)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   121
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   122
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   123
lemma floorlog_eq_if:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   124
  fixes b x y :: nat
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   125
  assumes "x div b = y div b" "b > 1" "x > 0" "x div b \<ge> 1"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   126
  shows "floorlog b x = floorlog b y"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   127
proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   128
  have "y > 0" using assms by(auto intro: ccontr)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   129
  thus ?thesis using assms
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   130
    by(auto simp add: floorlog_def eq_nat_nat_iff intro: floor_log_eq_if)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   131
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   132
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   133
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   134
definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   135
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   136
lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   137
by (simp add: bitlen_def floorlog_def)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   138
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   139
lemma bitlen_nonneg: "0 \<le> bitlen x"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   140
by (simp add: bitlen_def)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   141
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   142
lemma bitlen_bounds:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   143
  assumes "x > 0"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   144
  shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   145
proof -
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   146
  from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   147
  with assms floorlog_bounds[of "nat x" 2] show ?thesis
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   148
    by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   149
qed
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   150
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   151
lemma bitlen_pow2[simp]:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   152
  assumes "b > 0"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   153
  shows "bitlen (b * 2 ^ c) = bitlen b + c"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   154
  using assms
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   155
  by (simp add: bitlen_def nat_mult_distrib nat_power_eq)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   156
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   157
lemma compute_bitlen[code]:
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   158
  "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)"
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   159
by (simp add: bitlen_def nat_div_distrib compute_floorlog)
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   160
63664
nipkow
parents: 63663
diff changeset
   161
lemma bitlen_eq_zero_iff: "bitlen x = 0 \<longleftrightarrow> x \<le> 0"
nipkow
parents: 63663
diff changeset
   162
by (auto simp add: bitlen_alt_def)
nipkow
parents: 63663
diff changeset
   163
   (metis compute_bitlen add.commute bitlen_alt_def bitlen_nonneg less_add_same_cancel2
nipkow
parents: 63663
diff changeset
   164
      not_less zero_less_one)
nipkow
parents: 63663
diff changeset
   165
nipkow
parents: 63663
diff changeset
   166
lemma bitlen_div:
nipkow
parents: 63663
diff changeset
   167
  assumes "0 < m"
nipkow
parents: 63663
diff changeset
   168
  shows "1 \<le> real_of_int m / 2^nat (bitlen m - 1)"
nipkow
parents: 63663
diff changeset
   169
    and "real_of_int m / 2^nat (bitlen m - 1) < 2"
nipkow
parents: 63663
diff changeset
   170
proof -
nipkow
parents: 63663
diff changeset
   171
  let ?B = "2^nat (bitlen m - 1)"
nipkow
parents: 63663
diff changeset
   172
nipkow
parents: 63663
diff changeset
   173
  have "?B \<le> m" using bitlen_bounds[OF \<open>0 <m\<close>] ..
nipkow
parents: 63663
diff changeset
   174
  then have "1 * ?B \<le> real_of_int m"
nipkow
parents: 63663
diff changeset
   175
    unfolding of_int_le_iff[symmetric] by auto
nipkow
parents: 63663
diff changeset
   176
  then show "1 \<le> real_of_int m / ?B" by auto
nipkow
parents: 63663
diff changeset
   177
nipkow
parents: 63663
diff changeset
   178
  from assms have "m \<noteq> 0" by auto
nipkow
parents: 63663
diff changeset
   179
  from assms have "0 \<le> bitlen m - 1" by (auto simp: bitlen_alt_def)
nipkow
parents: 63663
diff changeset
   180
nipkow
parents: 63663
diff changeset
   181
  have "m < 2^nat(bitlen m)" using bitlen_bounds[OF assms] ..
nipkow
parents: 63663
diff changeset
   182
  also from assms have "\<dots> = 2^nat(bitlen m - 1 + 1)"
nipkow
parents: 63663
diff changeset
   183
    by (auto simp: bitlen_def)
nipkow
parents: 63663
diff changeset
   184
  also have "\<dots> = ?B * 2"
nipkow
parents: 63663
diff changeset
   185
    unfolding nat_add_distrib[OF \<open>0 \<le> bitlen m - 1\<close> zero_le_one] by auto
nipkow
parents: 63663
diff changeset
   186
  finally have "real_of_int m < 2 * ?B"
nipkow
parents: 63663
diff changeset
   187
    by (metis (full_types) mult.commute power.simps(2) real_of_int_less_numeral_power_cancel_iff)
nipkow
parents: 63663
diff changeset
   188
  then have "real_of_int m / ?B < 2 * ?B / ?B"
nipkow
parents: 63663
diff changeset
   189
    by (rule divide_strict_right_mono) auto
nipkow
parents: 63663
diff changeset
   190
  then show "real_of_int m / ?B < 2" by auto
nipkow
parents: 63663
diff changeset
   191
qed
nipkow
parents: 63663
diff changeset
   192
63663
28d1deca302e Extracted floorlog and bitlen to separate theory Log_Nat
nipkow
parents:
diff changeset
   193
end