equal
deleted
inserted
replaced
7 |
7 |
8 theory Exponent |
8 theory Exponent |
9 imports Main Primes Binomial |
9 imports Main Primes Binomial |
10 begin |
10 begin |
11 |
11 |
12 section {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
12 section {*Sylow's Theorem*} |
|
13 |
|
14 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} |
|
15 |
13 definition exponent :: "nat => nat => nat" where |
16 definition exponent :: "nat => nat => nat" where |
14 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" |
17 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0" |
15 |
18 |
16 |
19 |
17 subsection{*Prime Theorems*} |
20 text{*Prime Theorems*} |
18 |
21 |
19 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |
22 lemma prime_imp_one_less: "prime p ==> Suc 0 < p" |
20 by (unfold prime_def, force) |
23 by (unfold prime_def, force) |
21 |
24 |
22 lemma prime_iff: |
25 lemma prime_iff: |
104 apply (drule dvd_imp_le) |
107 apply (drule dvd_imp_le) |
105 apply (drule_tac [2] n = n in Suc_le_power, auto) |
108 apply (drule_tac [2] n = n in Suc_le_power, auto) |
106 done |
109 done |
107 |
110 |
108 |
111 |
109 subsection{*Exponent Theorems*} |
112 text{*Exponent Theorems*} |
110 |
113 |
111 lemma exponent_ge [rule_format]: |
114 lemma exponent_ge [rule_format]: |
112 "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n" |
115 "[|p^k dvd n; prime p; 0<n|] ==> k <= exponent p n" |
113 apply (simp add: exponent_def) |
116 apply (simp add: exponent_def) |
114 apply (erule Greatest_le) |
117 apply (erule Greatest_le) |
184 apply (case_tac "prime p") |
187 apply (case_tac "prime p") |
185 apply (auto simp add: prime_iff not_divides_exponent_0) |
188 apply (auto simp add: prime_iff not_divides_exponent_0) |
186 done |
189 done |
187 |
190 |
188 |
191 |
189 subsection{*Main Combinatorial Argument*} |
192 text{*Main Combinatorial Argument*} |
190 |
193 |
191 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" |
194 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)" |
192 apply (rule_tac P = "%x. x <= b * c" in subst) |
195 apply (rule_tac P = "%x. x <= b * c" in subst) |
193 apply (rule mult_1_right) |
196 apply (rule mult_1_right) |
194 apply (rule mult_le_mono, auto) |
197 apply (rule mult_le_mono, auto) |