author  wenzelm 
Fri, 19 Jun 2015 23:40:46 +0200  
changeset 60527  eb431a5651fe 
parent 60526  fad653acf58f 
child 60528  190b4a7d8b87 
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 

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

11 
imports UniqueFactorization MiscAlgebra 
31719  12 
begin 
13 

60527  14 
subsection \<open>A locale for residue rings\<close> 
31719  15 

60527  16 
definition residue_ring :: "int \<Rightarrow> int ring" 
17 
where 

18 
"residue_ring m = 

19 
\<lparr>carrier = {0..m  1}, 

20 
mult = \<lambda>x y. (x * y) mod m, 

21 
one = 1, 

22 
zero = 0, 

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

31719  24 

25 
locale residues = 

26 
fixes m :: int and R (structure) 

27 
assumes m_gt_one: "m > 1" 

60527  28 
defines "R \<equiv> residue_ring m" 
44872  29 
begin 
31719  30 

31 
lemma abelian_group: "abelian_group R" 

32 
apply (insert m_gt_one) 

33 
apply (rule abelian_groupI) 

34 
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

35 
apply (auto simp add: mod_add_right_eq [symmetric] ac_simps) 
31719  36 
apply (case_tac "x = 0") 
37 
apply force 

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

39 
apply (erule bexI) 

40 
apply auto 

41541  41 
done 
31719  42 

43 
lemma comm_monoid: "comm_monoid R" 

44 
apply (insert m_gt_one) 

45 
apply (unfold R_def residue_ring_def) 

46 
apply (rule comm_monoidI) 

47 
apply auto 

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

49 
apply (erule ssubst) 

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

51 
apply (simp_all only: ac_simps) 
41541  52 
done 
31719  53 

54 
lemma cring: "cring R" 

55 
apply (rule cringI) 

56 
apply (rule abelian_group) 

57 
apply (rule comm_monoid) 

58 
apply (unfold R_def residue_ring_def, auto) 

59 
apply (subst mod_add_eq [symmetric]) 

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

60 
apply (subst mult.commute) 
47163  61 
apply (subst mod_mult_right_eq [symmetric]) 
36350  62 
apply (simp add: field_simps) 
41541  63 
done 
31719  64 

65 
end 

66 

67 
sublocale residues < cring 

68 
by (rule cring) 

69 

70 

41541  71 
context residues 
72 
begin 

31719  73 

60527  74 
text \<open> 
75 
These lemmas translate back and forth between internal and 

76 
external concepts. 

77 
\<close> 

31719  78 

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

44872  80 
unfolding R_def residue_ring_def by auto 
31719  81 

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

44872  83 
unfolding R_def residue_ring_def by auto 
31719  84 

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

44872  86 
unfolding R_def residue_ring_def by auto 
31719  87 

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

44872  89 
unfolding R_def residue_ring_def by auto 
31719  90 

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

44872  92 
unfolding R_def residue_ring_def units_of_def by auto 
31719  93 

60527  94 
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}" 
31719  95 
apply (insert m_gt_one) 
96 
apply (unfold Units_def R_def residue_ring_def) 

97 
apply auto 

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

101 
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

102 
apply (auto simp add: cong_int_def mult.commute) 
41541  103 
done 
31719  104 

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

106 
apply (insert m_gt_one) 

107 
apply (unfold R_def a_inv_def m_inv_def residue_ring_def) 

108 
apply auto 

109 
apply (rule the_equality) 

110 
apply auto 

111 
apply (subst mod_add_right_eq [symmetric]) 

112 
apply auto 

113 
apply (subst mod_add_left_eq [symmetric]) 

114 
apply auto 

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

116 
apply simp 

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

117 
apply (metis minus_add_cancel mod_mult_self1 mult.commute) 
41541  118 
done 
31719  119 

44872  120 
lemma finite [iff]: "finite (carrier R)" 
60527  121 
by (subst res_carrier_eq) auto 
31719  122 

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

124 
by (subst res_units_eq) auto 
31719  125 

60527  126 
text \<open> 
127 
The function @{text "a \<mapsto> a mod m"} maps the integers to the 

128 
residue classes. The following lemmas show that this mapping 

129 
respects addition and multiplication on the integers. 

130 
\<close> 

31719  131 

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

134 
using insert m_gt_one by auto 

31719  135 

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

44872  137 
unfolding R_def residue_ring_def 
138 
apply auto 

139 
apply presburger 

140 
done 

31719  141 

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

55352  143 
unfolding R_def residue_ring_def 
144 
by auto (metis mod_mult_eq) 

31719  145 

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

44872  147 
unfolding R_def residue_ring_def by auto 
31719  148 

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

44872  150 
using m_gt_one unfolding R_def residue_ring_def by auto 
31719  151 

