author  haftmann 
Sun, 09 Nov 2014 10:03:18 +0100  
changeset 58954  18750e86d5b8 
parent 58889  5b7a9633cfa8 
child 59667  651ea265d568 
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 

58889  8 
section {* Residue rings *} 
31719  9 

10 
theory Residues 

11 
imports 

41541  12 
UniqueFactorization 
13 
Binomial 

14 
MiscAlgebra 

31719  15 
begin 
16 

17 
(* 

44872  18 

31719  19 
A locale for residue rings 
20 

21 
*) 

22 

35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32479
diff
changeset

23 
definition residue_ring :: "int => int ring" where 
44872  24 
"residue_ring m == ( 
25 
carrier = {0..m  1}, 

31719  26 
mult = (%x y. (x * y) mod m), 
27 
one = 1, 

28 
zero = 0, 

29 
add = (%x y. (x + y) mod m) )" 

30 

31 
locale residues = 

32 
fixes m :: int and R (structure) 

33 
assumes m_gt_one: "m > 1" 

34 
defines "R == residue_ring m" 

35 

44872  36 
context residues 
37 
begin 

31719  38 

39 
lemma abelian_group: "abelian_group R" 

40 
apply (insert m_gt_one) 

41 
apply (rule abelian_groupI) 

42 
apply (unfold R_def residue_ring_def) 

57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

43 
apply (auto simp add: mod_add_right_eq [symmetric] ac_simps) 
31719  44 
apply (case_tac "x = 0") 
45 
apply force 

46 
apply (subgoal_tac "(x + (m  x)) mod m = 0") 

47 
apply (erule bexI) 

48 
apply auto 

41541  49 
done 
31719  50 

51 
lemma comm_monoid: "comm_monoid R" 

52 
apply (insert m_gt_one) 

53 
apply (unfold R_def residue_ring_def) 

54 
apply (rule comm_monoidI) 

55 
apply auto 

56 
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") 

57 
apply (erule ssubst) 

47163  58 
apply (subst mod_mult_right_eq [symmetric])+ 
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset

59 
apply (simp_all only: ac_simps) 
41541  60 
done 
31719  61 

62 
lemma cring: "cring R" 

63 
apply (rule cringI) 

64 
apply (rule abelian_group) 

65 
apply (rule comm_monoid) 

66 
apply (unfold R_def residue_ring_def, auto) 

67 
apply (subst mod_add_eq [symmetric]) 

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

68 
apply (subst mult.commute) 
47163  69 
apply (subst mod_mult_right_eq [symmetric]) 
36350  70 
apply (simp add: field_simps) 
41541  71 
done 
31719  72 

73 
end 

74 

75 
sublocale residues < cring 

76 
by (rule cring) 

77 

78 

41541  79 
context residues 
80 
begin 

31719  81 

44872  82 
(* These lemmas translate back and forth between internal and 
31719  83 
external concepts *) 
84 

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

44872  86 
unfolding R_def residue_ring_def by auto 
31719  87 

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

44872  89 
unfolding R_def residue_ring_def by auto 
31719  90 

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

44872  92 
unfolding R_def residue_ring_def by auto 
31719  93 

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

44872  95 
unfolding R_def residue_ring_def by auto 
31719  96 

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

44872  98 
unfolding R_def residue_ring_def units_of_def by auto 
31719  99 

100 
lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}" 

101 
apply (insert m_gt_one) 

102 
apply (unfold Units_def R_def residue_ring_def) 

103 
apply auto 

104 
apply (subgoal_tac "x ~= 0") 

105 
apply auto 

55352  106 
apply (metis invertible_coprime_int) 
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset

107 
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

108 
apply (auto simp add: cong_int_def mult.commute) 
41541  109 
done 
31719  110 

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

112 
apply (insert m_gt_one) 

113 
apply (unfold R_def a_inv_def m_inv_def residue_ring_def) 

114 
apply auto 

115 
apply (rule the_equality) 

116 
apply auto 

117 
apply (subst mod_add_right_eq [symmetric]) 

118 
apply auto 

119 
apply (subst mod_add_left_eq [symmetric]) 

120 
apply auto 

121 
apply (subgoal_tac "y mod m =  x mod m") 

122 
apply simp 

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

