author | nipkow |
Thu, 01 Sep 2016 15:57:54 +0200 | |
changeset 63755 | 182c111190e5 |
parent 63540 | f8652d0534fa |
child 63766 | 695d60817cb1 |
permissions | -rw-r--r-- |
59349 | 1 |
(* Author: Florian Haftmann, TU Muenchen *) |
51174 | 2 |
|
60500 | 3 |
section \<open>Common discrete functions\<close> |
51174 | 4 |
|
5 |
theory Discrete |
|
6 |
imports Main |
|
7 |
begin |
|
8 |
||
60500 | 9 |
subsection \<open>Discrete logarithm\<close> |
51174 | 10 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
11 |
context |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
12 |
begin |
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
13 |
|
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
14 |
qualified fun log :: "nat \<Rightarrow> nat" |
59349 | 15 |
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" |
51174 | 16 |
|
61831 | 17 |
lemma log_induct [consumes 1, case_names one double]: |
18 |
fixes n :: nat |
|
19 |
assumes "n > 0" |
|
20 |
assumes one: "P 1" |
|
21 |
assumes double: "\<And>n. n \<ge> 2 \<Longrightarrow> P (n div 2) \<Longrightarrow> P n" |
|
22 |
shows "P n" |
|
61975 | 23 |
using \<open>n > 0\<close> proof (induct n rule: log.induct) |
61831 | 24 |
fix n |
25 |
assume "\<not> n < 2 \<Longrightarrow> |
|
26 |
0 < n div 2 \<Longrightarrow> P (n div 2)" |
|
27 |
then have *: "n \<ge> 2 \<Longrightarrow> P (n div 2)" by simp |
|
28 |
assume "n > 0" |
|
29 |
show "P n" |
|
30 |
proof (cases "n = 1") |
|
63540 | 31 |
case True |
32 |
with one show ?thesis by simp |
|
61831 | 33 |
next |
63540 | 34 |
case False |
35 |
with \<open>n > 0\<close> have "n \<ge> 2" by auto |
|
36 |
with * have "P (n div 2)" . |
|
37 |
with \<open>n \<ge> 2\<close> show ?thesis by (rule double) |
|
61831 | 38 |
qed |
39 |
qed |
|
40 |
||
59349 | 41 |
lemma log_zero [simp]: "log 0 = 0" |
51174 | 42 |
by (simp add: log.simps) |
43 |
||
59349 | 44 |
lemma log_one [simp]: "log 1 = 0" |
51174 | 45 |
by (simp add: log.simps) |
46 |
||
59349 | 47 |
lemma log_Suc_zero [simp]: "log (Suc 0) = 0" |
51174 | 48 |
using log_one by simp |
49 |
||
59349 | 50 |
lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))" |
51174 | 51 |
by (simp add: log.simps) |
52 |
||
59349 | 53 |
lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)" |
51174 | 54 |
by (simp add: log_rec) |
55 |
||
59349 | 56 |
lemma log_half [simp]: "log (n div 2) = log n - 1" |
51174 | 57 |
proof (cases "n < 2") |
58 |
case True |
|
59 |
then have "n = 0 \<or> n = 1" by arith |
|
60 |
then show ?thesis by (auto simp del: One_nat_def) |
|
61 |
next |
|
59349 | 62 |
case False |
63 |
then show ?thesis by (simp add: log_rec) |
|
51174 | 64 |
qed |
65 |
||
59349 | 66 |
lemma log_exp [simp]: "log (2 ^ n) = n" |
51174 | 67 |
by (induct n) simp_all |
68 |
||
59349 | 69 |
lemma log_mono: "mono log" |
51174 | 70 |
proof |
71 |
fix m n :: nat |
|
72 |
assume "m \<le> n" |
|
73 |
then show "log m \<le> log n" |
|
74 |
proof (induct m arbitrary: n rule: log.induct) |
|
75 |
case (1 m) |
|
76 |
then have mn2: "m div 2 \<le> n div 2" by arith |
|
77 |
show "log m \<le> log n" |
|
61831 | 78 |
proof (cases "m \<ge> 2") |
79 |
case False |
|
51174 | 80 |
then have "m = 0 \<or> m = 1" by arith |
81 |
then show ?thesis by (auto simp del: One_nat_def) |
|
82 |
next |
|
61831 | 83 |
case True then have "\<not> m < 2" by simp |
84 |
with mn2 have "n \<ge> 2" by arith |
|
85 |
from True have m2_0: "m div 2 \<noteq> 0" by arith |
|
51174 | 86 |
with mn2 have n2_0: "n div 2 \<noteq> 0" by arith |
61975 | 87 |
from \<open>\<not> m < 2\<close> "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast |
51174 | 88 |
with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp |
60500 | 89 |
with m2_0 n2_0 \<open>m \<ge> 2\<close> \<open>n \<ge> 2\<close> show ?thesis by (simp only: log_rec [of m] log_rec [of n]) simp |
51174 | 90 |
qed |
91 |
qed |
|
92 |
qed |
|
93 |
||
61831 | 94 |
lemma log_exp2_le: |
95 |
assumes "n > 0" |
|
96 |
shows "2 ^ log n \<le> n" |
|
63516 | 97 |
using assms |
98 |
proof (induct n rule: log_induct) |
|
99 |
case one |
|
100 |
then show ?case by simp |
|
61831 | 101 |
next |
63516 | 102 |
case (double n) |
61831 | 103 |
with log_mono have "log n \<ge> Suc 0" |
104 |
by (simp add: log.simps) |
|
105 |
assume "2 ^ log (n div 2) \<le> n div 2" |
|
61975 | 106 |
with \<open>n \<ge> 2\<close> have "2 ^ (log n - Suc 0) \<le> n div 2" by simp |
61831 | 107 |
then have "2 ^ (log n - Suc 0) * 2 ^ 1 \<le> n div 2 * 2" by simp |
61975 | 108 |
with \<open>log n \<ge> Suc 0\<close> have "2 ^ log n \<le> n div 2 * 2" |
61831 | 109 |
unfolding power_add [symmetric] by simp |
110 |
also have "n div 2 * 2 \<le> n" by (cases "even n") simp_all |
|
63516 | 111 |
finally show ?case . |
61831 | 112 |
qed |
113 |
||
51174 | 114 |
|
60500 | 115 |
subsection \<open>Discrete square root\<close> |
51174 | 116 |
|
61115
3a4400985780
modernized name space management -- more uniform qualification;
wenzelm
parents:
60500
diff
changeset
|
117 |
qualified definition sqrt :: "nat \<Rightarrow> nat" |
59349 | 118 |
where "sqrt n = Max {m. m\<^sup>2 \<le> n}" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
119 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
120 |
lemma sqrt_aux: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
121 |
fixes n :: nat |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
122 |
shows "finite {m. m\<^sup>2 \<le> n}" and "{m. m\<^sup>2 \<le> n} \<noteq> {}" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
123 |
proof - |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
124 |
{ fix m |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
125 |
assume "m\<^sup>2 \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
126 |
then have "m \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
127 |
by (cases m) (simp_all add: power2_eq_square) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
128 |
} note ** = this |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
129 |
then have "{m. m\<^sup>2 \<le> n} \<subseteq> {m. m \<le> n}" by auto |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
130 |
then show "finite {m. m\<^sup>2 \<le> n}" by (rule finite_subset) rule |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
131 |
have "0\<^sup>2 \<le> n" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
132 |
then show *: "{m. m\<^sup>2 \<le> n} \<noteq> {}" by blast |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
133 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
134 |
|
59349 | 135 |
lemma [code]: "sqrt n = Max (Set.filter (\<lambda>m. m\<^sup>2 \<le> n) {0..n})" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
136 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
137 |
from power2_nat_le_imp_le [of _ n] have "{m. m \<le> n \<and> m\<^sup>2 \<le> n} = {m. m\<^sup>2 \<le> n}" by auto |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
138 |
then show ?thesis by (simp add: sqrt_def Set.filter_def) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
139 |
qed |
51174 | 140 |
|
59349 | 141 |
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n" |
51174 | 142 |
proof - |
143 |
have "{m. m \<le> n} \<noteq> {}" by auto |
|
144 |
then have "Max {m. m \<le> n} \<le> n" by auto |
|
145 |
then show ?thesis |
|
146 |
by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym) |
|
147 |
qed |
|
148 |
||
59349 | 149 |
lemma sqrt_zero [simp]: "sqrt 0 = 0" |
58787 | 150 |
using sqrt_inverse_power2 [of 0] by simp |
151 |
||
59349 | 152 |
lemma sqrt_one [simp]: "sqrt 1 = 1" |
58787 | 153 |
using sqrt_inverse_power2 [of 1] by simp |
154 |
||
59349 | 155 |
lemma mono_sqrt: "mono sqrt" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
156 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
157 |
fix m n :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
158 |
have *: "0 * 0 \<le> m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
159 |
assume "m \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
160 |
then show "sqrt m \<le> sqrt n" |
60500 | 161 |
by (auto intro!: Max_mono \<open>0 * 0 \<le> m\<close> finite_less_ub simp add: power2_eq_square sqrt_def) |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
162 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
163 |
|
59349 | 164 |
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0" |
51174 | 165 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
166 |
have *: "0 < Max {m. m\<^sup>2 \<le> n} \<longleftrightarrow> (\<exists>a\<in>{m. m\<^sup>2 \<le> n}. 0 < a)" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
167 |
by (rule Max_gr_iff) (fact sqrt_aux)+ |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
168 |
show ?thesis |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
169 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
170 |
assume "0 < sqrt n" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
171 |
then have "0 < Max {m. m\<^sup>2 \<le> n}" by (simp add: sqrt_def) |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
172 |
with * show "0 < n" by (auto dest: power2_nat_le_imp_le) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
173 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
174 |
assume "0 < n" |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
175 |
then have "1\<^sup>2 \<le> n \<and> 0 < (1::nat)" by simp |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
176 |
then have "\<exists>q. q\<^sup>2 \<le> n \<and> 0 < q" .. |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
177 |
with * have "0 < Max {m. m\<^sup>2 \<le> n}" by blast |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
178 |
then show "0 < sqrt n" by (simp add: sqrt_def) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
179 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
180 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
181 |
|
59349 | 182 |
lemma sqrt_power2_le [simp]: "(sqrt n)\<^sup>2 \<le> n" (* FIXME tune proof *) |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
183 |
proof (cases "n > 0") |
58787 | 184 |
case False then show ?thesis by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
185 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
186 |
case True then have "sqrt n > 0" by simp |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
187 |
then have "mono (times (Max {m. m\<^sup>2 \<le> n}))" by (auto intro: mono_times_nat simp add: sqrt_def) |
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
188 |
then have *: "Max {m. m\<^sup>2 \<le> n} * Max {m. m\<^sup>2 \<le> n} = Max (times (Max {m. m\<^sup>2 \<le> n}) ` {m. m\<^sup>2 \<le> n})" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
189 |
using sqrt_aux [of n] by (rule mono_Max_commute) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
190 |
have "Max (op * (Max {m. m * m \<le> n}) ` {m. m * m \<le> n}) \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
191 |
apply (subst Max_le_iff) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
192 |
apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
193 |
apply simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
194 |
apply (metis le0 mult_0_right) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
195 |
apply auto |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
196 |
proof - |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
197 |
fix q |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
198 |
assume "q * q \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
199 |
show "Max {m. m * m \<le> n} * q \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
200 |
proof (cases "q > 0") |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
201 |
case False then show ?thesis by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
202 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
203 |
case True then have "mono (times q)" by (rule mono_times_nat) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
204 |
then have "q * Max {m. m * m \<le> n} = Max (times q ` {m. m * m \<le> n})" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
205 |
using sqrt_aux [of n] by (auto simp add: power2_eq_square intro: mono_Max_commute) |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
53015
diff
changeset
|
206 |
then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps) |
59349 | 207 |
then show ?thesis |
208 |
apply simp |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
209 |
apply (subst Max_le_iff) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
210 |
apply auto |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
211 |
apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
60500 | 212 |
apply (metis \<open>q * q \<le> n\<close>) |
213 |
apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans) |
|
59349 | 214 |
done |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
215 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
216 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
217 |
with * show ?thesis by (simp add: sqrt_def power2_eq_square) |
51174 | 218 |
qed |
219 |
||
59349 | 220 |
lemma sqrt_le: "sqrt n \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
221 |
using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) |
51174 | 222 |
|
223 |
end |
|
224 |
||
62390 | 225 |
end |