60527  152 
(* FIXME revise algebra library to use 1? *) 
31719  153 
lemma pow_cong: "(x mod m) (^) n = x^n mod m" 
154 
apply (insert m_gt_one) 

155 
apply (induct n) 

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

157 
apply (metis mult.commute mult_cong) 
41541  158 
done 
31719  159 

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

55352  161 
by (metis mod_minus_eq res_neg_eq) 
31719  162 

60527  163 
lemma (in residues) prod_cong: "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (\<Prod>i\<in>A. f i) mod m" 
55352  164 
by (induct set: finite) (auto simp: one_cong mult_cong) 
31719  165 

60527  166 
lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m" 
55352  167 
by (induct set: finite) (auto simp: zero_cong add_cong) 
31719  168 

60527  169 
lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R" 
170 
apply (subst res_units_eq) 

171 
apply auto 

31719  172 
apply (insert pos_mod_sign [of m a]) 
60527  173 
apply (subgoal_tac "a mod m \<noteq> 0") 
31719  174 
apply arith 
175 
apply auto 

55352  176 
apply (metis gcd_int.commute gcd_red_int) 
41541  177 
done 
31719  178 

44872  179 
lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" 
31719  180 
unfolding cong_int_def by auto 
181 

182 

60527  183 
text \<open>Simplifying with these will translate a ring equation in R to a 
184 
congruence.\<close> 

31719  185 
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong 
186 
prod_cong sum_cong neg_cong res_eq_to_cong 

187 

60527  188 
text \<open>Other useful facts about the residue ring.\<close> 
31719  189 

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

191 
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

192 
apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff 
55352  193 
zero_neq_one zmod_zminus1_eq_if) 
41541  194 
done 
31719  195 

196 
end 

197 

198 

60527  199 
subsection \<open>Prime residues\<close> 
31719  200 

201 
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

202 
fixes p and R (structure) 
31719  203 
assumes p_prime [intro]: "prime p" 
60527  204 
defines "R \<equiv> residue_ring p" 
31719  205 

206 
sublocale residues_prime < residues p 

207 
apply (unfold R_def residues_def) 

208 
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

209 
apply (metis (full_types) int_1 of_nat_less_iff prime_gt_1_nat) 
41541  210 
done 
31719  211 

44872  212 
context residues_prime 
213 
begin 

31719  214 

215 
lemma is_field: "field R" 

216 
apply (rule cring.field_intro2) 

217 
apply (rule cring) 

44872  218 
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) 
31719  219 
apply (rule classical) 
220 
apply (erule notE) 

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

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

222 
apply (rule prime_imp_coprime_int) 
31719  223 
apply (rule p_prime) 
224 
apply (rule notI) 

225 
apply (frule zdvd_imp_le) 

226 
apply auto 

41541  227 
done 
31719  228 

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

230 
apply (subst res_units_eq) 

231 
apply auto 

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

232 
apply (subst gcd_commute_int) 
55352  233 
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) 
41541  234 
done 
31719  235 

236 
end 

237 

238 
sublocale residues_prime < field 

239 
by (rule is_field) 

240 

241 

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

60527  244 
subsection \<open>Euler's theorem\<close> 
31719  245 

60527  246 
text \<open>The definition of the phi function.\<close> 
31719  247 

60527  248 
definition phi :: "int \<Rightarrow> nat" 
249 
where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}" 

31719  250 

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

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

253 
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

254 
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

255 
apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) 
60527  256 
apply (metis One_nat_def int_0 int_1 int_less_0_conv int_nat_eq nat_int 
257 
transfer_int_nat_gcd(1) zless_int) 

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

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

259 

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

260 
lemma prime_phi: 
60527  261 
assumes "2 \<le> p" "phi p = p  1" 
262 
shows "prime p" 

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

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

264 
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

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

266 
by (intro card_seteq) fastforce+ 
60527  267 
then have cop: "\<And>x::nat. x \<in> {1..p  1} \<Longrightarrow> coprime x p" 
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

268 
by blast 
60527  269 
have False if *: "1 < x" "x < p" and "x dvd p" for x :: nat 
270 
proof  

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

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

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

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

274 
done 
60527  275 
with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis 
276 
by auto 

277 
qed 

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

278 
then show ?thesis 
60526  279 
using \<open>2 \<le> p\<close> 
55262  280 
by (simp add: prime_def) 
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

281 
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 
55352  282 
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

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

284 

31719  285 
lemma phi_zero [simp]: "phi 0 = 0" 
60527  286 
unfolding phi_def 
44872  287 
(* Auto hangs here. Once again, where is the simplification rule 
60527  288 
1 \<equiv> Suc 0 coming from? *) 
31719  289 
apply (auto simp add: card_eq_0_iff) 
290 
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) 

41541  291 
done 
31719  292 

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

44872  294 
by (auto simp add: phi_def card_eq_0_iff) 
31719  295 

