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