# HG changeset patch
# User haftmann
# Date 1361132970 -3600
# Node ID 3cbb4e95a5653fcf303c5d8d61037cbba66e63ca
# Parent  16eb76ca1e4afdd8e53af61bfd2466c3d92fcdc1
Sieve of Eratosthenes

diff -r 16eb76ca1e4a -r 3cbb4e95a565 CONTRIBUTORS
--- a/CONTRIBUTORS	Sun Feb 17 20:45:49 2013 +0100
+++ b/CONTRIBUTORS	Sun Feb 17 21:29:30 2013 +0100
@@ -6,10 +6,13 @@
 Contributions to this Isabelle version
 --------------------------------------
 
-* 2013: Florian Haftmann, TUM
+* Feb. 2013: Florian Haftmann, TUM
   Reworking and consolidation of code generation for target
   language numerals.
 
+* Feb. 2013: Florian Haftmann, TUM
+  Sieve of Eratosthenes.
+
 
 Contributions to Isabelle2013
 -----------------------------
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -8,7 +8,7 @@
   Complex_Main
   "~~/src/HOL/Library/Library"
   "~~/src/HOL/Library/Sublist_Order"
-  "~~/src/HOL/Number_Theory/Primes"
+  "~~/src/HOL/Number_Theory/Eratosthenes"
   "~~/src/HOL/ex/Records"
 begin
 
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Divides.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -740,6 +740,10 @@
   shows "m mod n < (n::nat)"
   using assms divmod_nat_rel [of m n] unfolding divmod_nat_rel_def by auto
 
+lemma mod_Suc_le_divisor [simp]:
+  "m mod Suc n \<le> n"
+  using mod_less_divisor [of "Suc n" m] by arith
+
 lemma mod_less_eq_dividend [simp]:
   fixes m n :: nat
   shows "m mod n \<le> m"
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/List.thy
--- a/src/HOL/List.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/List.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -196,6 +196,9 @@
 abbreviation length :: "'a list \<Rightarrow> nat" where
 "length \<equiv> size"
 
+definition enumerate :: "nat \<Rightarrow> 'a list \<Rightarrow> (nat \<times> 'a) list" where
+enumerate_eq_zip: "enumerate n xs = zip [n..<n + length xs] xs"
+
 primrec rotate1 :: "'a list \<Rightarrow> 'a list" where
 "rotate1 [] = []" |
 "rotate1 (x # xs) = xs @ [x]"
@@ -245,6 +248,7 @@
 @{lemma "foldl f x [a,b,c] = f (f (f x a) b) c" by simp}\\
 @{lemma "zip [a,b,c] [x,y,z] = [(a,x),(b,y),(c,z)]" by simp}\\
 @{lemma "zip [a,b] [x,y,z] = [(a,x),(b,y)]" by simp}\\
+@{lemma "enumerate 3 [a,b,c] = [(3,a),(4,b),(5,c)]" by normalization}\\
 @{lemma "List.product [a,b] [c,d] = [(a, c), (a, d), (b, c), (b, d)]" by simp}\\
 @{lemma "splice [a,b,c] [x,y,z] = [a,x,b,y,c,z]" by simp}\\
 @{lemma "splice [a,b,c,d] [x,y] = [a,x,b,y,c,d]" by simp}\\
@@ -2479,6 +2483,20 @@
   "length xs = length ys \<Longrightarrow> zip xs ys = zs \<longleftrightarrow> map fst zs = xs \<and> map snd zs = ys"
   by (auto simp add: zip_map_fst_snd)
 
+lemma in_set_zip:
+  "p \<in> set (zip xs ys) \<longleftrightarrow> (\<exists>n. xs ! n = fst p \<and> ys ! n = snd p
+    \<and> n < length xs \<and> n < length ys)"
+  by (cases p) (auto simp add: set_zip)
+
+lemma pair_list_eqI:
+  assumes "map fst xs = map fst ys" and "map snd xs = map snd ys"
+  shows "xs = ys"
+proof -
+  from assms(1) have "length xs = length ys" by (rule map_eq_imp_length_eq)
+  from this assms show ?thesis
+    by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI)
+qed
+
 
 subsubsection {* @{const list_all2} *}
 
@@ -3880,6 +3898,57 @@
 qed
 
 
