src/HOL/Algebra/Exponent.thy
changeset 13870 cf947d1ec5ff
child 14706 71590b7733b7
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/Algebra/Exponent.thy	Tue Mar 18 18:07:06 2003 +0100
     1.3 @@ -0,0 +1,351 @@
     1.4 +(*  Title:      HOL/GroupTheory/Exponent
     1.5 +    ID:         $Id$
     1.6 +    Author:     Florian Kammueller, with new proofs by L C Paulson
     1.7 +
     1.8 +    exponent p s   yields the greatest power of p that divides s.
     1.9 +*)
    1.10 +
    1.11 +header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
    1.12 +
    1.13 +theory Exponent = Main + Primes:
    1.14 +
    1.15 +constdefs
    1.16 +  exponent      :: "[nat, nat] => nat"
    1.17 +  "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
    1.18 +
    1.19 +subsection{*Prime Theorems*}
    1.20 +
    1.21 +lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
    1.22 +by (unfold prime_def, force)
    1.23 +
    1.24 +lemma prime_iff:
    1.25 +     "(p \<in> prime) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    1.26 +apply (auto simp add: prime_imp_one_less)
    1.27 +apply (blast dest!: prime_dvd_mult)
    1.28 +apply (auto simp add: prime_def)
    1.29 +apply (erule dvdE)
    1.30 +apply (case_tac "k=0", simp)
    1.31 +apply (drule_tac x = m in spec)
    1.32 +apply (drule_tac x = k in spec)
    1.33 +apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2, auto)
    1.34 +done
    1.35 +
    1.36 +lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
    1.37 +by (force simp add: prime_iff)
    1.38 +
    1.39 +
    1.40 +lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
    1.41 +apply (rule_tac P = "%x. x <= b * c" in subst)
    1.42 +apply (rule mult_1_right)
    1.43 +apply (rule mult_le_mono, auto)
    1.44 +done
    1.45 +
    1.46 +lemma insert_partition:
    1.47 +     "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
    1.48 +      ==> x \<inter> \<Union> F = {}"
    1.49 +by auto
    1.50 +
    1.51 +(* main cardinality theorem *)
    1.52 +lemma card_partition [rule_format]:
    1.53 +     "finite C ==>  
    1.54 +        finite (\<Union> C) -->  
    1.55 +        (\<forall>c\<in>C. card c = k) -->   
    1.56 +        (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
    1.57 +        k * card(C) = card (\<Union> C)"
    1.58 +apply (erule finite_induct, simp)
    1.59 +apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
    1.60 +       finite_subset [of _ "\<Union> (insert x F)"])
    1.61 +done
    1.62 +
    1.63 +lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
    1.64 +by (rule ccontr, simp)
    1.65 +
    1.66 +
    1.67 +lemma prime_dvd_cases:
    1.68 +     "[| p*k dvd m*n;  p \<in> prime |]  
    1.69 +      ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    1.70 +apply (simp add: prime_iff)
    1.71 +apply (frule dvd_mult_left)
    1.72 +apply (subgoal_tac "p dvd m | p dvd n")
    1.73 + prefer 2 apply blast
    1.74 +apply (erule disjE)
    1.75 +apply (rule disjI1)
    1.76 +apply (rule_tac [2] disjI2)
    1.77 +apply (erule_tac n = m in dvdE)
    1.78 +apply (erule_tac [2] n = n in dvdE, auto)
    1.79 +apply (rule_tac [2] k = p in dvd_mult_cancel)
    1.80 +apply (rule_tac k = p in dvd_mult_cancel)
    1.81 +apply (simp_all add: mult_ac)
    1.82 +done
    1.83 +
    1.84 +
    1.85 +lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime  
    1.86 +      ==> \<forall>m n. p^c dvd m*n -->  
    1.87 +          (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    1.88 +apply (induct_tac "c")
    1.89 + apply clarify
    1.90 + apply (case_tac "a")
    1.91 +  apply simp
    1.92 + apply simp
    1.93 +(*inductive step*)
    1.94 +apply simp
    1.95 +apply clarify
    1.96 +apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
    1.97 +(*case 1: p dvd m*)
    1.98 + apply (case_tac "a")
    1.99 +  apply simp
   1.100 + apply clarify
   1.101 + apply (drule spec, drule spec, erule (1) notE impE)
   1.102 + apply (drule_tac x = nat in spec)
   1.103 + apply (drule_tac x = b in spec)
   1.104 + apply simp
   1.105 + apply (blast intro: dvd_refl mult_dvd_mono)
   1.106 +(*case 2: p dvd n*)
   1.107 +apply (case_tac "b")
   1.108 + apply simp
   1.109 +apply clarify
   1.110 +apply (drule spec, drule spec, erule (1) notE impE)
   1.111 +apply (drule_tac x = a in spec)
   1.112 +apply (drule_tac x = nat in spec, simp)
   1.113 +apply (blast intro: dvd_refl mult_dvd_mono)
   1.114 +done
   1.115 +
   1.116 +(*needed in this form in Sylow.ML*)
   1.117 +lemma div_combine:
   1.118 +     "[| p \<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
   1.119 +      ==> p ^ a dvd k"
   1.120 +by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
   1.121 +
   1.122 +(*Lemma for power_dvd_bound*)
   1.123 +lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
   1.124 +apply (induct_tac "n")
   1.125 +apply (simp (no_asm_simp))
   1.126 +apply simp
   1.127 +apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
   1.128 +apply (subgoal_tac "2 * p^n <= p * p^n")
   1.129 +(*?arith_tac should handle all of this!*)
   1.130 +apply (rule order_trans)
   1.131 +prefer 2 apply assumption
   1.132 +apply (drule_tac k = 2 in mult_le_mono2, simp)
   1.133 +apply (rule mult_le_mono1, simp)
   1.134 +done
   1.135 +
   1.136 +(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
   1.137 +lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  0 < a|] ==> n < a"
   1.138 +apply (drule dvd_imp_le)
   1.139 +apply (drule_tac [2] n = n in Suc_le_power, auto)
   1.140 +done
   1.141 +
   1.142 +
   1.143 +subsection{*Exponent Theorems*}
   1.144 +
   1.145 +lemma exponent_ge [rule_format]:
   1.146 +     "[|p^k dvd n;  p \<in> prime;  0<n|] ==> k <= exponent p n"
   1.147 +apply (simp add: exponent_def)
   1.148 +apply (erule Greatest_le)
   1.149 +apply (blast dest: prime_imp_one_less power_dvd_bound)
   1.150 +done
   1.151 +
   1.152 +lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
   1.153 +apply (simp add: exponent_def)
   1.154 +apply clarify
   1.155 +apply (rule_tac k = 0 in GreatestI)
   1.156 +prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
   1.157 +done
   1.158 +
   1.159 +lemma power_Suc_exponent_Not_dvd:
   1.160 +     "[|(p * p ^ exponent p s) dvd s;  p \<in> prime |] ==> s=0"
   1.161 +apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
   1.162 + prefer 2 apply simp 
   1.163 +apply (rule ccontr)
   1.164 +apply (drule exponent_ge, auto)
   1.165 +done
   1.166 +
   1.167 +lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
   1.168 +apply (simp (no_asm_simp) add: exponent_def)
   1.169 +apply (rule Greatest_equality, simp)
   1.170 +apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
   1.171 +done
   1.172 +
   1.173 +lemma exponent_equalityI:
   1.174 +     "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   1.175 +by (simp (no_asm_simp) add: exponent_def)
   1.176 +
   1.177 +lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
   1.178 +by (simp (no_asm_simp) add: exponent_def)
   1.179 +
   1.180 +
   1.181 +(* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
   1.182 +lemma exponent_mult_add1:
   1.183 +     "[| 0 < a; 0 < b |]   
   1.184 +      ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   1.185 +apply (case_tac "p \<in> prime")
   1.186 +apply (rule exponent_ge)
   1.187 +apply (auto simp add: power_add)
   1.188 +apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
   1.189 +done
   1.190 +
   1.191 +(* exponent_mult_add, opposite inclusion *)
   1.192 +lemma exponent_mult_add2: "[| 0 < a; 0 < b |]  
   1.193 +      ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   1.194 +apply (case_tac "p \<in> prime")
   1.195 +apply (rule leI, clarify)
   1.196 +apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
   1.197 +apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
   1.198 +apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
   1.199 +  prefer 3 apply assumption
   1.200 + prefer 2 apply simp 
   1.201 +apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
   1.202 + apply (assumption, force, simp)
   1.203 +apply (blast dest: power_Suc_exponent_Not_dvd)
   1.204 +done
   1.205 +
   1.206 +lemma exponent_mult_add:
   1.207 +     "[| 0 < a; 0 < b |]  
   1.208 +      ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   1.209 +by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
   1.210 +
   1.211 +
   1.212 +lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
   1.213 +apply (case_tac "exponent p n", simp)
   1.214 +apply (case_tac "n", simp)
   1.215 +apply (cut_tac s = n and p = p in power_exponent_dvd)
   1.216 +apply (auto dest: dvd_mult_left)
   1.217 +done
   1.218 +
   1.219 +lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   1.220 +apply (case_tac "p \<in> prime")
   1.221 +apply (auto simp add: prime_iff not_divides_exponent_0)
   1.222 +done
   1.223 +
   1.224 +
   1.225 +subsection{*Lemmas for the Main Combinatorial Argument*}
   1.226 +
   1.227 +lemma p_fac_forw_lemma:
   1.228 +     "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   1.229 +apply (rule notnotD)
   1.230 +apply (rule notI)
   1.231 +apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
   1.232 +apply (drule_tac m = a in less_imp_le)
   1.233 +apply (drule le_imp_power_dvd)
   1.234 +apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
   1.235 +apply (frule_tac m = k in less_imp_le)
   1.236 +apply (drule_tac c = m in le_extend_mult, assumption)
   1.237 +apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
   1.238 +prefer 2 apply assumption
   1.239 +apply (rule dvd_refl [THEN dvd_mult2])
   1.240 +apply (drule_tac n = k in dvd_imp_le, auto)
   1.241 +done
   1.242 +
   1.243 +lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  
   1.244 +      ==> (p^r) dvd (p^a) - k"
   1.245 +apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
   1.246 +apply (subgoal_tac "p^r dvd p^a*m")
   1.247 + prefer 2 apply (blast intro: dvd_mult2)
   1.248 +apply (drule dvd_diffD1)
   1.249 +  apply assumption
   1.250 + prefer 2 apply (blast intro: dvd_diff)
   1.251 +apply (drule less_imp_Suc_add, auto)
   1.252 +done
   1.253 +
   1.254 +
   1.255 +lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
   1.256 +by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
   1.257 +
   1.258 +lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a;  (p^r) dvd p^a - k |]  
   1.259 +      ==> (p^r) dvd (p^a)*m - k"
   1.260 +apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
   1.261 +apply (subgoal_tac "p^r dvd p^a*m")
   1.262 + prefer 2 apply (blast intro: dvd_mult2)
   1.263 +apply (drule dvd_diffD1)
   1.264 +  apply assumption
   1.265 + prefer 2 apply (blast intro: dvd_diff)
   1.266 +apply (drule less_imp_Suc_add, auto)
   1.267 +done
   1.268 +
   1.269 +lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a |]  
   1.270 +      ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   1.271 +apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   1.272 +done
   1.273 +
   1.274 +text{*Suc rules that we have to delete from the simpset*}
   1.275 +lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
   1.276 +
   1.277 +(*The bound K is needed; otherwise it's too weak to be used.*)
   1.278 +lemma p_not_div_choose_lemma [rule_format]:
   1.279 +     "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   1.280 +      ==> k<K --> exponent p ((j+k) choose k) = 0"
   1.281 +apply (case_tac "p \<in> prime")
   1.282 + prefer 2 apply simp 
   1.283 +apply (induct_tac "k")
   1.284 +apply (simp (no_asm))
   1.285 +(*induction step*)
   1.286 +apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
   1.287 + prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
   1.288 +apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = 
   1.289 +                    exponent p (Suc n)")
   1.290 + txt{*First, use the assumed equation.  We simplify the LHS to
   1.291 +  @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
   1.292 +  the common terms cancel, proving the conclusion.*}
   1.293 + apply (simp del: bad_Sucs add: exponent_mult_add)
   1.294 +txt{*Establishing the equation requires first applying 
   1.295 +   @{text Suc_times_binomial_eq} ...*}
   1.296 +apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
   1.297 +txt{*...then @{text exponent_mult_add} and the quantified premise.*}
   1.298 +apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
   1.299 +done
   1.300 +
   1.301 +(*The lemma above, with two changes of variables*)
   1.302 +lemma p_not_div_choose:
   1.303 +     "[| k<K;  k<=n;   
   1.304 +       \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]  
   1.305 +      ==> exponent p (n choose k) = 0"
   1.306 +apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
   1.307 +  prefer 3 apply simp
   1.308 + prefer 2 apply assumption
   1.309 +apply (drule_tac x = "K - Suc i" in spec)
   1.310 +apply (simp add: Suc_diff_le)
   1.311 +done
   1.312 +
   1.313 +
   1.314 +lemma const_p_fac_right:
   1.315 +     "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   1.316 +apply (case_tac "p \<in> prime")
   1.317 + prefer 2 apply simp 
   1.318 +apply (frule_tac a = a in zero_less_prime_power)
   1.319 +apply (rule_tac K = "p^a" in p_not_div_choose)
   1.320 +   apply simp
   1.321 +  apply simp
   1.322 + apply (case_tac "m")
   1.323 +  apply (case_tac [2] "p^a")
   1.324 +   apply auto
   1.325 +(*now the hard case, simplified to
   1.326 +    exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
   1.327 +apply (subgoal_tac "0<p")
   1.328 + prefer 2 apply (force dest!: prime_imp_one_less)
   1.329 +apply (subst exponent_p_a_m_k_equation, auto)
   1.330 +done
   1.331 +
   1.332 +lemma const_p_fac:
   1.333 +     "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   1.334 +apply (case_tac "p \<in> prime")
   1.335 + prefer 2 apply simp 
   1.336 +apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   1.337 + prefer 2 apply (force simp add: prime_iff)
   1.338 +txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
   1.339 +  insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   1.340 +  first
   1.341 +  transform the binomial coefficient, then use @{text exponent_mult_add}.*}
   1.342 +apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
   1.343 +                    a + exponent p m")
   1.344 + apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
   1.345 +txt{*one subgoal left!*}
   1.346 +apply (subst times_binomial_minus1_eq, simp, simp)
   1.347 +apply (subst exponent_mult_add, simp)
   1.348 +apply (simp (no_asm_simp) add: zero_less_binomial_iff)
   1.349 +apply arith
   1.350 +apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
   1.351 +done
   1.352 +
   1.353 +
   1.354 +end