author | nipkow |
Sun, 22 Feb 2009 09:52:28 +0100 | |
changeset 30047 | 46c88406e6c0 |
parent 27982 | 2aaa4a5569a6 |
child 31953 | eeb8a300f362 |
permissions | -rw-r--r-- |
25422 | 1 |
(* Title: HOL/Extraction/Euclid.thy |
2 |
ID: $Id$ |
|
3 |
Author: Markus Wenzel, TU Muenchen |
|
4 |
Freek Wiedijk, Radboud University Nijmegen |
|
5 |
Stefan Berghofer, TU Muenchen |
|
6 |
*) |
|
7 |
||
8 |
header {* Euclid's theorem *} |
|
9 |
||
10 |
theory Euclid |
|
27982 | 11 |
imports "~~/src/HOL/NumberTheory/Factorization" Util Efficient_Nat |
25422 | 12 |
begin |
13 |
||
14 |
text {* |
|
15 |
A constructive version of the proof of Euclid's theorem by |
|
16 |
Markus Wenzel and Freek Wiedijk \cite{Wenzel-Wiedijk-JAR2002}. |
|
17 |
*} |
|
18 |
||
19 |
lemma prime_eq: "prime p = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))" |
|
20 |
apply (simp add: prime_def) |
|
21 |
apply (rule iffI) |
|
22 |
apply blast |
|
23 |
apply (erule conjE) |
|
24 |
apply (rule conjI) |
|
25 |
apply assumption |
|
26 |
apply (rule allI impI)+ |
|
27 |
apply (erule allE) |
|
28 |
apply (erule impE) |
|
29 |
apply assumption |
|
30 |
apply (case_tac "m=0") |
|
31 |
apply simp |
|
32 |
apply (case_tac "m=Suc 0") |
|
33 |
apply simp |
|
34 |
apply simp |
|
35 |
done |
|
36 |
||
37 |
lemma prime_eq': "prime p = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))" |
|
38 |
by (simp add: prime_eq dvd_def all_simps [symmetric] del: all_simps) |
|
39 |
||
40 |
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" |
|
41 |
by (induct m) auto |
|
42 |
||
43 |
lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k" |
|
44 |
by (induct k) auto |
|
45 |
||
46 |
lemma not_prime_ex_mk: |
|
47 |
assumes n: "Suc 0 < n" |
|
48 |
shows "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" |
|
49 |
proof - |
|
50 |
{ |
|
51 |
fix k |
|
52 |
from nat_eq_dec |
|
53 |
have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" |
|
54 |
by (rule search) |
|
55 |
} |
|
56 |
hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)" |
|
57 |
by (rule search) |
|
58 |
thus ?thesis |
|
59 |
proof |
|
60 |
assume "\<exists>k<n. \<exists>m<n. n = m * k" |
|
61 |
then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k" |
|
62 |
by iprover |
|
63 |
from nmk m k have "Suc 0 < m" by (rule factor_greater_one1) |
|
64 |
moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2) |
|
65 |
ultimately show ?thesis using k m nmk by iprover |
|
66 |
next |
|
67 |
assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)" |
|
68 |
hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover |
|
69 |
have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n" |
|
70 |
proof (intro allI impI) |
|
71 |
fix m k |
|
72 |
assume nmk: "n = m * k" |
|
73 |
assume m: "Suc 0 < m" |
|
74 |
from n m nmk have k: "0 < k" |
|
75 |
by (cases k) auto |
|
76 |
moreover from n have n: "0 < n" by simp |
|
77 |
moreover note m |
|
78 |
moreover from nmk have "m * k = n" by simp |
|
79 |
ultimately have kn: "k < n" by (rule prod_mn_less_k) |
|
80 |
show "m = n" |
|
81 |
proof (cases "k = Suc 0") |
|
82 |
case True |
|
83 |
with nmk show ?thesis by (simp only: mult_Suc_right) |
|
84 |
next |
|
85 |
case False |
|
86 |
from m have "0 < m" by simp |
|
87 |
moreover note n |
|
88 |
moreover from False n nmk k have "Suc 0 < k" by auto |
|
89 |
moreover from nmk have "k * m = n" by (simp only: mult_ac) |
|
90 |
ultimately have mn: "m < n" by (rule prod_mn_less_k) |
|
91 |
with kn A nmk show ?thesis by iprover |
|
92 |
qed |
|
93 |
qed |
|
94 |
with n have "prime n" |
|
95 |
by (simp only: prime_eq' One_nat_def simp_thms) |
|
96 |
thus ?thesis .. |
|
97 |
qed |
|
98 |
qed |
|
99 |
||
100 |
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>l. primel l \<and> prod l = n)" |
|
101 |
proof (induct n rule: nat_wf_ind) |
|
102 |
case (1 n) |
|
103 |
from `Suc 0 < n` |
|
104 |
have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" |
|
105 |
by (rule not_prime_ex_mk) |
|
106 |
then show ?case |
|
107 |
proof |
|
108 |
assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k" |
|
109 |
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" |
|
110 |
and kn: "k < n" and nmk: "n = m * k" by iprover |
|
111 |
from mn and m have "\<exists>l. primel l \<and> prod l = m" by (rule 1) |
|
112 |
then obtain l1 where primel_l1: "primel l1" and prod_l1_m: "prod l1 = m" |
|
113 |
by iprover |
|
114 |
from kn and k have "\<exists>l. primel l \<and> prod l = k" by (rule 1) |
|
115 |
then obtain l2 where primel_l2: "primel l2" and prod_l2_k: "prod l2 = k" |
|
116 |
by iprover |
|
117 |
from primel_l1 primel_l2 |
|
118 |
have "\<exists>l. primel l \<and> prod l = prod l1 * prod l2" |
|
25687
f92c9dfa7681
split_primel: salvaged original proof after blow with sledghammer
wenzelm
parents:
25422
diff
changeset
|
119 |
by (rule split_primel) |
25422 | 120 |
with prod_l1_m prod_l2_k nmk show ?thesis by simp |
121 |
next |
|
122 |
assume "prime n" |
|
123 |
hence "primel [n] \<and> prod [n] = n" by (rule prime_primel) |
|
124 |
thus ?thesis .. |
|
125 |
qed |
|
126 |
qed |
|
127 |
||
128 |
lemma dvd_prod [iff]: "n dvd prod (n # ns)" |
|
129 |
by simp |
|
130 |
||
25976 | 131 |
primrec fact :: "nat \<Rightarrow> nat" ("(_!)" [1000] 999) |
132 |
where |
|
133 |
"0! = 1" |
|
134 |
| "(Suc n)! = n! * Suc n" |
|
25422 | 135 |
|
136 |
lemma fact_greater_0 [iff]: "0 < n!" |
|
137 |
by (induct n) simp_all |
|
138 |
||
139 |
lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd n!" |
|
140 |
proof (induct n) |
|
141 |
case 0 |
|
142 |
then show ?case by simp |
|
143 |
next |
|
144 |
case (Suc n) |
|
145 |
from `m \<le> Suc n` show ?case |
|
146 |
proof (rule le_SucE) |
|
147 |
assume "m \<le> n" |
|
148 |
with `0 < m` have "m dvd n!" by (rule Suc) |
|
149 |
then have "m dvd (n! * Suc n)" by (rule dvd_mult2) |
|
150 |
then show ?thesis by simp |
|
151 |
next |
|
152 |
assume "m = Suc n" |
|
153 |
then have "m dvd (n! * Suc n)" |
|
154 |
by (auto intro: dvdI simp: mult_ac) |
|
155 |
then show ?thesis by simp |
|
156 |
qed |
|
157 |
qed |
|
158 |
||
159 |
lemma prime_factor_exists: |
|
160 |
assumes N: "(1::nat) < n" |
|
161 |
shows "\<exists>p. prime p \<and> p dvd n" |
|
162 |
proof - |
|
163 |
from N obtain l where primel_l: "primel l" |
|
164 |
and prod_l: "n = prod l" using factor_exists |
|
165 |
by simp iprover |
|
166 |
from prems have "l \<noteq> []" |
|
167 |
by (auto simp add: primel_nempty_g_one) |
|
168 |
then obtain x xs where l: "l = x # xs" |
|
169 |
by (cases l) simp |
|
170 |
from primel_l l have "prime x" by (simp add: primel_hd_tl) |
|
171 |
moreover from primel_l l prod_l |
|
172 |
have "x dvd n" by (simp only: dvd_prod) |
|
173 |
ultimately show ?thesis by iprover |
|
174 |
qed |
|
175 |
||
176 |
text {* |
|
177 |
Euclid's theorem: there are infinitely many primes. |
|
178 |
*} |
|
179 |
||
180 |
lemma Euclid: "\<exists>p. prime p \<and> n < p" |
|
181 |
proof - |
|
182 |
let ?k = "n! + 1" |
|
183 |
have "1 < n! + 1" by simp |
|
184 |
then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover |
|
185 |
have "n < p" |
|
186 |
proof - |
|
187 |
have "\<not> p \<le> n" |
|
188 |
proof |
|
189 |
assume pn: "p \<le> n" |
|
190 |
from `prime p` have "0 < p" by (rule prime_g_zero) |
|
191 |
then have "p dvd n!" using pn by (rule dvd_factorial) |
|
30047 | 192 |
with dvd have "p dvd ?k - n!" by (rule nat_dvd_diff) |
25422 | 193 |
then have "p dvd 1" by simp |
194 |
with prime show False using prime_nd_one by auto |
|
195 |
qed |
|
196 |
then show ?thesis by simp |
|
197 |
qed |
|
198 |
with prime show ?thesis by iprover |
|
199 |
qed |
|
200 |
||
201 |
extract Euclid |
|
202 |
||
203 |
text {* |
|
204 |
The program extracted from the proof of Euclid's theorem looks as follows. |
|
205 |
@{thm [display] Euclid_def} |
|
206 |
The program corresponding to the proof of the factorization theorem is |
|
207 |
@{thm [display] factor_exists_def} |
|
208 |
*} |
|
209 |
||
27982 | 210 |
instantiation nat :: default |
211 |
begin |
|
212 |
||
213 |
definition "default = (0::nat)" |
|
214 |
||
215 |
instance .. |
|
216 |
||
217 |
end |
|
25422 | 218 |
|
27982 | 219 |
instantiation list :: (type) default |
220 |
begin |
|
221 |
||
222 |
definition "default = []" |
|
223 |
||
224 |
instance .. |
|
225 |
||
226 |
end |
|
227 |
||
228 |
consts_code |
|
229 |
default ("(error \"default\")") |
|
25422 | 230 |
|
27982 | 231 |
lemma "factor_exists 1007 = [53, 19]" by evaluation |
232 |
lemma "factor_exists 1007 = [53, 19]" by eval |
|
233 |
||
234 |
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by evaluation |
|
235 |
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval |
|
236 |
||
237 |
lemma "factor_exists 345 = [23, 5, 3]" by evaluation |
|
238 |
lemma "factor_exists 345 = [23, 5, 3]" by eval |
|
239 |
||
240 |
lemma "factor_exists 999 = [37, 3, 3, 3]" by evaluation |
|
241 |
lemma "factor_exists 999 = [37, 3, 3, 3]" by eval |
|
25422 | 242 |
|
27982 | 243 |
lemma "factor_exists 876 = [73, 3, 2, 2]" by evaluation |
244 |
lemma "factor_exists 876 = [73, 3, 2, 2]" by eval |
|
245 |
||
246 |
primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where |
|
247 |
"iterate 0 f x = []" |
|
248 |
| "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" |
|
249 |
||
250 |
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by evaluation |
|
251 |
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval |
|
252 |
||
25422 | 253 |
end |