author | wenzelm |
Tue, 01 Sep 2015 22:32:58 +0200 | |
changeset 61076 | bdc1e2f0a86a |
parent 60515 | 484559628038 |
child 61762 | d50b993b4fb9 |
permissions | -rw-r--r-- |
39157
b98909faaea8
more explicit HOL-Proofs 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 tab-width;
wenzelm
parents:
32479
diff
changeset
|
3 |
Author: Freek Wiedijk, Radboud University Nijmegen |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
4 |
Author: Stefan Berghofer, TU Muenchen |
25422 | 5 |
*) |
6 |
||
58889 | 7 |
section {* Euclid's theorem *} |
25422 | 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 |
|
58622 | 18 |
Markus Wenzel and Freek Wiedijk @{cite "Wenzel-Wiedijk-JAR2002"}. |
25422 | 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 tab-width;
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 tab-width;
wenzelm
parents:
32479
diff
changeset
|
88 |
case True |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 tab-width;
wenzelm
parents:
32479
diff
changeset
|
91 |
case False |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
92 |
from m have "0 < m" by simp |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
wenzelm
parents:
32479
diff
changeset
|
93 |
moreover note n |
69916a850301
eliminated hard tabulators, guessing at each author's individual tab-width;
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 tab-width;
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 tab-width;
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 |
|
61076 | 126 |
lemma dvd_prod [iff]: "n dvd (PROD m::nat:#mset (n # ns). m)" |
37288
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" |
|
61076 | 143 |
shows "\<exists>qs. all_prime qs \<and> (PROD m::nat:#mset qs. m) = |
144 |
(PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)" (is "\<exists>qs. ?P qs \<and> ?Q qs") |
|
37288
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) |
|
61076 | 148 |
moreover from assms have "(PROD m::nat:#mset (ms @ ns). m) = |
149 |
(PROD m::nat:#mset ms. m) * (PROD m::nat:#mset ns. m)" |
|
37288
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> []" |
|
61076 | 157 |
shows "Suc 0 < (PROD m::nat:#mset 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 |
|
61076 | 161 |
lemma factor_exists: "Suc 0 < n \<Longrightarrow> (\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset 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 |
|
61076 | 172 |
from mn and m have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = m" by (rule 1) |
173 |
then obtain ps1 where "all_prime ps1" and prod_ps1_m: "(PROD m::nat:#mset ps1. m) = m" |
|
25422 | 174 |
by iprover |
61076 | 175 |
from kn and k have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = k" by (rule 1) |
176 |
then obtain ps2 where "all_prime ps2" and prod_ps2_k: "(PROD m::nat:#mset ps2. m) = k" |
|
25422 | 177 |
by iprover |
37335 | 178 |
from `all_prime ps1` `all_prime ps2` |
61076 | 179 |
have "\<exists>ps. all_prime ps \<and> (PROD m::nat:#mset ps. m) = |
180 |
(PROD m::nat:#mset ps1. m) * (PROD m::nat:#mset ps2. m)" |
|
37335 | 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) |
61076 | 185 |
moreover have "(PROD m::nat:#mset [n]. m) = n" by (simp add: msetprod_singleton) |
186 |
ultimately have "all_prime [n] \<and> (PROD m::nat:#mset [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" |
61076 | 196 |
and prod_ps: "n = (PROD m::nat:#mset 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 - |
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
213 |
let ?k = "fact n + (1::nat)" |
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
214 |
have "1 < ?k" 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 |