author | paulson <lp15@cam.ac.uk> |
Thu, 24 Aug 2023 21:40:24 +0100 | |
changeset 78522 | 918a9ed06898 |
parent 69597 | ff784d5a5bfb |
child 80914 | d97fdabd9e2b |
permissions | -rw-r--r-- |
51173 | 1 |
(* Title: HOL/Number_Theory/Eratosthenes.thy |
2 |
Author: Florian Haftmann, TU Muenchen |
|
3 |
*) |
|
4 |
||
60526 | 5 |
section \<open>The sieve of Eratosthenes\<close> |
51173 | 6 |
|
7 |
theory Eratosthenes |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
65417
diff
changeset
|
8 |
imports Main "HOL-Computational_Algebra.Primes" |
51173 | 9 |
begin |
10 |
||
52379 | 11 |
|
60526 | 12 |
subsection \<open>Preliminary: strict divisibility\<close> |
51173 | 13 |
|
14 |
context dvd |
|
15 |
begin |
|
16 |
||
17 |
abbreviation dvd_strict :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd'_strict" 50) |
|
18 |
where |
|
19 |
"b dvd_strict a \<equiv> b dvd a \<and> \<not> a dvd b" |
|
20 |
||
21 |
end |
|
22 |
||
60527 | 23 |
|
60526 | 24 |
subsection \<open>Main corpus\<close> |
51173 | 25 |
|
69597 | 26 |
text \<open>The sieve is modelled as a list of booleans, where \<^const>\<open>False\<close> means \emph{marked out}.\<close> |
51173 | 27 |
|
28 |
type_synonym marks = "bool list" |
|
29 |
||
30 |
definition numbers_of_marks :: "nat \<Rightarrow> marks \<Rightarrow> nat set" |
|
31 |
where |
|
32 |
"numbers_of_marks n bs = fst ` {x \<in> set (enumerate n bs). snd x}" |
|
33 |
||
34 |
lemma numbers_of_marks_simps [simp, code]: |
|
35 |
"numbers_of_marks n [] = {}" |
|
36 |
"numbers_of_marks n (True # bs) = insert n (numbers_of_marks (Suc n) bs)" |
|
37 |
"numbers_of_marks n (False # bs) = numbers_of_marks (Suc n) bs" |
|
38 |
by (auto simp add: numbers_of_marks_def intro!: image_eqI) |
|
39 |
||
40 |
lemma numbers_of_marks_Suc: |
|
41 |
"numbers_of_marks (Suc n) bs = Suc ` numbers_of_marks n bs" |
|
42 |
by (auto simp add: numbers_of_marks_def enumerate_Suc_eq image_iff Bex_def) |
|
43 |
||
44 |
lemma numbers_of_marks_replicate_False [simp]: |
|
45 |
"numbers_of_marks n (replicate m False) = {}" |
|
46 |
by (auto simp add: numbers_of_marks_def enumerate_replicate_eq) |
|
47 |
||
48 |
lemma numbers_of_marks_replicate_True [simp]: |
|
49 |
"numbers_of_marks n (replicate m True) = {n..<n+m}" |
|
50 |
by (auto simp add: numbers_of_marks_def enumerate_replicate_eq image_def) |
|
51 |
||
52 |
lemma in_numbers_of_marks_eq: |
|
53 |
"m \<in> numbers_of_marks n bs \<longleftrightarrow> m \<in> {n..<n + length bs} \<and> bs ! (m - n)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset
|
54 |
by (simp add: numbers_of_marks_def in_set_enumerate_eq image_iff add.commute) |
51173 | 55 |
|
52379 | 56 |
lemma sorted_list_of_set_numbers_of_marks: |
57 |
"sorted_list_of_set (numbers_of_marks n bs) = map fst (filter snd (enumerate n bs))" |
|
58 |
by (auto simp add: numbers_of_marks_def distinct_map |
|
59 |
intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique) |
|
60 |
||
51173 | 61 |
|
60526 | 62 |
text \<open>Marking out multiples in a sieve\<close> |
60527 | 63 |
|
51173 | 64 |
definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks" |
65 |
where |
|
66 |
"mark_out n bs = map (\<lambda>(q, b). b \<and> \<not> Suc n dvd Suc (Suc q)) (enumerate n bs)" |
|
67 |
||
60527 | 68 |
lemma mark_out_Nil [simp]: "mark_out n [] = []" |
51173 | 69 |
by (simp add: mark_out_def) |
60527 | 70 |
|
71 |
lemma length_mark_out [simp]: "length (mark_out n bs) = length bs" |
|
51173 | 72 |
by (simp add: mark_out_def) |
73 |
||
74 |
lemma numbers_of_marks_mark_out: |
|
60527 | 75 |
"numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}" |
51173 | 76 |
by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff |
54222 | 77 |
nth_enumerate_eq less_eq_dvd_minus) |
51173 | 78 |
|
79 |
||
60526 | 80 |
text \<open>Auxiliary operation for efficient implementation\<close> |
51173 | 81 |
|
82 |
definition mark_out_aux :: "nat \<Rightarrow> nat \<Rightarrow> marks \<Rightarrow> marks" |
|
83 |
where |
|
84 |
"mark_out_aux n m bs = |
|
85 |
map (\<lambda>(q, b). b \<and> (q < m + n \<or> \<not> Suc n dvd Suc (Suc q) + (n - m mod Suc n))) (enumerate n bs)" |
|
86 |
||
60527 | 87 |
lemma mark_out_code [code]: "mark_out n bs = mark_out_aux n n bs" |
51173 | 88 |
proof - |
60527 | 89 |
have aux: False |
90 |
if A: "Suc n dvd Suc (Suc a)" |
|
91 |
and B: "a < n + n" |
|
92 |
and C: "n \<le> a" |
|
93 |
for a |
|
94 |
proof (cases "n = 0") |
|
95 |
case True |
|
96 |
with A B C show ?thesis by simp |
|
97 |
next |
|
98 |
case False |
|
63040 | 99 |
define m where "m = Suc n" |
60527 | 100 |
then have "m > 0" by simp |
101 |
from False have "n > 0" by simp |
|
102 |
from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE) |
|
103 |
have "q > 0" |
|
104 |
proof (rule ccontr) |
|
105 |
assume "\<not> q > 0" |
|
106 |
with q show False by simp |
|
51173 | 107 |
qed |
60527 | 108 |
with \<open>n > 0\<close> have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc) |
109 |
with q have a: "a = Suc n * q - 2" by simp |
|
110 |
with B have "q + n * q < n + n + 2" by auto |
|
111 |
then have "m * q < m * 2" by (simp add: m_def) |
|
78522
918a9ed06898
some refinements in Algebra and Number_Theory
paulson <lp15@cam.ac.uk>
parents:
69597
diff
changeset
|
112 |
with \<open>m > 0\<close> \<open>q > 0\<close> have "q = 1" by simp |
60527 | 113 |
with a have "a = n - 1" by simp |
114 |
with \<open>n > 0\<close> C show False by simp |
|
115 |
qed |
|
51173 | 116 |
show ?thesis |
117 |
by (auto simp add: mark_out_def mark_out_aux_def in_set_enumerate_eq intro: aux) |
|
118 |
qed |
|
119 |
||
120 |
lemma mark_out_aux_simps [simp, code]: |
|
60583 | 121 |
"mark_out_aux n m [] = []" |
122 |
"mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs" |
|
123 |
"mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs" |
|
61166
5976fe402824
renamed method "goals" to "goal_cases" to emphasize its meaning;
wenzelm
parents:
60583
diff
changeset
|
124 |
proof goal_cases |
60583 | 125 |
case 1 |
126 |
show ?case |
|
51173 | 127 |
by (simp add: mark_out_aux_def) |
60583 | 128 |
next |
129 |
case 2 |
|
130 |
show ?case |
|
51173 | 131 |
by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def |
54222 | 132 |
enumerate_Suc_eq in_set_enumerate_eq less_eq_dvd_minus) |
60583 | 133 |
next |
134 |
case 3 |
|
63040 | 135 |
{ define v where "v = Suc m" |
136 |
define w where "w = Suc n" |
|
51173 | 137 |
fix q |
138 |
assume "m + n \<le> q" |
|
139 |
then obtain r where q: "q = m + n + r" by (auto simp add: le_iff_add) |
|
140 |
{ fix u |
|
141 |
from w_def have "u mod w < w" by simp |
|
142 |
then have "u + (w - u mod w) = w + (u - u mod w)" |
|
143 |
by simp |
|
144 |
then have "u + (w - u mod w) = w + u div w * w" |
|
64243 | 145 |
by (simp add: minus_mod_eq_div_mult) |
51173 | 146 |
} |
147 |
then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)" |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55337
diff
changeset
|
148 |
by (simp add: add.assoc add.left_commute [of m] add.left_commute [of v] |
58649
a62065b5e1e2
generalized and consolidated some theorems concerning divisibility
haftmann
parents:
57512
diff
changeset
|
149 |
dvd_add_left_iff dvd_add_right_iff) |
51173 | 150 |
moreover from q have "Suc q = m + w + r" by (simp add: w_def) |
151 |
moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def) |
|
152 |
ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))" |
|
153 |
by (simp only: add_Suc [symmetric]) |
|
154 |
then have "Suc n dvd Suc (Suc (Suc (q + n) - Suc m mod Suc n)) \<longleftrightarrow> |
|
155 |
Suc n dvd Suc (Suc (q + n - m mod Suc n))" |
|
156 |
by (simp add: v_def w_def Suc_diff_le trans_le_add2) |
|
157 |
} |
|
60583 | 158 |
then show ?case |
51173 | 159 |
by (auto simp add: mark_out_aux_def |
160 |
enumerate_Suc_eq in_set_enumerate_eq not_less) |
|
161 |
qed |
|
162 |
||
163 |
||
60526 | 164 |
text \<open>Main entry point to sieve\<close> |
51173 | 165 |
|
166 |
fun sieve :: "nat \<Rightarrow> marks \<Rightarrow> marks" |
|
167 |
where |
|
168 |
"sieve n [] = []" |
|
169 |
| "sieve n (False # bs) = False # sieve (Suc n) bs" |
|
170 |
| "sieve n (True # bs) = True # sieve (Suc n) (mark_out n bs)" |
|
171 |
||
60526 | 172 |
text \<open> |
51173 | 173 |
There are the following possible optimisations here: |
174 |
||
175 |
\begin{itemize} |
|
176 |
||
69597 | 177 |
\item \<^const>\<open>sieve\<close> can abort as soon as \<^term>\<open>n\<close> is too big to let |
178 |
\<^const>\<open>mark_out\<close> have any effect. |
|
51173 | 179 |
|
180 |
\item Search for further primes can be given up as soon as the search |
|
181 |
position exceeds the square root of the maximum candidate. |
|
182 |
||
183 |
\end{itemize} |
|
184 |
||
185 |
This is left as an constructive exercise to the reader. |
|
60526 | 186 |
\<close> |
51173 | 187 |
|
188 |
lemma numbers_of_marks_sieve: |
|
189 |
"numbers_of_marks (Suc n) (sieve n bs) = |
|
190 |
{q \<in> numbers_of_marks (Suc n) bs. \<forall>m \<in> numbers_of_marks (Suc n) bs. \<not> m dvd_strict q}" |
|
191 |
proof (induct n bs rule: sieve.induct) |
|
60527 | 192 |
case 1 |
193 |
show ?case by simp |
|
51173 | 194 |
next |
60527 | 195 |
case 2 |
196 |
then show ?case by simp |
|
51173 | 197 |
next |
198 |
case (3 n bs) |
|
60527 | 199 |
have aux: "n \<in> Suc ` M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M" (is "?lhs \<longleftrightarrow> ?rhs") for M n |
51173 | 200 |
proof |
60527 | 201 |
show ?rhs if ?lhs using that by auto |
202 |
show ?lhs if ?rhs |
|
203 |
proof - |
|
204 |
from that have "n > 0" and "n - 1 \<in> M" by auto |
|
205 |
then have "Suc (n - 1) \<in> Suc ` M" by blast |
|
206 |
with \<open>n > 0\<close> show "n \<in> Suc ` M" by simp |
|
207 |
qed |
|
51173 | 208 |
qed |
60527 | 209 |
have aux1: False if "Suc (Suc n) \<le> m" and "m dvd Suc n" for m :: nat |
210 |
proof - |
|
60526 | 211 |
from \<open>m dvd Suc n\<close> obtain q where "Suc n = m * q" .. |
212 |
with \<open>Suc (Suc n) \<le> m\<close> have "Suc (m * q) \<le> m" by simp |
|
51173 | 213 |
then have "m * q < m" by arith |
60527 | 214 |
with \<open>Suc n = m * q\<close> show ?thesis by simp |
215 |
qed |
|
216 |
have aux2: "m dvd q" |
|
217 |
if 1: "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs) \<longrightarrow> |
|
218 |
bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q" |
|
219 |
and 2: "\<not> Suc n dvd m" "q dvd m" |
|
220 |
and 3: "Suc n < q" "q \<le> Suc (n + length bs)" "bs ! (q - Suc (Suc n))" |
|
221 |
for m q :: nat |
|
222 |
proof - |
|
223 |
from 1 have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs) \<Longrightarrow> |
|
224 |
bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q" |
|
51173 | 225 |
by auto |
60527 | 226 |
from 2 have "\<not> Suc n dvd q" by (auto elim: dvdE) |
227 |
moreover note 3 |
|
60526 | 228 |
moreover note \<open>q dvd m\<close> |
60527 | 229 |
ultimately show ?thesis by (auto intro: *) |
230 |
qed |
|
51173 | 231 |
from 3 show ?case |
60527 | 232 |
apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq |
233 |
inj_image_eq_iff in_numbers_of_marks_eq Ball_def imp_conjL aux) |
|
51173 | 234 |
apply safe |
235 |
apply (simp_all add: less_diff_conv2 le_diff_conv2 dvd_minus_self not_less) |
|
236 |
apply (clarsimp dest!: aux1) |
|
237 |
apply (simp add: Suc_le_eq less_Suc_eq_le) |
|
60527 | 238 |
apply (rule aux2) |
239 |
apply (clarsimp dest!: aux1)+ |
|
51173 | 240 |
done |
241 |
qed |
|
242 |
||
243 |
||
60526 | 244 |
text \<open>Relation of the sieve algorithm to actual primes\<close> |
51173 | 245 |
|
52379 | 246 |
definition primes_upto :: "nat \<Rightarrow> nat list" |
51173 | 247 |
where |
52379 | 248 |
"primes_upto n = sorted_list_of_set {m. m \<le> n \<and> prime m}" |
51173 | 249 |
|
60527 | 250 |
lemma set_primes_upto: "set (primes_upto n) = {m. m \<le> n \<and> prime m}" |
51173 | 251 |
by (simp add: primes_upto_def) |
252 |
||
60527 | 253 |
lemma sorted_primes_upto [iff]: "sorted (primes_upto n)" |
52379 | 254 |
by (simp add: primes_upto_def) |
255 |
||
60527 | 256 |
lemma distinct_primes_upto [iff]: "distinct (primes_upto n)" |
52379 | 257 |
by (simp add: primes_upto_def) |
258 |
||
259 |
lemma set_primes_upto_sieve: |
|
260 |
"set (primes_upto n) = numbers_of_marks 2 (sieve 1 (replicate (n - 1) True))" |
|
60527 | 261 |
proof - |
262 |
consider "n = 0 \<or> n = 1" | "n > 1" by arith |
|
51173 | 263 |
then show ?thesis |
60527 | 264 |
proof cases |
265 |
case 1 |
|
266 |
then show ?thesis |
|
267 |
by (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto |
|
55337
5d45fb978d5a
Number_Theory no longer introduces One_nat_def as a simprule. Tidied some proofs.
paulson <lp15@cam.ac.uk>
parents:
55130
diff
changeset
|
268 |
dest: prime_gt_Suc_0_nat) |
60527 | 269 |
next |
270 |
case 2 |
|
271 |
{ |
|
272 |
fix m q |
|
273 |
assume "Suc (Suc 0) \<le> q" |
|
274 |
and "q < Suc n" |
|
275 |
and "m dvd q" |
|
276 |
then have "m < Suc n" by (auto dest: dvd_imp_le) |
|
277 |
assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m" |
|
278 |
and "m dvd q" and "m \<noteq> 1" |
|
279 |
have "m = q" |
|
280 |
proof (cases "m = 0") |
|
281 |
case True with \<open>m dvd q\<close> show ?thesis by simp |
|
282 |
next |
|
283 |
case False with \<open>m \<noteq> 1\<close> have "Suc (Suc 0) \<le> m" by arith |
|
284 |
with \<open>m < Suc n\<close> * \<open>m dvd q\<close> have "q dvd m" by simp |
|
62349
7c23469b5118
cleansed junk-producing interpretations for gcd/lcm on nat altogether
haftmann
parents:
61762
diff
changeset
|
285 |
with \<open>m dvd q\<close> show ?thesis by (simp add: dvd_antisym) |
60527 | 286 |
qed |
287 |
} |
|
288 |
then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow> |
|
289 |
q < Suc n \<Longrightarrow> |
|
290 |
m dvd q \<Longrightarrow> |
|
291 |
\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow> |
|
292 |
m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto |
|
293 |
from 2 show ?thesis |
|
294 |
apply (auto simp add: numbers_of_marks_sieve numeral_2_eq_2 set_primes_upto |
|
295 |
dest: prime_gt_Suc_0_nat) |
|
63633 | 296 |
apply (metis One_nat_def Suc_le_eq less_not_refl prime_nat_iff) |
297 |
apply (metis One_nat_def Suc_le_eq aux prime_nat_iff) |
|
60527 | 298 |
done |
299 |
qed |
|
51173 | 300 |
qed |
301 |
||
52379 | 302 |
lemma primes_upto_sieve [code]: |
303 |
"primes_upto n = map fst (filter snd (enumerate 2 (sieve 1 (replicate (n - 1) True))))" |
|
78522
918a9ed06898
some refinements in Algebra and Number_Theory
paulson <lp15@cam.ac.uk>
parents:
69597
diff
changeset
|
304 |
using primes_upto_def set_primes_upto set_primes_upto_sieve sorted_list_of_set_numbers_of_marks by presburger |
52379 | 305 |
|
60527 | 306 |
lemma prime_in_primes_upto: "prime n \<longleftrightarrow> n \<in> set (primes_upto n)" |
52379 | 307 |
by (simp add: set_primes_upto) |
308 |
||
309 |
||
60526 | 310 |
subsection \<open>Application: smallest prime beyond a certain number\<close> |
52379 | 311 |
|
312 |
definition smallest_prime_beyond :: "nat \<Rightarrow> nat" |
|
313 |
where |
|
314 |
"smallest_prime_beyond n = (LEAST p. prime p \<and> p \<ge> n)" |
|
315 |
||
60527 | 316 |
lemma prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P) |
52379 | 317 |
and smallest_prime_beyond_le [iff]: "smallest_prime_beyond n \<ge> n" (is ?Q) |
318 |
proof - |
|
319 |
let ?least = "LEAST p. prime p \<and> p \<ge> n" |
|
320 |
from primes_infinite obtain q where "prime q \<and> q \<ge> n" |
|
321 |
by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear) |
|
60527 | 322 |
then have "prime ?least \<and> ?least \<ge> n" |
323 |
by (rule LeastI) |
|
324 |
then show ?P and ?Q |
|
325 |
by (simp_all add: smallest_prime_beyond_def) |
|
52379 | 326 |
qed |
327 |
||
60527 | 328 |
lemma smallest_prime_beyond_smallest: "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p" |
52379 | 329 |
by (simp only: smallest_prime_beyond_def) (auto intro: Least_le) |
330 |
||
331 |
lemma smallest_prime_beyond_eq: |
|
332 |
"prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> (\<And>q. prime q \<Longrightarrow> q \<ge> n \<Longrightarrow> q \<ge> p) \<Longrightarrow> smallest_prime_beyond n = p" |
|
333 |
by (simp only: smallest_prime_beyond_def) (auto intro: Least_equality) |
|
334 |
||
335 |
definition smallest_prime_between :: "nat \<Rightarrow> nat \<Rightarrow> nat option" |
|
336 |
where |
|
337 |
"smallest_prime_between m n = |
|
338 |
(if (\<exists>p. prime p \<and> m \<le> p \<and> p \<le> n) then Some (smallest_prime_beyond m) else None)" |
|
339 |
||
340 |
lemma smallest_prime_between_None: |
|
341 |
"smallest_prime_between m n = None \<longleftrightarrow> (\<forall>q. m \<le> q \<and> q \<le> n \<longrightarrow> \<not> prime q)" |
|
342 |
by (auto simp add: smallest_prime_between_def) |
|
343 |
||
344 |
lemma smallest_prime_betwen_Some: |
|
345 |
"smallest_prime_between m n = Some p \<longleftrightarrow> smallest_prime_beyond m = p \<and> p \<le> n" |
|
346 |
by (auto simp add: smallest_prime_between_def dest: smallest_prime_beyond_smallest [of _ m]) |
|
347 |
||
60527 | 348 |
lemma [code]: "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)" |
52379 | 349 |
proof - |
60527 | 350 |
have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)" |
351 |
if assms: "m \<le> p" "prime p" "p \<le> n" for p |
|
352 |
proof - |
|
63040 | 353 |
define A where "A = {p. p \<le> n \<and> prime p \<and> m \<le> p}" |
60527 | 354 |
from assms have "smallest_prime_beyond m \<le> p" |
355 |
by (auto intro: smallest_prime_beyond_smallest) |
|
356 |
from this \<open>p \<le> n\<close> have *: "smallest_prime_beyond m \<le> n" |
|
357 |
by (rule order_trans) |
|
358 |
from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" |
|
359 |
by auto |
|
360 |
then have "finite A" |
|
361 |
by (auto simp add: A_def) |
|
52379 | 362 |
with * have "Min A = smallest_prime_beyond m" |
363 |
by (auto simp add: A_def intro: Min_eqI smallest_prime_beyond_smallest) |
|
60527 | 364 |
with ex sorted_primes_upto show ?thesis |
52379 | 365 |
by (auto simp add: set_primes_upto sorted_find_Min A_def) |
60527 | 366 |
qed |
367 |
then show ?thesis |
|
368 |
by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto |
|
369 |
intro!: sym [of _ None]) |
|
52379 | 370 |
qed |
371 |
||
372 |
definition smallest_prime_beyond_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat" |
|
373 |
where |
|
374 |
"smallest_prime_beyond_aux k n = smallest_prime_beyond n" |
|
375 |
||
376 |
lemma [code]: |
|
377 |
"smallest_prime_beyond_aux k n = |
|
60527 | 378 |
(case smallest_prime_between n (k * n) of |
379 |
Some p \<Rightarrow> p |
|
380 |
| None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)" |
|
52379 | 381 |
by (simp add: smallest_prime_beyond_aux_def smallest_prime_betwen_Some split: option.split) |
382 |
||
60527 | 383 |
lemma [code]: "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n" |
52379 | 384 |
by (simp add: smallest_prime_beyond_aux_def) |
385 |
||
51173 | 386 |
end |