60527  296 
lemma (in residues) phi_eq: "phi m = card (Units R)" 
31719  297 
by (simp add: phi_def res_units_eq) 
298 

44872  299 
lemma (in residues) euler_theorem1: 
31719  300 
assumes a: "gcd a m = 1" 
301 
shows "[a^phi m = 1] (mod m)" 

302 
proof  

60527  303 
from a m_gt_one have [simp]: "a mod m \<in> Units R" 
31719  304 
by (intro mod_in_res_units) 
305 
from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" 

306 
by simp 

44872  307 
also have "\<dots> = \<one>" 
60527  308 
by (intro units_power_order_eq_one) auto 
31719  309 
finally show ?thesis 
310 
by (simp add: res_to_cong_simps) 

311 
qed 

312 

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

314 

44872  315 
lemma (in residues) euler_theorem1: 
31719  316 
assumes a: "gcd a m = 1" 
317 
shows "[a^phi m = 1] (mod m)" 

318 
proof  

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

320 
by (simp add: phi_eq units_power_order_eq_one a m_gt_one) 

44872  321 
then show ?thesis 
31719  322 
by (simp add: res_to_cong_simps) 
323 
qed 

324 

325 
*) 

326 

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

328 

329 
lemma euler_theorem: 

60527  330 
assumes "m \<ge> 0" 
331 
and "gcd a m = 1" 

31719  332 
shows "[a^phi m = 1] (mod m)" 
60527  333 
proof (cases "m = 0  m = 1") 
334 
case True 

44872  335 
then show ?thesis by auto 
31719  336 
next 
60527  337 
case False 
41541  338 
with assms show ?thesis 
31719  339 
by (intro residues.euler_theorem1, unfold residues_def, auto) 
340 
qed 

341 

60527  342 
lemma (in residues_prime) phi_prime: "phi p = nat p  1" 
31719  343 
apply (subst phi_eq) 
344 
apply (subst res_prime_units_eq) 

345 
apply auto 

41541  346 
done 
31719  347 

60527  348 
lemma phi_prime: "prime p \<Longrightarrow> phi p = nat p  1" 
31719  349 
apply (rule residues_prime.phi_prime) 
350 
apply (erule residues_prime.intro) 

41541  351 
done 
31719  352 

353 
lemma fermat_theorem: 

60527  354 
fixes a :: int 
355 
assumes "prime p" 

356 
and "\<not> 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

357 
shows "[a^(p  1) = 1] (mod p)" 
31719  358 
proof  
60527  359 
from assms have "[a ^ phi p = 1] (mod p)" 
31719  360 
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

361 
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

362 
apply (metis gcd_int.commute prime_imp_coprime_int) 
31719  363 
done 
364 
also have "phi p = nat p  1" 

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

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

367 
by (metis nat_int) 
31719  368 
qed 
369 

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

370 
lemma fermat_theorem_nat: 
60527  371 
assumes "prime p" and "\<not> p dvd a" 
372 
shows "[a ^ (p  1) = 1] (mod p)" 

373 
using fermat_theorem [of p a] assms 

374 
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

375 

31719  376 

60526  377 
subsection \<open>Wilson's theorem\<close> 
31719  378 

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

31719  381 
apply auto 
55352  382 
apply (metis Units_inv_inv)+ 
41541  383 
done 
31719  384 

385 
lemma (in residues_prime) wilson_theorem1: 

386 
assumes a: "p > 2" 

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

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

31719  391 
by auto 
60527  392 
have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)" 
31732  393 
apply (subst UR) 
31719  394 
apply (subst finprod_Un_disjoint) 
55352  395 
apply (auto intro: funcsetI) 
60527  396 
using inv_one apply auto[1] 
397 
using inv_eq_neg_one_eq apply auto 

31719  398 
done 
60527  399 
also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" 
31719  400 
apply (subst finprod_insert) 
401 
apply auto 

402 
apply (frule one_eq_neg_one) 

60527  403 
using a apply force 
31719  404 
done 
60527  405 
also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))" 
406 
apply (subst finprod_Union_disjoint) 

407 
apply auto 

55352  408 
apply (metis Units_inv_inv)+ 
31719  409 
done 
410 
also have "\<dots> = \<one>" 

60527  411 
apply (rule finprod_one) 
412 
apply auto 

413 
apply (subst finprod_insert) 

414 
apply auto 

55352  415 
apply (metis inv_eq_self) 
31719  416 
done 
60527  417 
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" 
31719  418 
by simp 
60527  419 
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" 
31719  420 
apply (rule finprod_cong') 
60527  421 
apply auto 
31719  422 
apply (subst (asm) res_prime_units_eq) 
423 
apply auto 

424 
done 

60527  425 
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" 
31719  426 
apply (rule prod_cong) 
427 
apply auto 

428 
done 

429 
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

430 
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

431 
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

432 
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

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

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

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

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

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

444 
case True 
55352  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 