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