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