selection operator smallest_prime_beyond

--- a/src/HOL/Big_Operators.thy	Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/Big_Operators.thy	Sat Jun 15 17:19:23 2013 +0200
@@ -2107,6 +2107,24 @@
   "\<lbrakk>finite A; P {}; \<And>b A. \<lbrakk>finite A; \<forall>a\<in>A. b < a; P A\<rbrakk> \<Longrightarrow> P (insert b A)\<rbrakk> \<Longrightarrow> P A"
   by (rule linorder.finite_linorder_max_induct [OF dual_linorder])
 
+lemma Least_Min:
+  assumes "finite {a. P a}" and "\<exists>a. P a"
+  shows "(LEAST a. P a) = Min {a. P a}"
+proof -
+  { fix A :: "'a set"
+    assume A: "finite A" "A \<noteq> {}"
+    have "(LEAST a. a \<in> A) = Min A"
+    using A proof (induct A rule: finite_ne_induct)
+      case singleton show ?case by (rule Least_equality) simp_all
+    next
+      case (insert a A)
+      have "(LEAST b. b = a \<or> b \<in> A) = min a (LEAST a. a \<in> A)"
+        by (auto intro!: Least_equality simp add: min_def not_le Min_le_iff insert.hyps dest!: less_imp_le)
+      with insert show ?case by simp
+    qed
+  } from this [of "{a. P a}"] assms show ?thesis by simp
+qed
+
 end
 
 context linordered_ab_semigroup_add
@@ -2177,4 +2195,3 @@
 end
 
 end
-

--- a/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/List.thy	Sat Jun 15 17:19:23 2013 +0200
@@ -3515,6 +3515,12 @@
   thus ?thesis using Some by auto
 qed
 
+lemma find_dropWhile:
+  "List.find P xs = (case dropWhile (Not \<circ> P) xs
+   of [] \<Rightarrow> None
+    | x # _ \<Rightarrow> Some x)"
+  by (induct xs) simp_all
+
 
 subsubsection {* @{const remove1} *}
 
@@ -3864,6 +3870,10 @@
   by (rule pair_list_eqI)
     (simp_all add: not_le, simp del: map_map [simp del] add: map_Suc_upt map_map [symmetric])
 
+lemma distinct_enumerate [simp]:
+  "distinct (enumerate n xs)"
+  by (simp add: enumerate_eq_zip distinct_zipI1)
+
 
 subsubsection {* @{const rotate1} and @{const rotate} *}
 
@@ -4693,6 +4703,22 @@
 apply(simp add:sorted_Cons)
 done
 
+lemma sorted_find_Min:
+  assumes "sorted xs"
+  assumes "\<exists>x \<in> set xs. P x"
+  shows "List.find P xs = Some (Min {x\<in>set xs. P x})"
+using assms proof (induct xs rule: sorted.induct)
+  case Nil then show ?case by simp
+next
+  case (Cons xs x) show ?case proof (cases "P x")
+    case True with Cons show ?thesis by (auto intro: Min_eqI [symmetric])
+  next
+    case False then have "{y. (y = x \<or> y \<in> set xs) \<and> P y} = {y \<in> set xs. P y}"
+      by auto
+    with Cons False show ?thesis by simp_all
+  qed
+qed
+
 
 subsubsection {* @{const transpose} on sorted lists *}
 

--- a/src/HOL/Number_Theory/Eratosthenes.thy	Sat Jun 15 17:19:23 2013 +0200
+++ b/src/HOL/Number_Theory/Eratosthenes.thy	Sat Jun 15 17:19:23 2013 +0200
@@ -5,9 +5,10 @@
 header {* The sieve of Eratosthenes *}
 
 theory Eratosthenes
-imports Primes
+imports Main Primes
 begin
 
+
 subsection {* Preliminary: strict divisibility *}
 
 context dvd
@@ -51,6 +52,11 @@
   "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)
 
+lemma sorted_list_of_set_numbers_of_marks:
+  "sorted_list_of_set (numbers_of_marks n bs) = map fst (filter snd (enumerate n bs))"
+  by (auto simp add: numbers_of_marks_def distinct_map
+    intro!: sorted_filter distinct_filter inj_onI sorted_distinct_set_unique)
+
 
 text {* Marking out multiples in a sieve  *}
  
@@ -228,22 +234,30 @@
 qed
 
 
-text {* Relation the sieve algorithm to actual primes *}
+text {* Relation of the sieve algorithm to actual primes *}
 
-definition primes_upto :: "nat \<Rightarrow> nat set"
+definition primes_upto :: "nat \<Rightarrow> nat list"
 where
-  "primes_upto n = {m. m \<le> n \<and> prime m}"
+  "primes_upto n = sorted_list_of_set {m. m \<le> n \<and> prime m}"
 
