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