123 
apply (metis minus_add_cancel mod_mult_self1 mult.commute) 
41541  124 
done 
31719  125 

44872  126 
lemma finite [iff]: "finite (carrier R)" 
31719  127 
by (subst res_carrier_eq, auto) 
128 

44872  129 
lemma finite_Units [iff]: "finite (Units R)" 
50027
7747a9f4c358
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
bulwahn
parents:
47163
diff
changeset

130 
by (subst res_units_eq) auto 
31719  131 

44872  132 
(* The function a > a mod m maps the integers to the 
133 
residue classes. The following lemmas show that this mapping 

31719  134 
respects addition and multiplication on the integers. *) 
135 

136 
lemma mod_in_carrier [iff]: "a mod m : carrier R" 

137 
apply (unfold res_carrier_eq) 

138 
apply (insert m_gt_one, auto) 

41541  139 
done 
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 
143 
apply auto 

144 
apply presburger 

145 
done 

31719  146 

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

55352  148 
unfolding R_def residue_ring_def 
149 
by auto (metis mod_mult_eq) 

31719  150 

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

44872  152 
unfolding R_def residue_ring_def by auto 
31719  153 

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

44872  155 
using m_gt_one unfolding R_def residue_ring_def by auto 
31719  156 

157 
(* revise algebra library to use 1? *) 

158 
lemma pow_cong: "(x mod m) (^) n = x^n mod m" 

159 
apply (insert m_gt_one) 

160 
apply (induct n) 

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

162 
apply (metis mult.commute mult_cong) 
41541  163 
done 
31719  164 

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

55352  166 
by (metis mod_minus_eq res_neg_eq) 
31719  167 

44872  168 
lemma (in residues) prod_cong: 
169 
"finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m" 

55352  170 
by (induct set: finite) (auto simp: one_cong mult_cong) 
31719  171 

172 
lemma (in residues) sum_cong: 

44872  173 
"finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m" 
55352  174 
by (induct set: finite) (auto simp: zero_cong add_cong) 
31719  175 

44872  176 
lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> 
31719  177 
a mod m : Units R" 
178 
apply (subst res_units_eq, auto) 

179 
apply (insert pos_mod_sign [of m a]) 

180 
apply (subgoal_tac "a mod m ~= 0") 

181 
apply arith 

182 
apply auto 

55352  183 
apply (metis gcd_int.commute gcd_red_int) 
41541  184 
done 
31719  185 

44872  186 
lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" 
31719  187 
unfolding cong_int_def by auto 
188 

44872  189 
(* Simplifying with these will translate a ring equation in R to a 
31719  190 
congruence. *) 
191 

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 

195 
(* Other useful facts about the residue ring *) 

196 

197 
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" 

198 
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

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

203 
end 

204 

205 

206 
(* prime residues *) 

207 

208 
locale residues_prime = 

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

209 
fixes p and R (structure) 
31719  210 
assumes p_prime [intro]: "prime p" 
211 
defines "R == residue_ring p" 

212 

213 
sublocale residues_prime < residues p 

214 
apply (unfold R_def residues_def) 

215 
using p_prime apply auto 

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

216 
apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat) 
41541  217 
done 
31719  218 

44872  219 
context residues_prime 
220 
begin 

31719  221 

222 
lemma is_field: "field R" 

223 
apply (rule cring.field_intro2) 

224 
apply (rule cring) 

44872  225 
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) 
31719  226 
apply (rule classical) 
227 
apply (erule notE) 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset

228 
apply (subst gcd_commute_int) 
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset

229 
apply (rule prime_imp_coprime_int) 
31719  230 
apply (rule p_prime) 
231 
apply (rule notI) 

232 
apply (frule zdvd_imp_le) 

233 
apply auto 

41541  234 
done 
31719  235 

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

237 
apply (subst res_units_eq) 

238 
apply auto 

31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz > xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset

239 
apply (subst gcd_commute_int) 
55352  240 
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) 
41541  241 
done 
31719  242 

243 
end 

244 

245 
sublocale residues_prime < field 

246 
by (rule is_field) 

247 

248 

249 
(* 

250 
Test cases: Euler's theorem and Wilson's theorem. 

251 
*) 

252 

253 