-lemma in_primes_upto:
-  "m \<in> primes_upto n \<longleftrightarrow> m \<le> n \<and> prime m"
+lemma set_primes_upto:
+  "set (primes_upto n) = {m. 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))"
+lemma sorted_primes_upto [iff]:
+  "sorted (primes_upto n)"
+  by (simp add: primes_upto_def)
+
+lemma distinct_primes_upto [iff]:
+  "distinct (primes_upto n)"
+  by (simp add: primes_upto_def)
+
+lemma set_primes_upto_sieve:
+  "set (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)
+    by (auto simp add: numbers_of_marks_sieve One_nat_def numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
 next
   { fix m q
     assume "Suc (Suc 0) \<le> q"
@@ -266,11 +280,98 @@
     \<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 (auto simp add: numbers_of_marks_sieve One_nat_def numeral_2_eq_2 set_primes_upto dest: prime_gt_Suc_0_nat)
     apply (simp add: prime_nat_def dvd_def)
     apply (auto simp add: prime_nat_def aux)
     done
 qed
 
+lemma primes_upto_sieve [code]:
+  "primes_upto n = map fst (filter snd (enumerate 2 (sieve 1 (replicate (n - 1) True))))"
+proof -
+  have "primes_upto n = sorted_list_of_set (numbers_of_marks 2 (sieve 1 (replicate (n - 1) True)))"
+    apply (rule sorted_distinct_set_unique)
+    apply (simp_all only: set_primes_upto_sieve numbers_of_marks_def)
+    apply auto
+    done
+  then show ?thesis by (simp add: sorted_list_of_set_numbers_of_marks)
+qed
+
+lemma prime_in_primes_upto:
+  "prime n \<longleftrightarrow> n \<in> set (primes_upto n)"
+  by (simp add: set_primes_upto)
+
+
+subsection {* Application: smallest prime beyond a certain number *}
+
+definition smallest_prime_beyond :: "nat \<Rightarrow> nat"
+where
+  "smallest_prime_beyond n = (LEAST p. prime p \<and> p \<ge> n)"
+
+lemma
+  prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P)
+  and smallest_prime_beyond_le [iff]: "smallest_prime_beyond n \<ge> n" (is ?Q)
+proof -
+  let ?least = "LEAST p. prime p \<and> p \<ge> n"
+  from primes_infinite obtain q where "prime q \<and> q \<ge> n"
+    by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear)
+  then have "prime ?least \<and> ?least \<ge> n" by (rule LeastI)
+  then show ?P and ?Q by (simp_all add: smallest_prime_beyond_def)
+qed
+
+lemma smallest_prime_beyond_smallest:
+  "prime p \<Longrightarrow> p \<ge> n \<Longrightarrow> smallest_prime_beyond n \<le> p"
+  by (simp only: smallest_prime_beyond_def) (auto intro: Least_le)
+
+lemma smallest_prime_beyond_eq:
+  "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"
+  by (simp only: smallest_prime_beyond_def) (auto intro: Least_equality)
+
+definition smallest_prime_between :: "nat \<Rightarrow> nat \<Rightarrow> nat option"
+where
+  "smallest_prime_between m n =
+    (if (\<exists>p. prime p \<and> m \<le> p \<and> p \<le> n) then Some (smallest_prime_beyond m) else None)"
+
+lemma smallest_prime_between_None:
+  "smallest_prime_between m n = None \<longleftrightarrow> (\<forall>q. m \<le> q \<and> q \<le> n \<longrightarrow> \<not> prime q)"
+  by (auto simp add: smallest_prime_between_def)
+
+lemma smallest_prime_betwen_Some:
+  "smallest_prime_between m n = Some p \<longleftrightarrow> smallest_prime_beyond m = p \<and> p \<le> n"
+  by (auto simp add: smallest_prime_between_def dest: smallest_prime_beyond_smallest [of _ m])
+
+lemma [code]:
+  "smallest_prime_between m n = List.find (\<lambda>p. p \<ge> m) (primes_upto n)"
+proof -
+  { fix p
+    def A \<equiv> "{p. p \<le> n \<and> prime p \<and> m \<le> p}"
+    assume assms: "m \<le> p" "prime p" "p \<le> n"
+    then have "smallest_prime_beyond m \<le> p" by (auto intro: smallest_prime_beyond_smallest)
+    from this `p \<le> n` have *: "smallest_prime_beyond m \<le> n" by (rule order_trans)
+    from assms have ex: "\<exists>p\<le>n. prime p \<and> m \<le> p" by auto
+    then have "finite A" by (auto simp add: A_def)
+    with * have "Min A = smallest_prime_beyond m"
+      by (auto simp add: A_def intro: Min_eqI smallest_prime_beyond_smallest)
+    with ex sorted_primes_upto have "List.find (\<lambda>p. p \<ge> m) (primes_upto n) = Some (smallest_prime_beyond m)"
+      by (auto simp add: set_primes_upto sorted_find_Min A_def)
+  } then show ?thesis  
+  by (auto simp add: smallest_prime_between_def find_None_iff set_primes_upto intro!: sym [of _ None])
+qed
+
+definition smallest_prime_beyond_aux :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where
+  "smallest_prime_beyond_aux k n = smallest_prime_beyond n"
+
+lemma [code]:
+  "smallest_prime_beyond_aux k n =
+    (case smallest_prime_between n (k * n)
+     of Some p \<Rightarrow> p
+      | None \<Rightarrow> smallest_prime_beyond_aux (Suc k) n)"
+  by (simp add: smallest_prime_beyond_aux_def smallest_prime_betwen_Some split: option.split)
+
+lemma [code]:
+  "smallest_prime_beyond n = smallest_prime_beyond_aux 2 n"
+  by (simp add: smallest_prime_beyond_aux_def)
+
 end