author  wenzelm 
Mon, 22 May 2017 14:08:22 +0200  
changeset 65899  ab7d8c999531 
parent 65726  f5d64d094efe 
child 66304  cde6ceffcbc7 
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) 

65899  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)" 
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

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

252 
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

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

254 
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

255 
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

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

257 
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

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

259 
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

260 
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

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

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

263 
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

264 
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

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

266 

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

267 
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

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

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

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

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

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

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

274 
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

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

31719  278 
qed 
279 

280 
lemma euler_theorem: 

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

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

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

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

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

290 
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

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

294 
lemma fermat_theorem: 

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

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

296 
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

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

299 
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

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

301 
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

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

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

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

305 
finally show ?thesis . 
31719  306 
qed 
307 

308 

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

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

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

317 
lemma (in residues_prime) wilson_theorem1: 

318 
assumes a: "p > 2" 

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

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

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

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

334 
apply (frule one_eq_neg_one) 

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

339 
apply auto 

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

60527  343 
apply (rule finprod_one) 
344 
apply auto 

345 
apply (subst finprod_insert) 

346 
apply auto 

55352  347 
apply (metis inv_eq_self) 
31719  348 
done 
60527  349 
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" 
31719  350 
by simp 
60527  351 
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" 
65066  352 
by (rule finprod_cong') (auto simp: res_units_eq) 
60527  353 
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" 
65066  354 
by (rule prod_cong) auto 
31719  355 
also have "\<dots> = fact (p  1) mod p" 
64272  356 
apply (simp add: fact_prod) 
65066  357 
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

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

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

31719  365 
qed 
366 

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

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

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

376 
then show ?thesis 

377 
using assms prime_ge_2_nat 

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

379 
qed 

31719  380 

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

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

382 
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

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

384 

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

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

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

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

388 
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

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

390 
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

391 

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

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

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

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

395 
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

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

397 
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

398 
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

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

400 
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

401 
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

402 
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

403 
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

404 
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

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

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

407 
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

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

409 
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

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

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

412 
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

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

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

415 
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

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

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

418 
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

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

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

421 
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

422 
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

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

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

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

426 
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

427 
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

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

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

430 
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

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

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

433 
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

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

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

436 

31719  437 
end 