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