author | wenzelm |
Mon, 06 Jul 2015 22:06:02 +0200 | |
changeset 60678 | 17ba2df56dee |
parent 60500 | 903bb1495239 |
child 61115 | 3a4400985780 |
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 |
|
59349 | 11 |
fun log :: "nat \<Rightarrow> nat" |
12 |
where [simp del]: "log n = (if n < 2 then 0 else Suc (log (n div 2)))" |
|
51174 | 13 |
|
59349 | 14 |
lemma log_zero [simp]: "log 0 = 0" |
51174 | 15 |
by (simp add: log.simps) |
16 |
||
59349 | 17 |
lemma log_one [simp]: "log 1 = 0" |
51174 | 18 |
by (simp add: log.simps) |
19 |
||
59349 | 20 |
lemma log_Suc_zero [simp]: "log (Suc 0) = 0" |
51174 | 21 |
using log_one by simp |
22 |
||
59349 | 23 |
lemma log_rec: "n \<ge> 2 \<Longrightarrow> log n = Suc (log (n div 2))" |
51174 | 24 |
by (simp add: log.simps) |
25 |
||
59349 | 26 |
lemma log_twice [simp]: "n \<noteq> 0 \<Longrightarrow> log (2 * n) = Suc (log n)" |
51174 | 27 |
by (simp add: log_rec) |
28 |
||
59349 | 29 |
lemma log_half [simp]: "log (n div 2) = log n - 1" |
51174 | 30 |
proof (cases "n < 2") |
31 |
case True |
|
32 |
then have "n = 0 \<or> n = 1" by arith |
|
33 |
then show ?thesis by (auto simp del: One_nat_def) |
|
34 |
next |
|
59349 | 35 |
case False |
36 |
then show ?thesis by (simp add: log_rec) |
|
51174 | 37 |
qed |
38 |
||
59349 | 39 |
lemma log_exp [simp]: "log (2 ^ n) = n" |
51174 | 40 |
by (induct n) simp_all |
41 |
||
59349 | 42 |
lemma log_mono: "mono log" |
51174 | 43 |
proof |
44 |
fix m n :: nat |
|
45 |
assume "m \<le> n" |
|
46 |
then show "log m \<le> log n" |
|
47 |
proof (induct m arbitrary: n rule: log.induct) |
|
48 |
case (1 m) |
|
49 |
then have mn2: "m div 2 \<le> n div 2" by arith |
|
50 |
show "log m \<le> log n" |
|
51 |
proof (cases "m < 2") |
|
52 |
case True |
|
53 |
then have "m = 0 \<or> m = 1" by arith |
|
54 |
then show ?thesis by (auto simp del: One_nat_def) |
|
55 |
next |
|
56 |
case False |
|
57 |
with mn2 have "m \<ge> 2" and "n \<ge> 2" by auto arith |
|
58 |
from False have m2_0: "m div 2 \<noteq> 0" by arith |
|
59 |
with mn2 have n2_0: "n div 2 \<noteq> 0" by arith |
|
60 |
from False "1.hyps" mn2 have "log (m div 2) \<le> log (n div 2)" by blast |
|
61 |
with m2_0 n2_0 have "log (2 * (m div 2)) \<le> log (2 * (n div 2))" by simp |
|
60500 | 62 |
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 | 63 |
qed |
64 |
qed |
|
65 |
qed |
|
66 |
||
67 |
||
60500 | 68 |
subsection \<open>Discrete square root\<close> |
51174 | 69 |
|
70 |
definition sqrt :: "nat \<Rightarrow> nat" |
|
59349 | 71 |
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
|
72 |
|
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
73 |
lemma sqrt_aux: |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
74 |
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
|
75 |
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
|
76 |
proof - |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
77 |
{ fix m |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
78 |
assume "m\<^sup>2 \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
79 |
then have "m \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
80 |
by (cases m) (simp_all add: power2_eq_square) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
81 |
} note ** = this |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
82 |
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
|
83 |
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
|
84 |
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
|
85 |
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
|
86 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
87 |
|
59349 | 88 |
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
|
89 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
90 |
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
|
91 |
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
|
92 |
qed |
51174 | 93 |
|
59349 | 94 |
lemma sqrt_inverse_power2 [simp]: "sqrt (n\<^sup>2) = n" |
51174 | 95 |
proof - |
96 |
have "{m. m \<le> n} \<noteq> {}" by auto |
|
97 |
then have "Max {m. m \<le> n} \<le> n" by auto |
|
98 |
then show ?thesis |
|
99 |
by (auto simp add: sqrt_def power2_nat_le_eq_le intro: antisym) |
|
100 |
qed |
|
101 |
||
59349 | 102 |
lemma sqrt_zero [simp]: "sqrt 0 = 0" |
58787 | 103 |
using sqrt_inverse_power2 [of 0] by simp |
104 |
||
59349 | 105 |
lemma sqrt_one [simp]: "sqrt 1 = 1" |
58787 | 106 |
using sqrt_inverse_power2 [of 1] by simp |
107 |
||
59349 | 108 |
lemma mono_sqrt: "mono sqrt" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
109 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
110 |
fix m n :: nat |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
111 |
have *: "0 * 0 \<le> m" by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
112 |
assume "m \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
113 |
then show "sqrt m \<le> sqrt n" |
60500 | 114 |
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
|
115 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
116 |
|
59349 | 117 |
lemma sqrt_greater_zero_iff [simp]: "sqrt n > 0 \<longleftrightarrow> n > 0" |
51174 | 118 |
proof - |
53015
a1119cf551e8
standardized symbols via "isabelle update_sub_sup", excluding src/Pure and src/Tools/WWW_Find;
wenzelm
parents:
51263
diff
changeset
|
119 |
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
|
120 |
by (rule Max_gr_iff) (fact sqrt_aux)+ |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
121 |
show ?thesis |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
122 |
proof |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
123 |
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
|
124 |
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
|
125 |
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
|
126 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
127 |
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
|
128 |
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
|
129 |
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
|
130 |
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
|
131 |
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
|
132 |
qed |
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 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
|
136 |
proof (cases "n > 0") |
58787 | 137 |
case False then show ?thesis by simp |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
138 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
139 |
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
|
140 |
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
|
141 |
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
|
142 |
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
|
143 |
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
|
144 |
apply (subst Max_le_iff) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
145 |
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
|
146 |
apply simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
147 |
apply (metis le0 mult_0_right) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
148 |
apply auto |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
149 |
proof - |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
150 |
fix q |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
151 |
assume "q * q \<le> n" |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
152 |
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
|
153 |
proof (cases "q > 0") |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
154 |
case False then show ?thesis by simp |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
155 |
next |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
156 |
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
|
157 |
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
|
158 |
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
|
159 |
then have "Max {m. m * m \<le> n} * q = Max (times q ` {m. m * m \<le> n})" by (simp add: ac_simps) |
59349 | 160 |
then show ?thesis |
161 |
apply simp |
|
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
162 |
apply (subst Max_le_iff) |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
163 |
apply auto |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
164 |
apply (metis (mono_tags) finite_imageI finite_less_ub le_square) |
60500 | 165 |
apply (metis \<open>q * q \<le> n\<close>) |
166 |
apply (metis \<open>q * q \<le> n\<close> le_cases mult_le_mono1 mult_le_mono2 order_trans) |
|
59349 | 167 |
done |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
168 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
169 |
qed |
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
170 |
with * show ?thesis by (simp add: sqrt_def power2_eq_square) |
51174 | 171 |
qed |
172 |
||
59349 | 173 |
lemma sqrt_le: "sqrt n \<le> n" |
51263
31e786e0e6a7
turned example into library for comparing growth of functions
haftmann
parents:
51174
diff
changeset
|
174 |
using sqrt_aux [of n] by (auto simp add: sqrt_def intro: power2_nat_le_imp_le) |
51174 | 175 |
|
176 |
hide_const (open) log sqrt |
|
177 |
||
178 |
end |
|
179 |