+subsubsection {* @{const enumerate} *}
+
+lemma enumerate_simps [simp, code]:
+  "enumerate n [] = []"
+  "enumerate n (x # xs) = (n, x) # enumerate (Suc n) xs"
+  apply (auto simp add: enumerate_eq_zip not_le)
+  apply (cases "n < n + length xs")
+  apply (auto simp add: upt_conv_Cons)
+  done
+
+lemma length_enumerate [simp]:
+  "length (enumerate n xs) = length xs"
+  by (simp add: enumerate_eq_zip)
+
+lemma map_fst_enumerate [simp]:
+  "map fst (enumerate n xs) = [n..<n + length xs]"
+  by (simp add: enumerate_eq_zip)
+
+lemma map_snd_enumerate [simp]:
+  "map snd (enumerate n xs) = xs"
+  by (simp add: enumerate_eq_zip)
+  
+lemma in_set_enumerate_eq:
+  "p \<in> set (enumerate n xs) \<longleftrightarrow> n \<le> fst p \<and> fst p < length xs + n \<and> nth xs (fst p - n) = snd p"
+proof -
+  { fix m
+    assume "n \<le> m"
+    moreover assume "m < length xs + n"
+    ultimately have "[n..<n + length xs] ! (m - n) = m \<and>
+      xs ! (m - n) = xs ! (m - n) \<and> m - n < length xs" by auto
+    then have "\<exists>q. [n..<n + length xs] ! q = m \<and>
+        xs ! q = xs ! (m - n) \<and> q < length xs" ..
+  } then show ?thesis by (cases p) (auto simp add: enumerate_eq_zip in_set_zip)
+qed
+
+lemma nth_enumerate_eq:
+  assumes "m < length xs"
+  shows "enumerate n xs ! m = (n + m, xs ! m)"
+  using assms by (simp add: enumerate_eq_zip)
+
+lemma enumerate_replicate_eq:
+  "enumerate n (replicate m a) = map (\<lambda>q. (q, a)) [n..<n + m]"
+  by (rule pair_list_eqI)
+    (simp_all add: enumerate_eq_zip comp_def map_replicate_const)
+
+lemma enumerate_Suc_eq:
+  "enumerate (Suc n) xs = map (apfst Suc) (enumerate n xs)"
+  by (rule pair_list_eqI)
+    (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
+
+
 subsubsection {* @{const rotate1} and @{const rotate} *}
 
 lemma rotate0[simp]: "rotate 0 = id"
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Nat.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -1587,6 +1587,12 @@
 lemma less_diff_conv: "(i < j-k) = (i+k < (j::nat))"
 by arith
 
+lemma less_diff_conv2:
+  fixes j k i :: nat
+  assumes "k \<le> j"
+  shows "j - k < i \<longleftrightarrow> j < i + k"
+  using assms by arith
+
 lemma le_diff_conv: "(j-k \<le> (i::nat)) = (j \<le> i+k)"
 by arith
 
@@ -1801,6 +1807,74 @@
   shows "0 < m \<Longrightarrow> m < n \<Longrightarrow> \<not> n dvd m"
 by (auto elim!: dvdE) (auto simp add: gr0_conv_Suc)
 
+lemma dvd_plusE:
+  fixes m n q :: nat
+  assumes "m dvd n + q" "m dvd n"
+  obtains "m dvd q"
+proof (cases "m = 0")
+  case True with assms that show thesis by simp
+next
+  case False then have "m > 0" by simp
+  from assms obtain r s where "n = m * r" and "n + q = m * s" by (blast elim: dvdE)
+  then have *: "m * r + q = m * s" by simp
+  show thesis proof (cases "r \<le> s")
+    case False then have "s < r" by (simp add: not_le)
+    with * have "m * r + q - m * s = m * s - m * s" by simp
+    then have "m * r + q - m * s = 0" by simp
+    with `m > 0` `s < r` have "m * r - m * s + q = 0" by simp
+    then have "m * (r - s) + q = 0" by auto
+    then have "m * (r - s) = 0" by simp
+    then have "m = 0 \<or> r - s = 0" by simp
+    with `s < r` have "m = 0" by arith
+    with `m > 0` show thesis by auto
+  next
+    case True with * have "m * r + q - m * r = m * s - m * r" by simp
+    with `m > 0` `r \<le> s` have "m * r - m * r + q = m * s - m * r" by simp
+    then have "q = m * (s - r)" by (simp add: diff_mult_distrib2)
+    with assms that show thesis by (auto intro: dvdI)
+  qed
+qed
+
+lemma dvd_plus_eq_right:
+  fixes m n q :: nat
+  assumes "m dvd n"
+  shows "m dvd n + q \<longleftrightarrow> m dvd q"
+  using assms by (auto elim: dvd_plusE)
+
+lemma dvd_plus_eq_left:
+  fixes m n q :: nat
+  assumes "m dvd q"
+  shows "m dvd n + q \<longleftrightarrow> m dvd n"
+  using assms by (simp add: dvd_plus_eq_right add_commute [of n])
+
+lemma less_dvd_minus:
+  fixes m n :: nat
+  assumes "m < n"
+  shows "m dvd n \<longleftrightarrow> m dvd (n - m)"
+proof -
+  from assms have "n = m + (n - m)" by arith
+  then obtain q where "n = m + q" ..
+  then show ?thesis by (simp add: dvd_reduce add_commute [of m])
+qed
+
+lemma dvd_minus_self:
+  fixes m n :: nat
+  shows "m dvd n - m \<longleftrightarrow> n < m \<or> m dvd n"
+  by (cases "n < m") (auto elim!: dvdE simp add: not_less le_imp_diff_is_add)
+
+lemma dvd_minus_add:
+  fixes m n q r :: nat
+  assumes "q \<le> n" "q \<le> r * m"
+  shows "m dvd n - q \<longleftrightarrow> m dvd n + (r * m - q)"
+proof -
+  have "m dvd n - q \<longleftrightarrow> m dvd r * m + (n - q)"
+    by (auto elim: dvd_plusE)
+  also with assms have "\<dots> \<longleftrightarrow> m dvd r * m + n - q" by simp
+  also with assms have "\<dots> \<longleftrightarrow> m dvd (r * m - q) + n" by simp
+  also have "\<dots> \<longleftrightarrow> m dvd n + (r * m - q)" by (simp add: add_commute)
+  finally show ?thesis .
+qed
+
 
 subsection {* aliasses *}
 
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Number_Theory/Eratosthenes.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -0,0 +1,276 @@
+(*  Title:      HOL/Number_Theory/Eratosthenes.thy
+    Author:     Florian Haftmann, TU Muenchen
+*)
+
+header {* The sieve of Eratosthenes *}
+
+theory Eratosthenes
+imports Primes
+begin
+
+subsection {* Preliminary: strict divisibility *}
+
+context dvd
+begin
+
+abbreviation dvd_strict :: "'a \<Rightarrow> 'a \<Rightarrow> bool" (infixl "dvd'_strict" 50)
+where
+  "b dvd_strict a \<equiv> b dvd a \<and> \<not> a dvd b"
+
+end
+
+subsection {* Main corpus *}
+
+text {* The sieve is modelled as a list of booleans, where @{const False} means \emph{marked out}. *}
+
+type_synonym marks = "bool list"
+
+definition numbers_of_marks :: "nat \<Rightarrow> marks \<Rightarrow> nat set"
+where
+  "numbers_of_marks n bs = fst ` {x \<in> set (enumerate n bs). snd x}"
+
+lemma numbers_of_marks_simps [simp, code]:
+  "numbers_of_marks n [] = {}"
+  "numbers_of_marks n (True # bs) = insert n (numbers_of_marks (Suc n) bs)"
+  "numbers_of_marks n (False # bs) = numbers_of_marks (Suc n) bs"
+  by (auto simp add: numbers_of_marks_def intro!: image_eqI)
+
+lemma numbers_of_marks_Suc:
+  "numbers_of_marks (Suc n) bs = Suc ` numbers_of_marks n bs"
+  by (auto simp add: numbers_of_marks_def enumerate_Suc_eq image_iff Bex_def)
+
+lemma numbers_of_marks_replicate_False [simp]:
+  "numbers_of_marks n (replicate m False) = {}"
+  by (auto simp add: numbers_of_marks_def enumerate_replicate_eq)
+
+lemma numbers_of_marks_replicate_True [simp]:
+  "numbers_of_marks n (replicate m True) = {n..<n+m}"
+  by (auto simp add: numbers_of_marks_def enumerate_replicate_eq image_def)
+
+lemma in_numbers_of_marks_eq:
+  "m \<in> numbers_of_marks n bs \<longleftrightarrow> m \<in> {n..<n + length bs} \<and> bs ! (m - n)"
+  by (simp add: numbers_of_marks_def in_set_enumerate_eq image_iff add_commute)
+
+
+text {* Marking out multiples in a sieve  *}
+ 
+definition mark_out :: "nat \<Rightarrow> marks \<Rightarrow> marks"
+where
+  "mark_out n bs = map (\<lambda>(q, b). b \<and> \<not> Suc n dvd Suc (Suc q)) (enumerate n bs)"
+
+lemma mark_out_Nil [simp]:
+  "mark_out n [] = []"
+  by (simp add: mark_out_def)
+  
+lemma length_mark_out [simp]:
+  "length (mark_out n bs) = length bs"
+  by (simp add: mark_out_def)
+
+lemma numbers_of_marks_mark_out:
+  "numbers_of_marks n (mark_out m bs) = {q \<in> numbers_of_marks n bs. \<not> Suc m dvd Suc q - n}"
+  by (auto simp add: numbers_of_marks_def mark_out_def in_set_enumerate_eq image_iff
+    nth_enumerate_eq less_dvd_minus)
+
+
+text {* Auxiliary operation for efficient implementation  *}
+
+definition mark_out_aux :: "nat \<Rightarrow> nat \<Rightarrow> marks \<Rightarrow> marks"
+where
+  "mark_out_aux n m bs =
+    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)"
+
+lemma mark_out_code [code]:
+  "mark_out n bs = mark_out_aux n n bs"
+proof -
+  { fix a
+    assume A: "Suc n dvd Suc (Suc a)"
+      and B: "a < n + n"
+      and C: "n \<le> a"
+    have False
+    proof (cases "n = 0")
+      case True with A B C show False by simp
+    next
+      def m \<equiv> "Suc n" then have "m > 0" by simp
+      case False then have "n > 0" by simp
+      from A obtain q where q: "Suc (Suc a) = Suc n * q" by (rule dvdE)
+      have "q > 0"
+      proof (rule ccontr)
+        assume "\<not> q > 0"
+        with q show False by simp
+      qed
+      with `n > 0` have "Suc n * q \<ge> 2" by (auto simp add: gr0_conv_Suc)
+      with q have a: "a = Suc n * q - 2" by simp
+      with B have "q + n * q < n + n + 2"
+        by auto
+      then have "m * q < m * 2" by (simp add: m_def)
+      with `m > 0` have "q < 2" by simp
+      with `q > 0` have "q = 1" by simp
+      with a have "a = n - 1" by simp
+      with `n > 0` C show False by simp
+    qed
+  } note aux = this 
+  show ?thesis
+    by (auto simp add: mark_out_def mark_out_aux_def in_set_enumerate_eq intro: aux)
+qed
+
+lemma mark_out_aux_simps [simp, code]:
+  "mark_out_aux n m [] = []" (is ?thesis1)
+  "mark_out_aux n 0 (b # bs) = False # mark_out_aux n n bs" (is ?thesis2)
+  "mark_out_aux n (Suc m) (b # bs) = b # mark_out_aux n m bs" (is ?thesis3)
+proof -
+  show ?thesis1
+    by (simp add: mark_out_aux_def)
+  show ?thesis2
+    by (auto simp add: mark_out_code [symmetric] mark_out_aux_def mark_out_def
+      enumerate_Suc_eq in_set_enumerate_eq less_dvd_minus)
+  { def v \<equiv> "Suc m" and w \<equiv> "Suc n"
+    fix q
+    assume "m + n \<le> q"
+    then obtain r where q: "q = m + n + r" by (auto simp add: le_iff_add)
+    { fix u
+      from w_def have "u mod w < w" by simp
+      then have "u + (w - u mod w) = w + (u - u mod w)"
+        by simp
+      then have "u + (w - u mod w) = w + u div w * w"
+        by (simp add: div_mod_equality' [symmetric])
+    }
+    then have "w dvd v + w + r + (w - v mod w) \<longleftrightarrow> w dvd m + w + r + (w - m mod w)"
+      by (simp add: add_assoc add_left_commute [of m] add_left_commute [of v]
+        dvd_plus_eq_left dvd_plus_eq_right)
+    moreover from q have "Suc q = m + w + r" by (simp add: w_def)
+    moreover from q have "Suc (Suc q) = v + w + r" by (simp add: v_def w_def)
+    ultimately have "w dvd Suc (Suc (q + (w - v mod w))) \<longleftrightarrow> w dvd Suc (q + (w - m mod w))"
+      by (simp only: add_Suc [symmetric])
+    then have "Suc n dvd Suc (Suc (Suc (q + n) - Suc m mod Suc n)) \<longleftrightarrow>
+      Suc n dvd Suc (Suc (q + n - m mod Suc n))"
+      by (simp add: v_def w_def Suc_diff_le trans_le_add2)
+  }
+  then show ?thesis3
+    by (auto simp add: mark_out_aux_def
+      enumerate_Suc_eq in_set_enumerate_eq not_less)
+qed
+
+
+text {* Main entry point to sieve *}
+
+fun sieve :: "nat \<Rightarrow> marks \<Rightarrow> marks"
+where
+  "sieve n [] = []"
+| "sieve n (False # bs) = False # sieve (Suc n) bs"
+| "sieve n (True # bs) = True # sieve (Suc n) (mark_out n bs)"
+
+text {*
+  There are the following possible optimisations here:
+
+  \begin{itemize}
+
+    \item @{const sieve} can abort as soon as @{term n} is too big to let
+      @{const mark_out} have any effect.
+
+    \item Search for further primes can be given up as soon as the search
+      position exceeds the square root of the maximum candidate.
+
+  \end{itemize}
+
+  This is left as an constructive exercise to the reader.
+*}
+
+lemma numbers_of_marks_sieve:
+  "numbers_of_marks (Suc n) (sieve n bs) =
+    {q \<in> numbers_of_marks (Suc n) bs. \<forall>m \<in> numbers_of_marks (Suc n) bs. \<not> m dvd_strict q}"
+proof (induct n bs rule: sieve.induct)
+  case 1 show ?case by simp
+next
+  case 2 then show ?case by simp
+next
+  case (3 n bs)
+  have aux: "\<And>M n. n \<in> Suc ` M \<longleftrightarrow> n > 0 \<and> n - 1 \<in> M"
+  proof
+    fix M and n
+    assume "n \<in> Suc ` M" then show "n > 0 \<and> n - 1 \<in> M" by auto
+  next
+    fix M and n :: nat
+    assume "n > 0 \<and> n - 1 \<in> M"
+    then have "n > 0" and "n - 1 \<in> M" by auto
+    then have "Suc (n - 1) \<in> Suc ` M" by blast
+    with `n > 0` show "n \<in> Suc ` M" by simp
+  qed
+  { fix m :: nat
+    assume "Suc (Suc n) \<le> m" and "m dvd Suc n"
+    from `m dvd Suc n` obtain q where "Suc n = m * q" ..
+    with `Suc (Suc n) \<le> m` have "Suc (m * q) \<le> m" by simp
+    then have "m * q < m" by arith
+    then have "q = 0" by simp
+    with `Suc n = m * q` have False by simp
+  } note aux1 = this
+  { fix m q :: nat
+    assume "\<forall>q>0. 1 < q \<longrightarrow> Suc n < q \<longrightarrow> q \<le> Suc (n + length bs)
+      \<longrightarrow> bs ! (q - Suc (Suc n)) \<longrightarrow> \<not> Suc n dvd q \<longrightarrow> q dvd m \<longrightarrow> m dvd q"
+    then have *: "\<And>q. Suc n < q \<Longrightarrow> q \<le> Suc (n + length bs)
+      \<Longrightarrow> bs ! (q - Suc (Suc n)) \<Longrightarrow> \<not> Suc n dvd q \<Longrightarrow> q dvd m \<Longrightarrow> m dvd q"
+      by auto
+    assume "\<not> Suc n dvd m" and "q dvd m"
+    then have "\<not> Suc n dvd q" by (auto elim: dvdE)
+    moreover assume "Suc n < q" and "q \<le> Suc (n + length bs)"
+      and "bs ! (q - Suc (Suc n))"
+    moreover note `q dvd m`
+    ultimately have "m dvd q" by (auto intro: *)
+  } note aux2 = this
+  from 3 show ?case
+    apply (simp_all add: numbers_of_marks_mark_out numbers_of_marks_Suc Compr_image_eq inj_image_eq_iff
+      in_numbers_of_marks_eq Ball_def imp_conjL aux)
+    apply safe
+    apply (simp_all add: less_diff_conv2 le_diff_conv2 dvd_minus_self not_less)
+    apply (clarsimp dest!: aux1)
+    apply (simp add: Suc_le_eq less_Suc_eq_le)
+    apply (rule aux2) apply (clarsimp dest!: aux1)+
+    done
+qed
+
+
+text {* Relation the sieve algorithm to actual primes *}
+
+definition primes_upto :: "nat \<Rightarrow> nat set"
+where
+  "primes_upto n = {m. m \<le> n \<and> prime m}"
+
+lemma in_primes_upto:
+  "m \<in> primes_upto n \<longleftrightarrow> m \<le> n \<and> prime m"
+  by (simp add: primes_upto_def)
+
+lemma primes_upto_sieve [code]:
+  "primes_upto n = numbers_of_marks 2 (sieve 1 (replicate (n - 1) True))"
+proof (cases "n > 1")
+  case False then have "n = 0 \<or> n = 1" by arith
+  then show ?thesis
+    by (auto simp add: numbers_of_marks_sieve One_nat_def numeral_2_eq_2 primes_upto_def dest: prime_gt_Suc_0_nat)
+next
+  { fix m q
+    assume "Suc (Suc 0) \<le> q"
+      and "q < Suc n"
+      and "m dvd q"
+    then have "m < Suc n" by (auto dest: dvd_imp_le)
+    assume *: "\<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m"
+      and "m dvd q" and "m \<noteq> 1"
+    have "m = q" proof (cases "m = 0")
+      case True with `m dvd q` show ?thesis by simp
+    next
+      case False with `m \<noteq> 1` have "Suc (Suc 0) \<le> m" by arith
+      with `m < Suc n` * `m dvd q` have "q dvd m" by simp
+      with `m dvd q` show ?thesis by (simp add: dvd.eq_iff)
+    qed
+  }
+  then have aux: "\<And>m q. Suc (Suc 0) \<le> q \<Longrightarrow>
+    q < Suc n \<Longrightarrow>
+    m dvd q \<Longrightarrow>
+    \<forall>m\<in>{Suc (Suc 0)..<Suc n}. m dvd q \<longrightarrow> q dvd m \<Longrightarrow>
+    m dvd q \<Longrightarrow> m \<noteq> q \<Longrightarrow> m = 1" by auto
+  case True then show ?thesis
+    apply (auto simp add: numbers_of_marks_sieve One_nat_def numeral_2_eq_2 primes_upto_def dest: prime_gt_Suc_0_nat)
+    apply (simp add: prime_nat_def dvd_def)
+    apply (auto simp add: prime_nat_def aux)
+    done
+qed
+
+end
+
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Number_Theory/Number_Theory.thy
--- a/src/HOL/Number_Theory/Number_Theory.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Number_Theory/Number_Theory.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -2,7 +2,8 @@
 header {* Comprehensive number theory *}
 
 theory Number_Theory
-imports Fib Residues
+imports Fib Residues Eratosthenes
 begin
 
 end
+
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Product_Type.thy
--- a/src/HOL/Product_Type.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Product_Type.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -835,18 +835,34 @@
   "fst (apfst f x) = f (fst x)"
   by (cases x) simp
 
+lemma fst_comp_apfst [simp]:
+  "fst \<circ> apfst f = f \<circ> fst"
+  by (simp add: fun_eq_iff)
+
 lemma fst_apsnd [simp]:
   "fst (apsnd f x) = fst x"
   by (cases x) simp
 
+lemma fst_comp_apsnd [simp]:
+  "fst \<circ> apsnd f = fst"
+  by (simp add: fun_eq_iff)
+
 lemma snd_apfst [simp]:
   "snd (apfst f x) = snd x"
   by (cases x) simp
 
+lemma snd_comp_apfst [simp]:
+  "snd \<circ> apfst f = snd"
+  by (simp add: fun_eq_iff)
+
 lemma snd_apsnd [simp]:
   "snd (apsnd f x) = f (snd x)"
   by (cases x) simp
 
+lemma snd_comp_apsnd [simp]:
+  "snd \<circ> apsnd f = f \<circ> snd"
+  by (simp add: fun_eq_iff)
+
 lemma apfst_compose:
   "apfst f (apfst g x) = apfst (f \<circ> g) x"
   by (cases x) simp
diff -r 16eb76ca1e4a -r 3cbb4e95a565 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sun Feb 17 20:45:49 2013 +0100
+++ b/src/HOL/Set.thy	Sun Feb 17 21:29:30 2013 +0100
@@ -908,6 +908,10 @@
   -- {* The eta-expansion gives variable-name preservation. *}
   by (unfold image_def) blast
 
+lemma Compr_image_eq:
+  "{x \<in> f ` A. P x} = f ` {x \<in> A. P (f x)}"
+  by auto
+
 lemma image_Un: "f`(A Un B) = f`A Un f`B"
   by blast