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