7 |
7 |
8 theory Exponent imports Main Primes Binomial begin |
8 theory Exponent imports Main Primes Binomial begin |
9 |
9 |
10 |
10 |
11 section {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
11 section {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
12 constdefs |
12 definition exponent :: "nat => nat => nat" where |
13 exponent :: "[nat, nat] => nat" |
13 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" |
14 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" |
|
15 |
14 |
16 |
15 |
17 subsection{*Prime Theorems*} |
16 subsection{*Prime Theorems*} |
18 |
17 |
19 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |
18 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |
20 by (unfold prime_def, force) |
19 by (unfold prime_def, force) |
21 |
20 |
22 lemma prime_iff: |
21 lemma prime_iff: |
23 "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))" |
22 "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))" |
24 apply (auto simp add: prime_imp_one_less) |
23 apply (auto simp add: prime_imp_one_less) |
25 apply (blast dest!: prime_dvd_mult) |
24 apply (blast dest!: prime_dvd_mult) |
26 apply (auto simp add: prime_def) |
25 apply (auto simp add: prime_def) |
27 apply (erule dvdE) |
26 apply (erule dvdE) |
28 apply (case_tac "k=0", simp) |
27 apply (case_tac "k=0", simp) |
83 apply (drule_tac x = nat in spec, simp) |
82 apply (drule_tac x = nat in spec, simp) |
84 done |
83 done |
85 |
84 |
86 (*needed in this form in Sylow.ML*) |
85 (*needed in this form in Sylow.ML*) |
87 lemma div_combine: |
86 lemma div_combine: |
88 "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] |
87 "[| prime p; ~ (p ^ (Suc r) dvd n); p^(a+r) dvd n*k |] |
89 ==> p ^ a dvd k" |
88 ==> p ^ a dvd k" |
90 by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto) |
89 by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto) |
91 |
90 |
92 (*Lemma for power_dvd_bound*) |
91 (*Lemma for power_dvd_bound*) |
93 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" |
92 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n" |
94 apply (induct_tac "n") |
93 apply (induct_tac "n") |
95 apply (simp (no_asm_simp)) |
94 apply (simp (no_asm_simp)) |
96 apply simp |
95 apply simp |
97 apply (subgoal_tac "2 * n + 2 <= p * p^n", simp) |
96 apply (subgoal_tac "2 * n + 2 <= p * p^n", simp) |
98 apply (subgoal_tac "2 * p^n <= p * p^n") |
97 apply (subgoal_tac "2 * p^n <= p * p^n") |
99 (*?arith_tac should handle all of this!*) |
98 apply arith |
100 apply (rule order_trans) |
|
101 prefer 2 apply assumption |
|
102 apply (drule_tac k = 2 in mult_le_mono2, simp) |
99 apply (drule_tac k = 2 in mult_le_mono2, simp) |
103 apply (rule mult_le_mono1, simp) |
|
104 done |
100 done |
105 |
101 |
106 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) |
102 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) |
107 lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; 0 < a|] ==> n < a" |
103 lemma power_dvd_bound: "[|p^n dvd a; Suc 0 < p; a \<noteq> 0|] ==> n < a" |
108 apply (drule dvd_imp_le) |
104 apply (drule dvd_imp_le) |
109 apply (drule_tac [2] n = n in Suc_le_power, auto) |
105 apply (drule_tac [2] n = n in Suc_le_power, auto) |
110 done |
106 done |
111 |
107 |
112 |
108 |
113 subsection{*Exponent Theorems*} |
109 subsection{*Exponent Theorems*} |
114 |
110 |
115 lemma exponent_ge [rule_format]: |
111 lemma exponent_ge [rule_format]: |
116 "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n" |
112 "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n" |
117 apply (simp add: exponent_def) |
113 apply (simp add: exponent_def) |
118 apply (erule Greatest_le) |
114 apply (erule Greatest_le) |
119 apply (blast dest: prime_imp_one_less power_dvd_bound) |
115 apply (blast dest: prime_imp_one_less power_dvd_bound) |
120 done |
116 done |
121 |
117 |
122 lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s" |
118 lemma power_exponent_dvd: "s\<noteq>0 ==> (p ^ exponent p s) dvd s" |
123 apply (simp add: exponent_def) |
119 apply (simp add: exponent_def) |
124 apply clarify |
120 apply clarify |
125 apply (rule_tac k = 0 in GreatestI) |
121 apply (rule_tac k = 0 in GreatestI) |
126 prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp) |
122 prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp) |
127 done |
123 done |
128 |
124 |
129 lemma power_Suc_exponent_Not_dvd: |
125 lemma power_Suc_exponent_Not_dvd: |
130 "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0" |
126 "[|(p * p ^ exponent p s) dvd s; prime p |] ==> s=0" |
131 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s") |
127 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s") |
132 prefer 2 apply simp |
128 prefer 2 apply simp |
133 apply (rule ccontr) |
129 apply (rule ccontr) |
134 apply (drule exponent_ge, auto) |
130 apply (drule exponent_ge, auto) |
135 done |
131 done |
139 apply (rule Greatest_equality, simp) |
135 apply (rule Greatest_equality, simp) |
140 apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le) |
136 apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le) |
141 done |
137 done |
142 |
138 |
143 lemma exponent_equalityI: |
139 lemma exponent_equalityI: |
144 "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b" |
140 "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b" |
145 by (simp (no_asm_simp) add: exponent_def) |
141 by (simp (no_asm_simp) add: exponent_def) |
146 |
142 |
147 lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0" |
143 lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0" |
148 by (simp (no_asm_simp) add: exponent_def) |
144 by (simp (no_asm_simp) add: exponent_def) |
149 |
145 |
150 |
146 |
151 (* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *) |
147 (* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *) |
152 lemma exponent_mult_add1: |
148 lemma exponent_mult_add1: "[| a \<noteq> 0; b \<noteq> 0 |] |
153 "[| 0 < a; 0 < b |] |
149 ==> (exponent p a) + (exponent p b) <= exponent p (a * b)" |
154 ==> (exponent p a) + (exponent p b) <= exponent p (a * b)" |
|
155 apply (case_tac "prime p") |
150 apply (case_tac "prime p") |
156 apply (rule exponent_ge) |
151 apply (rule exponent_ge) |
157 apply (auto simp add: power_add) |
152 apply (auto simp add: power_add) |
158 apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono) |
153 apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono) |
159 done |
154 done |
160 |
155 |
161 (* exponent_mult_add, opposite inclusion *) |
156 (* exponent_mult_add, opposite inclusion *) |
162 lemma exponent_mult_add2: "[| 0 < a; 0 < b |] |
157 lemma exponent_mult_add2: "[| a \<noteq> 0; b \<noteq> 0 |] |
163 ==> exponent p (a * b) <= (exponent p a) + (exponent p b)" |
158 ==> exponent p (a * b) <= (exponent p a) + (exponent p b)" |
164 apply (case_tac "prime p") |
159 apply (case_tac "prime p") |
165 apply (rule leI, clarify) |
160 apply (rule leI, clarify) |
166 apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto) |
161 apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto) |
167 apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b") |
162 apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b") |
168 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans]) |
163 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans]) |
192 done |
186 done |
193 |
187 |
194 |
188 |
195 subsection{*Main Combinatorial Argument*} |
189 subsection{*Main Combinatorial Argument*} |
196 |
190 |
197 lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)" |
191 lemma le_extend_mult: "[| c \<noteq> 0; a <= b |] ==> a <= b * (c::nat)" |
198 apply (rule_tac P = "%x. x <= b * c" in subst) |
192 apply (rule_tac P = "%x. x <= b * c" in subst) |
199 apply (rule mult_1_right) |
193 apply (rule mult_1_right) |
200 apply (rule mult_le_mono, auto) |
194 apply (rule mult_le_mono, auto) |
201 done |
195 done |
202 |
196 |
203 lemma p_fac_forw_lemma: |
197 lemma p_fac_forw_lemma: |
204 "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a" |
198 "[| (m::nat) \<noteq> 0; k \<noteq> 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a" |
205 apply (rule notnotD) |
199 apply (rule notnotD) |
206 apply (rule notI) |
200 apply (rule notI) |
207 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) |
201 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption) |
208 apply (drule less_imp_le [of a]) |
202 apply (drule less_imp_le [of a]) |
209 apply (drule le_imp_power_dvd) |
203 apply (drule le_imp_power_dvd) |
210 apply (drule_tac n = "p ^ r" in dvd_trans, assumption) |
204 apply (drule_tac n = "p ^ r" in dvd_trans, assumption) |
211 apply (metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less) |
205 apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv) |
212 done |
206 done |
213 |
207 |
214 lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] |
208 lemma p_fac_forw: "[| (m::nat) \<noteq> 0; k\<noteq>0; k < p^a; (p^r) dvd (p^a)* m - k |] |
215 ==> (p^r) dvd (p^a) - k" |
209 ==> (p^r) dvd (p^a) - k" |
216 apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto) |
210 apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto) |
217 apply (subgoal_tac "p^r dvd p^a*m") |
211 apply (subgoal_tac "p^r dvd p^a*m") |
218 prefer 2 apply (blast intro: dvd_mult2) |
212 prefer 2 apply (blast intro: dvd_mult2) |
219 apply (drule dvd_diffD1) |
213 apply (drule dvd_diffD1) |
220 apply assumption |
214 apply assumption |
221 prefer 2 apply (blast intro: dvd_diff) |
215 prefer 2 apply (blast intro: dvd_diff) |
222 apply (drule less_imp_Suc_add, auto) |
216 apply (drule not0_implies_Suc, auto) |
223 done |
217 done |
224 |
218 |
225 |
219 |
226 lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a" |
220 lemma r_le_a_forw: |
|
221 "[| (k::nat) \<noteq> 0; k < p^a; p\<noteq>0; (p^r) dvd (p^a) - k |] ==> r <= a" |
227 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto) |
222 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto) |
228 |
223 |
229 lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat); k < p^a; (p^r) dvd p^a - k |] |
224 lemma p_fac_backw: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0; k < p^a; (p^r) dvd p^a - k |] |
230 ==> (p^r) dvd (p^a)*m - k" |
225 ==> (p^r) dvd (p^a)*m - k" |
231 apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto) |
226 apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto) |
232 apply (subgoal_tac "p^r dvd p^a*m") |
227 apply (subgoal_tac "p^r dvd p^a*m") |
233 prefer 2 apply (blast intro: dvd_mult2) |
228 prefer 2 apply (blast intro: dvd_mult2) |
234 apply (drule dvd_diffD1) |
229 apply (drule dvd_diffD1) |
235 apply assumption |
230 apply assumption |
236 prefer 2 apply (blast intro: dvd_diff) |
231 prefer 2 apply (blast intro: dvd_diff) |
237 apply (drule less_imp_Suc_add, auto) |
232 apply (drule less_imp_Suc_add, auto) |
238 done |
233 done |
239 |
234 |
240 lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat); k < p^a |] |
235 lemma exponent_p_a_m_k_equation: "[| m\<noteq>0; k\<noteq>0; (p::nat)\<noteq>0; k < p^a |] |
241 ==> exponent p (p^a * m - k) = exponent p (p^a - k)" |
236 ==> exponent p (p^a * m - k) = exponent p (p^a - k)" |
242 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw) |
237 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw) |
243 done |
238 done |
244 |
239 |
245 text{*Suc rules that we have to delete from the simpset*} |
240 text{*Suc rules that we have to delete from the simpset*} |
246 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right |
241 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right |
247 |
242 |
248 (*The bound K is needed; otherwise it's too weak to be used.*) |
243 (*The bound K is needed; otherwise it's too weak to be used.*) |
249 lemma p_not_div_choose_lemma [rule_format]: |
244 lemma p_not_div_choose_lemma [rule_format]: |
250 "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] |
245 "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|] |
251 ==> k<K --> exponent p ((j+k) choose k) = 0" |
246 ==> k<K --> exponent p ((j+k) choose k) = 0" |
252 apply (case_tac "prime p") |
247 apply (case_tac "prime p") |
253 prefer 2 apply simp |
248 prefer 2 apply simp |
254 apply (induct_tac "k") |
249 apply (induct_tac "k") |
255 apply (simp (no_asm)) |
250 apply (simp (no_asm)) |
256 (*induction step*) |
251 (*induction step*) |
257 apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ") |
252 apply (subgoal_tac "(Suc (j+n) choose Suc n) \<noteq> 0") |
258 prefer 2 apply (simp add: zero_less_binomial_iff, clarify) |
253 prefer 2 apply (simp add: zero_less_binomial_iff, clarify) |
259 apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = |
254 apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = |
260 exponent p (Suc n)") |
255 exponent p (Suc n)") |
261 txt{*First, use the assumed equation. We simplify the LHS to |
256 txt{*First, use the assumed equation. We simplify the LHS to |
262 @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"} |
257 @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"} |
269 apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add) |
264 apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add) |
270 done |
265 done |
271 |
266 |
272 (*The lemma above, with two changes of variables*) |
267 (*The lemma above, with two changes of variables*) |
273 lemma p_not_div_choose: |
268 lemma p_not_div_choose: |
274 "[| k<K; k<=n; |
269 "[| k<K; k<=n; |
275 \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|] |
270 \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|] |
276 ==> exponent p (n choose k) = 0" |
271 ==> exponent p (n choose k) = 0" |
277 apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma) |
272 apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma) |
278 prefer 3 apply simp |
273 prefer 3 apply simp |
279 prefer 2 apply assumption |
274 prefer 2 apply assumption |
280 apply (drule_tac x = "K - Suc i" in spec) |
275 apply (drule_tac x = "K - Suc i" in spec) |
281 apply (simp add: Suc_diff_le) |
276 apply (simp add: Suc_diff_le) |
282 done |
277 done |
283 |
278 |
284 |
279 |
285 lemma const_p_fac_right: |
280 lemma const_p_fac_right: |
286 "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0" |
281 "m\<noteq>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0" |
287 apply (case_tac "prime p") |
282 apply (case_tac "prime p") |
288 prefer 2 apply simp |
283 prefer 2 apply simp |
289 apply (frule_tac a = a in zero_less_prime_power) |
284 apply (frule_tac a = a in zero_less_prime_power) |
290 apply (rule_tac K = "p^a" in p_not_div_choose) |
285 apply (rule_tac K = "p^a" in p_not_div_choose) |
291 apply simp |
286 apply simp |