254 
subsection{* Euler's theorem *} 

255 

256 
(* the definition of the phi function *) 

257 

44872  258 
definition phi :: "int => nat" 
259 
where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})" 

31719  260 

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

261 
lemma phi_def_nat: "phi m = card({ x. 0 < x & x < nat m & gcd x (nat m) = 1})" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

262 
apply (simp add: phi_def) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

263 
apply (rule bij_betw_same_card [of nat]) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

264 
apply (auto simp add: inj_on_def bij_betw_def image_def) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

265 
apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

266 
apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int transfer_int_nat_gcd(1) zless_int) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

268 

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

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

270 
assumes "2 \<le> p" "phi p = p  1" shows "prime p" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

272 
have "{x. 0 < x \<and> x < p \<and> coprime x p} = {1..p  1}" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

273 
using assms unfolding phi_def_nat 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

274 
by (intro card_seteq) fastforce+ 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

275 
then have cop: "\<And>x. x \<in> {1::nat..p  1} \<Longrightarrow> coprime x p" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

277 
{ fix x::nat assume *: "1 < x" "x < p" and "x dvd p" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

278 
have "coprime x p" 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

279 
apply (rule cop) 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

280 
using * apply auto 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

282 
with `x dvd p` `1 < x` have "False" by auto } 
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

283 
then show ?thesis 
55262  284 
using `2 \<le> p` 
285 
by (simp add: prime_def) 

55352  286 
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
287 
not_numeral_le_zero one_dvd) 

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

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

289 

31719  290 
lemma phi_zero [simp]: "phi 0 = 0" 
291 
apply (subst phi_def) 

44872  292 
(* Auto hangs here. Once again, where is the simplification rule 
31719  293 
1 == Suc 0 coming from? *) 
294 
apply (auto simp add: card_eq_0_iff) 

295 
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) 

41541  296 
done 
31719  297 

298 
lemma phi_one [simp]: "phi 1 = 0" 

44872  299 
by (auto simp add: phi_def card_eq_0_iff) 
31719  300 

301 
lemma (in residues) phi_eq: "phi m = card(Units R)" 

302 
by (simp add: phi_def res_units_eq) 

303 

44872  304 
lemma (in residues) euler_theorem1: 
31719  305 
assumes a: "gcd a m = 1" 
306 
shows "[a^phi m = 1] (mod m)" 

307 
proof  

308 
from a m_gt_one have [simp]: "a mod m : Units R" 

309 
by (intro mod_in_res_units) 

310 
from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" 

311 
by simp 

44872  312 
also have "\<dots> = \<one>" 
31719  313 
by (intro units_power_order_eq_one, auto) 
314 
finally show ?thesis 

315 
by (simp add: res_to_cong_simps) 

316 
qed 

317 

318 
(* In fact, there is a two line proof! 

319 

44872  320 
lemma (in residues) euler_theorem1: 
31719  321 
assumes a: "gcd a m = 1" 
322 
shows "[a^phi m = 1] (mod m)" 

323 
proof  

324 
have "(a mod m) (^) (phi m) = \<one>" 

325 
by (simp add: phi_eq units_power_order_eq_one a m_gt_one) 

44872  326 
then show ?thesis 
31719  327 
by (simp add: res_to_cong_simps) 
328 
qed 

329 

330 
*) 

331 

332 
(* outside the locale, we can relax the restriction m > 1 *) 

333 

334 
lemma euler_theorem: 

335 
assumes "m >= 0" and "gcd a m = 1" 

336 
shows "[a^phi m = 1] (mod m)" 

337 
proof (cases) 

338 
assume "m = 0  m = 1" 

44872  339 
then show ?thesis by auto 
31719  340 
next 
341 
assume "~(m = 0  m = 1)" 

41541  342 
with assms show ?thesis 
31719  343 
by (intro residues.euler_theorem1, unfold residues_def, auto) 
344 
qed 

345 

346 
lemma (in residues_prime) phi_prime: "phi p = (nat p  1)" 

347 
apply (subst phi_eq) 

348 
apply (subst res_prime_units_eq) 

349 
apply auto 

41541  350 
done 
31719  351 

352 
lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p  1)" 

353 
apply (rule residues_prime.phi_prime) 

354 
apply (erule residues_prime.intro) 

