author  ballarin 
Tue, 16 Dec 2008 21:10:53 +0100  
changeset 29237  e90d9d51106b 
parent 27717  21bbd410ba04 
child 30011  cc264a9a033d 
child 30240  5b25fee0362c 
permissions  rwrr 
14706  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  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  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  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  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  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  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  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  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  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  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  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  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  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  194 
lemma le_extend_mult: "[ c > 0; a <= b ] ==> a <= b * (c::nat)" 
14889  195 
apply (rule_tac P = "%x. x <= b * c" in subst) 
196 
apply (rule mult_1_right) 

197 
apply (rule mult_le_mono, auto) 

198 
done 

199 

13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

200 
lemma p_fac_forw_lemma: 
25162  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 sideeffect 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  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  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  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  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  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 = "nk" 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  284 
"m>0 ==> exponent p ((p^a * m  Suc 0) choose (p^a  Suc 0)) = 0" 
16663  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  302 
"m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m" 
16663  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 