author  paulson <lp15@cam.ac.uk> 
Tue, 28 Feb 2017 15:17:57 +0000  
changeset 65066  c64d778a593a 
parent 64593  50c715579715 
child 65416  f707dbcf11e3 
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 

63537
831816778409
Removed redundant material related to primes
eberlm <eberlm@in.tum.de>
parents:
63534
diff
changeset

11 
imports Cong MiscAlgebra 
31719  12 
begin 
13 

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

14 
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

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

16 

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

17 
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

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

19 
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

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

21 

60527  22 
subsection \<open>A locale for residue rings\<close> 
31719  23 

60527  24 
definition residue_ring :: "int \<Rightarrow> int ring" 
60528  25 
where 
60527  26 
"residue_ring m = 
27 
\<lparr>carrier = {0..m  1}, 

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

29 
one = 1, 

30 
zero = 0, 

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

31719  32 

33 
locale residues = 

34 
fixes m :: int and R (structure) 

35 
assumes m_gt_one: "m > 1" 

60527  36 
defines "R \<equiv> residue_ring m" 
44872  37 
begin 
31719  38 

39 
lemma abelian_group: "abelian_group R" 

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

42 
proof (cases "x = 0") 

43 
case True 

44 
with m_gt_one show ?thesis by simp 

45 
next 

46 
case False 

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

48 
by simp 

49 
with m_gt_one that show ?thesis 

50 
by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le) 

51 
qed 

52 
with m_gt_one show ?thesis 

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

54 
qed 

31719  55 

56 
lemma comm_monoid: "comm_monoid R" 

65066  57 
unfolding R_def residue_ring_def 
31719  58 
apply (rule comm_monoidI) 
65066  59 
using m_gt_one apply auto 
60 
apply (metis mod_mult_right_eq mult.assoc mult.commute) 

61 
apply (metis mult.commute) 

41541  62 
done 
31719  63 

64 
lemma cring: "cring R" 

65066  65 
apply (intro cringI abelian_group comm_monoid) 
66 
unfolding R_def residue_ring_def 

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

41541  68 
done 
31719  69 

70 
end 

71 

72 
sublocale residues < cring 

73 
by (rule cring) 

74 

75 

41541  76 
context residues 
77 
begin 

31719  78 

60527  79 
text \<open> 
80 
These lemmas translate back and forth between internal and 

81 
external concepts. 

82 
\<close> 

31719  83 

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

44872  85 
unfolding R_def residue_ring_def by auto 
31719  86 

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

44872  88 
unfolding R_def residue_ring_def by auto 
31719  89 

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

44872  91 
unfolding R_def residue_ring_def by auto 
31719  92 

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

44872  94 
unfolding R_def residue_ring_def by auto 
31719  95 

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

44872  97 
unfolding R_def residue_ring_def units_of_def by auto 
31719  98 

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

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

106 
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

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

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

65066  111 
using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def 
112 
apply simp 

31719  113 
apply (rule the_equality) 
65066  114 
apply (simp add: mod_add_right_eq) 
115 
apply (simp add: add.commute mod_add_right_eq) 

116 
apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial) 

41541  117 
done 
31719  118 

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

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

123 
by (subst res_units_eq) auto 
31719  124 

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

129 
\<close> 

31719  130 

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

133 
using insert m_gt_one by auto 

31719  134 

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

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

137 
by (auto simp add: mod_simps) 
31719  138 

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

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

141 
by (auto simp add: mod_simps) 
31719  142 

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

44872  144 
unfolding R_def residue_ring_def by auto 
31719  145 

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

44872  147 
using m_gt_one unfolding R_def residue_ring_def by auto 
31719  148 

60527  149 
(* FIXME revise algebra library to use 1? *) 
31719  150 
lemma pow_cong: "(x mod m) (^) n = x^n mod m" 
65066  151 
using m_gt_one 
31719  152 
apply (induct n) 
41541  153 
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

154 
apply (metis mult.commute mult_cong) 
41541  155 
done 
31719  156 

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

55352  158 
by (metis mod_minus_eq res_neg_eq) 
31719  159 

