1(* Title: HOL/Proofs/Extraction/Euclid.thy 2 Author: Markus Wenzel, TU Muenchen 3 Author: Freek Wiedijk, Radboud University Nijmegen 4 Author: Stefan Berghofer, TU Muenchen 5*) 6 7section \<open>Euclid's theorem\<close> 8 9theory Euclid 10imports 11 "HOL-Computational_Algebra.Primes" 12 Util 13 "HOL-Library.Code_Target_Numeral" 14 "HOL-Library.Realizers" 15begin 16 17text \<open> 18 A constructive version of the proof of Euclid's theorem by 19 Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. 20\<close> 21 22lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" 23 by (induct m) auto 24 25lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k" 26 by (induct k) auto 27 28lemma prod_mn_less_k: "0 < n \<Longrightarrow> 0 < k \<Longrightarrow> Suc 0 < m \<Longrightarrow> m * n = k \<Longrightarrow> n < k" 29 by (induct m) auto 30 31lemma prime_eq: "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p)" 32 apply (simp add: prime_nat_iff) 33 apply (rule iffI) 34 apply blast 35 apply (erule conjE) 36 apply (rule conjI) 37 apply assumption 38 apply (rule allI impI)+ 39 apply (erule allE) 40 apply (erule impE) 41 apply assumption 42 apply (case_tac "m = 0") 43 apply simp 44 apply (case_tac "m = Suc 0") 45 apply simp 46 apply simp 47 done 48 49lemma prime_eq': "prime (p::nat) \<longleftrightarrow> 1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p)" 50 by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) 51 52lemma not_prime_ex_mk: 53 assumes n: "Suc 0 < n" 54 shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" 55proof - 56 from nat_eq_dec have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" for k 57 by (rule search) 58 then have "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)" 59 by (rule search) 60 then show ?thesis 61 proof 62 assume "\<exists>k<n. \<exists>m<n. n = m * k" 63 then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k" 64 by iprover 65 from nmk m k have "Suc 0 < m" by (rule factor_greater_one1) 66 moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2) 67 ultimately show ?thesis using k m nmk by iprover 68 next 69 assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)" 70 then have A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover 71 have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n" 72 proof (intro allI impI) 73 fix m k 74 assume nmk: "n = m * k" 75 assume m: "Suc 0 < m" 76 from n m nmk have k: "0 < k" 77 by (cases k) auto 78 moreover from n have n: "0 < n" by simp 79 moreover note m 80 moreover from nmk have "m * k = n" by simp 81 ultimately have kn: "k < n" by (rule prod_mn_less_k) 82 show "m = n" 83 proof (cases "k = Suc 0") 84 case True 85 with nmk show ?thesis by (simp only: mult_Suc_right) 86 next 87 case False 88 from m have "0 < m" by simp 89 moreover note n 90 moreover from False n nmk k have "Suc 0 < k" by auto 91 moreover from nmk have "k * m = n" by (simp only: ac_simps) 92 ultimately have mn: "m < n" by (rule prod_mn_less_k) 93 with kn A nmk show ?thesis by iprover 94 qed 95 qed 96 with n have "prime n" 97 by (simp only: prime_eq' One_nat_def simp_thms) 98 then show ?thesis .. 99 qed 100qed 101 102lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact n" 103proof (induct n rule: nat_induct) 104 case 0 105 then show ?case by simp 106next 107 case (Suc n) 108 from \<open>m \<le> Suc n\<close> show ?case 109 proof (rule le_SucE) 110 assume "m \<le> n" 111 with \<open>0 < m\<close> have "m dvd fact n" by (rule Suc) 112 then have "m dvd (fact n * Suc n)" by (rule dvd_mult2) 113 then show ?thesis by (simp add: mult.commute) 114 next 115 assume "m = Suc n" 116 then have "m dvd (fact n * Suc n)" 117 by (auto intro: dvdI simp: ac_simps) 118 then show ?thesis by (simp add: mult.commute) 119 qed 120qed 121 122lemma dvd_prod [iff]: "n dvd (\<Prod>m::nat \<in># mset (n # ns). m)" 123 by (simp add: prod_mset_Un) 124 125definition all_prime :: "nat list \<Rightarrow> bool" 126 where "all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)" 127 128lemma all_prime_simps: 129 "all_prime []" 130 "all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps" 131 by (simp_all add: all_prime_def) 132 133lemma all_prime_append: "all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs" 134 by (simp add: all_prime_def ball_Un) 135 136lemma split_all_prime: 137 assumes "all_prime ms" and "all_prime ns" 138 shows "\<exists>qs. all_prime qs \<and> 139 (\<Prod>m::nat \<in># mset qs. m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" 140 (is "\<exists>qs. ?P qs \<and> ?Q qs") 141proof - 142 from assms have "all_prime (ms @ ns)" 143 by (simp add: all_prime_append) 144 moreover 145 have "(\<Prod>m::nat \<in># mset (ms @ ns). m) = (\<Prod>m::nat \<in># mset ms. m) * (\<Prod>m::nat \<in># mset ns. m)" 146 using assms by (simp add: prod_mset_Un) 147 ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" .. 148 then show ?thesis .. 149qed 150 151lemma all_prime_nempty_g_one: 152 assumes "all_prime ps" and "ps \<noteq> []" 153 shows "Suc 0 < (\<Prod>m::nat \<in># mset ps. m)" 154 using \<open>ps \<noteq> []\<close> \<open>all_prime ps\<close> 155 unfolding One_nat_def [symmetric] 156 by (induct ps rule: list_nonempty_induct) 157 (simp_all add: all_prime_simps prod_mset_Un prime_gt_1_nat less_1_mult del: One_nat_def) 158 159lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = n)" 160proof (induct n rule: nat_wf_ind) 161 case (1 n) 162 from \<open>Suc 0 < n\<close> 163 have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" 164 by (rule not_prime_ex_mk) 165 then show ?case 166 proof 167 assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k" 168 then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" 169 and kn: "k < n" and nmk: "n = m * k" 170 by iprover 171 from mn and m have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = m" 172 by (rule 1) 173 then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(\<Prod>m::nat \<in># mset ps1. m) = m" 174 by iprover 175 from kn and k have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = k" 176 by (rule 1) 177 then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(\<Prod>m::nat \<in># mset ps2. m) = k" 178 by iprover 179 from \<open>all_prime ps1\<close> \<open>all_prime ps2\<close> 180 have "\<exists>ps. all_prime ps \<and> (\<Prod>m::nat \<in># mset ps. m) = 181 (\<Prod>m::nat \<in># mset ps1. m) * (\<Prod>m::nat \<in># mset ps2. m)" 182 by (rule split_all_prime) 183 with prod_ps1_m prod_ps2_k nmk show ?thesis by simp 184 next 185 assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps) 186 moreover have "(\<Prod>m::nat \<in># mset [n]. m) = n" by (simp) 187 ultimately have "all_prime [n] \<and> (\<Prod>m::nat \<in># mset [n]. m) = n" .. 188 then show ?thesis .. 189 qed 190qed 191 192lemma prime_factor_exists: 193 assumes N: "(1::nat) < n" 194 shows "\<exists>p. prime p \<and> p dvd n" 195proof - 196 from N obtain ps where "all_prime ps" and prod_ps: "n = (\<Prod>m::nat \<in># mset ps. m)" 197 using factor_exists by simp iprover 198 with N have "ps \<noteq> []" 199 by (auto simp add: all_prime_nempty_g_one) 200 then obtain p qs where ps: "ps = p # qs" 201 by (cases ps) simp 202 with \<open>all_prime ps\<close> have "prime p" 203 by (simp add: all_prime_simps) 204 moreover from \<open>all_prime ps\<close> ps prod_ps have "p dvd n" 205 by (simp only: dvd_prod) 206 ultimately show ?thesis by iprover 207qed 208 209text \<open>Euclid's theorem: there are infinitely many primes.\<close> 210 211lemma Euclid: "\<exists>p::nat. prime p \<and> n < p" 212proof - 213 let ?k = "fact n + (1::nat)" 214 have "1 < ?k" by simp 215 then obtain p where prime: "prime p" and dvd: "p dvd ?k" 216 using prime_factor_exists by iprover 217 have "n < p" 218 proof - 219 have "\<not> p \<le> n" 220 proof 221 assume pn: "p \<le> n" 222 from \<open>prime p\<close> have "0 < p" by (rule prime_gt_0_nat) 223 then have "p dvd fact n" using pn by (rule dvd_factorial) 224 with dvd have "p dvd ?k - fact n" by (rule dvd_diff_nat) 225 then have "p dvd 1" by simp 226 with prime show False by auto 227 qed 228 then show ?thesis by simp 229 qed 230 with prime show ?thesis by iprover 231qed 232 233extract Euclid 234 235text \<open> 236 The program extracted from the proof of Euclid's theorem looks as follows. 237 @{thm [display] Euclid_def} 238 The program corresponding to the proof of the factorization theorem is 239 @{thm [display] factor_exists_def} 240\<close> 241 242instantiation nat :: default 243begin 244 245definition "default = (0::nat)" 246 247instance .. 248 249end 250 251instantiation list :: (type) default 252begin 253 254definition "default = []" 255 256instance .. 257 258end 259 260primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" 261where 262 "iterate 0 f x = []" 263| "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" 264 265lemma "factor_exists 1007 = [53, 19]" by eval 266lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval 267lemma "factor_exists 345 = [23, 5, 3]" by eval 268lemma "factor_exists 999 = [37, 3, 3, 3]" by eval 269lemma "factor_exists 876 = [73, 3, 2, 2]" by eval 270 271lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval 272 273end 274