author  haftmann 
Sat, 05 Jul 2014 11:01:53 +0200  
changeset 57514  bdc2c6b40bf2 
parent 57512  cc97b347b301 
child 58622  aa99568f56de 
permissions  rwrr 
39157
b98909faaea8
more explicit HOLProofs sessions, including former ex/Hilbert_Classical.thy which works in parallel mode without the antiquotation option "margin" (which is still critical);
wenzelm
parents:
37598
diff
changeset

1 
(* Title: HOL/Proofs/Extraction/Euclid.thy 
25422  2 
Author: Markus Wenzel, TU Muenchen 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

3 
Author: Freek Wiedijk, Radboud University Nijmegen 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

4 
Author: Stefan Berghofer, TU Muenchen 
25422  5 
*) 
6 

7 
header {* Euclid's theorem *} 

8 

9 
theory Euclid 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39157
diff
changeset

10 
imports 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39157
diff
changeset

11 
"~~/src/HOL/Number_Theory/UniqueFactorization" 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
39157
diff
changeset

12 
Util 
51143
0a2371e7ced3
two target language numeral types: integer and natural, as replacement for code_numeral;
haftmann
parents:
45170
diff
changeset

13 
"~~/src/HOL/Library/Code_Target_Numeral" 
25422  14 
begin 
15 

16 
text {* 

17 
A constructive version of the proof of Euclid's theorem by 

18 
Markus Wenzel and Freek Wiedijk \cite{WenzelWiedijkJAR2002}. 

19 
*} 

20 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

21 
lemma factor_greater_one1: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < m" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

22 
by (induct m) auto 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

23 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

24 
lemma factor_greater_one2: "n = m * k \<Longrightarrow> m < n \<Longrightarrow> k < n \<Longrightarrow> Suc 0 < k" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

25 
by (induct k) auto 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

26 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

27 
lemma prod_mn_less_k: 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

28 
"(0::nat) < n ==> 0 < k ==> Suc 0 < m ==> m * n = k ==> n < k" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

29 
by (induct m) auto 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

30 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

31 
lemma prime_eq: "prime (p::nat) = (1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> 1 < m \<longrightarrow> m = p))" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

32 
apply (simp add: prime_nat_def) 
25422  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 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

49 
lemma prime_eq': "prime (p::nat) = (1 < p \<and> (\<forall>m k. p = m * k \<longrightarrow> 1 < m \<longrightarrow> m = p))" 
37598  50 
by (simp add: prime_eq dvd_def HOL.all_simps [symmetric] del: HOL.all_simps) 
25422  51 

52 
lemma 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" 

55 
proof  

56 
{ 

57 
fix k 

58 
from nat_eq_dec 

59 
have "(\<exists>m<n. n = m * k) \<or> \<not> (\<exists>m<n. n = m * k)" 

60 
by (rule search) 

61 
} 

62 
hence "(\<exists>k<n. \<exists>m<n. n = m * k) \<or> \<not> (\<exists>k<n. \<exists>m<n. n = m * k)" 

63 
by (rule search) 

64 
thus ?thesis 

65 
proof 

66 
assume "\<exists>k<n. \<exists>m<n. n = m * k" 

67 
then obtain k m where k: "k<n" and m: "m<n" and nmk: "n = m * k" 

68 
by iprover 

69 
from nmk m k have "Suc 0 < m" by (rule factor_greater_one1) 

70 
moreover from nmk m k have "Suc 0 < k" by (rule factor_greater_one2) 

71 
ultimately show ?thesis using k m nmk by iprover 

72 
next 

73 
assume "\<not> (\<exists>k<n. \<exists>m<n. n = m * k)" 

74 
hence A: "\<forall>k<n. \<forall>m<n. n \<noteq> m * k" by iprover 

75 
have "\<forall>m k. n = m * k \<longrightarrow> Suc 0 < m \<longrightarrow> m = n" 

76 
proof (intro allI impI) 

77 
fix m k 

78 
assume nmk: "n = m * k" 

79 
assume m: "Suc 0 < m" 

80 
from n m nmk have k: "0 < k" 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

81 
by (cases k) auto 
25422  82 
moreover from n have n: "0 < n" by simp 
83 
moreover note m 

84 
moreover from nmk have "m * k = n" by simp 

85 
ultimately have kn: "k < n" by (rule prod_mn_less_k) 

86 
show "m = n" 

87 
proof (cases "k = Suc 0") 

32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

88 
case True 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

89 
with nmk show ?thesis by (simp only: mult_Suc_right) 
25422  90 
next 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

91 
case False 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

92 
from m have "0 < m" by simp 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

93 
moreover note n 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

94 
moreover from False n nmk k have "Suc 0 < k" by auto 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

95 
moreover from nmk have "k * m = n" by (simp only: ac_simps) 
32960
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

96 
ultimately have mn: "m < n" by (rule prod_mn_less_k) 
69916a850301
eliminated hard tabulators, guessing at each author's individual tabwidth;
wenzelm
parents:
32479
diff
changeset

97 
with kn A nmk show ?thesis by iprover 
25422  98 
qed 
99 
qed 

100 
with n have "prime n" 

101 
by (simp only: prime_eq' One_nat_def simp_thms) 

102 
thus ?thesis .. 

103 
qed 

104 
qed 

105 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

106 
lemma dvd_factorial: "0 < m \<Longrightarrow> m \<le> n \<Longrightarrow> m dvd fact (n::nat)" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

107 
proof (induct n rule: nat_induct) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

108 
case 0 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

109 
then show ?case by simp 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

110 
next 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

111 
case (Suc n) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

112 
from `m \<le> Suc n` show ?case 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

113 
proof (rule le_SucE) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

114 
assume "m \<le> n" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

115 
with `0 < m` have "m dvd fact n" by (rule Suc) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

116 
then have "m dvd (fact n * Suc n)" by (rule dvd_mult2) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
51143
diff
changeset

117 
then show ?thesis by (simp add: mult.commute) 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

118 
next 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

119 
assume "m = Suc n" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

120 
then have "m dvd (fact n * Suc n)" 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

121 
by (auto intro: dvdI simp: ac_simps) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
51143
diff
changeset

122 
then show ?thesis by (simp add: mult.commute) 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

123 
qed 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

124 
qed 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

125 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

126 
lemma dvd_prod [iff]: "n dvd (PROD m\<Colon>nat:#multiset_of (n # ns). m)" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

127 
by (simp add: msetprod_Un msetprod_singleton) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

128 

37335  129 
definition all_prime :: "nat list \<Rightarrow> bool" where 
130 
"all_prime ps \<longleftrightarrow> (\<forall>p\<in>set ps. prime p)" 

131 

132 
lemma all_prime_simps: 

133 
"all_prime []" 

134 
"all_prime (p # ps) \<longleftrightarrow> prime p \<and> all_prime ps" 

135 
by (simp_all add: all_prime_def) 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

136 

37335  137 
lemma all_prime_append: 
138 
"all_prime (ps @ qs) \<longleftrightarrow> all_prime ps \<and> all_prime qs" 

139 
by (simp add: all_prime_def ball_Un) 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

140 

37335  141 
lemma split_all_prime: 
142 
assumes "all_prime ms" and "all_prime ns" 

143 
shows "\<exists>qs. all_prime qs \<and> (PROD m\<Colon>nat:#multiset_of qs. m) = 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

144 
(PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs") 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

145 
proof  
37335  146 
from assms have "all_prime (ms @ ns)" 
147 
by (simp add: all_prime_append) 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

148 
moreover from assms have "(PROD m\<Colon>nat:#multiset_of (ms @ ns). m) = 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

149 
(PROD m\<Colon>nat:#multiset_of ms. m) * (PROD m\<Colon>nat:#multiset_of ns. m)" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

150 
by (simp add: msetprod_Un) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

151 
ultimately have "?P (ms @ ns) \<and> ?Q (ms @ ns)" .. 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

152 
then show ?thesis .. 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

153 
qed 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

154 

37335  155 
lemma all_prime_nempty_g_one: 
156 
assumes "all_prime ps" and "ps \<noteq> []" 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

157 
shows "Suc 0 < (PROD m\<Colon>nat:#multiset_of ps. m)" 
37335  158 
using `ps \<noteq> []` `all_prime ps` unfolding One_nat_def [symmetric] by (induct ps rule: list_nonempty_induct) 
37336  159 
(simp_all add: all_prime_simps msetprod_singleton msetprod_Un prime_gt_1_nat less_1_mult del: One_nat_def) 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

160 

37335  161 
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = n)" 
25422  162 
proof (induct n rule: nat_wf_ind) 
163 
case (1 n) 

164 
from `Suc 0 < n` 

165 
have "(\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k) \<or> prime n" 

166 
by (rule not_prime_ex_mk) 

167 
then show ?case 

168 
proof 

169 
assume "\<exists>m k. Suc 0 < m \<and> Suc 0 < k \<and> m < n \<and> k < n \<and> n = m * k" 

170 
then obtain m k where m: "Suc 0 < m" and k: "Suc 0 < k" and mn: "m < n" 

171 
and kn: "k < n" and nmk: "n = m * k" by iprover 

37335  172 
from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = m" by (rule 1) 
173 
then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m\<Colon>nat:#multiset_of ps1. m) = m" 

25422  174 
by iprover 
37335  175 
from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = k" by (rule 1) 
176 
then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m\<Colon>nat:#multiset_of ps2. m) = k" 

25422  177 
by iprover 
37335  178 
from `all_prime ps1` `all_prime ps2` 
179 
have "\<exists>ps. all_prime ps \<and> (PROD m\<Colon>nat:#multiset_of ps. m) = 

180 
(PROD m\<Colon>nat:#multiset_of ps1. m) * (PROD m\<Colon>nat:#multiset_of ps2. m)" 

181 
by (rule split_all_prime) 

182 
with prod_ps1_m prod_ps2_k nmk show ?thesis by simp 

25422  183 
next 
37335  184 
assume "prime n" then have "all_prime [n]" by (simp add: all_prime_simps) 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

185 
moreover have "(PROD m\<Colon>nat:#multiset_of [n]. m) = n" by (simp add: msetprod_singleton) 
37335  186 
ultimately have "all_prime [n] \<and> (PROD m\<Colon>nat:#multiset_of [n]. m) = n" .. 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

187 
then show ?thesis .. 
25422  188 
qed 
189 
qed 

190 

191 
lemma prime_factor_exists: 

192 
assumes N: "(1::nat) < n" 

193 
shows "\<exists>p. prime p \<and> p dvd n" 

194 
proof  

37335  195 
from N obtain ps where "all_prime ps" 
196 
and prod_ps: "n = (PROD m\<Colon>nat:#multiset_of ps. m)" using factor_exists 

25422  197 
by simp iprover 
37335  198 
with N have "ps \<noteq> []" 
199 
by (auto simp add: all_prime_nempty_g_one msetprod_empty) 

200 
then obtain p qs where ps: "ps = p # qs" by (cases ps) simp 

201 
with `all_prime ps` have "prime p" by (simp add: all_prime_simps) 

202 
moreover from `all_prime ps` ps prod_ps 

203 
have "p dvd n" by (simp only: dvd_prod) 

25422  204 
ultimately show ?thesis by iprover 
205 
qed 

206 

207 
text {* 

208 
Euclid's theorem: there are infinitely many primes. 

209 
*} 

210 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

211 
lemma Euclid: "\<exists>p::nat. prime p \<and> n < p" 
25422  212 
proof  
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

213 
let ?k = "fact n + 1" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

214 
have "1 < fact n + 1" by simp 
25422  215 
then obtain p where prime: "prime p" and dvd: "p dvd ?k" using prime_factor_exists by iprover 
216 
have "n < p" 

217 
proof  

218 
have "\<not> p \<le> n" 

219 
proof 

220 
assume pn: "p \<le> n" 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

221 
from `prime p` have "0 < p" by (rule prime_gt_0_nat) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

222 
then have "p dvd fact n" using pn by (rule dvd_factorial) 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

223 
with dvd have "p dvd ?k  fact n" by (rule dvd_diff_nat) 
25422  224 
then have "p dvd 1" by simp 
37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

225 
with prime show False by auto 
25422  226 
qed 
227 
then show ?thesis by simp 

228 
qed 

229 
with prime show ?thesis by iprover 

230 
qed 

231 

232 
extract Euclid 

233 

234 
text {* 

235 
The program extracted from the proof of Euclid's theorem looks as follows. 

236 
@{thm [display] Euclid_def} 

237 
The program corresponding to the proof of the factorization theorem is 

238 
@{thm [display] factor_exists_def} 

239 
*} 

240 

27982  241 
instantiation nat :: default 
242 
begin 

243 

244 
definition "default = (0::nat)" 

245 

246 
instance .. 

247 

248 
end 

25422  249 

27982  250 
instantiation list :: (type) default 
251 
begin 

252 

253 
definition "default = []" 

254 

255 
instance .. 

256 

257 
end 

258 

37288
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

259 
primrec iterate :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a \<Rightarrow> 'a list" where 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

260 
"iterate 0 f x = []" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

261 
 "iterate (Suc n) f x = (let y = f x in y # iterate n f y)" 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

262 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

263 
lemma "factor_exists 1007 = [53, 19]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

264 
lemma "factor_exists 567 = [7, 3, 3, 3, 3]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

265 
lemma "factor_exists 345 = [23, 5, 3]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

266 
lemma "factor_exists 999 = [37, 3, 3, 3]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

267 
lemma "factor_exists 876 = [73, 3, 2, 2]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

268 

2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

269 
lemma "iterate 4 Euclid 0 = [2, 3, 7, 71]" by eval 
2b1c6dd48995
removed dependency of Euclid on Old_Number_Theory
haftmann
parents:
32960
diff
changeset

270 

25422  271 
end 