author  eberlm <eberlm@in.tum.de> 
Thu, 04 May 2017 16:49:29 +0200  
changeset 65726  f5d64d094efe 
parent 65465  067210a08a22 
child 65899  ab7d8c999531 
permissions  rwrr 
41959  1 
(* Title: HOL/Number_Theory/Residues.thy 
31719  2 
Author: Jeremy Avigad 
3 

41541  4 
An algebraic treatment of residue rings, and resulting proofs of 
41959  5 
Euler's theorem and Wilson's theorem. 
31719  6 
*) 
7 

60526  8 
section \<open>Residue rings\<close> 
31719  9 

10 
theory Residues 

65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

11 
imports 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

12 
Cong 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

13 
"~~/src/HOL/Algebra/More_Group" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

14 
"~~/src/HOL/Algebra/More_Ring" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

15 
"~~/src/HOL/Algebra/More_Finite_Product" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

16 
"~~/src/HOL/Algebra/Multiplicative_Group" 
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

17 
Totient 
31719  18 
begin 
19 

64282
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

20 
definition QuadRes :: "int \<Rightarrow> int \<Rightarrow> bool" where 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

21 
"QuadRes p a = (\<exists>y. ([y^2 = a] (mod p)))" 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

22 

261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

23 
definition Legendre :: "int \<Rightarrow> int \<Rightarrow> int" where 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

24 
"Legendre a p = (if ([a = 0] (mod p)) then 0 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

25 
else if QuadRes p a then 1 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

26 
else 1)" 
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset

27 

60527  28 
subsection \<open>A locale for residue rings\<close> 
31719  29 

60527  30 
definition residue_ring :: "int \<Rightarrow> int ring" 
60528  31 
where 
60527  32 
"residue_ring m = 
33 
\<lparr>carrier = {0..m  1}, 

65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

34 
monoid.mult = \<lambda>x y. (x * y) mod m, 
60527  35 
one = 1, 
36 
zero = 0, 

37 
add = \<lambda>x y. (x + y) mod m\<rparr>" 

31719  38 

39 
locale residues = 

40 
fixes m :: int and R (structure) 

41 
assumes m_gt_one: "m > 1" 

60527  42 
defines "R \<equiv> residue_ring m" 
44872  43 
begin 
31719  44 

45 
lemma abelian_group: "abelian_group R" 

65066  46 
proof  
47 
have "\<exists>y\<in>{0..m  1}. (x + y) mod m = 0" if "0 \<le> x" "x < m" for x 

48 
proof (cases "x = 0") 

49 
case True 

50 
with m_gt_one show ?thesis by simp 

51 
next 

52 
case False 

53 
then have "(x + (m  x)) mod m = 0" 

54 
by simp 

55 
with m_gt_one that show ?thesis 

56 
by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le) 

57 
qed 

58 
with m_gt_one show ?thesis 

59 
by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps intro!: abelian_groupI) 

60 
qed 

31719  61 

62 
lemma comm_monoid: "comm_monoid R" 

65066  63 
unfolding R_def residue_ring_def 
31719  64 
apply (rule comm_monoidI) 
65066  65 
using m_gt_one apply auto 
66 
apply (metis mod_mult_right_eq mult.assoc mult.commute) 

67 
apply (metis mult.commute) 

41541  68 
done 
31719  69 

70 
lemma cring: "cring R" 

65066  71 
apply (intro cringI abelian_group comm_monoid) 
72 
unfolding R_def residue_ring_def 

73 
apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq) 

41541  74 
done 
31719  75 

76 
end 

77 

78 
sublocale residues < cring 

79 
by (rule cring) 

80 

81 

41541  82 
context residues 
83 
begin 

31719  84 

60527  85 
text \<open> 
86 
These lemmas translate back and forth between internal and 

87 
external concepts. 

88 
\<close> 

31719  89 

90 
lemma res_carrier_eq: "carrier R = {0..m  1}" 

