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