|
1 (* Title: HOL/GroupTheory/Exponent |
|
2 ID: $Id$ |
|
3 Author: Florian Kammueller, with new proofs by L C Paulson |
|
4 Copyright 2001 University of Cambridge |
|
5 *) |
|
6 |
|
7 (*??Two more for Divides.ML *) |
|
8 Goal "0<m ==> (m*n dvd m) = (n=1)"; |
|
9 by Auto_tac; |
|
10 by (subgoal_tac "m*n dvd m*1" 1); |
|
11 by (dtac dvd_mult_cancel 1); |
|
12 by Auto_tac; |
|
13 qed "dvd_mult_cancel1"; |
|
14 |
|
15 Goal "0<m ==> (n*m dvd m) = (n=1)"; |
|
16 by (stac mult_commute 1); |
|
17 by (etac dvd_mult_cancel1 1); |
|
18 qed "dvd_mult_cancel2"; |
|
19 |
|
20 |
|
21 (*** prime theorems ***) |
|
22 |
|
23 val prime_def = thm "prime_def"; |
|
24 |
|
25 Goalw [prime_def] "p\\<in>prime ==> 1 < p"; |
|
26 by (Blast_tac 1); |
|
27 qed "prime_imp_one_less"; |
|
28 |
|
29 Goal "(p\\<in>prime) = (1<p & (\\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"; |
|
30 by (auto_tac (claset(), simpset() addsimps [prime_imp_one_less])); |
|
31 by (blast_tac (claset() addSDs [thm "prime_dvd_mult"]) 1); |
|
32 by (auto_tac (claset(), simpset() addsimps [prime_def])); |
|
33 by (etac dvdE 1); |
|
34 by (case_tac "k=0" 1); |
|
35 by (Asm_full_simp_tac 1); |
|
36 by (dres_inst_tac [("x","m")] spec 1); |
|
37 by (dres_inst_tac [("x","k")] spec 1); |
|
38 by (asm_full_simp_tac |
|
39 (simpset() addsimps [dvd_mult_cancel1, dvd_mult_cancel2]) 1); |
|
40 qed "prime_iff"; |
|
41 |
|
42 Goal "p\\<in>prime ==> 0 < p^a"; |
|
43 by (rtac zero_less_power 1); |
|
44 by (force_tac (claset(), simpset() addsimps [prime_iff]) 1); |
|
45 qed "zero_less_prime_power"; |
|
46 |
|
47 |
|
48 (*First some things about HOL and sets *) |
|
49 val [p1] = goal (the_context()) "(P x y) ==> ( (x, y)\\<in>{(a,b). P a b})"; |
|
50 by (rtac CollectI 1); |
|
51 by (rewrite_goals_tac [split RS eq_reflection]); |
|
52 by (rtac p1 1); |
|
53 qed "CollectI_prod"; |
|
54 |
|
55 val [p1] = goal (the_context()) "( (x, y)\\<in>{(a,b). P a b}) ==> (P x y)"; |
|
56 by (res_inst_tac [("c1","P")] (split RS subst) 1); |
|
57 by (res_inst_tac [("a","(x,y)")] CollectD 1); |
|
58 by (rtac p1 1); |
|
59 qed "CollectD_prod"; |
|
60 |
|
61 val [p1] = goal (the_context()) "(P x y z v) ==> ( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d})"; |
|
62 by (rtac CollectI_prod 1); |
|
63 by (rewrite_goals_tac [split RS eq_reflection]); |
|
64 by (rtac p1 1); |
|
65 qed "CollectI_prod4"; |
|
66 |
|
67 Goal "( (x, y, z, v)\\<in>{(a,b,c,d). P a b c d}) ==> (P x y z v)"; |
|
68 by Auto_tac; |
|
69 qed "CollectD_prod4"; |
|
70 |
|
71 |
|
72 |
|
73 val [p1] = goal (the_context()) "x\\<in>{y. P(y) & Q(y)} ==> P(x)"; |
|
74 by (res_inst_tac [("Q","Q x"),("P", "P x")] conjE 1); |
|
75 by (assume_tac 2); |
|
76 by (res_inst_tac [("a", "x")] CollectD 1); |
|
77 by (rtac p1 1); |
|
78 qed "subset_lemma1"; |
|
79 |
|
80 val [p1,p2] = goal (the_context()) "[|P == Q; P|] ==> Q"; |
|
81 by (fold_goals_tac [p1]); |
|
82 by (rtac p2 1); |
|
83 qed "apply_def"; |
|
84 |
|
85 Goal "S \\<noteq> {} ==> \\<exists>x. x\\<in>S"; |
|
86 by Auto_tac; |
|
87 qed "NotEmpty_ExEl"; |
|
88 |
|
89 Goal "\\<exists>x. x: S ==> S \\<noteq> {}"; |
|
90 by Auto_tac; |
|
91 qed "ExEl_NotEmpty"; |
|
92 |
|
93 |
|
94 (* The following lemmas are needed for existsM1inM *) |
|
95 |
|
96 Goal "[| {} \\<notin> A; M\\<in>A |] ==> M \\<noteq> {}"; |
|
97 by Auto_tac; |
|
98 qed "MnotEqempty"; |
|
99 |
|
100 val [p1] = goal (the_context()) "\\<exists>g \\<in> A. x = P(g) ==> \\<exists>g \\<in> A. P(g) = x"; |
|
101 by (rtac bexE 1); |
|
102 by (rtac p1 1); |
|
103 by (rtac bexI 1); |
|
104 by (rtac sym 1); |
|
105 by (assume_tac 1); |
|
106 by (assume_tac 1); |
|
107 qed "bex_sym"; |
|
108 |
|
109 Goalw [equiv_def,quotient_def,sym_def,trans_def] |
|
110 "[| equiv A r; C\\<in>A // r |] ==> \\<forall>x \\<in> C. \\<forall>y \\<in> C. (x,y)\\<in>r"; |
|
111 by (Blast_tac 1); |
|
112 qed "ElemClassEquiv"; |
|
113 |
|
114 Goalw [equiv_def,quotient_def,sym_def,trans_def] |
|
115 "[|equiv A r; M\\<in>A // r; M1\\<in>M; (M1, M2)\\<in>r |] ==> M2\\<in>M"; |
|
116 by (Blast_tac 1); |
|
117 qed "EquivElemClass"; |
|
118 |
|
119 Goal "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"; |
|
120 by (res_inst_tac [("P","%x. x <= b * c")] subst 1); |
|
121 by (rtac mult_1_right 1); |
|
122 by (rtac mult_le_mono 1); |
|
123 by (assume_tac 1); |
|
124 by (stac Suc_le_eq 1); |
|
125 by (assume_tac 1); |
|
126 qed "le_extend_mult"; |
|
127 |
|
128 |
|
129 (* card_inj lemma: F. Kammueller, 4.9. 96 |
|
130 |
|
131 The sequel contains a proof of the lemma "card_inj" used in the |
|
132 plus preparations. The provable form here differs from the |
|
133 one used in Group in that it contains the additional neccessary assumptions |
|
134 "finite A" and "finite B" *) |
|
135 |
|
136 Goal "0 < card(S) ==> S \\<noteq> {}"; |
|
137 by (force_tac (claset(), simpset() addsimps [card_empty]) 1); |
|
138 qed "card_nonempty"; |
|
139 |
|
140 Goal "[| finite(A); finite(B); f \\<in> A -> B; inj_on f A |] ==> card A <= card B"; |
|
141 bw funcset_def; |
|
142 by (rtac card_inj_on_le 1); |
|
143 by (assume_tac 4); |
|
144 by Auto_tac; |
|
145 qed "card_inj"; |
|
146 |
|
147 Goal "[| x \\<notin> F; \ |
|
148 \ \\<forall>c1\\<in>insert x F. \\<forall>c2 \\<in> insert x F. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}|]\ |
|
149 \ ==> x \\<inter> \\<Union> F = {}"; |
|
150 by Auto_tac; |
|
151 qed "insert_partition"; |
|
152 |
|
153 (* main cardinality theorem *) |
|
154 Goal "finite C ==> \ |
|
155 \ finite (\\<Union> C) --> \ |
|
156 \ (\\<forall>c\\<in>C. card c = k) --> \ |
|
157 \ (\\<forall>c1 \\<in> C. \\<forall>c2 \\<in> C. c1 \\<noteq> c2 --> c1 \\<inter> c2 = {}) --> \ |
|
158 \ k * card(C) = card (\\<Union> C)"; |
|
159 by (etac finite_induct 1); |
|
160 by (Asm_full_simp_tac 1); |
|
161 by (asm_full_simp_tac |
|
162 (simpset() addsimps [card_insert_disjoint, card_Un_disjoint, |
|
163 insert_partition, inst "B" "\\<Union>(insert x F)" finite_subset]) 1); |
|
164 qed_spec_mp "card_partition"; |
|
165 |
|
166 Goal "[| finite S; S \\<noteq> {} |] ==> 0 < card(S)"; |
|
167 by (swap_res_tac [card_0_eq RS iffD1] 1); |
|
168 by Auto_tac; |
|
169 qed "zero_less_card_empty"; |
|
170 |
|
171 |
|
172 Goal "[| p*k dvd m*n; p\\<in>prime |] \ |
|
173 \ ==> (\\<exists>x. k dvd x*n & m = p*x) | (\\<exists>y. k dvd m*y & n = p*y)"; |
|
174 by (asm_full_simp_tac (simpset() addsimps [prime_iff]) 1); |
|
175 by (ftac dvd_mult_left 1); |
|
176 by (subgoal_tac "p dvd m | p dvd n" 1); |
|
177 by (Blast_tac 2); |
|
178 by (etac disjE 1); |
|
179 by (rtac disjI1 1); |
|
180 by (rtac disjI2 2); |
|
181 by (eres_inst_tac [("n","m")] dvdE 1); |
|
182 by (eres_inst_tac [("n","n")] dvdE 2); |
|
183 by Auto_tac; |
|
184 by (res_inst_tac [("k","p")] dvd_mult_cancel 2); |
|
185 by (res_inst_tac [("k","p")] dvd_mult_cancel 1); |
|
186 by (ALLGOALS (asm_full_simp_tac (simpset() addsimps mult_ac))); |
|
187 qed "prime_dvd_cases"; |
|
188 |
|
189 |
|
190 Goal "p\\<in>prime \ |
|
191 \ ==> \\<forall>m n. p^c dvd m*n --> \ |
|
192 \ (\\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"; |
|
193 by (induct_tac "c" 1); |
|
194 by (Clarify_tac 1); |
|
195 by (case_tac "a" 1); |
|
196 by (Asm_full_simp_tac 1); |
|
197 by (Asm_full_simp_tac 1); |
|
198 (*inductive step*) |
|
199 by (Asm_full_simp_tac 1); |
|
200 by (Clarify_tac 1); |
|
201 by (etac (prime_dvd_cases RS disjE) 1); |
|
202 by (assume_tac 1); |
|
203 by Auto_tac; |
|
204 (*case 1: p dvd m*) |
|
205 by (case_tac "a" 1); |
|
206 by (Asm_full_simp_tac 1); |
|
207 by (Clarify_tac 1); |
|
208 by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1); |
|
209 by (dres_inst_tac [("x","nat")] spec 1); |
|
210 by (dres_inst_tac [("x","b")] spec 1); |
|
211 by (Asm_full_simp_tac 1); |
|
212 by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1); |
|
213 (*case 2: p dvd n*) |
|
214 by (case_tac "b" 1); |
|
215 by (Asm_full_simp_tac 1); |
|
216 by (Clarify_tac 1); |
|
217 by (dtac spec 1 THEN dtac spec 1 THEN mp_tac 1); |
|
218 by (dres_inst_tac [("x","a")] spec 1); |
|
219 by (dres_inst_tac [("x","nat")] spec 1); |
|
220 by (Asm_full_simp_tac 1); |
|
221 by (blast_tac (claset() addIs [dvd_refl, mult_dvd_mono]) 1); |
|
222 qed_spec_mp "prime_power_dvd_cases"; |
|
223 |
|
224 (*needed in this form in Sylow.ML*) |
|
225 Goal "[| p\\<in>prime; ~(p ^ (r+1) dvd n); p ^ (a+r) dvd n * k |] \ |
|
226 \ ==> p ^ a dvd k"; |
|
227 by (dres_inst_tac [("a","r+1"), ("b","a")] prime_power_dvd_cases 1); |
|
228 by (assume_tac 1); |
|
229 by Auto_tac; |
|
230 qed "div_combine"; |
|
231 |
|
232 (*Lemma for power_dvd_bound*) |
|
233 Goal "1 < p ==> Suc n <= p^n"; |
|
234 by (induct_tac "n" 1); |
|
235 by (Asm_simp_tac 1); |
|
236 by (Asm_full_simp_tac 1); |
|
237 by (subgoal_tac "2*n + #2 <= p * p^n" 1); |
|
238 by (Asm_full_simp_tac 1); |
|
239 by (subgoal_tac "#2 * p^n <= p * p^n" 1); |
|
240 (*?arith_tac should handle all of this!*) |
|
241 by (rtac order_trans 1); |
|
242 by (assume_tac 2); |
|
243 by (dres_inst_tac [("k","#2")] mult_le_mono2 1); |
|
244 by (Asm_full_simp_tac 1); |
|
245 by (rtac mult_le_mono1 1); |
|
246 by (Asm_full_simp_tac 1); |
|
247 qed "Suc_le_power"; |
|
248 |
|
249 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) |
|
250 Goal "[|p^n dvd a; 1 < p; 0 < a|] ==> n < a"; |
|
251 by (dtac dvd_imp_le 1); |
|
252 by (dres_inst_tac [("n","n")] Suc_le_power 2); |
|
253 by Auto_tac; |
|
254 qed "power_dvd_bound"; |
|
255 |
|
256 |
|
257 (*** exponent theorems ***) |
|
258 |
|
259 Goal "[|p^k dvd n; p\\<in>prime; 0<n|] ==> k <= exponent p n"; |
|
260 by (asm_full_simp_tac (simpset() addsimps [exponent_def]) 1); |
|
261 by (etac GreatestM_nat_le 1); |
|
262 by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 1); |
|
263 qed_spec_mp "exponent_ge"; |
|
264 |
|
265 Goal "0<s ==> (p ^ exponent p s) dvd s"; |
|
266 by (simp_tac (simpset() addsimps [exponent_def]) 1); |
|
267 by (Clarify_tac 1); |
|
268 by (res_inst_tac [("k","0")] GreatestI 1); |
|
269 by (blast_tac (claset() addDs [prime_imp_one_less, power_dvd_bound]) 2); |
|
270 by (Asm_full_simp_tac 1); |
|
271 qed "power_exponent_dvd"; |
|
272 |
|
273 Goal "[|(p * p ^ exponent p s) dvd s; p\\<in>prime |] ==> s=0"; |
|
274 by (subgoal_tac "p ^ Suc(exponent p s) dvd s" 1); |
|
275 by (Asm_full_simp_tac 2); |
|
276 by (rtac ccontr 1); |
|
277 by (dtac exponent_ge 1); |
|
278 by Auto_tac; |
|
279 qed "power_Suc_exponent_Not_dvd"; |
|
280 |
|
281 Goal "p\\<in>prime ==> exponent p (p^a) = a"; |
|
282 by (asm_simp_tac (simpset() addsimps [exponent_def]) 1); |
|
283 by (rtac Greatest_equality 1); |
|
284 by (Asm_full_simp_tac 1); |
|
285 by (blast_tac (claset() addIs [prime_imp_one_less, power_dvd_imp_le]) 1); |
|
286 qed "exponent_power_eq"; |
|
287 Addsimps [exponent_power_eq]; |
|
288 |
|
289 Goal "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"; |
|
290 by (asm_simp_tac (simpset() addsimps [exponent_def]) 1); |
|
291 qed "exponent_equalityI"; |
|
292 |
|
293 Goal "p \\<notin> prime ==> exponent p s = 0"; |
|
294 by (asm_simp_tac (simpset() addsimps [exponent_def]) 1); |
|
295 qed "exponent_eq_0"; |
|
296 Addsimps [exponent_eq_0]; |
|
297 |
|
298 |
|
299 (* exponent_mult_add, easy inclusion. Could weaken p\\<in>prime to 1<p *) |
|
300 Goal "[| 0 < a; 0 < b |] \ |
|
301 \ ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"; |
|
302 by (case_tac "p \\<in> prime" 1); |
|
303 by (rtac exponent_ge 1); |
|
304 by (auto_tac (claset(), simpset() addsimps [power_add])); |
|
305 by (blast_tac (claset() addIs [prime_imp_one_less, power_exponent_dvd, |
|
306 mult_dvd_mono]) 1); |
|
307 qed "exponent_mult_add1"; |
|
308 |
|
309 (* exponent_mult_add, opposite inclusion *) |
|
310 Goal "[| 0 < a; 0 < b |] \ |
|
311 \ ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"; |
|
312 by (case_tac "p\\<in>prime" 1); |
|
313 by (rtac leI 1); |
|
314 by (Clarify_tac 1); |
|
315 by (cut_inst_tac [("p","p"),("s","a*b")] power_exponent_dvd 1); |
|
316 by Auto_tac; |
|
317 by (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b" 1); |
|
318 by (rtac (le_imp_power_dvd RS dvd_trans) 2); |
|
319 by (assume_tac 3); |
|
320 by (Asm_full_simp_tac 2); |
|
321 by (forw_inst_tac [("a","Suc (exponent p a)"), ("b","Suc (exponent p b)")] |
|
322 prime_power_dvd_cases 1); |
|
323 by (assume_tac 1 THEN Force_tac 1); |
|
324 by (Asm_full_simp_tac 1); |
|
325 by (blast_tac (claset() addDs [power_Suc_exponent_Not_dvd]) 1); |
|
326 qed "exponent_mult_add2"; |
|
327 |
|
328 Goal "[| 0 < a; 0 < b |] \ |
|
329 \ ==> exponent p (a * b) = (exponent p a) + (exponent p b)"; |
|
330 by (blast_tac (claset() addIs [exponent_mult_add1, exponent_mult_add2, |
|
331 order_antisym]) 1); |
|
332 qed "exponent_mult_add"; |
|
333 |
|
334 |
|
335 Goal "~ (p dvd n) ==> exponent p n = 0"; |
|
336 by (case_tac "exponent p n" 1); |
|
337 by (Asm_full_simp_tac 1); |
|
338 by (case_tac "n" 1); |
|
339 by (Asm_full_simp_tac 1); |
|
340 by (cut_inst_tac [("s","n"),("p","p")] power_exponent_dvd 1); |
|
341 by (auto_tac (claset() addDs [dvd_mult_left], simpset())); |
|
342 qed "not_divides_exponent_0"; |
|
343 |
|
344 Goal "exponent p 1 = 0"; |
|
345 by (case_tac "p \\<in> prime" 1); |
|
346 by (auto_tac (claset(), |
|
347 simpset() addsimps [prime_iff, not_divides_exponent_0])); |
|
348 qed "exponent_1_eq_0"; |
|
349 Addsimps [exponent_1_eq_0]; |
|
350 |
|
351 |
|
352 (*** Lemmas for the main combinatorial argument ***) |
|
353 |
|
354 Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"; |
|
355 by (rtac notnotD 1); |
|
356 by (rtac notI 1); |
|
357 by (dtac (leI RSN (2, contrapos_nn) RS notnotD) 1); |
|
358 by (assume_tac 1); |
|
359 by (dres_inst_tac [("m","a")] less_imp_le 1); |
|
360 by (dtac le_imp_power_dvd 1); |
|
361 by (dres_inst_tac [("n","p ^ r")] dvd_trans 1); |
|
362 by (assume_tac 1); |
|
363 by (forw_inst_tac [("m","k")] less_imp_le 1); |
|
364 by (dres_inst_tac [("c","m")] le_extend_mult 1); |
|
365 by (assume_tac 1); |
|
366 by (dres_inst_tac [("k","p ^ a"),("m","(p ^ a) * m")] dvd_diffD1 1); |
|
367 by (assume_tac 2); |
|
368 by (rtac (dvd_refl RS dvd_mult2) 1); |
|
369 by (dres_inst_tac [("n","k")] dvd_imp_le 1); |
|
370 by Auto_tac; |
|
371 qed "p_fac_forw_lemma"; |
|
372 |
|
373 Goal "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] \ |
|
374 \ ==> (p^r) dvd (p^a) - k"; |
|
375 by (forw_inst_tac [("k1","k"),("i","p")] |
|
376 (p_fac_forw_lemma RS le_imp_power_dvd) 1); |
|
377 by Auto_tac; |
|
378 by (subgoal_tac "p^r dvd p^a*m" 1); |
|
379 by (blast_tac (claset() addIs [dvd_mult2]) 2); |
|
380 by (dtac dvd_diffD1 1); |
|
381 by (assume_tac 1); |
|
382 by (blast_tac (claset() addIs [dvd_diff]) 2); |
|
383 by (dtac less_imp_Suc_add 1); |
|
384 by Auto_tac; |
|
385 qed "p_fac_forw"; |
|
386 |
|
387 |
|
388 Goal "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"; |
|
389 by (res_inst_tac [("m","1")] p_fac_forw_lemma 1); |
|
390 by Auto_tac; |
|
391 qed "r_le_a_forw"; |
|
392 |
|
393 Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |] \ |
|
394 \ ==> (p^r) dvd (p^a)*m - k"; |
|
395 by (forw_inst_tac [("k1","k"),("i","p")] (r_le_a_forw RS le_imp_power_dvd) 1); |
|
396 by Auto_tac; |
|
397 by (subgoal_tac "p^r dvd p^a*m" 1); |
|
398 by (blast_tac (claset() addIs [dvd_mult2]) 2); |
|
399 by (dtac dvd_diffD1 1); |
|
400 by (assume_tac 1); |
|
401 by (blast_tac (claset() addIs [dvd_diff]) 2); |
|
402 by (dtac less_imp_Suc_add 1); |
|
403 by Auto_tac; |
|
404 qed "p_fac_backw"; |
|
405 |
|
406 Goal "[| 0<m; 0<k; 0 < (p::nat); k < p^a |] \ |
|
407 \ ==> exponent p (p^a * m - k) = exponent p (p^a - k)"; |
|
408 by (blast_tac (claset() addIs [exponent_equalityI, p_fac_forw, |
|
409 p_fac_backw]) 1); |
|
410 qed "exponent_p_a_m_k_equation"; |
|
411 |
|
412 (*Suc rules that we have to delete from the simpset*) |
|
413 val bad_Sucs = [binomial_Suc_Suc, mult_Suc, mult_Suc_right]; |
|
414 |
|
415 (*The bound K is needed; otherwise it's too weak to be used.*) |
|
416 Goal "[| \\<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] \ |
|
417 \ ==> k<K --> exponent p ((j+k) choose k) = 0"; |
|
418 by (case_tac "p \\<in> prime" 1); |
|
419 by (Asm_simp_tac 2); |
|
420 by (induct_tac "k" 1); |
|
421 by (Simp_tac 1); |
|
422 (*induction step*) |
|
423 by (subgoal_tac "0 < (Suc(j+n) choose Suc n)" 1); |
|
424 by (simp_tac (simpset() addsimps [zero_less_binomial_iff]) 2); |
|
425 by (Clarify_tac 1); |
|
426 by (subgoal_tac |
|
427 "exponent p ((Suc(j+n) choose Suc n) * Suc n) = exponent p (Suc n)" 1); |
|
428 (*First, use the assumed equation. We simplify the LHS to |
|
429 exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n); |
|
430 the common terms cancel, proving the conclusion.*) |
|
431 by (asm_full_simp_tac (simpset() delsimps bad_Sucs |
|
432 addsimps [exponent_mult_add]) 1); |
|
433 (*Establishing the equation requires first applying Suc_times_binomial_eq...*) |
|
434 by (asm_full_simp_tac (simpset() delsimps bad_Sucs |
|
435 addsimps [Suc_times_binomial_eq RS sym]) 1); |
|
436 (*...then exponent_mult_add and the quantified premise.*) |
|
437 by (asm_full_simp_tac (simpset() delsimps bad_Sucs |
|
438 addsimps [zero_less_binomial_iff, exponent_mult_add]) 1); |
|
439 qed_spec_mp "p_not_div_choose_lemma"; |
|
440 |
|
441 (*The lemma above, with two changes of variables*) |
|
442 Goal "[| k<K; k<=n; \ |
|
443 \ \\<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|] \ |
|
444 \ ==> exponent p (n choose k) = 0"; |
|
445 by (cut_inst_tac [("j","n-k"),("k","k"),("p","p")] p_not_div_choose_lemma 1); |
|
446 by (assume_tac 2); |
|
447 by (Asm_full_simp_tac 2); |
|
448 by (Clarify_tac 1); |
|
449 by (dres_inst_tac [("x","K - Suc i")] spec 1); |
|
450 by (asm_full_simp_tac (simpset() addsimps [Suc_diff_le]) 1); |
|
451 qed "p_not_div_choose"; |
|
452 |
|
453 |
|
454 Goal "0 < m ==> exponent p ((p^a * m - 1) choose (p^a - 1)) = 0"; |
|
455 by (case_tac "p \\<in> prime" 1); |
|
456 by (Asm_simp_tac 2); |
|
457 by (forw_inst_tac [("a","a")] zero_less_prime_power 1); |
|
458 by (res_inst_tac [("K","p^a")] p_not_div_choose 1); |
|
459 by (Asm_full_simp_tac 1); |
|
460 by (Asm_full_simp_tac 1); |
|
461 by (case_tac "m" 1); |
|
462 by (case_tac "p^a" 2); |
|
463 by Auto_tac; |
|
464 (*now the hard case, simplified to |
|
465 exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *) |
|
466 by (subgoal_tac "0<p" 1); |
|
467 by (force_tac (claset() addSDs [prime_imp_one_less], simpset()) 2); |
|
468 by (stac exponent_p_a_m_k_equation 1); |
|
469 by Auto_tac; |
|
470 qed "const_p_fac_right"; |
|
471 |
|
472 Goal "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"; |
|
473 by (case_tac "p \\<in> prime" 1); |
|
474 by (Asm_simp_tac 2); |
|
475 by (forw_inst_tac [("a","a")] zero_less_prime_power 1); |
|
476 by (subgoal_tac "0 < p^a * m & p^a <= p^a * m" 1); |
|
477 by (Asm_full_simp_tac 2); |
|
478 (*A similar trick to the one used in p_not_div_choose_lemma: |
|
479 insert an equation; use exponent_mult_add on the LHS; on the RHS, first |
|
480 transform the binomial coefficient, then use exponent_mult_add.*) |
|
481 by (subgoal_tac |
|
482 "exponent p ((((p^a) * m) choose p^a) * p^a) = a + exponent p m" 1); |
|
483 by (asm_full_simp_tac (simpset() delsimps bad_Sucs |
|
484 addsimps [zero_less_binomial_iff, exponent_mult_add, prime_iff]) 1); |
|
485 (*one subgoal left!*) |
|
486 by (stac times_binomial_minus1_eq 1); |
|
487 by (Asm_full_simp_tac 1); |
|
488 by (Asm_full_simp_tac 1); |
|
489 by (stac exponent_mult_add 1); |
|
490 by (Asm_full_simp_tac 1); |
|
491 by (asm_simp_tac (simpset() addsimps [zero_less_binomial_iff]) 1); |
|
492 by (arith_tac 1); |
|
493 by (asm_simp_tac (simpset() delsimps bad_Sucs |
|
494 addsimps [exponent_mult_add, const_p_fac_right]) 1); |
|
495 qed "const_p_fac"; |