44872  91 
unfolding R_def residue_ring_def by auto 
31719  92 

93 
lemma res_add_eq: "x \<oplus> y = (x + y) mod m" 

44872  94 
unfolding R_def residue_ring_def by auto 
31719  95 

96 
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" 

44872  97 
unfolding R_def residue_ring_def by auto 
31719  98 

99 
lemma res_zero_eq: "\<zero> = 0" 

44872  100 
unfolding R_def residue_ring_def by auto 
31719  101 

102 
lemma res_one_eq: "\<one> = 1" 

44872  103 
unfolding R_def residue_ring_def units_of_def by auto 
31719  104 

60527  105 
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}" 
65066  106 
using m_gt_one 
107 
unfolding Units_def R_def residue_ring_def 

31719  108 
apply auto 
60527  109 
apply (subgoal_tac "x \<noteq> 0") 
31719  110 
apply auto 
55352  111 
apply (metis invertible_coprime_int) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset

112 
apply (subst (asm) coprime_iff_invertible'_int) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset

113 
apply (auto simp add: cong_int_def mult.commute) 
41541  114 
done 
31719  115 

116 
lemma res_neg_eq: "\<ominus> x = ( x) mod m" 

65066  117 
using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def 
118 
apply simp 

31719  119 
apply (rule the_equality) 
65066  120 
apply (simp add: mod_add_right_eq) 
121 
apply (simp add: add.commute mod_add_right_eq) 

122 
apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial) 

41541  123 
done 
31719  124 

44872  125 
lemma finite [iff]: "finite (carrier R)" 
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

126 
by (simp add: res_carrier_eq) 
31719  127 

44872  128 
lemma finite_Units [iff]: "finite (Units R)" 
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

129 
by (simp add: finite_ring_finite_units) 
31719  130 

60527  131 
text \<open> 
63167  132 
The function \<open>a \<mapsto> a mod m\<close> maps the integers to the 
60527  133 
residue classes. The following lemmas show that this mapping 
134 
respects addition and multiplication on the integers. 

135 
\<close> 

31719  136 

60527  137 
lemma mod_in_carrier [iff]: "a mod m \<in> carrier R" 
138 
unfolding res_carrier_eq 

139 
using insert m_gt_one by auto 

31719  140 

141 
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" 

44872  142 
unfolding R_def residue_ring_def 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64282
diff
changeset

143 
by (auto simp add: mod_simps) 
31719  144 

145 
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" 

55352  146 
unfolding R_def residue_ring_def 
64593
50c715579715
reoriented congruence rules in nonexplosive direction
haftmann
parents:
64282
diff
changeset

147 
by (auto simp add: mod_simps) 
31719  148 

149 
lemma zero_cong: "\<zero> = 0" 

44872  150 
unfolding R_def residue_ring_def by auto 
31719  151 

152 
lemma one_cong: "\<one> = 1 mod m" 

44872  153 
using m_gt_one unfolding R_def residue_ring_def by auto 
31719  154 

60527  155 
(* FIXME revise algebra library to use 1? *) 
31719  156 
lemma pow_cong: "(x mod m) (^) n = x^n mod m" 
65066  157 
using m_gt_one 
31719  158 
apply (induct n) 
41541  159 
apply (auto simp add: nat_pow_def one_cong) 
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset

160 
apply (metis mult.commute mult_cong) 
41541  161 
done 
31719  162 

163 
lemma neg_cong: "\<ominus> (x mod m) = ( x) mod m" 

55352  164 
by (metis mod_minus_eq res_neg_eq) 
31719  165 

60528  166 
lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes>i\<in>A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m" 
55352  167 
by (induct set: finite) (auto simp: one_cong mult_cong) 
31719  168 

60528  169 
lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m" 
55352  170 
by (induct set: finite) (auto simp: zero_cong add_cong) 
31719  171 

60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

172 
lemma mod_in_res_units [simp]: 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