60528  160 
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  161 
by (induct set: finite) (auto simp: one_cong mult_cong) 
31719  162 

60528  163 
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  164 
by (induct set: finite) (auto simp: zero_cong add_cong) 
31719  165 

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

166 
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

167 
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

168 
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

169 
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

170 
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

171 
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

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

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

174 
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

175 
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

176 
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

177 
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

178 
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

179 
qed 
31719  180 

60528  181 
lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)" 
31719  182 
unfolding cong_int_def by auto 
183 

184 

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

188 

60527  189 
text \<open>Other useful facts about the residue ring.\<close> 
31719  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 
60528  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 = 

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

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

204 
defines "R \<equiv> residue_ring (int p)" 
31719  205 

206 
sublocale residues_prime < residues p 

65066  207 
unfolding R_def residues_def 
31719  208 
using p_prime apply auto 
62348  209 
apply (metis (full_types) of_nat_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" 

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

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

219 
then show ?thesis 

220 
apply (intro cring.field_intro2 cring) 

44872  221 
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) 
65066  222 
done 
223 
qed 

31719  224 

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

226 
apply (subst res_units_eq) 

227 
apply auto 

62348  228 
apply (subst gcd.commute) 
55352  229 
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) 
41541  230 
done 
31719  231 

232 
end 

233 

234 
sublocale residues_prime < field 

235 
by (rule is_field) 

236 

237 

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

60527  240 
subsection \<open>Euler's theorem\<close> 
31719  241 

65066  242 
text \<open>The definition of the totient function.\<close> 
31719  243 

60527  244 
definition phi :: "int \<Rightarrow> nat" 
65066  245 
where "phi m = card {x. 0 < x \<and> x < m \<and> coprime x m}" 
31719  246 

65066  247 
lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}" 
248 
unfolding phi_def 

249 
proof (rule bij_betw_same_card [of nat]) 

250 
show "bij_betw nat {x. 0 < x \<and> x < m \<and> coprime x m} {x. 0 < x \<and> x < nat m \<and> coprime x (nat m)}" 

251 
apply (auto simp add: inj_on_def bij_betw_def image_def) 

252 
apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) 

253 
apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int 

254 
transfer_int_nat_gcd(1) of_nat_less_iff) 

255 
done 

256 
qed 

257 

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

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

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

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

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

264 
by (intro card_seteq) fastforce+ 
60528  265 
have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat 
60527  266 
proof  
60528  267 
from * have cop: "x \<in> {1..p  1} \<Longrightarrow> coprime x p" 
268 
by blast 

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

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

270 
apply (rule cop) 
60528  271 
using ** apply auto 
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset

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

275 
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

276 
then show ?thesis 
60526  277 
using \<open>2 \<le> p\<close> 
63633  278 
by (simp add: prime_nat_iff) 
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

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

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

282 

31719  283 
lemma phi_zero [simp]: "phi 0 = 0" 
65066  284 
unfolding phi_def by (auto simp add: card_eq_0_iff) 
31719  285 

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

44872  287 
by (auto simp add: phi_def card_eq_0_iff) 
31719  288 

60527  289 
lemma (in residues) phi_eq: "phi m = card (Units R)" 
31719  290 
by (simp add: phi_def res_units_eq) 
291 

44872  292 
lemma (in residues) euler_theorem1: 
31719  293 
assumes a: "gcd a m = 1" 
294 
shows "[a^phi m = 1] (mod m)" 

295 
proof  

65066  296 
have "a ^ phi m mod m = 1 mod m" 
297 
by (metis assms finite_Units m_gt_one mod_in_res_units one_cong phi_eq pow_cong units_power_order_eq_one) 

298 
then show ?thesis 

299 
using res_eq_to_cong by blast 

31719  300 
qed 
301 

63167  302 
text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close> 
31719  303 
lemma euler_theorem: 
60527  304 
assumes "m \<ge> 0" 
305 
and "gcd a m = 1" 

31719  306 
shows "[a^phi m = 1] (mod m)" 
60527  307 
proof (cases "m = 0  m = 1") 
308 
case True 

