author  wenzelm 
Tue, 07 Jul 2009 20:16:06 +0200  
changeset 31953  eeb8a300f362 
parent 30047  46c88406e6c0 
child 32479  521cc9bf2958 
permissions  rwrr 
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{WenzelWiedijkJAR2002}. 

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) 

31953  192 
with dvd have "p dvd ?k  n!" by (rule dvd_diff_nat) 
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 