(* Title: HOL/Proofs/Extraction/Euclid.thy Author: Markus Wenzel, TU Muenchen Author: Freek Wiedijk, Radboud University Nijmegen Author: Stefan Berghofer, TU Muenchen *) section ‹Euclid's theorem› theory Euclid imports "HOL-Computational_Algebra.Primes" Util "HOL-Library.Code_Target_Numeral" "HOL-Library.Realizers" begin text ‹ A constructive version of the proof of Euclid's theorem by Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. › lemma factor_greater_one1: "n = m * k ⟹ m < n ⟹ k < n ⟹ Suc 0 < m" by (induct m) auto lemma factor_greater_one2: "n = m * k ⟹ m < n ⟹ k < n ⟹ Suc 0 < k" by (induct k) auto lemma prod_mn_less_k: "0 < n ⟹ 0 < k ⟹ Suc 0 < m ⟹ m * n = k ⟹ n < k" by (induct m) auto lemma prime_eq: "prime (p::nat) ⟷ 1 < p ∧ (∀m. m dvd p ⟶ 1 < m ⟶ m = p)" apply (simp add: prime_nat_iff) apply (rule iffI) apply blast apply (erule conjE) apply (rule conjI) apply assumption apply (rule allI impI)+ apply (erule allE) apply (erule impE) apply assumption apply (case_tac "m = 0") apply simp apply (case_tac "m = Suc 0") apply simp apply simp done lemma prime_eq': "prime (p::nat) ⟷ 1 < p ∧ (∀m k. p = m * k ⟶ 1 < m ⟶ m = p)" by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) lemma not_prime_ex_mk: assumes n: "Suc 0 < n" shows "(∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k) ∨ prime n" proof - from nat_eq_dec have "(∃m<n. n = m * k) ∨ ¬ (∃m<n. n = m * k)" for k by (rule search) then have "(∃k<n. ∃m<n. n = m * k) ∨ ¬ (∃k<n. ∃m<n. n = m * k)" by (rule search) then show ?thesis proof assume "∃k<n. ∃m<n. n = m * k" then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k" by iprover from nmk m k have "Suc 0 < m" by (rule factor_greater_one1) moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2) ultimately show ?thesis using k m nmk by iprover next assume "¬ (∃k<n. ∃m<n. n = m * k)" then have A: "∀k<n. ∀m<n. n ≠ m * k" by iprover have "∀m k. n = m * k ⟶ Suc 0 < m ⟶ m = n" proof (intro allI impI) fix m k assume nmk: "n = m * k" assume m: "Suc 0 < m" from n m nmk have k: "0 < k" by (cases k) auto moreover from n have n: "0 < n" by simp moreover note m moreover from nmk have "m * k = n" by simp ultimately have kn: "k < n" by (rule prod_mn_less_k) show "m = n" proof (cases "k = Suc 0") case True with nmk show ?thesis by (simp only: mult_Suc_right) next case False from m have "0 < m" by simp moreover note n moreover from False n nmk k have "Suc 0 < k" by auto moreover from nmk have "k * m = n" by (simp only: ac_simps) ultimately have mn: "m < n" by (rule prod_mn_less_k) with kn A nmk show ?thesis by iprover qed qed with n have "prime n" by (simp only: prime_eq' One_nat_def simp_thms) then show ?thesis .. qed qed lemma dvd_factorial: "0 < m ⟹ m ≤ n ⟹ m dvd fact n" proof (induct n rule: nat_induct) case 0 then show ?case by simp next case (Suc n) from ‹m ≤ Suc n› show ?case proof (rule le_SucE) assume "m ≤ n" with ‹0 < m› have "m dvd fact n" by (rule Suc) then have "m dvd (fact n * Suc n)" by (rule dvd_mult2) then show ?thesis by (simp add: mult.commute) next assume "m = Suc n" then have "m dvd (fact n * Suc n)" by (auto intro: dvdI simp: ac_simps) then show ?thesis by (simp add: mult.commute) qed qed lemma dvd_prod [iff]: "n dvd (∏m::nat ∈# mset (n # ns). m)" by (simp add: prod_mset_Un) definition all_prime :: "nat list ⇒ bool" where "all_prime ps ⟷ (∀p∈set ps. prime p)" lemma all_prime_simps: "all_prime []" "all_prime (p # ps) ⟷ prime p ∧ all_prime ps" by (simp_all add: all_prime_def) lemma all_prime_append: "all_prime (ps @ qs) ⟷ all_prime ps ∧ all_prime qs" by (simp add: all_prime_def ball_Un) lemma split_all_prime: assumes "all_prime ms" and "all_prime ns" shows "∃qs. all_prime qs ∧ (∏m::nat ∈# mset qs. m) = (∏m::nat ∈# mset ms. m) * (∏m::nat ∈# mset ns. m)" (is "∃qs. ?P qs ∧ ?Q qs") proof - from assms have "all_prime (ms @ ns)" by (simp add: all_prime_append) moreover have "(∏m::nat ∈# mset (ms @ ns). m) = (∏m::nat ∈# mset ms. m) * (∏m::nat ∈# mset ns. m)" using assms by (simp add: prod_mset_Un) ultimately have "?P (ms @ ns) ∧ ?Q (ms @ ns)" .. then show ?thesis .. qed lemma all_prime_nempty_g_one: assumes "all_prime ps" and "ps ≠ []" shows "Suc 0 < (∏m::nat ∈# mset ps. m)" using ‹ps ≠ []› ‹all_prime ps› unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct) (simp_all add: all_prime_simps prod_mset_Un prime_gt_1_nat less_1_mult del: One_nat_def) lemma factor_exists: "Suc 0 < n ⟹ (∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = n)" proof (induct n rule: nat_wf_ind) case (1 n) from ‹Suc 0 < n› have "(∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k) ∨ prime n" by (rule not_prime_ex_mk) then show ?case proof assume "∃m k. Suc 0 < m ∧ Suc 0 < k ∧ m < n ∧ k < n ∧ n = m * k" then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" and kn: "k < n" and nmk: "n = m * k" by iprover from mn and m have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = m" by (rule 1) then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(∏m::nat ∈# mset ps1. m) = m" by iprover from kn and k have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = k" by (rule 1) then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(∏m::nat ∈# mset ps2. m) = k" by iprover from ‹all_prime ps1› ‹all_prime ps2› have "∃ps. all_prime ps ∧ (∏m::nat ∈# mset ps. m) = (∏m::nat ∈# mset ps1. m) * (∏m::nat ∈# mset ps2. m)" by (rule split_all_prime) with prod_ps1_m prod_ps2_k nmk show ?thesis by simp next assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps) moreover have "(∏m::nat ∈# mset [n]. m) = n" by (simp) ultimately have "all_prime [n] ∧ (∏m::nat ∈# mset [n]. m) = n" .. then show ?thesis .. qed qed lemma prime_factor_exists: assumes N: "(1::nat) < n" shows "∃p. prime p ∧ p dvd n" proof - from N obtain ps where "all_prime ps" and prod_ps: "n = (∏m::nat ∈# mset ps. m)" using factor_exists by simp iprover with N have "ps ≠ []" by (auto simp add: all_prime_nempty_g_one) then obtain p qs where ps: "ps = p # qs" by (cases ps) simp with ‹all_prime ps› have "prime p" by (simp add: all_prime_simps) moreover from ‹all_prime ps› ps prod_ps have "p dvd n" by (simp only: dvd_prod) ultimately show ?thesis by iprover qed text ‹Euclid's theorem: there are infinitely many primes.› lemma Euclid: "∃p::nat. prime p ∧ n < p" proof - let ?k = "fact n + (1::nat)" have "1 < ?k" by simp then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover have "n < p" proof - have "¬ p ≤ n" proof assume pn: "p ≤ n" from ‹prime p› have "0 < p" by (rule prime_gt_0_nat) then have "p dvd fact n" using pn by (rule dvd_factorial) with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat) then have "p dvd 1" by simp with prime show False by auto qed then show ?thesis by simp qed with prime show ?thesis by iprover qed extract Euclid text ‹ The program extracted from the proof of Euclid's theorem looks as follows. @{thm [display] Euclid_def} The program corresponding to the proof of the factorization theorem is @{thm [display] factor_exists_def} › instantiation nat :: default begin definition "default = (0::nat)" instance .. end instantiation list :: (type) default begin definition "default = []" instance .. end primrec iterate :: "nat ⇒ ('a ⇒ 'a) ⇒ 'a ⇒ 'a list" where "iterate 0 f x = []" | "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" lemma "factor_exists 1007 = [53, 19]" by eval lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval lemma "factor_exists 345 = [23, 5, 3]" by eval lemma "factor_exists 999 = [37, 3, 3, 3]" by eval lemma "factor_exists 876 = [73, 3, 2, 2]" by eval lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval end