|
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 add: powr_realpow[symmetric]) |
|
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 definition bitlen :: "int \<Rightarrow> int" where "bitlen a = floorlog 2 (nat a)" |
|
135 |
|
136 lemma bitlen_alt_def: "bitlen a = (if a > 0 then \<lfloor>log 2 a\<rfloor> + 1 else 0)" |
|
137 by (simp add: bitlen_def floorlog_def) |
|
138 |
|
139 lemma bitlen_nonneg: "0 \<le> bitlen x" |
|
140 by (simp add: bitlen_def) |
|
141 |
|
142 lemma bitlen_bounds: |
|
143 assumes "x > 0" |
|
144 shows "2 ^ nat (bitlen x - 1) \<le> x \<and> x < 2 ^ nat (bitlen x)" |
|
145 proof - |
|
146 from assms have "bitlen x \<ge> 1" by (auto simp: bitlen_alt_def) |
|
147 with assms floorlog_bounds[of "nat x" 2] show ?thesis |
|
148 by (auto simp add: bitlen_def le_nat_iff nat_less_iff nat_diff_distrib) |
|
149 qed |
|
150 |
|
151 lemma bitlen_pow2[simp]: |
|
152 assumes "b > 0" |
|
153 shows "bitlen (b * 2 ^ c) = bitlen b + c" |
|
154 using assms |
|
155 by (simp add: bitlen_def nat_mult_distrib nat_power_eq) |
|
156 |
|
157 lemma compute_bitlen[code]: |
|
158 "bitlen x = (if x > 0 then bitlen (x div 2) + 1 else 0)" |
|
159 by (simp add: bitlen_def nat_div_distrib compute_floorlog) |
|
160 |
|
161 end |