173 
assumes "1 < m" and "coprime a m" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

174 
shows "a mod m \<in> Units R" 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

175 
proof (cases "a mod m = 0") 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

176 
case True with assms show ?thesis 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

177 
by (auto simp add: res_units_eq gcd_red_int [symmetric]) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

178 
next 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

179 
case False 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

180 
from assms have "0 < m" by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

181 
with pos_mod_sign [of m a] have "0 \<le> a mod m" . 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

182 
with False have "0 < a mod m" by simp 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

183 
with assms show ?thesis 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

184 
by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps) 
01488b559910
avoid explicit definition of the relation of associated elements in a ring  prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset

185 
qed 
31719  186 

60528  187 
lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)" 
31719  188 
unfolding cong_int_def by auto 
189 

190 

60528  191 
text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close> 
31719  192 
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong 
193 
prod_cong sum_cong neg_cong res_eq_to_cong 

194 

60527  195 
text \<open>Other useful facts about the residue ring.\<close> 
31719  196 
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" 
197 
apply (simp add: res_one_eq res_neg_eq) 

57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset

198 
apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff 
60528  199 
zero_neq_one zmod_zminus1_eq_if) 
41541  200 
done 
31719  201 

202 
end 

203 

204 

60527  205 
subsection \<open>Prime residues\<close> 
31719  206 

207 
locale residues_prime = 

63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

208 
fixes p :: nat and R (structure) 
31719  209 
assumes p_prime [intro]: "prime p" 
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

210 
defines "R \<equiv> residue_ring (int p)" 
31719  211 

212 
sublocale residues_prime < residues p 

65066  213 
unfolding R_def residues_def 
31719  214 
using p_prime apply auto 
62348  215 
apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) 
41541  216 
done 
31719  217 

44872  218 
context residues_prime 
219 
begin 

31719  220 

221 
lemma is_field: "field R" 

65066  222 
proof  
223 
have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0" 

224 
by (metis dual_order.order_iff_strict gcd.commute less_le_not_le p_prime prime_imp_coprime prime_nat_int_transfer zdvd_imp_le) 

225 
then show ?thesis 

226 
apply (intro cring.field_intro2 cring) 

44872  227 
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) 
65066  228 
done 
229 
qed 

31719  230 

231 
lemma res_prime_units_eq: "Units R = {1..p  1}" 

232 
apply (subst res_units_eq) 

233 
apply auto 

62348  234 
apply (subst gcd.commute) 
55352  235 
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) 
41541  236 
done 
31719  237 

238 
end 

239 

240 
sublocale residues_prime < field 

241 
by (rule is_field) 

242 

243 

60527  244 
section \<open>Test cases: Euler's theorem and Wilson's theorem\<close> 
31719  245 

60527  246 
subsection \<open>Euler's theorem\<close> 
31719  247 

65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

248 
lemma (in residues) totient_eq: 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

249 
"totient (nat m) = card (Units R)" 
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

250 
thm R_def 
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

251 
proof  
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

252 
have *: "inj_on nat (Units R)" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

253 
by (rule inj_onI) (auto simp add: res_units_eq) 
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

254 
define m' where "m' = nat m" 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

255 
from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def) 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

256 
from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

257 
unfolding res_units_eq 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

258 
by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd) 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

259 
hence "Units R = int ` totatives m'" by blast 
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

260 
hence "totatives m' = nat ` Units R" by (simp add: image_image) 
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

261 
then have "card (totatives (nat m)) = card (nat ` Units R)" 
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

