author | paulson |
Mon, 20 Mar 2000 18:24:11 +0100 | |
changeset 8528 | 6c48043ccd0e |
parent 8442 | 96023903c2df |
child 8600 | a466c687c726 |
permissions | -rw-r--r-- |
8353 | 1 |
(* Title: HOL/ex/Factorization.thy |
2 |
ID: $Id$ |
|
3 |
Author: Thomas Marthedal Rasmussen |
|
4 |
Copyright 2000 University of Cambridge |
|
5 |
||
6 |
Fundamental Theorem of Arithmetic (unique factorization into primes) |
|
7 |
*) |
|
8 |
||
9 |
||
10 |
(* --- Arithmetic --- *) |
|
11 |
||
12 |
Goal "[| m ~= m*k; m ~= 1 |] ==> 1<m"; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
13 |
by (case_tac "m" 1); |
8353 | 14 |
by Auto_tac; |
15 |
qed "one_less_m"; |
|
16 |
||
17 |
Goal "[| m ~= m*k; 1<m*k |] ==> 1<k"; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
18 |
by (case_tac "k" 1); |
8353 | 19 |
by Auto_tac; |
20 |
qed "one_less_k"; |
|
21 |
||
22 |
Goal "[| 0<k; k*n=k*m |] ==> n=m"; |
|
23 |
by Auto_tac; |
|
24 |
qed "mult_left_cancel"; |
|
25 |
||
26 |
Goal "[| 0<m; m*n = m |] ==> n=1"; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
27 |
by (case_tac "n" 1); |
8353 | 28 |
by Auto_tac; |
29 |
qed "mn_eq_m_one"; |
|
30 |
||
31 |
Goal "[| 0<n; 0<k |] ==> 1<m --> m*n = k --> n<k"; |
|
32 |
by (induct_tac "m" 1); |
|
33 |
by Auto_tac; |
|
34 |
qed_spec_mp "prod_mn_less_k"; |
|
35 |
||
36 |
||
37 |
(* --- Prime List & Product --- *) |
|
38 |
||
39 |
Goal "prod (xs @ ys) = prod xs * prod ys"; |
|
40 |
by (induct_tac "xs" 1); |
|
41 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps [mult_assoc]))); |
|
42 |
qed "prod_append"; |
|
43 |
||
44 |
Goal "prod (x#xs) = prod (y#ys) ==> x*prod xs = y*prod ys"; |
|
45 |
by Auto_tac; |
|
46 |
qed "prod_xy_prod"; |
|
47 |
||
48 |
Goalw [primel_def] "primel (xs @ ys) = (primel xs & primel ys)"; |
|
49 |
by Auto_tac; |
|
50 |
qed "primel_append"; |
|
51 |
||
52 |
Goalw [primel_def] "n:prime ==> primel [n] & prod [n] = n"; |
|
53 |
by Auto_tac; |
|
54 |
qed "prime_primel"; |
|
55 |
||
56 |
Goalw [prime_def,dvd_def] "p:prime ==> ~(p dvd 1)"; |
|
57 |
by Auto_tac; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
58 |
by (case_tac "k" 1); |
8353 | 59 |
by Auto_tac; |
60 |
qed "prime_nd_one"; |
|
61 |
||
62 |
Goalw [dvd_def] "[| prod (x#xs) = prod ys |] ==> x dvd (prod ys)"; |
|
63 |
by (rtac exI 1); |
|
64 |
by (rtac sym 1); |
|
65 |
by (Asm_full_simp_tac 1); |
|
66 |
qed "hd_dvd_prod"; |
|
67 |
||
68 |
Goalw [primel_def] "primel (x#xs) ==> primel xs"; |
|
69 |
by Auto_tac; |
|
70 |
qed "primel_tl"; |
|
71 |
||
72 |
Goalw [primel_def] "(primel (x#xs)) = (x:prime & primel xs)"; |
|
73 |
by Auto_tac; |
|
74 |
qed "primel_hd_tl"; |
|
75 |
||
76 |
Goalw [prime_def] "[| p:prime; q:prime; p dvd q |] ==> p=q"; |
|
77 |
by Auto_tac; |
|
78 |
qed "primes_eq"; |
|
79 |
||
80 |
Goalw [primel_def,prime_def] "[| primel xs; prod xs = 1 |] ==> xs = []"; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
81 |
by (case_tac "xs" 1); |
8353 | 82 |
by (ALLGOALS Asm_full_simp_tac); |
83 |
qed "primel_one_empty"; |
|
84 |
||
85 |
Goalw [prime_def] "p:prime ==> 1<p"; |
|
86 |
by Auto_tac; |
|
87 |
qed "prime_g_one"; |
|
88 |
||
89 |
Goalw [prime_def] "p:prime ==> 0<p"; |
|
90 |
by Auto_tac; |
|
91 |
qed "prime_g_zero"; |
|
92 |
||
93 |
Goalw [primel_def,prime_def] "primel xs --> xs ~= [] --> 1 < prod xs"; |
|
94 |
by (induct_tac "xs" 1); |
|
95 |
by (auto_tac (claset() addEs [one_less_mult], simpset())); |
|
96 |
qed_spec_mp "primel_nempty_g_one"; |
|
97 |
||
98 |
Goalw [primel_def,prime_def] "primel xs --> 0 < prod xs"; |
|
99 |
by (induct_tac "xs" 1); |
|
100 |
by Auto_tac; |
|
101 |
qed_spec_mp "primel_prod_gz"; |
|
102 |
||
103 |
||
104 |
(* --- Sorting --- *) |
|
105 |
||
106 |
Goal "nondec xs --> nondec (oinsert x xs)"; |
|
107 |
by (induct_tac "xs" 1); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
108 |
by (case_tac "list" 2); |
8353 | 109 |
by (ALLGOALS (Asm_full_simp_tac)); |
110 |
qed_spec_mp "nondec_oinsert"; |
|
111 |
||
112 |
Goal "nondec (sort xs)"; |
|
113 |
by (induct_tac "xs" 1); |
|
114 |
by (ALLGOALS (Asm_full_simp_tac)); |
|
115 |
by (etac nondec_oinsert 1); |
|
116 |
qed "nondec_sort"; |
|
117 |
||
118 |
Goal "[| x<=y; l=y#ys |] ==> x#l = oinsert x l"; |
|
119 |
by (ALLGOALS Asm_full_simp_tac); |
|
120 |
qed "x_less_y_oinsert"; |
|
121 |
||
122 |
Goal "nondec xs --> xs = sort xs"; |
|
123 |
by (induct_tac "xs" 1); |
|
124 |
by Safe_tac; |
|
125 |
by (ALLGOALS Asm_full_simp_tac); |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
126 |
by (case_tac "list" 1); |
8353 | 127 |
by (ALLGOALS Asm_full_simp_tac); |
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
128 |
by (case_tac "list" 1); |
8353 | 129 |
by (Asm_full_simp_tac 1); |
130 |
by (res_inst_tac [("y","aa"),("ys","lista")] x_less_y_oinsert 1); |
|
131 |
by (ALLGOALS Asm_full_simp_tac); |
|
132 |
qed_spec_mp "nondec_sort_eq"; |
|
133 |
||
134 |
Goal "oinsert x (oinsert y l) = oinsert y (oinsert x l)"; |
|
135 |
by (induct_tac "l" 1); |
|
8528 | 136 |
by Auto_tac; |
8353 | 137 |
qed "oinsert_x_y"; |
138 |
||
139 |
||
140 |
(* --- Permutation --- *) |
|
141 |
||
142 |
Goalw [primel_def] "xs <~~> ys ==> primel xs --> primel ys"; |
|
143 |
by (etac perm.induct 1); |
|
144 |
by (ALLGOALS Asm_simp_tac); |
|
145 |
qed_spec_mp "perm_primel"; |
|
146 |
||
147 |
Goal "xs <~~> ys ==> prod xs = prod ys"; |
|
148 |
by (etac perm.induct 1); |
|
8528 | 149 |
by (ALLGOALS (asm_simp_tac (simpset() addsimps mult_ac))); |
8353 | 150 |
qed_spec_mp "perm_prod"; |
151 |
||
152 |
Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys"; |
|
153 |
by (etac perm.induct 1); |
|
8528 | 154 |
by Auto_tac; |
8353 | 155 |
qed "perm_subst_oinsert"; |
156 |
||
157 |
Goal "x#xs <~~> oinsert x xs"; |
|
158 |
by (induct_tac "xs" 1); |
|
8528 | 159 |
by Auto_tac; |
8353 | 160 |
qed "perm_oinsert"; |
161 |
||
162 |
Goal "xs <~~> sort xs"; |
|
163 |
by (induct_tac "xs" 1); |
|
8528 | 164 |
by (auto_tac (claset() addIs [perm_oinsert] |
8353 | 165 |
addEs [perm_subst_oinsert], |
8528 | 166 |
simpset())); |
8353 | 167 |
qed "perm_sort"; |
168 |
||
169 |
Goal "xs <~~> ys ==> sort xs = sort ys"; |
|
170 |
by (etac perm.induct 1); |
|
171 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [oinsert_x_y]))); |
|
172 |
qed "perm_sort_eq"; |
|
173 |
||
174 |
||
175 |
(* --- Existence --- *) |
|
176 |
||
177 |
Goal "primel xs ==> EX ys. primel ys & nondec ys & prod ys = prod xs"; |
|
178 |
by (blast_tac (claset() addIs [nondec_sort, perm_prod,perm_primel,perm_sort, |
|
179 |
perm_sym]) 1); |
|
180 |
qed "ex_nondec_lemma"; |
|
181 |
||
182 |
Goalw [prime_def,dvd_def] |
|
183 |
"1<n & n~:prime --> (EX m k.1<m & 1<k & m<n & k<n & n=m*k)"; |
|
184 |
by (auto_tac (claset() addIs [n_less_m_mult_n, n_less_n_mult_m, |
|
185 |
one_less_m, one_less_k], |
|
186 |
simpset())); |
|
187 |
qed_spec_mp "not_prime_ex_mk"; |
|
188 |
||
189 |
Goal "[| primel xs; primel ys |] \ |
|
190 |
\ ==> EX l. primel l & prod l = prod xs * prod ys"; |
|
191 |
by (rtac exI 1); |
|
192 |
by Safe_tac; |
|
193 |
by (rtac prod_append 2); |
|
194 |
by (asm_simp_tac (simpset() addsimps [primel_append]) 1); |
|
195 |
qed "split_primel"; |
|
196 |
||
197 |
Goal "1<n --> (EX l. primel l & prod l = n)"; |
|
198 |
by (res_inst_tac [("n","n")] less_induct 1); |
|
199 |
by (rtac impI 1); |
|
200 |
by (case_tac "n:prime" 1); |
|
201 |
by (rtac exI 1); |
|
202 |
by (etac prime_primel 1); |
|
203 |
by (cut_inst_tac [("n","n")] not_prime_ex_mk 1); |
|
204 |
by (auto_tac (claset() addSIs [split_primel], simpset())); |
|
205 |
qed_spec_mp "factor_exists"; |
|
206 |
||
207 |
Goal "1<n ==> (EX l. primel l & nondec l & prod l = n)"; |
|
208 |
by (etac (factor_exists RS exE) 1); |
|
209 |
by (blast_tac (claset() addSIs [ex_nondec_lemma]) 1); |
|
210 |
qed "nondec_factor_exists"; |
|
211 |
||
212 |
||
213 |
(* --- Uniqueness --- *) |
|
214 |
||
215 |
Goal "p:prime ==> p dvd (prod xs) --> (EX m. m:set xs & p dvd m)"; |
|
216 |
by (induct_tac "xs" 1); |
|
217 |
by (ALLGOALS Asm_full_simp_tac); |
|
218 |
by (etac prime_nd_one 1); |
|
219 |
by (rtac impI 1); |
|
220 |
by (dtac prime_dvd_mult 1); |
|
221 |
by Auto_tac; |
|
222 |
qed_spec_mp "prime_dvd_mult_list"; |
|
223 |
||
224 |
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ |
|
225 |
\ ==> EX m. m :set ys & x dvd m"; |
|
226 |
by (rtac prime_dvd_mult_list 1); |
|
227 |
by (etac hd_dvd_prod 2); |
|
228 |
by (asm_full_simp_tac (simpset() addsimps [primel_hd_tl]) 1); |
|
229 |
qed "hd_xs_dvd_prod"; |
|
230 |
||
231 |
Goal "[| primel (x#xs); primel ys; m:set ys; x dvd m |] ==> x=m"; |
|
232 |
by (rtac primes_eq 1); |
|
233 |
by (auto_tac (claset(), simpset() addsimps [primel_def,primel_hd_tl])); |
|
234 |
qed "prime_dvd_eq"; |
|
235 |
||
236 |
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] ==> x:set ys"; |
|
237 |
by (ftac hd_xs_dvd_prod 1); |
|
238 |
by Auto_tac; |
|
239 |
by (dtac prime_dvd_eq 1); |
|
240 |
by Auto_tac; |
|
241 |
qed "hd_xs_eq_prod"; |
|
242 |
||
243 |
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ |
|
244 |
\ ==> EX l. ys <~~> (x#l)"; |
|
245 |
by (rtac exI 1); |
|
246 |
by (rtac perm_remove 1); |
|
247 |
by (etac hd_xs_eq_prod 1); |
|
248 |
by (ALLGOALS assume_tac); |
|
249 |
qed "perm_primel_ex"; |
|
250 |
||
251 |
Goal "[| primel (x#xs); primel ys; prod (x#xs) = prod ys |] \ |
|
252 |
\ ==> prod xs < prod ys"; |
|
253 |
by (auto_tac (claset() addIs [prod_mn_less_k,prime_g_one,primel_prod_gz], |
|
254 |
simpset() addsimps [primel_hd_tl])); |
|
255 |
qed "primel_prod_less"; |
|
256 |
||
257 |
Goal "[| primel xs; p*prod xs = p; p:prime |] ==> xs=[]"; |
|
258 |
by (auto_tac (claset() addIs [primel_one_empty,mn_eq_m_one,prime_g_zero], |
|
259 |
simpset())); |
|
260 |
qed "prod_one_empty"; |
|
261 |
||
262 |
Goal "[| ALL m. m < prod ys --> (ALL xs ys. primel xs & primel ys & \ |
|
263 |
\ prod xs = prod ys & prod xs = m --> xs <~~> ys); primel list; \ |
|
264 |
\ primel x; prod list = prod x; prod x < prod ys |] ==> x <~~> list"; |
|
265 |
by (Asm_full_simp_tac 1); |
|
266 |
qed "uniq_ex_lemma"; |
|
267 |
||
268 |
Goal "ALL xs ys. (primel xs & primel ys & prod xs = prod ys & prod xs = n \ |
|
269 |
\ --> xs <~~> ys)"; |
|
270 |
by (res_inst_tac [("n","n")] less_induct 1); |
|
271 |
by Safe_tac; |
|
8442
96023903c2df
case_tac now subsumes both boolean and datatype cases;
wenzelm
parents:
8423
diff
changeset
|
272 |
by (case_tac "xs" 1); |
8353 | 273 |
by (force_tac (claset() addIs [primel_one_empty], simpset()) 1); |
274 |
by (rtac (perm_primel_ex RS exE) 1); |
|
275 |
by (ALLGOALS Asm_full_simp_tac); |
|
276 |
by (rtac (perm.trans RS perm_sym) 1); |
|
277 |
by (assume_tac 1); |
|
278 |
by (rtac perm.Cons 1); |
|
279 |
by (case_tac "x=[]" 1); |
|
280 |
by (asm_full_simp_tac (simpset() addsimps [perm_sing_eq,primel_hd_tl]) 1); |
|
281 |
by (res_inst_tac [("p","a")] prod_one_empty 1); |
|
282 |
by (ALLGOALS Asm_full_simp_tac); |
|
283 |
by (etac uniq_ex_lemma 1); |
|
284 |
by (auto_tac (claset() addIs [primel_tl,perm_primel], |
|
285 |
simpset() addsimps [primel_hd_tl])); |
|
286 |
by (res_inst_tac [("k","a"),("n","prod list"),("m","prod x")] mult_left_cancel 1); |
|
287 |
by (res_inst_tac [("x","a")] primel_prod_less 3); |
|
288 |
by (rtac prod_xy_prod 2); |
|
289 |
by (res_inst_tac [("s","prod ys")] trans 2); |
|
290 |
by (etac perm_prod 3); |
|
291 |
by (etac (perm_prod RS sym) 5); |
|
292 |
by (auto_tac (claset() addIs [perm_primel,prime_g_zero], simpset())); |
|
293 |
qed_spec_mp "factor_unique"; |
|
294 |
||
295 |
Goal "[| xs <~~> ys; nondec xs; nondec ys |] ==> xs = ys"; |
|
296 |
by (rtac trans 1); |
|
297 |
by (rtac trans 1); |
|
298 |
by (etac nondec_sort_eq 1); |
|
299 |
by (etac perm_sort_eq 1); |
|
300 |
by (etac (nondec_sort_eq RS sym) 1); |
|
301 |
qed "perm_nondec_unique"; |
|
302 |
||
303 |
Goal "ALL n. 1<n --> (EX! l. primel l & nondec l & prod l = n)"; |
|
304 |
by Safe_tac; |
|
305 |
by (etac nondec_factor_exists 1); |
|
306 |
by (rtac perm_nondec_unique 1); |
|
307 |
by (rtac factor_unique 1); |
|
308 |
by (ALLGOALS Asm_full_simp_tac); |
|
309 |
qed_spec_mp "unique_prime_factorization"; |