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";
|
8423
|
13 |
by (cases_tac "m" 1);
|
8353
|
14 |
by Auto_tac;
|
|
15 |
qed "one_less_m";
|
|
16 |
|
|
17 |
Goal "[| m ~= m*k; 1<m*k |] ==> 1<k";
|
8423
|
18 |
by (cases_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";
|
8423
|
27 |
by (cases_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;
|
8423
|
58 |
by (cases_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 = []";
|
8423
|
81 |
by (cases_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);
|
8423
|
108 |
by (cases_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);
|
8423
|
126 |
by (cases_tac "list" 1);
|
8353
|
127 |
by (ALLGOALS Asm_full_simp_tac);
|
8423
|
128 |
by (cases_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);
|
|
136 |
by (ALLGOALS Asm_full_simp_tac);
|
|
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);
|
|
149 |
by (ALLGOALS (asm_full_simp_tac (simpset() addsimps [mult_left_commute])));
|
|
150 |
qed_spec_mp "perm_prod";
|
|
151 |
|
|
152 |
Goal "xs <~~> ys ==> oinsert a xs <~~> oinsert a ys";
|
|
153 |
by (etac perm.induct 1);
|
|
154 |
by (auto_tac (claset() addIs perm_rules, simpset()));
|
|
155 |
qed "perm_subst_oinsert";
|
|
156 |
|
|
157 |
Goal "x#xs <~~> oinsert x xs";
|
|
158 |
by (induct_tac "xs" 1);
|
|
159 |
by (auto_tac (claset() addIs perm_rules, simpset()));
|
|
160 |
qed "perm_oinsert";
|
|
161 |
|
|
162 |
Goal "xs <~~> sort xs";
|
|
163 |
by (induct_tac "xs" 1);
|
|
164 |
by (auto_tac (claset() addIs [perm.trans,perm_oinsert]
|
|
165 |
addEs [perm_subst_oinsert],
|
|
166 |
simpset() addsimps [perm_refl]));
|
|
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;
|
8423
|
272 |
by (cases_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";
|