262 
by (simp add: m'_def) 
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

263 
also have "\<dots> = card (Units R)" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

264 
using * card_image [of nat "Units R"] by auto 
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

265 
finally show ?thesis by (simp add: totient_def) 
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

266 
qed 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

267 

65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

268 
lemma (in residues_prime) totient_eq: "totient p = p  1" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

269 
using totient_eq by (simp add: res_prime_units_eq) 
31719  270 

65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

271 
lemma (in residues) euler_theorem: 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

272 
assumes "coprime a m" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

273 
shows "[a ^ totient (nat m) = 1] (mod m)" 
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

274 
proof  
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

275 
have "a ^ totient (nat m) mod m = 1 mod m" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

276 
by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one) 
65066  277 
then show ?thesis 
278 
using res_eq_to_cong by blast 

31719  279 
qed 
280 

281 
lemma euler_theorem: 

65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

282 
fixes a m :: nat 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

283 
assumes "coprime a m" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

284 
shows "[a ^ totient m = 1] (mod m)" 
60527  285 
proof (cases "m = 0  m = 1") 
286 
case True 

44872  287 
then show ?thesis by auto 
31719  288 
next 
60527  289 
case False 
41541  290 
with assms show ?thesis 
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

291 
using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

292 
by (auto simp add: residues_def transfer_int_nat_gcd(1)) force 
31719  293 
qed 
294 

295 
lemma fermat_theorem: 

65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

296 
fixes p a :: nat 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

297 
assumes "prime p" and "\<not> p dvd a" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

298 
shows "[a ^ (p  1) = 1] (mod p)" 
31719  299 
proof  
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

300 
from assms prime_imp_coprime [of p a] have "coprime a p" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

301 
by (auto simp add: ac_simps) 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

302 
then have "[a ^ totient p = 1] (mod p)" 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

303 
by (rule euler_theorem) 
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

304 
also have "totient p = p  1" 
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset

305 
by (rule totient_prime) (rule assms) 
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset

306 
finally show ?thesis . 
31719  307 
qed 
308 

309 

60526  310 
subsection \<open>Wilson's theorem\<close> 
31719  311 

60527  312 
lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow> 
313 
{x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}" 

31719  314 
apply auto 
55352  315 
apply (metis Units_inv_inv)+ 
41541  316 
done 
31719  317 

318 
lemma (in residues_prime) wilson_theorem1: 

319 
assumes a: "p > 2" 

59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset

320 
shows "[fact (p  1) = (1::int)] (mod p)" 
31719  321 
proof  
60527  322 
let ?Inverse_Pairs = "{{x, inv x} x. x \<in> Units R  {\<one>, \<ominus> \<one>}}" 
323 
have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs" 

31719  324 
by auto 
60527  325 
have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)" 
31732  326 
apply (subst UR) 
31719  327 
apply (subst finprod_Un_disjoint) 
55352  328 
apply (auto intro: funcsetI) 
60527  329 
using inv_one apply auto[1] 
330 
using inv_eq_neg_one_eq apply auto 

31719  331 
done 
60527  332 
also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" 
31719  333 
apply (subst finprod_insert) 
334 
apply auto 

335 
apply (frule one_eq_neg_one) 

60527  336 
using a apply force 
31719  337 
done 
60527  338 
also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))" 
339 
apply (subst finprod_Union_disjoint) 

340 
apply auto 

55352  341 
apply (metis Units_inv_inv)+ 
31719  342 
done 
343 
also have "\<dots> = \<one>" 

60527  344 
apply (rule finprod_one) 
345 
apply auto 

346 
apply (subst finprod_insert) 

347 
apply auto 

