src/HOL/Algebra/Exponent.thy
author paulson
Tue Mar 18 18:07:06 2003 +0100 (2003-03-18)
changeset 13870 cf947d1ec5ff
child 14706 71590b7733b7
permissions -rw-r--r--
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
to the new Group setup.

Deleted Ring, Module from GroupTheory

Minor UNITY changes
     1 (*  Title:      HOL/GroupTheory/Exponent
     2     ID:         $Id$
     3     Author:     Florian Kammueller, with new proofs by L C Paulson
     4 
     5     exponent p s   yields the greatest power of p that divides s.
     6 *)
     7 
     8 header{*The Combinatorial Argument Underlying the First Sylow Theorem*}
     9 
    10 theory Exponent = Main + Primes:
    11 
    12 constdefs
    13   exponent      :: "[nat, nat] => nat"
    14   "exponent p s == if p \<in> prime then (GREATEST r. p^r dvd s) else 0"
    15 
    16 subsection{*Prime Theorems*}
    17 
    18 lemma prime_imp_one_less: "p \<in> prime ==> Suc 0 < p"
    19 by (unfold prime_def, force)
    20 
    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
    32 
    33 lemma zero_less_prime_power: "p \<in> prime ==> 0 < p^a"
    34 by (force simp add: prime_iff)
    35 
    36 
    37 lemma le_extend_mult: "[| 0 < c; a <= b |] ==> a <= b * (c::nat)"
    38 apply (rule_tac P = "%x. x <= b * c" in subst)
    39 apply (rule mult_1_right)
    40 apply (rule mult_le_mono, auto)
    41 done
    42 
    43 lemma insert_partition:
    44      "[| x \<notin> F; \<forall>c1\<in>insert x F. \<forall>c2 \<in> insert x F. c1 \<noteq> c2 --> c1 \<inter> c2 = {}|] 
    45       ==> x \<inter> \<Union> F = {}"
    46 by auto
    47 
    48 (* main cardinality theorem *)
    49 lemma card_partition [rule_format]:
    50      "finite C ==>  
    51         finite (\<Union> C) -->  
    52         (\<forall>c\<in>C. card c = k) -->   
    53         (\<forall>c1 \<in> C. \<forall>c2 \<in> C. c1 \<noteq> c2 --> c1 \<inter> c2 = {}) -->  
    54         k * card(C) = card (\<Union> C)"
    55 apply (erule finite_induct, simp)
    56 apply (simp add: card_insert_disjoint card_Un_disjoint insert_partition 
    57        finite_subset [of _ "\<Union> (insert x F)"])
    58 done
    59 
    60 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
    61 by (rule ccontr, simp)
    62 
    63 
    64 lemma prime_dvd_cases:
    65      "[| p*k dvd m*n;  p \<in> prime |]  
    66       ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    67 apply (simp add: prime_iff)
    68 apply (frule dvd_mult_left)
    69 apply (subgoal_tac "p dvd m | p dvd n")
    70  prefer 2 apply blast
    71 apply (erule disjE)
    72 apply (rule disjI1)
    73 apply (rule_tac [2] disjI2)
    74 apply (erule_tac n = m in dvdE)
    75 apply (erule_tac [2] n = n in dvdE, auto)
    76 apply (rule_tac [2] k = p in dvd_mult_cancel)
    77 apply (rule_tac k = p in dvd_mult_cancel)
    78 apply (simp_all add: mult_ac)
    79 done
    80 
    81 
    82 lemma prime_power_dvd_cases [rule_format (no_asm)]: "p \<in> prime  
    83       ==> \<forall>m n. p^c dvd m*n -->  
    84           (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    85 apply (induct_tac "c")
    86  apply clarify
    87  apply (case_tac "a")
    88   apply simp
    89  apply simp
    90 (*inductive step*)
    91 apply simp
    92 apply clarify
    93 apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
    94 (*case 1: p dvd m*)
    95  apply (case_tac "a")
    96   apply simp
    97  apply clarify
    98  apply (drule spec, drule spec, erule (1) notE impE)
    99  apply (drule_tac x = nat in spec)
   100  apply (drule_tac x = b in spec)
   101  apply simp
   102  apply (blast intro: dvd_refl mult_dvd_mono)
   103 (*case 2: p dvd n*)
   104 apply (case_tac "b")
   105  apply simp
   106 apply clarify
   107 apply (drule spec, drule spec, erule (1) notE impE)
   108 apply (drule_tac x = a in spec)
   109 apply (drule_tac x = nat in spec, simp)
   110 apply (blast intro: dvd_refl mult_dvd_mono)
   111 done
   112 
   113 (*needed in this form in Sylow.ML*)
   114 lemma div_combine:
   115      "[| p \<in> prime; ~ (p ^ (Suc r) dvd n);  p^(a+r) dvd n*k |]  
   116       ==> p ^ a dvd k"
   117 by (drule_tac a = "Suc r" and b = a in prime_power_dvd_cases, assumption, auto)
   118 
   119 (*Lemma for power_dvd_bound*)
   120 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
   121 apply (induct_tac "n")
   122 apply (simp (no_asm_simp))
   123 apply simp
   124 apply (subgoal_tac "2 * n + 2 <= p * p^n", simp)
   125 apply (subgoal_tac "2 * p^n <= p * p^n")
   126 (*?arith_tac should handle all of this!*)
   127 apply (rule order_trans)
   128 prefer 2 apply assumption
   129 apply (drule_tac k = 2 in mult_le_mono2, simp)
   130 apply (rule mult_le_mono1, simp)
   131 done
   132 
   133 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
   134 lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  0 < a|] ==> n < a"
   135 apply (drule dvd_imp_le)
   136 apply (drule_tac [2] n = n in Suc_le_power, auto)
   137 done
   138 
   139 
   140 subsection{*Exponent Theorems*}
   141 
   142 lemma exponent_ge [rule_format]:
   143      "[|p^k dvd n;  p \<in> prime;  0<n|] ==> k <= exponent p n"
   144 apply (simp add: exponent_def)
   145 apply (erule Greatest_le)
   146 apply (blast dest: prime_imp_one_less power_dvd_bound)
   147 done
   148 
   149 lemma power_exponent_dvd: "0<s ==> (p ^ exponent p s) dvd s"
   150 apply (simp add: exponent_def)
   151 apply clarify
   152 apply (rule_tac k = 0 in GreatestI)
   153 prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
   154 done
   155 
   156 lemma power_Suc_exponent_Not_dvd:
   157      "[|(p * p ^ exponent p s) dvd s;  p \<in> prime |] ==> s=0"
   158 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
   159  prefer 2 apply simp 
   160 apply (rule ccontr)
   161 apply (drule exponent_ge, auto)
   162 done
   163 
   164 lemma exponent_power_eq [simp]: "p \<in> prime ==> exponent p (p^a) = a"
   165 apply (simp (no_asm_simp) add: exponent_def)
   166 apply (rule Greatest_equality, simp)
   167 apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
   168 done
   169 
   170 lemma exponent_equalityI:
   171      "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   172 by (simp (no_asm_simp) add: exponent_def)
   173 
   174 lemma exponent_eq_0 [simp]: "p \<notin> prime ==> exponent p s = 0"
   175 by (simp (no_asm_simp) add: exponent_def)
   176 
   177 
   178 (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
   179 lemma exponent_mult_add1:
   180      "[| 0 < a; 0 < b |]   
   181       ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   182 apply (case_tac "p \<in> prime")
   183 apply (rule exponent_ge)
   184 apply (auto simp add: power_add)
   185 apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
   186 done
   187 
   188 (* exponent_mult_add, opposite inclusion *)
   189 lemma exponent_mult_add2: "[| 0 < a; 0 < b |]  
   190       ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   191 apply (case_tac "p \<in> prime")
   192 apply (rule leI, clarify)
   193 apply (cut_tac p = p and s = "a*b" in power_exponent_dvd, auto)
   194 apply (subgoal_tac "p ^ (Suc (exponent p a + exponent p b)) dvd a * b")
   195 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
   196   prefer 3 apply assumption
   197  prefer 2 apply simp 
   198 apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
   199  apply (assumption, force, simp)
   200 apply (blast dest: power_Suc_exponent_Not_dvd)
   201 done
   202 
   203 lemma exponent_mult_add:
   204      "[| 0 < a; 0 < b |]  
   205       ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   206 by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
   207 
   208 
   209 lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
   210 apply (case_tac "exponent p n", simp)
   211 apply (case_tac "n", simp)
   212 apply (cut_tac s = n and p = p in power_exponent_dvd)
   213 apply (auto dest: dvd_mult_left)
   214 done
   215 
   216 lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   217 apply (case_tac "p \<in> prime")
   218 apply (auto simp add: prime_iff not_divides_exponent_0)
   219 done
   220 
   221 
   222 subsection{*Lemmas for the Main Combinatorial Argument*}
   223 
   224 lemma p_fac_forw_lemma:
   225      "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   226 apply (rule notnotD)
   227 apply (rule notI)
   228 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
   229 apply (drule_tac m = a in less_imp_le)
   230 apply (drule le_imp_power_dvd)
   231 apply (drule_tac n = "p ^ r" in dvd_trans, assumption)
   232 apply (frule_tac m = k in less_imp_le)
   233 apply (drule_tac c = m in le_extend_mult, assumption)
   234 apply (drule_tac k = "p ^ a" and m = " (p ^ a) * m" in dvd_diffD1)
   235 prefer 2 apply assumption
   236 apply (rule dvd_refl [THEN dvd_mult2])
   237 apply (drule_tac n = k in dvd_imp_le, auto)
   238 done
   239 
   240 lemma p_fac_forw: "[| 0 < (m::nat); 0<k; k < p^a; (p^r) dvd (p^a)* m - k |]  
   241       ==> (p^r) dvd (p^a) - k"
   242 apply (frule_tac k1 = k and i = p in p_fac_forw_lemma [THEN le_imp_power_dvd], auto)
   243 apply (subgoal_tac "p^r dvd p^a*m")
   244  prefer 2 apply (blast intro: dvd_mult2)
   245 apply (drule dvd_diffD1)
   246   apply assumption
   247  prefer 2 apply (blast intro: dvd_diff)
   248 apply (drule less_imp_Suc_add, auto)
   249 done
   250 
   251 
   252 lemma r_le_a_forw: "[| 0 < (k::nat); k < p^a; 0 < p; (p^r) dvd (p^a) - k |] ==> r <= a"
   253 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
   254 
   255 lemma p_fac_backw: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a;  (p^r) dvd p^a - k |]  
   256       ==> (p^r) dvd (p^a)*m - k"
   257 apply (frule_tac k1 = k and i = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
   258 apply (subgoal_tac "p^r dvd p^a*m")
   259  prefer 2 apply (blast intro: dvd_mult2)
   260 apply (drule dvd_diffD1)
   261   apply assumption
   262  prefer 2 apply (blast intro: dvd_diff)
   263 apply (drule less_imp_Suc_add, auto)
   264 done
   265 
   266 lemma exponent_p_a_m_k_equation: "[| 0<m; 0<k; 0 < (p::nat);  k < p^a |]  
   267       ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   268 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   269 done
   270 
   271 text{*Suc rules that we have to delete from the simpset*}
   272 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
   273 
   274 (*The bound K is needed; otherwise it's too weak to be used.*)
   275 lemma p_not_div_choose_lemma [rule_format]:
   276      "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   277       ==> k<K --> exponent p ((j+k) choose k) = 0"
   278 apply (case_tac "p \<in> prime")
   279  prefer 2 apply simp 
   280 apply (induct_tac "k")
   281 apply (simp (no_asm))
   282 (*induction step*)
   283 apply (subgoal_tac "0 < (Suc (j+n) choose Suc n) ")
   284  prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
   285 apply (subgoal_tac "exponent p ((Suc (j+n) choose Suc n) * Suc n) = 
   286                     exponent p (Suc n)")
   287  txt{*First, use the assumed equation.  We simplify the LHS to
   288   @{term "exponent p (Suc (j + n) choose Suc n) + exponent p (Suc n)"}
   289   the common terms cancel, proving the conclusion.*}
   290  apply (simp del: bad_Sucs add: exponent_mult_add)
   291 txt{*Establishing the equation requires first applying 
   292    @{text Suc_times_binomial_eq} ...*}
   293 apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
   294 txt{*...then @{text exponent_mult_add} and the quantified premise.*}
   295 apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
   296 done
   297 
   298 (*The lemma above, with two changes of variables*)
   299 lemma p_not_div_choose:
   300      "[| k<K;  k<=n;   
   301        \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]  
   302       ==> exponent p (n choose k) = 0"
   303 apply (cut_tac j = "n-k" and k = k and p = p in p_not_div_choose_lemma)
   304   prefer 3 apply simp
   305  prefer 2 apply assumption
   306 apply (drule_tac x = "K - Suc i" in spec)
   307 apply (simp add: Suc_diff_le)
   308 done
   309 
   310 
   311 lemma const_p_fac_right:
   312      "0 < m ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   313 apply (case_tac "p \<in> prime")
   314  prefer 2 apply simp 
   315 apply (frule_tac a = a in zero_less_prime_power)
   316 apply (rule_tac K = "p^a" in p_not_div_choose)
   317    apply simp
   318   apply simp
   319  apply (case_tac "m")
   320   apply (case_tac [2] "p^a")
   321    apply auto
   322 (*now the hard case, simplified to
   323     exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
   324 apply (subgoal_tac "0<p")
   325  prefer 2 apply (force dest!: prime_imp_one_less)
   326 apply (subst exponent_p_a_m_k_equation, auto)
   327 done
   328 
   329 lemma const_p_fac:
   330      "0 < m ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   331 apply (case_tac "p \<in> prime")
   332  prefer 2 apply simp 
   333 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   334  prefer 2 apply (force simp add: prime_iff)
   335 txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
   336   insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   337   first
   338   transform the binomial coefficient, then use @{text exponent_mult_add}.*}
   339 apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
   340                     a + exponent p m")
   341  apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
   342 txt{*one subgoal left!*}
   343 apply (subst times_binomial_minus1_eq, simp, simp)
   344 apply (subst exponent_mult_add, simp)
   345 apply (simp (no_asm_simp) add: zero_less_binomial_iff)
   346 apply arith
   347 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
   348 done
   349 
   350 
   351 end