14 MiscAlgebra |
14 MiscAlgebra |
15 begin |
15 begin |
16 |
16 |
17 |
17 |
18 (* |
18 (* |
19 |
19 |
20 A locale for residue rings |
20 A locale for residue rings |
21 |
21 |
22 *) |
22 *) |
23 |
23 |
24 definition residue_ring :: "int => int ring" where |
24 definition residue_ring :: "int => int ring" where |
25 "residue_ring m == (| |
25 "residue_ring m == (| |
26 carrier = {0..m - 1}, |
26 carrier = {0..m - 1}, |
27 mult = (%x y. (x * y) mod m), |
27 mult = (%x y. (x * y) mod m), |
28 one = 1, |
28 one = 1, |
29 zero = 0, |
29 zero = 0, |
30 add = (%x y. (x + y) mod m) |)" |
30 add = (%x y. (x + y) mod m) |)" |
31 |
31 |
32 locale residues = |
32 locale residues = |
33 fixes m :: int and R (structure) |
33 fixes m :: int and R (structure) |
34 assumes m_gt_one: "m > 1" |
34 assumes m_gt_one: "m > 1" |
35 defines "R == residue_ring m" |
35 defines "R == residue_ring m" |
36 |
36 |
37 context residues begin |
37 context residues |
|
38 begin |
38 |
39 |
39 lemma abelian_group: "abelian_group R" |
40 lemma abelian_group: "abelian_group R" |
40 apply (insert m_gt_one) |
41 apply (insert m_gt_one) |
41 apply (rule abelian_groupI) |
42 apply (rule abelian_groupI) |
42 apply (unfold R_def residue_ring_def) |
43 apply (unfold R_def residue_ring_def) |
77 |
78 |
78 |
79 |
79 context residues |
80 context residues |
80 begin |
81 begin |
81 |
82 |
82 (* These lemmas translate back and forth between internal and |
83 (* These lemmas translate back and forth between internal and |
83 external concepts *) |
84 external concepts *) |
84 |
85 |
85 lemma res_carrier_eq: "carrier R = {0..m - 1}" |
86 lemma res_carrier_eq: "carrier R = {0..m - 1}" |
86 by (unfold R_def residue_ring_def, auto) |
87 unfolding R_def residue_ring_def by auto |
87 |
88 |
88 lemma res_add_eq: "x \<oplus> y = (x + y) mod m" |
89 lemma res_add_eq: "x \<oplus> y = (x + y) mod m" |
89 by (unfold R_def residue_ring_def, auto) |
90 unfolding R_def residue_ring_def by auto |
90 |
91 |
91 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" |
92 lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" |
92 by (unfold R_def residue_ring_def, auto) |
93 unfolding R_def residue_ring_def by auto |
93 |
94 |
94 lemma res_zero_eq: "\<zero> = 0" |
95 lemma res_zero_eq: "\<zero> = 0" |
95 by (unfold R_def residue_ring_def, auto) |
96 unfolding R_def residue_ring_def by auto |
96 |
97 |
97 lemma res_one_eq: "\<one> = 1" |
98 lemma res_one_eq: "\<one> = 1" |
98 by (unfold R_def residue_ring_def units_of_def, auto) |
99 unfolding R_def residue_ring_def units_of_def by auto |
99 |
100 |
100 lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}" |
101 lemma res_units_eq: "Units R = { x. 0 < x & x < m & coprime x m}" |
101 apply (insert m_gt_one) |
102 apply (insert m_gt_one) |
102 apply (unfold Units_def R_def residue_ring_def) |
103 apply (unfold Units_def R_def residue_ring_def) |
103 apply auto |
104 apply auto |
125 apply simp |
126 apply simp |
126 apply (subst zmod_eq_dvd_iff) |
127 apply (subst zmod_eq_dvd_iff) |
127 apply auto |
128 apply auto |
128 done |
129 done |
129 |
130 |
130 lemma finite [iff]: "finite(carrier R)" |
131 lemma finite [iff]: "finite (carrier R)" |
131 by (subst res_carrier_eq, auto) |
132 by (subst res_carrier_eq, auto) |
132 |
133 |
133 lemma finite_Units [iff]: "finite(Units R)" |
134 lemma finite_Units [iff]: "finite (Units R)" |
134 by (subst res_units_eq, auto) |
135 by (subst res_units_eq, auto) |
135 |
136 |
136 (* The function a -> a mod m maps the integers to the |
137 (* The function a -> a mod m maps the integers to the |
137 residue classes. The following lemmas show that this mapping |
138 residue classes. The following lemmas show that this mapping |
138 respects addition and multiplication on the integers. *) |
139 respects addition and multiplication on the integers. *) |
139 |
140 |
140 lemma mod_in_carrier [iff]: "a mod m : carrier R" |
141 lemma mod_in_carrier [iff]: "a mod m : carrier R" |
141 apply (unfold res_carrier_eq) |
142 apply (unfold res_carrier_eq) |
142 apply (insert m_gt_one, auto) |
143 apply (insert m_gt_one, auto) |
143 done |
144 done |
144 |
145 |
145 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
146 lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
146 by (unfold R_def residue_ring_def, auto, arith) |
147 unfolding R_def residue_ring_def |
|
148 apply auto |
|
149 apply presburger |
|
150 done |
147 |
151 |
148 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
152 lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
149 apply (unfold R_def residue_ring_def, auto) |
153 apply (unfold R_def residue_ring_def, auto) |
150 apply (subst zmod_zmult1_eq [symmetric]) |
154 apply (subst zmod_zmult1_eq [symmetric]) |
151 apply (subst mult_commute) |
155 apply (subst mult_commute) |
153 apply (subst mult_commute) |
157 apply (subst mult_commute) |
154 apply auto |
158 apply auto |
155 done |
159 done |
156 |
160 |
157 lemma zero_cong: "\<zero> = 0" |
161 lemma zero_cong: "\<zero> = 0" |
158 apply (unfold R_def residue_ring_def, auto) |
162 unfolding R_def residue_ring_def by auto |
159 done |
|
160 |
163 |
161 lemma one_cong: "\<one> = 1 mod m" |
164 lemma one_cong: "\<one> = 1 mod m" |
162 apply (insert m_gt_one) |
165 using m_gt_one unfolding R_def residue_ring_def by auto |
163 apply (unfold R_def residue_ring_def, auto) |
|
164 done |
|
165 |
166 |
166 (* revise algebra library to use 1? *) |
167 (* revise algebra library to use 1? *) |
167 lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
168 lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
168 apply (insert m_gt_one) |
169 apply (insert m_gt_one) |
169 apply (induct n) |
170 apply (induct n) |
179 apply (subst add_cong) |
180 apply (subst add_cong) |
180 apply (subst zero_cong) |
181 apply (subst zero_cong) |
181 apply auto |
182 apply auto |
182 done |
183 done |
183 |
184 |
184 lemma (in residues) prod_cong: |
185 lemma (in residues) prod_cong: |
185 "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m" |
186 "finite A \<Longrightarrow> (\<Otimes> i:A. (f i) mod m) = (PROD i:A. f i) mod m" |
186 apply (induct set: finite) |
187 apply (induct set: finite) |
187 apply (auto simp: one_cong mult_cong) |
188 apply (auto simp: one_cong mult_cong) |
188 done |
189 done |
189 |
190 |
190 lemma (in residues) sum_cong: |
191 lemma (in residues) sum_cong: |
191 "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m" |
192 "finite A \<Longrightarrow> (\<Oplus> i:A. (f i) mod m) = (SUM i: A. f i) mod m" |
192 apply (induct set: finite) |
193 apply (induct set: finite) |
193 apply (auto simp: zero_cong add_cong) |
194 apply (auto simp: zero_cong add_cong) |
194 done |
195 done |
195 |
196 |
196 lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> |
197 lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> |
197 a mod m : Units R" |
198 a mod m : Units R" |
198 apply (subst res_units_eq, auto) |
199 apply (subst res_units_eq, auto) |
199 apply (insert pos_mod_sign [of m a]) |
200 apply (insert pos_mod_sign [of m a]) |
200 apply (subgoal_tac "a mod m ~= 0") |
201 apply (subgoal_tac "a mod m ~= 0") |
201 apply arith |
202 apply arith |
202 apply auto |
203 apply auto |
203 apply (subst (asm) gcd_red_int) |
204 apply (subst (asm) gcd_red_int) |
204 apply (subst gcd_commute_int, assumption) |
205 apply (subst gcd_commute_int, assumption) |
205 done |
206 done |
206 |
207 |
207 lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" |
208 lemma res_eq_to_cong: "((a mod m) = (b mod m)) = [a = b] (mod (m::int))" |
208 unfolding cong_int_def by auto |
209 unfolding cong_int_def by auto |
209 |
210 |
210 (* Simplifying with these will translate a ring equation in R to a |
211 (* Simplifying with these will translate a ring equation in R to a |
211 congruence. *) |
212 congruence. *) |
212 |
213 |
213 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong |
214 lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong |
214 prod_cong sum_cong neg_cong res_eq_to_cong |
215 prod_cong sum_cong neg_cong res_eq_to_cong |
215 |
216 |
241 sublocale residues_prime < residues p |
242 sublocale residues_prime < residues p |
242 apply (unfold R_def residues_def) |
243 apply (unfold R_def residues_def) |
243 using p_prime apply auto |
244 using p_prime apply auto |
244 done |
245 done |
245 |
246 |
246 context residues_prime begin |
247 context residues_prime |
|
248 begin |
247 |
249 |
248 lemma is_field: "field R" |
250 lemma is_field: "field R" |
249 apply (rule cring.field_intro2) |
251 apply (rule cring.field_intro2) |
250 apply (rule cring) |
252 apply (rule cring) |
251 apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq |
253 apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) |
252 res_units_eq) |
|
253 apply (rule classical) |
254 apply (rule classical) |
254 apply (erule notE) |
255 apply (erule notE) |
255 apply (subst gcd_commute_int) |
256 apply (subst gcd_commute_int) |
256 apply (rule prime_imp_coprime_int) |
257 apply (rule prime_imp_coprime_int) |
257 apply (rule p_prime) |
258 apply (rule p_prime) |
283 |
284 |
284 subsection{* Euler's theorem *} |
285 subsection{* Euler's theorem *} |
285 |
286 |
286 (* the definition of the phi function *) |
287 (* the definition of the phi function *) |
287 |
288 |
288 definition phi :: "int => nat" where |
289 definition phi :: "int => nat" |
289 "phi m == card({ x. 0 < x & x < m & gcd x m = 1})" |
290 where "phi m = card({ x. 0 < x & x < m & gcd x m = 1})" |
290 |
291 |
291 lemma phi_zero [simp]: "phi 0 = 0" |
292 lemma phi_zero [simp]: "phi 0 = 0" |
292 apply (subst phi_def) |
293 apply (subst phi_def) |
293 (* Auto hangs here. Once again, where is the simplification rule |
294 (* Auto hangs here. Once again, where is the simplification rule |
294 1 == Suc 0 coming from? *) |
295 1 == Suc 0 coming from? *) |
295 apply (auto simp add: card_eq_0_iff) |
296 apply (auto simp add: card_eq_0_iff) |
296 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) |
297 (* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) |
297 done |
298 done |
298 |
299 |
299 lemma phi_one [simp]: "phi 1 = 0" |
300 lemma phi_one [simp]: "phi 1 = 0" |
300 apply (auto simp add: phi_def card_eq_0_iff) |
301 by (auto simp add: phi_def card_eq_0_iff) |
301 done |
|
302 |
302 |
303 lemma (in residues) phi_eq: "phi m = card(Units R)" |
303 lemma (in residues) phi_eq: "phi m = card(Units R)" |
304 by (simp add: phi_def res_units_eq) |
304 by (simp add: phi_def res_units_eq) |
305 |
305 |
306 lemma (in residues) euler_theorem1: |
306 lemma (in residues) euler_theorem1: |
307 assumes a: "gcd a m = 1" |
307 assumes a: "gcd a m = 1" |
308 shows "[a^phi m = 1] (mod m)" |
308 shows "[a^phi m = 1] (mod m)" |
309 proof - |
309 proof - |
310 from a m_gt_one have [simp]: "a mod m : Units R" |
310 from a m_gt_one have [simp]: "a mod m : Units R" |
311 by (intro mod_in_res_units) |
311 by (intro mod_in_res_units) |
312 from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" |
312 from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" |
313 by simp |
313 by simp |
314 also have "\<dots> = \<one>" |
314 also have "\<dots> = \<one>" |
315 by (intro units_power_order_eq_one, auto) |
315 by (intro units_power_order_eq_one, auto) |
316 finally show ?thesis |
316 finally show ?thesis |
317 by (simp add: res_to_cong_simps) |
317 by (simp add: res_to_cong_simps) |
318 qed |
318 qed |
319 |
319 |
320 (* In fact, there is a two line proof! |
320 (* In fact, there is a two line proof! |
321 |
321 |
322 lemma (in residues) euler_theorem1: |
322 lemma (in residues) euler_theorem1: |
323 assumes a: "gcd a m = 1" |
323 assumes a: "gcd a m = 1" |
324 shows "[a^phi m = 1] (mod m)" |
324 shows "[a^phi m = 1] (mod m)" |
325 proof - |
325 proof - |
326 have "(a mod m) (^) (phi m) = \<one>" |
326 have "(a mod m) (^) (phi m) = \<one>" |
327 by (simp add: phi_eq units_power_order_eq_one a m_gt_one) |
327 by (simp add: phi_eq units_power_order_eq_one a m_gt_one) |
328 thus ?thesis |
328 then show ?thesis |
329 by (simp add: res_to_cong_simps) |
329 by (simp add: res_to_cong_simps) |
330 qed |
330 qed |
331 |
331 |
332 *) |
332 *) |
333 |
333 |
336 lemma euler_theorem: |
336 lemma euler_theorem: |
337 assumes "m >= 0" and "gcd a m = 1" |
337 assumes "m >= 0" and "gcd a m = 1" |
338 shows "[a^phi m = 1] (mod m)" |
338 shows "[a^phi m = 1] (mod m)" |
339 proof (cases) |
339 proof (cases) |
340 assume "m = 0 | m = 1" |
340 assume "m = 0 | m = 1" |
341 thus ?thesis by auto |
341 then show ?thesis by auto |
342 next |
342 next |
343 assume "~(m = 0 | m = 1)" |
343 assume "~(m = 0 | m = 1)" |
344 with assms show ?thesis |
344 with assms show ?thesis |
345 by (intro residues.euler_theorem1, unfold residues_def, auto) |
345 by (intro residues.euler_theorem1, unfold residues_def, auto) |
346 qed |
346 qed |
388 |
388 |
389 lemma (in residues_prime) wilson_theorem1: |
389 lemma (in residues_prime) wilson_theorem1: |
390 assumes a: "p > 2" |
390 assumes a: "p > 2" |
391 shows "[fact (p - 1) = - 1] (mod p)" |
391 shows "[fact (p - 1) = - 1] (mod p)" |
392 proof - |
392 proof - |
393 let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" |
393 let ?InversePairs = "{ {x, inv x} | x. x : Units R - {\<one>, \<ominus> \<one>}}" |
394 have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)" |
394 have UR: "Units R = {\<one>, \<ominus> \<one>} Un (Union ?InversePairs)" |
395 by auto |
395 by auto |
396 have "(\<Otimes>i: Units R. i) = |
396 have "(\<Otimes>i: Units R. i) = |
397 (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)" |
397 (\<Otimes>i: {\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i: Union ?InversePairs. i)" |
398 apply (subst UR) |
398 apply (subst UR) |
399 apply (subst finprod_Un_disjoint) |
399 apply (subst finprod_Un_disjoint) |
400 apply (auto intro:funcsetI) |
400 apply (auto intro:funcsetI) |
401 apply (drule sym, subst (asm) inv_eq_one_eq) |
401 apply (drule sym, subst (asm) inv_eq_one_eq) |
407 apply (subst finprod_insert) |
407 apply (subst finprod_insert) |
408 apply auto |
408 apply auto |
409 apply (frule one_eq_neg_one) |
409 apply (frule one_eq_neg_one) |
410 apply (insert a, force) |
410 apply (insert a, force) |
411 done |
411 done |
412 also have "(\<Otimes>i:(Union ?InversePairs). i) = |
412 also have "(\<Otimes>i:(Union ?InversePairs). i) = |
413 (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))" |
413 (\<Otimes>A: ?InversePairs. (\<Otimes>y:A. y))" |
414 apply (subst finprod_Union_disjoint) |
414 apply (subst finprod_Union_disjoint) |
415 apply force |
415 apply force |
416 apply force |
416 apply force |
417 apply clarify |
417 apply clarify |
442 apply (subst fact_altdef_int) |
442 apply (subst fact_altdef_int) |
443 apply (insert assms, force) |
443 apply (insert assms, force) |
444 apply (subst res_prime_units_eq, rule refl) |
444 apply (subst res_prime_units_eq, rule refl) |
445 done |
445 done |
446 finally have "fact (p - 1) mod p = \<ominus> \<one>". |
446 finally have "fact (p - 1) mod p = \<ominus> \<one>". |
447 thus ?thesis |
447 then show ?thesis by (simp add: res_to_cong_simps) |
448 by (simp add: res_to_cong_simps) |
|
449 qed |
448 qed |
450 |
449 |
451 lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)" |
450 lemma wilson_theorem: "prime (p::int) \<Longrightarrow> [fact (p - 1) = - 1] (mod p)" |
452 apply (frule prime_gt_1_int) |
451 apply (frule prime_gt_1_int) |
453 apply (case_tac "p = 2") |
452 apply (case_tac "p = 2") |