55352  348 
apply (metis inv_eq_self) 
31719  349 
done 
60527  350 
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" 
31719  351 
by simp 
60527  352 
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" 
65066  353 
by (rule finprod_cong') (auto simp: res_units_eq) 
60527  354 
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" 
65066  355 
by (rule prod_cong) auto 
31719  356 
also have "\<dots> = fact (p  1) mod p" 
64272  357 
apply (simp add: fact_prod) 
65066  358 
using assms 
55242
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55227
diff
changeset

359 
apply (subst res_prime_units_eq) 
64272  360 
apply (simp add: int_prod zmod_int prod_int_eq) 
31719  361 
done 
60527  362 
finally have "fact (p  1) mod p = \<ominus> \<one>" . 
363 
then show ?thesis 

60528  364 
by (metis of_nat_fact Divides.transfer_int_nat_functions(2) 
365 
cong_int_def res_neg_eq res_one_eq) 

31719  366 
qed 
367 

55352  368 
lemma wilson_theorem: 
60527  369 
assumes "prime p" 
370 
shows "[fact (p  1) =  1] (mod p)" 

55352  371 
proof (cases "p = 2") 
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset

372 
case True 
55352  373 
then show ?thesis 
64272  374 
by (simp add: cong_int_def fact_prod) 
55352  375 
next 
376 
case False 

377 
then show ?thesis 

378 
using assms prime_ge_2_nat 

379 
by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) 

380 
qed 

31719  381 

65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

382 
text {* 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

383 
This result can be transferred to the multiplicative group of 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

384 
$\mathbb{Z}/p\mathbb{Z}$ for $p$ prime. *} 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

385 

f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

386 
lemma mod_nat_int_pow_eq: 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

387 
fixes n :: nat and p a :: int 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

388 
assumes "a \<ge> 0" "p \<ge> 0" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

389 
shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

390 
using assms 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

391 
by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric]) 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

392 

f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

393 
theorem residue_prime_mult_group_has_gen : 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

394 
fixes p :: nat 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

395 
assumes prime_p : "prime p" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

396 
shows "\<exists>a \<in> {1 .. p  1}. {1 .. p  1} = {a^i mod pi . i \<in> UNIV}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

397 
proof  
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

398 
have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

399 
interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

400 
by (simp add: prime_p) 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

401 
have car: "carrier (residue_ring (int p))  {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p  1}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

402 
by (auto simp add: R.zero_cong R.res_carrier_eq) 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

403 
obtain a where a:"a \<in> {1 .. int p  1}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

404 
and a_gen:"{1 .. int p  1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>ii::nat . i \<in> UNIV}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

405 
apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field] 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

406 
by (auto simp add: car[symmetric] carrier_mult_of) 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

407 
{ fix x fix i :: nat assume x: "x \<in> {1 .. int p  1}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

408 
hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto} 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

409 
note * = this 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

410 
have **:"nat ` {1 .. int p  1} = {1 .. p  1}" (is "?L = ?R") 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

411 
proof 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

412 
{ fix n assume n: "n \<in> ?L" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

413 
then have "n \<in> ?R" using `p\<ge>2` by force 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

414 
} thus "?L \<subseteq> ?R" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

415 
{ fix n assume n: "n \<in> ?R" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

416 
then have "n \<in> ?L" using `p\<ge>2` Set_Interval.transfer_nat_int_set_functions(2) by fastforce 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

417 
} thus "?R \<subseteq> ?L" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

418 
qed 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

419 
have "nat ` {a^i mod (int p)  i::nat. i \<in> UNIV} = {nat a^i mod p  i . i \<in> UNIV}" (is "?L = ?R") 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

420 
proof 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

421 
{ fix x assume x: "x \<in> ?L" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

422 
then obtain i where i:"x = nat (a^i mod (int p))" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

423 
hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

424 
hence "x \<in> ?R" using i by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

425 
} thus "?L \<subseteq> ?R" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

426 
{ fix x assume x: "x \<in> ?R" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

427 
then obtain i where i:"x = nat a^i mod p" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

428 
hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a `p\<ge>2` by auto 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

429 
} thus "?R \<subseteq> ?L" by blast 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

430 
qed 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

431 
hence "{1 .. p  1} = {nat a^i mod p  i. i \<in> UNIV}" 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

432 
using * a a_gen ** by presburger 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

433 
moreover 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

434 
have "nat a \<in> {1 .. p  1}" using a by force 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

435 
ultimately show ?thesis .. 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

436 
qed 
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset

437 

31719  438 
end 