# HG changeset patch # User haftmann # Date 1371309563 -7200 # Node ID 7f864f2219a97d4e766ad4b81bc7677a882d51f4 # Parent 08dbf9ff21402d97951c686c7c80b9033ad9d8f2 selection operator smallest_prime_beyond diff -r 08dbf9ff2140 -r 7f864f2219a9 src/HOL/Big_Operators.thy --- 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 @@ "\finite A; P {}; \b A. \finite A; \a\A. b < a; P A\ \ P (insert b A)\ \ P A" by (rule linorder.finite_linorder_max_induct [OF dual_linorder]) +lemma Least_Min: + assumes "finite {a. P a}" and "\a. P a" + shows "(LEAST a. P a) = Min {a. P a}" +proof - + { fix A :: "'a set" + assume A: "finite A" "A \ {}" + have "(LEAST a. a \ 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 \ b \ A) = min a (LEAST a. a \ 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 - diff -r 08dbf9ff2140 -r 7f864f2219a9 src/HOL/List.thy --- 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 \ P) xs + of [] \ None + | x # _ \ 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 "\x \ set xs. P x" + shows "List.find P xs = Some (Min {x\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 \ y \ set xs) \ P y} = {y \ set xs. P y}" + by auto + with Cons False show ?thesis by simp_all + qed +qed + subsubsection {* @{const transpose} on sorted lists *} diff -r 08dbf9ff2140 -r 7f864f2219a9 src/HOL/Number_Theory/Eratosthenes.thy --- 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 \ numbers_of_marks n bs \ m \ {n.. 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 \ nat set" +definition primes_upto :: "nat \ nat list" where - "primes_upto n = {m. m \ n \ prime m}" + "primes_upto n = sorted_list_of_set {m. m \ n \ prime m}" -lemma in_primes_upto: - "m \ primes_upto n \ m \ n \ prime m" +lemma set_primes_upto: + "set (primes_upto n) = {m. m \ n \ 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 \ 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) \ q" @@ -266,11 +280,98 @@ \m\{Suc (Suc 0).. q dvd m \ m dvd q \ m \ q \ 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 \ n \ set (primes_upto n)" + by (simp add: set_primes_upto) + + +subsection {* Application: smallest prime beyond a certain number *} + +definition smallest_prime_beyond :: "nat \ nat" +where + "smallest_prime_beyond n = (LEAST p. prime p \ p \ n)" + +lemma + prime_smallest_prime_beyond [iff]: "prime (smallest_prime_beyond n)" (is ?P) + and smallest_prime_beyond_le [iff]: "smallest_prime_beyond n \ n" (is ?Q) +proof - + let ?least = "LEAST p. prime p \ p \ n" + from primes_infinite obtain q where "prime q \ q \ n" + by (metis finite_nat_set_iff_bounded_le mem_Collect_eq nat_le_linear) + then have "prime ?least \ ?least \ 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 \ p \ n \ smallest_prime_beyond n \ p" + by (simp only: smallest_prime_beyond_def) (auto intro: Least_le) + +lemma smallest_prime_beyond_eq: + "prime p \ p \ n \ (\q. prime q \ q \ n \ q \ p) \ smallest_prime_beyond n = p" + by (simp only: smallest_prime_beyond_def) (auto intro: Least_equality) + +definition smallest_prime_between :: "nat \ nat \ nat option" +where + "smallest_prime_between m n = + (if (\p. prime p \ m \ p \ p \ n) then Some (smallest_prime_beyond m) else None)" + +lemma smallest_prime_between_None: + "smallest_prime_between m n = None \ (\q. m \ q \ q \ n \ \ prime q)" + by (auto simp add: smallest_prime_between_def) + +lemma smallest_prime_betwen_Some: + "smallest_prime_between m n = Some p \ smallest_prime_beyond m = p \ p \ 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 (\p. p \ m) (primes_upto n)" +proof - + { fix p + def A \ "{p. p \ n \ prime p \ m \ p}" + assume assms: "m \ p" "prime p" "p \ n" + then have "smallest_prime_beyond m \ p" by (auto intro: smallest_prime_beyond_smallest) + from this `p \ n` have *: "smallest_prime_beyond m \ n" by (rule order_trans) + from assms have ex: "\p\n. prime p \ m \ 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 (\p. p \ 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 \ nat \ 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 \ p + | None \ 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