author | haftmann |
Tue, 13 Jul 2010 16:00:56 +0200 | |
changeset 37804 | 0145e59c1f6c |
parent 36350 | bc7982c54e37 |
child 41541 | 1fa4725c4656 |
permissions | -rw-r--r-- |
31719 | 1 |
(* Title: HOL/Library/Residues.thy |
2 |
ID: |
|
3 |
Author: Jeremy Avigad |
|
4 |
||
5 |
An algebraic treatment of residue rings, and resulting proofs of |
|
6 |
Euler's theorem and Wilson's theorem. |
|
7 |
*) |
|
8 |
||
9 |
header {* Residue rings *} |
|
10 |
||
11 |
theory Residues |
|
12 |
imports |
|
13 |
UniqueFactorization |
|
14 |
Binomial |
|
15 |
MiscAlgebra |
|
16 |
begin |
|
17 |
||
18 |
||
19 |
(* |
|
20 |
||
21 |
A locale for residue rings |
|
22 |
||
23 |
*) |
|
24 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32479
diff
changeset
|
25 |
definition residue_ring :: "int => int ring" where |
31719 | 26 |
"residue_ring m == (| |
27 |
carrier = {0..m - 1}, |
|
28 |
mult = (%x y. (x * y) mod m), |
|
29 |
one = 1, |
|
30 |
zero = 0, |
|
31 |
add = (%x y. (x + y) mod m) |)" |
|
32 |
||
33 |
locale residues = |
|
34 |
fixes m :: int and R (structure) |
|
35 |
assumes m_gt_one: "m > 1" |
|
36 |
defines "R == residue_ring m" |
|
37 |
||
38 |
context residues begin |
|
39 |
||
40 |
lemma abelian_group: "abelian_group R" |
|
41 |
apply (insert m_gt_one) |
|
42 |
apply (rule abelian_groupI) |
|
43 |
apply (unfold R_def residue_ring_def) |
|
44 |
apply (auto simp add: mod_pos_pos_trivial mod_add_right_eq [symmetric] |
|
45 |
add_ac) |
|
46 |
apply (case_tac "x = 0") |
|
47 |
apply force |
|
48 |
apply (subgoal_tac "(x + (m - x)) mod m = 0") |
|
49 |
apply (erule bexI) |
|
50 |
apply auto |
|
51 |
done |
|
52 |
||
53 |
lemma comm_monoid: "comm_monoid R" |
|
54 |
apply (insert m_gt_one) |
|
55 |
apply (unfold R_def residue_ring_def) |
|
56 |
apply (rule comm_monoidI) |
|
57 |
apply auto |
|
58 |
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") |
|
59 |
apply (erule ssubst) |
|
60 |
apply (subst zmod_zmult1_eq [symmetric])+ |
|
61 |
apply (simp_all only: mult_ac) |
|
62 |
done |
|
63 |
||
64 |
lemma cring: "cring R" |
|
65 |
apply (rule cringI) |
|
66 |
apply (rule abelian_group) |
|
67 |
apply (rule comm_monoid) |
|
68 |
apply (unfold R_def residue_ring_def, auto) |
|
69 |
apply (subst mod_add_eq [symmetric]) |
|
70 |
apply (subst mult_commute) |
|
71 |
apply (subst zmod_zmult1_eq [symmetric]) |
|
36350 | 72 |
apply (simp add: field_simps) |
31719 | 73 |
done |
74 |
||
75 |
end |
|
76 |
||
77 |
sublocale residues < cring |
|
78 |
by (rule cring) |
|
79 |
||
80 |
||
81 |
context residues begin |
|
82 |
||
83 |
(* These lemmas translate back and forth between internal and |
|
84 |
external concepts *) |
|
85 |
||
86 |
lemma res_carrier_eq: "carrier R = {0..m - 1}" |
|
87 |
by (unfold R_def residue_ring_def, auto) |
|
88 |
||
89 |
lemma res_add_eq: "x \<oplus> y = (x + y) mod m" |
|
90 |
by (unfold R_def residue_ring_def, auto) |
|
91 |
||
92 |
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" |
|
93 |
by (unfold R_def residue_ring_def, auto) |
|
94 |
||
95 |
lemma res_zero_eq: "\<zero> = 0" |
|
96 |
by (unfold R_def residue_ring_def, auto) |
|
97 |
||
98 |
lemma res_one_eq: "\<one> = 1" |
|
99 |
by (unfold R_def residue_ring_def units_of_def residue_ring_def, auto) |
|
100 |
||
101 |
lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}" |
|
102 |
apply (insert m_gt_one) |
|
103 |
apply (unfold Units_def R_def residue_ring_def) |
|
104 |
apply auto |
|
105 |
apply (subgoal_tac "x ~= 0") |
|
106 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
107 |
apply (rule invertible_coprime_int) |
31719 | 108 |
apply (subgoal_tac "x ~= 0") |
109 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
110 |
apply (subst (asm) coprime_iff_invertible'_int) |
31719 | 111 |
apply (rule m_gt_one) |
112 |
apply (auto simp add: cong_int_def mult_commute) |
|
113 |
done |
|
114 |
||
115 |
lemma res_neg_eq: "\<ominus> x = (- x) mod m" |
|
116 |
apply (insert m_gt_one) |
|
117 |
apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
|
118 |
apply auto |
|
119 |
apply (rule the_equality) |
|
120 |
apply auto |
|
121 |
apply (subst mod_add_right_eq [symmetric]) |
|
122 |
apply auto |
|
123 |
apply (subst mod_add_left_eq [symmetric]) |
|
124 |
apply auto |
|
125 |
apply (subgoal_tac "y mod m = - x mod m") |
|
126 |
apply simp |
|
127 |
apply (subst zmod_eq_dvd_iff) |
|
128 |
apply auto |
|
129 |
done |
|
130 |
||
131 |
lemma finite [iff]: "finite(carrier R)" |
|
132 |
by (subst res_carrier_eq, auto) |
|
133 |
||
134 |
lemma finite_Units [iff]: "finite(Units R)" |
|
135 |
by (subst res_units_eq, auto) |
|
136 |
||
137 |
(* The function a -> a mod m maps the integers to the |
|
138 |
residue classes. The following lemmas show that this mapping |
|
139 |
respects addition and multiplication on the integers. *) |
|
140 |
||
141 |
lemma mod_in_carrier [iff]: "a mod m : carrier R" |
|
142 |
apply (unfold res_carrier_eq) |
|
143 |
apply (insert m_gt_one, auto) |
|
144 |
done |
|
145 |
||
146 |
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
|
147 |
by (unfold R_def residue_ring_def, auto, arith) |
|
148 |
||
149 |
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
|
150 |
apply (unfold R_def residue_ring_def, auto) |
|
151 |
apply (subst zmod_zmult1_eq [symmetric]) |
|
152 |
apply (subst mult_commute) |
|
153 |
apply (subst zmod_zmult1_eq [symmetric]) |
|
154 |
apply (subst mult_commute) |
|
155 |
apply auto |
|
156 |
done |
|
157 |
||
158 |
lemma zero_cong: "\<zero> = 0" |
|
159 |
apply (unfold R_def residue_ring_def, auto) |
|
160 |
done |
|
161 |
||
162 |
lemma one_cong: "\<one> = 1 mod m" |
|
163 |
apply (insert m_gt_one) |
|
164 |
apply (unfold R_def residue_ring_def, auto) |
|
165 |
done |
|
166 |
||
167 |
(* revise algebra library to use 1? *) |
|
168 |
lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
|
169 |
apply (insert m_gt_one) |
|
170 |
apply (induct n) |
|
171 |
apply (auto simp add: nat_pow_def one_cong One_nat_def) |
|
172 |
apply (subst mult_commute) |
|
173 |
apply (rule mult_cong) |
|
174 |
done |
|
175 |
||
176 |
lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m" |
|
177 |
apply (rule sym) |
|
178 |
apply (rule sum_zero_eq_neg) |
|
179 |
apply auto |
|
180 |
apply (subst add_cong) |
|
181 |
apply (subst zero_cong) |
|
182 |
apply auto |
|
183 |
done |
|
184 |
||
185 |
lemma (in residues) prod_cong: |
|
186 |
"finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m" |
|
187 |
apply (induct set: finite) |
|
31727 | 188 |
apply (auto simp: one_cong mult_cong) |
31719 | 189 |
done |
190 |
||
191 |
lemma (in residues) sum_cong: |
|
192 |
"finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m" |
|
193 |
apply (induct set: finite) |
|
31727 | 194 |
apply (auto simp: zero_cong add_cong) |
31719 | 195 |
done |
196 |
||
197 |
lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> |
|
198 |
a mod m : Units R" |
|
199 |
apply (subst res_units_eq, auto) |
|
200 |
apply (insert pos_mod_sign [of m a]) |
|
201 |
apply (subgoal_tac "a mod m ~= 0") |
|
202 |
apply arith |
|
203 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
204 |
apply (subst (asm) gcd_red_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
205 |
apply (subst gcd_commute_int, assumption) |
31719 | 206 |
done |
207 |
||
208 |
lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" |
|
209 |
unfolding cong_int_def by auto |
|
210 |
||
211 |
(* Simplifying with these will translate a ring equation in R to a |
|
212 |
congruence. *) |
|
213 |
||
214 |
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong |
|
215 |
prod_cong sum_cong neg_cong res_eq_to_cong |
|
216 |
||
217 |
(* Other useful facts about the residue ring *) |
|
218 |
||
219 |
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" |
|
220 |
apply (simp add: res_one_eq res_neg_eq) |
|
221 |
apply (insert m_gt_one) |
|
222 |
apply (subgoal_tac "~(m > 2)") |
|
223 |
apply arith |
|
224 |
apply (rule notI) |
|
225 |
apply (subgoal_tac "-1 mod m = m - 1") |
|
226 |
apply force |
|
227 |
apply (subst mod_add_self2 [symmetric]) |
|
228 |
apply (subst mod_pos_pos_trivial) |
|
229 |
apply auto |
|
230 |
done |
|
231 |
||
232 |
end |
|
233 |
||
234 |
||
235 |
(* prime residues *) |
|
236 |
||
237 |
locale residues_prime = |
|
238 |
fixes p :: int and R (structure) |
|
239 |
assumes p_prime [intro]: "prime p" |
|
240 |
defines "R == residue_ring p" |
|
241 |
||
242 |
sublocale residues_prime < residues p |
|
243 |
apply (unfold R_def residues_def) |
|
244 |
using p_prime apply auto |
|
245 |
done |
|
246 |
||
247 |
context residues_prime begin |
|
248 |
||
249 |
lemma is_field: "field R" |
|
250 |
apply (rule cring.field_intro2) |
|
251 |
apply (rule cring) |
|
252 |
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq |
|
253 |
res_units_eq) |
|
254 |
apply (rule classical) |
|
255 |
apply (erule notE) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
256 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
257 |
apply (rule prime_imp_coprime_int) |
31719 | 258 |
apply (rule p_prime) |
259 |
apply (rule notI) |
|
260 |
apply (frule zdvd_imp_le) |
|
261 |
apply auto |
|
262 |
done |
|
263 |
||
264 |
lemma res_prime_units_eq: "Units R = {1..p - 1}" |
|
265 |
apply (subst res_units_eq) |
|
266 |
apply auto |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
267 |
apply (subst gcd_commute_int) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
268 |
apply (rule prime_imp_coprime_int) |
31719 | 269 |
apply (rule p_prime) |
270 |
apply (rule zdvd_not_zless) |
|
271 |
apply auto |
|
272 |
done |
|
273 |
||
274 |
end |
|
275 |
||
276 |
sublocale residues_prime < field |
|
277 |
by (rule is_field) |
|
278 |
||
279 |
||
280 |
(* |
|
281 |
Test cases: Euler's theorem and Wilson's theorem. |
|
282 |
*) |
|
283 |
||
284 |
||
285 |
subsection{* Euler's theorem *} |
|
286 |
||
287 |
(* the definition of the phi function *) |
|
288 |
||
35416
d8d7d1b785af
replaced a couple of constsdefs by definitions (also some old primrecs by modern ones)
haftmann
parents:
32479
diff
changeset
|
289 |
definition phi :: "int => nat" where |
31719 | 290 |
"phi m == card({ x. 0 < x & x < m & gcd x m = 1})" |
291 |
||
292 |
lemma phi_zero [simp]: "phi 0 = 0" |
|
293 |
apply (subst phi_def) |
|
294 |
(* Auto hangs here. Once again, where is the simplification rule |
|
295 |
1 == Suc 0 coming from? *) |
|
296 |
apply (auto simp add: card_eq_0_iff) |
|
297 |
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) |
|
298 |
done |
|
299 |
||
300 |
lemma phi_one [simp]: "phi 1 = 0" |
|
301 |
apply (auto simp add: phi_def card_eq_0_iff) |
|
302 |
done |
|
303 |
||
304 |
lemma (in residues) phi_eq: "phi m = card(Units R)" |
|
305 |
by (simp add: phi_def res_units_eq) |
|
306 |
||
307 |
lemma (in residues) euler_theorem1: |
|
308 |
assumes a: "gcd a m = 1" |
|
309 |
shows "[a^phi m = 1] (mod m)" |
|
310 |
proof - |
|
311 |
from a m_gt_one have [simp]: "a mod m : Units R" |
|
312 |
by (intro mod_in_res_units) |
|
313 |
from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" |
|
314 |
by simp |
|
315 |
also have "\<dots> = \<one>" |
|
316 |
by (intro units_power_order_eq_one, auto) |
|
317 |
finally show ?thesis |
|
318 |
by (simp add: res_to_cong_simps) |
|
319 |
qed |
|
320 |
||
321 |
(* In fact, there is a two line proof! |
|
322 |
||
323 |
lemma (in residues) euler_theorem1: |
|
324 |
assumes a: "gcd a m = 1" |
|
325 |
shows "[a^phi m = 1] (mod m)" |
|
326 |
proof - |
|
327 |
have "(a mod m) (^) (phi m) = \<one>" |
|
328 |
by (simp add: phi_eq units_power_order_eq_one a m_gt_one) |
|
329 |
thus ?thesis |
|
330 |
by (simp add: res_to_cong_simps) |
|
331 |
qed |
|
332 |
||
333 |
*) |
|
334 |
||
335 |
(* outside the locale, we can relax the restriction m > 1 *) |
|
336 |
||
337 |
lemma euler_theorem: |
|
338 |
assumes "m >= 0" and "gcd a m = 1" |
|
339 |
shows "[a^phi m = 1] (mod m)" |
|
340 |
proof (cases) |
|
341 |
assume "m = 0 | m = 1" |
|
342 |
thus ?thesis by auto |
|
343 |
next |
|
344 |
assume "~(m = 0 | m = 1)" |
|
345 |
with prems show ?thesis |
|
346 |
by (intro residues.euler_theorem1, unfold residues_def, auto) |
|
347 |
qed |
|
348 |
||
349 |
lemma (in residues_prime) phi_prime: "phi p = (nat p - 1)" |
|
350 |
apply (subst phi_eq) |
|
351 |
apply (subst res_prime_units_eq) |
|
352 |
apply auto |
|
353 |
done |
|
354 |
||
355 |
lemma phi_prime: "prime p \<Longrightarrow> phi p = (nat p - 1)" |
|
356 |
apply (rule residues_prime.phi_prime) |
|
357 |
apply (erule residues_prime.intro) |
|
358 |
done |
|
359 |
||
360 |
lemma fermat_theorem: |
|
361 |
assumes "prime p" and "~ (p dvd a)" |
|
362 |
shows "[a^(nat p - 1) = 1] (mod p)" |
|
363 |
proof - |
|
364 |
from prems have "[a^phi p = 1] (mod p)" |
|
365 |
apply (intro euler_theorem) |
|
366 |
(* auto should get this next part. matching across |
|
367 |
substitutions is needed. *) |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
368 |
apply (frule prime_gt_1_int, arith) |
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
369 |
apply (subst gcd_commute_int, erule prime_imp_coprime_int, assumption) |
31719 | 370 |
done |
371 |
also have "phi p = nat p - 1" |
|
372 |
by (rule phi_prime, rule prems) |
|
373 |
finally show ?thesis . |
|
374 |
qed |
|
375 |
||
376 |
||
377 |
subsection {* Wilson's theorem *} |
|
378 |
||
379 |
lemma (in field) inv_pair_lemma: "x : Units R \<Longrightarrow> y : Units R \<Longrightarrow> |
|
380 |
{x, inv x} ~= {y, inv y} \<Longrightarrow> {x, inv x} Int {y, inv y} = {}" |
|
381 |
apply auto |
|
382 |
apply (erule notE) |
|
383 |
apply (erule inv_eq_imp_eq) |
|
384 |
apply auto |
|
385 |
apply (erule notE) |
|
386 |
apply (erule inv_eq_imp_eq) |
|
387 |
apply auto |
|
388 |
done |
|
389 |
||
390 |
lemma (in residues_prime) wilson_theorem1: |
|
391 |
assumes a: "p > 2" |
|
392 |
shows "[fact (p - 1) = - 1] (mod p)" |
|
393 |
proof - |
|
394 |
let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" |
|
31732 | 395 |
have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)" |
31719 | 396 |
by auto |
31732 | 397 |
have "(\<Otimes>i: Units R. i) = |
31719 | 398 |
(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)" |
31732 | 399 |
apply (subst UR) |
31719 | 400 |
apply (subst finprod_Un_disjoint) |
31732 | 401 |
apply (auto intro:funcsetI) |
31719 | 402 |
apply (drule sym, subst (asm) inv_eq_one_eq) |
403 |
apply auto |
|
404 |
apply (drule sym, subst (asm) inv_eq_neg_one_eq) |
|
405 |
apply auto |
|
406 |
done |
|
407 |
also have "(\<Otimes>i: {\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" |
|
408 |
apply (subst finprod_insert) |
|
409 |
apply auto |
|
410 |
apply (frule one_eq_neg_one) |
|
411 |
apply (insert a, force) |
|
412 |
done |
|
413 |
also have "(\<Otimes>i:(Union ?InversePairs). i) = |
|
414 |
(\<Otimes> A: ?InversePairs. (\<Otimes> y:A. y))" |
|
415 |
apply (subst finprod_Union_disjoint) |
|
416 |
apply force |
|
417 |
apply force |
|
418 |
apply clarify |
|
419 |
apply (rule inv_pair_lemma) |
|
420 |
apply auto |
|
421 |
done |
|
422 |
also have "\<dots> = \<one>" |
|
423 |
apply (rule finprod_one) |
|
424 |
apply auto |
|
425 |
apply (subst finprod_insert) |
|
426 |
apply auto |
|
427 |
apply (frule inv_eq_self) |
|
31732 | 428 |
apply (auto) |
31719 | 429 |
done |
430 |
finally have "(\<Otimes>i: Units R. i) = \<ominus> \<one>" |
|
431 |
by simp |
|
432 |
also have "(\<Otimes>i: Units R. i) = (\<Otimes>i: Units R. i mod p)" |
|
433 |
apply (rule finprod_cong') |
|
31732 | 434 |
apply (auto) |
31719 | 435 |
apply (subst (asm) res_prime_units_eq) |
436 |
apply auto |
|
437 |
done |
|
438 |
also have "\<dots> = (PROD i: Units R. i) mod p" |
|
439 |
apply (rule prod_cong) |
|
440 |
apply auto |
|
441 |
done |
|
442 |
also have "\<dots> = fact (p - 1) mod p" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
443 |
apply (subst fact_altdef_int) |
31719 | 444 |
apply (insert prems, force) |
445 |
apply (subst res_prime_units_eq, rule refl) |
|
446 |
done |
|
447 |
finally have "fact (p - 1) mod p = \<ominus> \<one>". |
|
448 |
thus ?thesis |
|
449 |
by (simp add: res_to_cong_simps) |
|
450 |
qed |
|
451 |
||
452 |
lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)" |
|
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
453 |
apply (frule prime_gt_1_int) |
31719 | 454 |
apply (case_tac "p = 2") |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
455 |
apply (subst fact_altdef_int, simp) |
31719 | 456 |
apply (subst cong_int_def) |
457 |
apply simp |
|
458 |
apply (rule residues_prime.wilson_theorem1) |
|
459 |
apply (rule residues_prime.intro) |
|
460 |
apply auto |
|
461 |
done |
|
462 |
||
463 |
||
464 |
end |