src/HOL/Algebra/Exponent.thy
author huffman
Thu Jun 18 18:31:14 2009 -0700 (2009-06-18)
changeset 31717 d1f7b6245a75
parent 30242 aea5d7fa7ef5
child 31952 40501bb2d57c
permissions -rw-r--r--
fix name clash with old/new prime libraries
     1 (*  Title:      HOL/Algebra/Exponent.thy
     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 theory Exponent
     9 imports Main Primes Binomial
    10 begin
    11 
    12 hide (open) const GCD.gcd GCD.coprime GCD.prime
    13 
    14 section {*Sylow's Theorem*}
    15 
    16 subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*}
    17 
    18 definition exponent :: "nat => nat => nat" where
    19 "exponent p s == if prime p then (GREATEST r. p^r dvd s) else 0"
    20 
    21 
    22 text{*Prime Theorems*}
    23 
    24 lemma prime_imp_one_less: "prime p ==> Suc 0 < p"
    25 by (unfold prime_def, force)
    26 
    27 lemma prime_iff:
    28   "(prime p) = (Suc 0 < p & (\<forall>a b. p dvd a*b --> (p dvd a) | (p dvd b)))"
    29 apply (auto simp add: prime_imp_one_less)
    30 apply (blast dest!: prime_dvd_mult)
    31 apply (auto simp add: prime_def)
    32 apply (erule dvdE)
    33 apply (case_tac "k=0", simp)
    34 apply (drule_tac x = m in spec)
    35 apply (drule_tac x = k in spec)
    36 apply (simp add: dvd_mult_cancel1 dvd_mult_cancel2)
    37 done
    38 
    39 lemma zero_less_prime_power: "prime p ==> 0 < p^a"
    40 by (force simp add: prime_iff)
    41 
    42 
    43 lemma zero_less_card_empty: "[| finite S; S \<noteq> {} |] ==> 0 < card(S)"
    44 by (rule ccontr, simp)
    45 
    46 
    47 lemma prime_dvd_cases:
    48   "[| p*k dvd m*n;  prime p |]  
    49    ==> (\<exists>x. k dvd x*n & m = p*x) | (\<exists>y. k dvd m*y & n = p*y)"
    50 apply (simp add: prime_iff)
    51 apply (frule dvd_mult_left)
    52 apply (subgoal_tac "p dvd m | p dvd n")
    53  prefer 2 apply blast
    54 apply (erule disjE)
    55 apply (rule disjI1)
    56 apply (rule_tac [2] disjI2)
    57 apply (auto elim!: dvdE)
    58 done
    59 
    60 
    61 lemma prime_power_dvd_cases [rule_format (no_asm)]: "prime p
    62   ==> \<forall>m n. p^c dvd m*n -->  
    63         (\<forall>a b. a+b = Suc c --> p^a dvd m | p^b dvd n)"
    64 apply (induct c)
    65  apply clarify
    66  apply (case_tac "a")
    67   apply simp
    68  apply simp
    69 (*inductive step*)
    70 apply simp
    71 apply clarify
    72 apply (erule prime_dvd_cases [THEN disjE], assumption, auto)
    73 (*case 1: p dvd m*)
    74  apply (case_tac "a")
    75   apply simp
    76  apply clarify
    77  apply (drule spec, drule spec, erule (1) notE impE)
    78  apply (drule_tac x = nat in spec)
    79  apply (drule_tac x = b in spec)
    80  apply simp
    81 (*case 2: p dvd n*)
    82 apply (case_tac "b")
    83  apply simp
    84 apply clarify
    85 apply (drule spec, drule spec, erule (1) notE impE)
    86 apply (drule_tac x = a in spec)
    87 apply (drule_tac x = nat in spec, simp)
    88 done
    89 
    90 (*needed in this form in Sylow.ML*)
    91 lemma div_combine:
    92   "[| prime p; ~ (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)
    95 
    96 (*Lemma for power_dvd_bound*)
    97 lemma Suc_le_power: "Suc 0 < p ==> Suc n <= p^n"
    98 apply (induct 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 apply arith
   104 apply (drule_tac k = 2 in mult_le_mono2, simp)
   105 done
   106 
   107 (*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*)
   108 lemma power_dvd_bound: "[|p^n dvd a;  Suc 0 < p;  a > 0|] ==> n < a"
   109 apply (drule dvd_imp_le)
   110 apply (drule_tac [2] n = n in Suc_le_power, auto)
   111 done
   112 
   113 
   114 text{*Exponent Theorems*}
   115 
   116 lemma exponent_ge [rule_format]:
   117   "[|p^k dvd n;  prime p;  0<n|] ==> k <= exponent p n"
   118 apply (simp add: exponent_def)
   119 apply (erule Greatest_le)
   120 apply (blast dest: prime_imp_one_less power_dvd_bound)
   121 done
   122 
   123 lemma power_exponent_dvd: "s>0 ==> (p ^ exponent p s) dvd s"
   124 apply (simp add: exponent_def)
   125 apply clarify
   126 apply (rule_tac k = 0 in GreatestI)
   127 prefer 2 apply (blast dest: prime_imp_one_less power_dvd_bound, simp)
   128 done
   129 
   130 lemma power_Suc_exponent_Not_dvd:
   131   "[|(p * p ^ exponent p s) dvd s;  prime p |] ==> s=0"
   132 apply (subgoal_tac "p ^ Suc (exponent p s) dvd s")
   133  prefer 2 apply simp 
   134 apply (rule ccontr)
   135 apply (drule exponent_ge, auto)
   136 done
   137 
   138 lemma exponent_power_eq [simp]: "prime p ==> exponent p (p^a) = a"
   139 apply (simp (no_asm_simp) add: exponent_def)
   140 apply (rule Greatest_equality, simp)
   141 apply (simp (no_asm_simp) add: prime_imp_one_less power_dvd_imp_le)
   142 done
   143 
   144 lemma exponent_equalityI:
   145   "!r::nat. (p^r dvd a) = (p^r dvd b) ==> exponent p a = exponent p b"
   146 by (simp (no_asm_simp) add: exponent_def)
   147 
   148 lemma exponent_eq_0 [simp]: "\<not> prime p ==> exponent p s = 0"
   149 by (simp (no_asm_simp) add: exponent_def)
   150 
   151 
   152 (* exponent_mult_add, easy inclusion.  Could weaken p \<in> prime to Suc 0 < p *)
   153 lemma exponent_mult_add1: "[| a > 0; b > 0 |]
   154   ==> (exponent p a) + (exponent p b) <= exponent p (a * b)"
   155 apply (case_tac "prime p")
   156 apply (rule exponent_ge)
   157 apply (auto simp add: power_add)
   158 apply (blast intro: prime_imp_one_less power_exponent_dvd mult_dvd_mono)
   159 done
   160 
   161 (* exponent_mult_add, opposite inclusion *)
   162 lemma exponent_mult_add2: "[| a > 0; b > 0 |]  
   163   ==> exponent p (a * b) <= (exponent p a) + (exponent p b)"
   164 apply (case_tac "prime p")
   165 apply (rule leI, clarify)
   166 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")
   168 apply (rule_tac [2] le_imp_power_dvd [THEN dvd_trans])
   169   prefer 3 apply assumption
   170  prefer 2 apply simp 
   171 apply (frule_tac a = "Suc (exponent p a) " and b = "Suc (exponent p b) " in prime_power_dvd_cases)
   172  apply (assumption, force, simp)
   173 apply (blast dest: power_Suc_exponent_Not_dvd)
   174 done
   175 
   176 lemma exponent_mult_add: "[| a > 0; b > 0 |]
   177    ==> exponent p (a * b) = (exponent p a) + (exponent p b)"
   178 by (blast intro: exponent_mult_add1 exponent_mult_add2 order_antisym)
   179 
   180 
   181 lemma not_divides_exponent_0: "~ (p dvd n) ==> exponent p n = 0"
   182 apply (case_tac "exponent p n", simp)
   183 apply (case_tac "n", simp)
   184 apply (cut_tac s = n and p = p in power_exponent_dvd)
   185 apply (auto dest: dvd_mult_left)
   186 done
   187 
   188 lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0"
   189 apply (case_tac "prime p")
   190 apply (auto simp add: prime_iff not_divides_exponent_0)
   191 done
   192 
   193 
   194 text{*Main Combinatorial Argument*}
   195 
   196 lemma le_extend_mult: "[| c > 0; a <= b |] ==> a <= b * (c::nat)"
   197 apply (rule_tac P = "%x. x <= b * c" in subst)
   198 apply (rule mult_1_right)
   199 apply (rule mult_le_mono, auto)
   200 done
   201 
   202 lemma p_fac_forw_lemma:
   203   "[| (m::nat) > 0; k > 0; k < p^a; (p^r) dvd (p^a)* m - k |] ==> r <= a"
   204 apply (rule notnotD)
   205 apply (rule notI)
   206 apply (drule contrapos_nn [OF _ leI, THEN notnotD], assumption)
   207 apply (drule less_imp_le [of a])
   208 apply (drule le_imp_power_dvd)
   209 apply (drule_tac b = "p ^ r" in dvd_trans, assumption)
   210 apply(metis dvd_diffD1 dvd_triv_right le_extend_mult linorder_linear linorder_not_less mult_commute nat_dvd_not_less neq0_conv)
   211 done
   212 
   213 lemma p_fac_forw: "[| (m::nat) > 0; k>0; k < p^a; (p^r) dvd (p^a)* m - k |]  
   214   ==> (p^r) dvd (p^a) - k"
   215 apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto)
   216 apply (subgoal_tac "p^r dvd p^a*m")
   217  prefer 2 apply (blast intro: dvd_mult2)
   218 apply (drule dvd_diffD1)
   219   apply assumption
   220  prefer 2 apply (blast intro: nat_dvd_diff)
   221 apply (drule gr0_implies_Suc, auto)
   222 done
   223 
   224 
   225 lemma r_le_a_forw:
   226   "[| (k::nat) > 0; k < p^a; p>0; (p^r) dvd (p^a) - k |] ==> r <= a"
   227 by (rule_tac m = "Suc 0" in p_fac_forw_lemma, auto)
   228 
   229 lemma p_fac_backw: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a;  (p^r) dvd p^a - k |]  
   230   ==> (p^r) dvd (p^a)*m - k"
   231 apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto)
   232 apply (subgoal_tac "p^r dvd p^a*m")
   233  prefer 2 apply (blast intro: dvd_mult2)
   234 apply (drule dvd_diffD1)
   235   apply assumption
   236  prefer 2 apply (blast intro: nat_dvd_diff)
   237 apply (drule less_imp_Suc_add, auto)
   238 done
   239 
   240 lemma exponent_p_a_m_k_equation: "[| m>0; k>0; (p::nat)\<noteq>0;  k < p^a |]  
   241   ==> exponent p (p^a * m - k) = exponent p (p^a - k)"
   242 apply (blast intro: exponent_equalityI p_fac_forw p_fac_backw)
   243 done
   244 
   245 text{*Suc rules that we have to delete from the simpset*}
   246 lemmas bad_Sucs = binomial_Suc_Suc mult_Suc mult_Suc_right
   247 
   248 (*The bound K is needed; otherwise it's too weak to be used.*)
   249 lemma p_not_div_choose_lemma [rule_format]:
   250   "[| \<forall>i. Suc i < K --> exponent p (Suc i) = exponent p (Suc(j+i))|]  
   251    ==> k<K --> exponent p ((j+k) choose k) = 0"
   252 apply (cases "prime p")
   253  prefer 2 apply simp 
   254 apply (induct k)
   255 apply (simp (no_asm))
   256 (*induction step*)
   257 apply (subgoal_tac "(Suc (j+k) choose Suc k) > 0")
   258  prefer 2 apply (simp add: zero_less_binomial_iff, clarify)
   259 apply (subgoal_tac "exponent p ((Suc (j+k) choose Suc k) * Suc k) = 
   260                     exponent p (Suc k)")
   261  txt{*First, use the assumed equation.  We simplify the LHS to
   262   @{term "exponent p (Suc (j + k) choose Suc k) + exponent p (Suc k)"}
   263   the common terms cancel, proving the conclusion.*}
   264  apply (simp del: bad_Sucs add: exponent_mult_add)
   265 txt{*Establishing the equation requires first applying 
   266    @{text Suc_times_binomial_eq} ...*}
   267 apply (simp del: bad_Sucs add: Suc_times_binomial_eq [symmetric])
   268 txt{*...then @{text exponent_mult_add} and the quantified premise.*}
   269 apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add)
   270 done
   271 
   272 (*The lemma above, with two changes of variables*)
   273 lemma p_not_div_choose:
   274   "[| k<K;  k<=n;
   275       \<forall>j. 0<j & j<K --> exponent p (n - k + (K - j)) = exponent p (K - j)|]
   276    ==> 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)
   278   prefer 3 apply simp
   279  prefer 2 apply assumption
   280 apply (drule_tac x = "K - Suc i" in spec)
   281 apply (simp add: Suc_diff_le)
   282 done
   283 
   284 
   285 lemma const_p_fac_right:
   286   "m>0 ==> exponent p ((p^a * m - Suc 0) choose (p^a - Suc 0)) = 0"
   287 apply (case_tac "prime p")
   288  prefer 2 apply simp 
   289 apply (frule_tac a = a in zero_less_prime_power)
   290 apply (rule_tac K = "p^a" in p_not_div_choose)
   291    apply simp
   292   apply simp
   293  apply (case_tac "m")
   294   apply (case_tac [2] "p^a")
   295    apply auto
   296 (*now the hard case, simplified to
   297     exponent p (Suc (p ^ a * m + i - p ^ a)) = exponent p (Suc i) *)
   298 apply (subgoal_tac "0<p")
   299  prefer 2 apply (force dest!: prime_imp_one_less)
   300 apply (subst exponent_p_a_m_k_equation, auto)
   301 done
   302 
   303 lemma const_p_fac:
   304   "m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m"
   305 apply (case_tac "prime p")
   306  prefer 2 apply simp 
   307 apply (subgoal_tac "0 < p^a * m & p^a <= p^a * m")
   308  prefer 2 apply (force simp add: prime_iff)
   309 txt{*A similar trick to the one used in @{text p_not_div_choose_lemma}:
   310   insert an equation; use @{text exponent_mult_add} on the LHS; on the RHS,
   311   first
   312   transform the binomial coefficient, then use @{text exponent_mult_add}.*}
   313 apply (subgoal_tac "exponent p ((( (p^a) * m) choose p^a) * p^a) = 
   314                     a + exponent p m")
   315  apply (simp del: bad_Sucs add: zero_less_binomial_iff exponent_mult_add prime_iff)
   316 txt{*one subgoal left!*}
   317 apply (subst times_binomial_minus1_eq, simp, simp)
   318 apply (subst exponent_mult_add, simp)
   319 apply (simp (no_asm_simp) add: zero_less_binomial_iff)
   320 apply arith
   321 apply (simp del: bad_Sucs add: exponent_mult_add const_p_fac_right)
   322 done
   323 
   324 
   325 end