44872  309 
then show ?thesis by auto 
31719  310 
next 
60527  311 
case False 
41541  312 
with assms show ?thesis 
31719  313 
by (intro residues.euler_theorem1, unfold residues_def, auto) 
314 
qed 

315 

60527  316 
lemma (in residues_prime) phi_prime: "phi p = nat p  1" 
65066  317 
by (simp add: residues.phi_eq residues_axioms residues_prime.res_prime_units_eq residues_prime_axioms) 
31719  318 

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

319 
lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p  1" 
65066  320 
by (simp add: residues_prime.intro residues_prime.phi_prime) 
31719  321 

322 
lemma fermat_theorem: 

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

324 
assumes "prime (int p)" 
60527  325 
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

326 
shows "[a^(p  1) = 1] (mod p)" 
31719  327 
proof  
60527  328 
from assms have "[a ^ phi p = 1] (mod p)" 
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

329 
by (auto intro!: euler_theorem intro!: prime_imp_coprime_int[of p] 
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset

330 
simp: gcd.commute[of _ "int p"]) 
31719  331 
also have "phi p = nat p  1" 
60527  332 
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

333 
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

334 
by (metis nat_int) 
31719  335 
qed 
336 

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

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

338 
assumes "prime (int p)" and "\<not> p dvd a" 
60527  339 
shows "[a ^ (p  1) = 1] (mod p)" 
340 
using fermat_theorem [of p a] assms 

62348  341 
by (metis of_nat_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

342 

31719  343 

60526  344 
subsection \<open>Wilson's theorem\<close> 
31719  345 

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

31719  348 
apply auto 
55352  349 
apply (metis Units_inv_inv)+ 
41541  350 
done 
31719  351 

352 
lemma (in residues_prime) wilson_theorem1: 

353 
assumes a: "p > 2" 

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

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

31719  358 
by auto 
60527  359 
have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)" 
31732  360 
apply (subst UR) 
31719  361 
apply (subst finprod_Un_disjoint) 
55352  362 
apply (auto intro: funcsetI) 
60527  363 
using inv_one apply auto[1] 
364 
using inv_eq_neg_one_eq apply auto 

31719  365 
done 
60527  366 
also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" 
31719  367 
apply (subst finprod_insert) 
368 
apply auto 

369 
apply (frule one_eq_neg_one) 

60527  370 
using a apply force 
31719  371 
done 
60527  372 
also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))" 
373 
apply (subst finprod_Union_disjoint) 

374 
apply auto 

55352  375 
apply (metis Units_inv_inv)+ 
31719  376 
done 
377 
also have "\<dots> = \<one>" 

60527  378 
apply (rule finprod_one) 
379 
apply auto 

380 
apply (subst finprod_insert) 

381 
apply auto 

55352  382 
apply (metis inv_eq_self) 
31719  383 
done 
60527  384 
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" 
31719  385 
by simp 
60527  386 
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" 
65066  387 
by (rule finprod_cong') (auto simp: res_units_eq) 
60527  388 
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" 
65066  389 
by (rule prod_cong) auto 
31719  390 
also have "\<dots> = fact (p  1) mod p" 
64272  391 
apply (simp add: fact_prod) 
65066  392 
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

393 
apply (subst res_prime_units_eq) 
64272  394 
apply (simp add: int_prod zmod_int prod_int_eq) 
31719  395 
done 
60527  396 
finally have "fact (p  1) mod p = \<ominus> \<one>" . 
397 
then show ?thesis 

60528  398 
by (metis of_nat_fact Divides.transfer_int_nat_functions(2) 
399 
cong_int_def res_neg_eq res_one_eq) 

31719  400 
qed 
401 

55352  402 
lemma wilson_theorem: 
60527  403 
assumes "prime p" 
404 
shows "[fact (p  1) =  1] (mod p)" 

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

406 
case True 
55352  407 
then show ?thesis 
64272  408 
by (simp add: cong_int_def fact_prod) 
55352  409 
next 
410 
case False 

411 
then show ?thesis 

412 
using assms prime_ge_2_nat 

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

414 
qed 

31719  415 

416 
end 