41541  355 
done 
31719  356 

357 
lemma fermat_theorem: 

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 
fixes a::int 
31719  359 
assumes "prime p" and "~ (p dvd a)" 
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

360 
shows "[a^(p  1) = 1] (mod p)" 
31719  361 
proof  
41541  362 
from assms have "[a^phi p = 1] (mod p)" 
31719  363 
apply (intro euler_theorem) 
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

364 
apply (metis of_nat_0_le_iff) 
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

365 
apply (metis gcd_int.commute prime_imp_coprime_int) 
31719  366 
done 
367 
also have "phi p = nat p  1" 

41541  368 
by (rule phi_prime, rule 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

369 
finally show ?thesis 
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

370 
by (metis nat_int) 
31719  371 
qed 
372 

55227
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset

373 
lemma fermat_theorem_nat: 
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset

374 
assumes "prime p" and "~ (p dvd a)" 
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset

375 
shows "[a^(p  1) = 1] (mod p)" 
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset

376 
using fermat_theorem [of p a] 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

377 
by (metis int_1 of_nat_power transfer_int_nat_cong zdvd_int) 
55227
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset

378 

31719  379 

380 
subsection {* Wilson's theorem *} 

381 

44872  382 
lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> 
383 
{x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" 

31719  384 
apply auto 
55352  385 
apply (metis Units_inv_inv)+ 
41541  386 
done 
31719  387 

388 
lemma (in residues_prime) wilson_theorem1: 

389 
assumes a: "p > 2" 

390 
shows "[fact (p  1) =  1] (mod p)" 

391 
proof  

44872  392 
let ?InversePairs = "{ {x, inv x}  x. x : Units R  {\<one>, \<ominus> \<one>}}" 
31732  393 
have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)" 
31719  394 
by auto 
44872  395 
have "(\<Otimes>i: Units R. i) = 
31719  396 
(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)" 
31732  397 
apply (subst UR) 
31719  398 
apply (subst finprod_Un_disjoint) 
55352  399 
apply (auto intro: funcsetI) 
400 
apply (metis Units_inv_inv inv_one inv_neg_one)+ 

31719  401 
done 
402 
also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" 

403 
apply (subst finprod_insert) 

404 
apply auto 

405 
apply (frule one_eq_neg_one) 

406 
apply (insert a, force) 

407 
done 

44872  408 
also have "(\<Otimes>i:(Union ?InversePairs). i) = 
41541  409 
(\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))" 
55352  410 
apply (subst finprod_Union_disjoint, auto) 
411 
apply (metis Units_inv_inv)+ 

31719  412 
done 
413 
also have "\<dots> = \<one>" 

55352  414 
apply (rule finprod_one, auto) 
415 
apply (subst finprod_insert, auto) 

416 
apply (metis inv_eq_self) 

31719  417 
done 
418 
finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>" 

419 
by simp 

420 
also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)" 

421 
apply (rule finprod_cong') 

31732  422 
apply (auto) 
31719  423 
apply (subst (asm) res_prime_units_eq) 
424 
apply auto 

425 
done 

426 
also have "\<dots> = (PROD i: Units R. i) mod p" 

427 
apply (rule prod_cong) 

428 
apply auto 

429 
done 

430 
also have "\<dots> = fact (p  1) mod p" 

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

431 
apply (subst fact_altdef_nat) 
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

432 
apply (insert assms) 
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

433 
apply (subst res_prime_units_eq) 
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

434 
apply (simp add: int_setprod zmod_int setprod_int_eq) 
31719  435 
done 
436 
finally have "fact (p  1) mod p = \<ominus> \<one>". 

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

437 
then show ?thesis 
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

438 
by (metis Divides.transfer_int_nat_functions(2) cong_int_def res_neg_eq res_one_eq) 
31719  439 
qed 
440 

55352  441 
lemma wilson_theorem: 
442 
assumes "prime p" shows "[fact (p  1) =  1] (mod p)" 

443 
proof (cases "p = 2") 

444 
case True 

445 
then show ?thesis 

446 
by (simp add: cong_int_def fact_altdef_nat) 

447 
next 

448 
case False 

449 
then show ?thesis 

450 
using assms prime_ge_2_nat 

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

452 
qed 

31719  453 

454 
end 