src/HOL/Algebra/Exponent.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 16663 13e9c402308b permissions -rw-r--r--
Constant "If" is now local
1 (*  Title:      HOL/Algebra/Exponent.thy
2     ID:         \$Id\$
3     Author:     Florian Kammueller, with new proofs by L C Paulson
5     exponent p s   yields the greatest power of p that divides s.
6 *)
8 header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
10 theory Exponent imports Main Primes begin
12 constdefs
13   exponent      :: "[nat, nat] => nat"
14   "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
16 subsection{*Prime Theorems*}
18 lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
19 by (unfold prime_def, force)
21 lemma prime_iff:
22      "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
23 apply (auto simp add: prime_imp_one_less)
24 apply (blast dest!: prime_dvd_mult)
25 apply (auto simp add: prime_def)
26 apply (erule dvdE)
27 apply (case_tac "k=0", simp)
28 apply (drule_tac x = m in spec)
29 apply (drule_tac x = k in spec)
30 apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
31 done
33 lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
34 by (force simp add: prime_iff)
37 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
38 by (rule ccontr, simp)
41 lemma prime_dvd_cases:
42      "[| p*k dvd m*n;  p \<in> prime |]
43       ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
45 apply (frule dvd_mult_left)
46 apply (subgoal_tac "p dvd m | p dvd n")
47  prefer 2 apply blast
48 apply (erule disjE)
49 apply (rule disjI1)
50 apply (rule_tac [2] disjI2)
51 apply (erule_tac n = m in dvdE)
52 apply (erule_tac [2] n = n in dvdE, auto)
53 apply (rule_tac [2] k = p in dvd_mult_cancel)
54 apply (rule_tac k = p in dvd_mult_cancel)
56 done
59 lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime
60       ==> \<forall>m n. p^c dvd m*n -->
61           (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
62 apply (induct_tac "c")
63  apply clarify
64  apply (case_tac "a")
65   apply simp
66  apply simp
67 (*inductive step*)
68 apply simp
69 apply clarify
70 apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
71 (*case 1: p dvd m*)
72  apply (case_tac "a")
73   apply simp
74  apply clarify
75  apply (drule spec, drule spec, erule (1) notE impE)
76  apply (drule_tac x = nat in spec)
77  apply (drule_tac x = b in spec)
78  apply simp
79  apply (blast intro: dvd_refl mult_dvd_mono)
80 (*case 2: p dvd n*)
81 apply (case_tac "b")
82  apply simp
83 apply clarify
84 apply (drule spec, drule spec, erule (1) notE impE)
85 apply (drule_tac x = a in spec)
86 apply (drule_tac x = nat in spec, simp)
87 apply (blast intro: dvd_refl mult_dvd_mono)
88 done
90 (*needed in this form in Sylow.ML*)
91 lemma div_combine:
92      "[| p \<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]
93       ==> p ^ a dvd k"
94 by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
96 (*Lemma for power_dvd_bound*)
97 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
98 apply (induct_tac "n")
99 apply (simp (no_asm_simp))
100 apply simp
101 apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
102 apply (subgoal_tac "2 * p^n <= p * p^n")
103 (*?arith_tac should handle all of this!*)
104 apply (rule order_trans)
105 prefer 2 apply assumption
106 apply (drule_tac k = 2 in mult_le_mono2, simp)
107 apply (rule mult_le_mono1, simp)
108 done
110 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
111 lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  0 < a|] ==> n < a"
112 apply (drule dvd_imp_le)
113 apply (drule_tac [2] n = n in Suc_le_power, auto)
114 done
117 subsection{*Exponent Theorems*}
119 lemma exponent_ge [rule_format]:
120      "[|p^k dvd n;  p \<in> prime;  0<n|] ==> k <= exponent p n"
122 apply (erule Greatest_le)
123 apply (blast dest: prime_imp_one_less power_dvd_bound)
124 done
126 lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
128 apply clarify
129 apply (rule_tac k = 0 in GreatestI)
130 prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
131 done
133 lemma power_Suc_exponent_Not_dvd:
134      "[|(p * p ^ exponent p s) dvd s;  p \<in> prime |] ==> s=0"
135 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
136  prefer 2 apply simp
137 apply (rule ccontr)
138 apply (drule exponent_ge, auto)
139 done
141 lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
142 apply (simp (no_asm_simp) add: exponent_def)
143 apply (rule Greatest_equality, simp)
144 apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
145 done
147 lemma exponent_equalityI:
148      "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
149 by (simp (no_asm_simp) add: exponent_def)
151 lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
152 by (simp (no_asm_simp) add: exponent_def)
155 (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
157      "[| 0 < a; 0 < b |]
158       ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
159 apply (case_tac "p \<in> prime")
160 apply (rule exponent_ge)
162 apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
163 done
165 (* exponent_mult_add, opposite inclusion *)
166 lemma exponent_mult_add2: "[| 0 < a; 0 < b |]
167       ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
168 apply (case_tac "p \<in> prime")
169 apply (rule leI, clarify)
170 apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
171 apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
172 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
173   prefer 3 apply assumption
174  prefer 2 apply simp
175 apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
176  apply (assumption, force, simp)
177 apply (blast dest: power_Suc_exponent_Not_dvd)
178 done
181      "[| 0 < a; 0 < b |]
182       ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
186 lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
187 apply (case_tac "exponent p n", simp)
188 apply (case_tac "n", simp)
189 apply (cut_tac s = n and p = p in power_exponent_dvd)
190 apply (auto dest: dvd_mult_left)
191 done
193 lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
194 apply (case_tac "p \<in> prime")
195 apply (auto simp add: prime_iff not_divides_exponent_0)
196 done
199 subsection{*Lemmas for the Main Combinatorial Argument*}
201 lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
202 apply (rule_tac P = "%x. x <= b * c" in subst)
203 apply (rule mult_1_right)
204 apply (rule mult_le_mono, auto)
205 done
207 lemma p_fac_forw_lemma:
208      "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
209 apply (rule notnotD)
210 apply (rule notI)
211 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
212 apply (drule_tac m = a in less_imp_le)
213 apply (drule le_imp_power_dvd)
214 apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
215 apply (frule_tac m = k in less_imp_le)
216 apply (drule_tac c = m in le_extend_mult, assumption)
217 apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
218 prefer 2 apply assumption
219 apply (rule dvd_refl [THEN dvd_mult2])
220 apply (drule_tac n = k in dvd_imp_le, auto)
221 done
223 lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]
224       ==> (p^r) dvd (p^a) - k"
225 apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
226 apply (subgoal_tac "p^r dvd p^a*m")
227  prefer 2 apply (blast intro: dvd_mult2)
228 apply (drule dvd_diffD1)
229   apply assumption
230  prefer 2 apply (blast intro: dvd_diff)
232 done
235 lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
236 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
238 lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a;  (p^r) dvd p^a - k |]
239       ==> (p^r) dvd (p^a)*m - k"
240 apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
241 apply (subgoal_tac "p^r dvd p^a*m")
242  prefer 2 apply (blast intro: dvd_mult2)
243 apply (drule dvd_diffD1)
244   apply assumption
245  prefer 2 apply (blast intro: dvd_diff)
247 done
249 lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a |]
250       ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
251 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
252 done
254 text{*Suc rules that we have to delete from the simpset*}
255 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
257 (*The bound K is needed; otherwise it's too weak to be used.*)
258 lemma p_not_div_choose_lemma [rule_format]:
259      "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]
260       ==> k<K --> exponent p ((j+k) choose k) = 0"
261 apply (case_tac "p \<in> prime")
262  prefer 2 apply simp
263 apply (induct_tac "k")
264 apply (simp (no_asm))
265 (*induction step*)
266 apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
267  prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
268 apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) =
269                     exponent p (Suc n)")
270  txt{*First, use the assumed equation.  We simplify the LHS to
271   @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
272   the common terms cancel, proving the conclusion.*}
274 txt{*Establishing the equation requires first applying
275    @{text Suc_times_binomial_eq} ...*}
277 txt{*...then @{text exponent_mult_add} and the quantified premise.*}
279 done
281 (*The lemma above, with two changes of variables*)
282 lemma p_not_div_choose:
283      "[| k<K;  k<=n;
284        \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
285       ==> exponent p (n choose k) = 0"
286 apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
287   prefer 3 apply simp
288  prefer 2 apply assumption
289 apply (drule_tac x = "K - Suc i" in spec)
291 done
294 lemma const_p_fac_right:
295      "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
296 apply (case_tac "p \<in> prime")
297  prefer 2 apply simp
298 apply (frule_tac a = a in zero_less_prime_power)
299 apply (rule_tac K = "p^a" in p_not_div_choose)
300    apply simp
301   apply simp
302  apply (case_tac "m")
303   apply (case_tac [2] "p^a")
304    apply auto
305 (*now the hard case, simplified to
306     exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
307 apply (subgoal_tac "0<p")
308  prefer 2 apply (force dest!: prime_imp_one_less)
309 apply (subst exponent_p_a_m_k_equation, auto)
310 done
312 lemma const_p_fac:
313      "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
314 apply (case_tac "p \<in> prime")
315  prefer 2 apply simp
316 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
317  prefer 2 apply (force simp add: prime_iff)
318 txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
319   insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
320   first
321   transform the binomial coefficient, then use @{text exponent_mult_add}.*}
322 apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) =
323                     a + exponent p m")