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