author  nipkow 
Fri, 13 Nov 2009 14:14:04 +0100  
changeset 33657  a4179bf442d1 
parent 32946  22664da2923b 
child 35848  5443079512ea 
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 
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

3 

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

4 
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

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

6 

27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
25162
diff
changeset

7 
theory Exponent 
32480  8 
imports Main "~~/src/HOL/Old_Number_Theory/Primes" Binomial 
27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
25162
diff
changeset

9 
begin 
20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

10 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

11 
section {*Sylow's Theorem*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

12 

21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

13 
subsection {*The Combinatorial Argument Underlying the First Sylow Theorem*} 
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

14 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

15 
definition exponent :: "nat => nat => nat" where 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

16 
"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

17 

20318
0e0ea63fe768
Restructured algebra library, added ideals and quotient rings.
ballarin
parents:
20282
diff
changeset

18 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

19 
text{*Prime Theorems*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

20 

16663  21 
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

22 
by (unfold prime_def, force) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

23 

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

24 
lemma prime_iff: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

25 
"(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

26 
apply (auto simp add: prime_imp_one_less) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

27 
apply (blast dest!: prime_dvd_mult) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

28 
apply (auto simp add: prime_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

29 
apply (erule dvdE) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

30 
apply (case_tac "k=0", simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

31 
apply (drule_tac x = m in spec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

32 
apply (drule_tac x = k in spec) 
16733
236dfafbeb63
linear arithmetic now takes "&" in assumptions apart.
nipkow
parents:
16663
diff
changeset

33 
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

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

35 

16663  36 
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

37 
by (force simp add: prime_iff) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

38 

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 
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

41 
by (rule ccontr, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

42 

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 
lemma prime_dvd_cases: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

45 
"[ p*k dvd m*n; prime p ] 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

46 
==> (\<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

47 
apply (simp add: prime_iff) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

48 
apply (frule dvd_mult_left) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

49 
apply (subgoal_tac "p dvd m  p dvd n") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

50 
prefer 2 apply blast 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

51 
apply (erule disjE) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

52 
apply (rule disjI1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

53 
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

54 
apply (auto elim!: dvdE) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

56 

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

57 

16663  58 
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

59 
==> \<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

60 
(\<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

61 
apply (induct c) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

63 
apply (case_tac "a") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

64 
apply simp 
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 
(*inductive step*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

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

69 
apply (erule prime_dvd_cases [THEN disjE], assumption, auto) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

70 
(*case 1: p dvd m*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

71 
apply (case_tac "a") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

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

74 
apply (drule spec, drule spec, erule (1) notE impE) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

75 
apply (drule_tac x = nat in spec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

76 
apply (drule_tac x = b in spec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

78 
(*case 2: p dvd n*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

79 
apply (case_tac "b") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

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

82 
apply (drule spec, drule spec, erule (1) notE impE) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

83 
apply (drule_tac x = a in spec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

84 
apply (drule_tac x = nat in spec, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

86 

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

87 
(*needed in this form in Sylow.ML*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

88 
lemma div_combine: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

89 
"[ 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

90 
==> p ^ a dvd k" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

91 
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

92 

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

93 
(*Lemma for power_dvd_bound*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

94 
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

95 
apply (induct n) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

96 
apply (simp (no_asm_simp)) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

98 
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

99 
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

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

101 
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

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

103 

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

104 
(*An upper bound for the n such that p^n dvd a: needed for GREATEST to exist*) 
25162  105 
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

106 
apply (drule dvd_imp_le) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

107 
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

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

109 

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

110 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

111 
text{*Exponent Theorems*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

112 

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

113 
lemma exponent_ge [rule_format]: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

114 
"[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

115 
apply (simp add: exponent_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

116 
apply (erule Greatest_le) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

117 
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

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

119 

25162  120 
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

121 
apply (simp add: exponent_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

123 
apply (rule_tac k = 0 in GreatestI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

124 
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

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

126 

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

127 
lemma power_Suc_exponent_Not_dvd: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

128 
"[(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

129 
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

130 
prefer 2 apply simp 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

131 
apply (rule ccontr) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

132 
apply (drule exponent_ge, auto) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

134 

16663  135 
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

136 
apply (simp (no_asm_simp) add: exponent_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

137 
apply (rule Greatest_equality, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

138 
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

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

140 

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

141 
lemma exponent_equalityI: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

142 
"!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

143 
by (simp (no_asm_simp) add: exponent_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

144 

16663  145 
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

146 
by (simp (no_asm_simp) add: exponent_def) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

147 

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 
(* exponent_mult_add, easy inclusion. Could weaken p \<in> prime to Suc 0 < p *) 
25162  150 
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

151 
==> (exponent p a) + (exponent p b) <= exponent p (a * b)" 
16663  152 
apply (case_tac "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

153 
apply (rule exponent_ge) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

154 
apply (auto simp add: power_add) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

155 
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

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

157 

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

158 
(* exponent_mult_add, opposite inclusion *) 
25162  159 
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

160 
==> exponent p (a * b) <= (exponent p a) + (exponent p b)" 
16663  161 
apply (case_tac "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

162 
apply (rule leI, clarify) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

163 
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

164 
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

165 
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

166 
prefer 3 apply assumption 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

167 
prefer 2 apply simp 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

168 
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

169 
apply (assumption, force, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

170 
apply (blast dest: power_Suc_exponent_Not_dvd) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

172 

25162  173 
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

174 
==> 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

175 
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

176 

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 
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

179 
apply (case_tac "exponent p n", simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

180 
apply (case_tac "n", simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

181 
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

182 
apply (auto dest: dvd_mult_left) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

184 

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

185 
lemma exponent_1_eq_0 [simp]: "exponent p (Suc 0) = 0" 
16663  186 
apply (case_tac "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

187 
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

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

189 

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

190 

27717
21bbd410ba04
Generalised polynomial lemmas from cring to ring.
ballarin
parents:
27651
diff
changeset

191 
text{*Main Combinatorial Argument*} 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

192 

25162  193 
lemma le_extend_mult: "[ c > 0; a <= b ] ==> a <= b * (c::nat)" 
14889  194 
apply (rule_tac P = "%x. x <= b * c" in subst) 
195 
apply (rule mult_1_right) 

196 
apply (rule mult_le_mono, auto) 

197 
done 

198 

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

199 
lemma p_fac_forw_lemma: 
25162  200 
"[ (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

201 
apply (rule notnotD) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

202 
apply (rule notI) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

203 
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

204 
apply (drule less_imp_le [of a]) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

205 
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

206 
apply (drule_tac b = "p ^ r" in dvd_trans, assumption) 
32946  207 
apply (metis diff_is_0_eq dvd_diffD1 gcd_dvd2 gcd_mult' gr0I le_extend_mult less_diff_conv nat_dvd_not_less nat_mult_commute not_add_less2 xt1(10)) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

209 

25162  210 
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

211 
==> (p^r) dvd (p^a)  k" 
30011
cc264a9a033d
consider changes variable names in theorem le_imp_power_dvd
haftmann
parents:
27717
diff
changeset

212 
apply (frule p_fac_forw_lemma [THEN le_imp_power_dvd, of _ k p], auto) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

213 
apply (subgoal_tac "p^r dvd p^a*m") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

214 
prefer 2 apply (blast intro: dvd_mult2) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

215 
apply (drule dvd_diffD1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

216 
apply assumption 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31717
diff
changeset

217 
prefer 2 apply (blast intro: dvd_diff_nat) 
25162  218 
apply (drule gr0_implies_Suc, auto) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

220 

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

221 

25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

222 
lemma r_le_a_forw: 
25162  223 
"[ (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

224 
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

225 

25162  226 
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

227 
==> (p^r) dvd (p^a)*m  k" 
30011
cc264a9a033d
consider changes variable names in theorem le_imp_power_dvd
haftmann
parents:
27717
diff
changeset

228 
apply (frule_tac k1 = k and p1 = p in r_le_a_forw [THEN le_imp_power_dvd], auto) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

229 
apply (subgoal_tac "p^r dvd p^a*m") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

230 
prefer 2 apply (blast intro: dvd_mult2) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

231 
apply (drule dvd_diffD1) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

232 
apply assumption 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31717
diff
changeset

233 
prefer 2 apply (blast intro: dvd_diff_nat) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

234 
apply (drule less_imp_Suc_add, auto) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

236 

25162  237 
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

238 
==> 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

239 
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

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

241 

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

242 
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

243 
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

244 

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

245 
(*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

246 
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

247 
"[ \<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

248 
==> 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

249 
apply (cases "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

250 
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

251 
apply (induct k) 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

252 
apply (simp (no_asm)) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

253 
(*induction step*) 
27105
5f139027c365
slightly tuning of some proofs involving case distinction and induction on natural numbers and similar
haftmann
parents:
25162
diff
changeset

254 
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

255 
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

256 
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

257 
exponent p (Suc k)") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

258 
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

259 
@{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

260 
the common terms cancel, proving the conclusion.*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

261 
apply (simp del: bad_Sucs add: exponent_mult_add) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

262 
txt{*Establishing the equation requires first applying 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

263 
@{text Suc_times_binomial_eq} ...*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

264 
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

265 
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

266 
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

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

268 

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

269 
(*The lemma above, with two changes of variables*) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

270 
lemma p_not_div_choose: 
25134
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

271 
"[ k<K; k<=n; 
3d4953e88449
Eliminated most of the neq0_conv occurrences. As a result, many
nipkow
parents:
24742
diff
changeset

272 
\<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

273 
==> exponent p (n choose k) = 0" 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

274 
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

275 
prefer 3 apply simp 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

276 
prefer 2 apply assumption 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

277 
apply (drule_tac x = "K  Suc i" in spec) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

278 
apply (simp add: Suc_diff_le) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

280 

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 
lemma const_p_fac_right: 
25162  283 
"m>0 ==> exponent p ((p^a * m  Suc 0) choose (p^a  Suc 0)) = 0" 
16663  284 
apply (case_tac "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

285 
prefer 2 apply simp 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

286 
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

287 
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

288 
apply simp 
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 (case_tac "m") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

291 
apply (case_tac [2] "p^a") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

293 
(*now the hard case, simplified to 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

294 
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

295 
apply (subgoal_tac "0<p") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

296 
prefer 2 apply (force dest!: prime_imp_one_less) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

297 
apply (subst exponent_p_a_m_k_equation, auto) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

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

299 

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

300 
lemma const_p_fac: 
25162  301 
"m>0 ==> exponent p (((p^a) * m) choose p^a) = exponent p m" 
16663  302 
apply (case_tac "prime p") 
13870
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

303 
prefer 2 apply simp 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

304 
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

305 
prefer 2 apply (force simp add: prime_iff) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

306 
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

307 
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

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

309 
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

310 
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

311 
a + exponent p m") 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

312 
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

313 
txt{*one subgoal left!*} 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

314 
apply (subst times_binomial_minus1_eq, simp, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

315 
apply (subst exponent_mult_add, simp) 
cf947d1ec5ff
moved Exponent, Coset, Sylow from GroupTheory to Algebra, converting them
paulson
parents:
diff
changeset

316 
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

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

318 
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

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

320 

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 
end 