author | wenzelm |
Tue, 01 Aug 2017 17:33:04 +0200 | |
changeset 66304 | cde6ceffcbc7 |
parent 65899 | ab7d8c999531 |
child 66305 | 7454317f883c |
permissions | -rw-r--r-- |
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 |
|
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
11 |
imports |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
12 |
Cong |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
13 |
"~~/src/HOL/Algebra/More_Group" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
14 |
"~~/src/HOL/Algebra/More_Ring" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
15 |
"~~/src/HOL/Algebra/More_Finite_Product" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
16 |
"~~/src/HOL/Algebra/Multiplicative_Group" |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
17 |
Totient |
31719 | 18 |
begin |
19 |
||
64282
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset
|
20 |
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
|
21 |
"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
|
22 |
|
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset
|
23 |
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
|
24 |
"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
|
25 |
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
|
26 |
else -1)" |
261d42f0bfac
Removed Old_Number_Theory; all theories ported (thanks to Jaime Mendizabal Roche)
eberlm <eberlm@in.tum.de>
parents:
64272
diff
changeset
|
27 |
|
60527 | 28 |
subsection \<open>A locale for residue rings\<close> |
31719 | 29 |
|
60527 | 30 |
definition residue_ring :: "int \<Rightarrow> int ring" |
60528 | 31 |
where |
60527 | 32 |
"residue_ring m = |
33 |
\<lparr>carrier = {0..m - 1}, |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
34 |
monoid.mult = \<lambda>x y. (x * y) mod m, |
60527 | 35 |
one = 1, |
36 |
zero = 0, |
|
37 |
add = \<lambda>x y. (x + y) mod m\<rparr>" |
|
31719 | 38 |
|
39 |
locale residues = |
|
40 |
fixes m :: int and R (structure) |
|
41 |
assumes m_gt_one: "m > 1" |
|
60527 | 42 |
defines "R \<equiv> residue_ring m" |
44872 | 43 |
begin |
31719 | 44 |
|
45 |
lemma abelian_group: "abelian_group R" |
|
65066 | 46 |
proof - |
47 |
have "\<exists>y\<in>{0..m - 1}. (x + y) mod m = 0" if "0 \<le> x" "x < m" for x |
|
48 |
proof (cases "x = 0") |
|
49 |
case True |
|
50 |
with m_gt_one show ?thesis by simp |
|
51 |
next |
|
52 |
case False |
|
53 |
then have "(x + (m - x)) mod m = 0" |
|
54 |
by simp |
|
55 |
with m_gt_one that show ?thesis |
|
56 |
by (metis False atLeastAtMost_iff diff_ge_0_iff_ge diff_left_mono int_one_le_iff_zero_less less_le) |
|
57 |
qed |
|
58 |
with m_gt_one show ?thesis |
|
59 |
by (fastforce simp add: R_def residue_ring_def mod_add_right_eq ac_simps intro!: abelian_groupI) |
|
65899 | 60 |
qed |
31719 | 61 |
|
62 |
lemma comm_monoid: "comm_monoid R" |
|
65066 | 63 |
unfolding R_def residue_ring_def |
31719 | 64 |
apply (rule comm_monoidI) |
65066 | 65 |
using m_gt_one apply auto |
66 |
apply (metis mod_mult_right_eq mult.assoc mult.commute) |
|
67 |
apply (metis mult.commute) |
|
41541 | 68 |
done |
31719 | 69 |
|
70 |
lemma cring: "cring R" |
|
65066 | 71 |
apply (intro cringI abelian_group comm_monoid) |
72 |
unfolding R_def residue_ring_def |
|
73 |
apply (auto simp add: comm_semiring_class.distrib mod_add_eq mod_mult_left_eq) |
|
41541 | 74 |
done |
31719 | 75 |
|
76 |
end |
|
77 |
||
78 |
sublocale residues < cring |
|
79 |
by (rule cring) |
|
80 |
||
81 |
||
41541 | 82 |
context residues |
83 |
begin |
|
31719 | 84 |
|
60527 | 85 |
text \<open> |
86 |
These lemmas translate back and forth between internal and |
|
87 |
external concepts. |
|
88 |
\<close> |
|
31719 | 89 |
|
90 |
lemma res_carrier_eq: "carrier R = {0..m - 1}" |
|
44872 | 91 |
unfolding R_def residue_ring_def by auto |
31719 | 92 |
|
93 |
lemma res_add_eq: "x \<oplus> y = (x + y) mod m" |
|
44872 | 94 |
unfolding R_def residue_ring_def by auto |
31719 | 95 |
|
96 |
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" |
|
44872 | 97 |
unfolding R_def residue_ring_def by auto |
31719 | 98 |
|
99 |
lemma res_zero_eq: "\<zero> = 0" |
|
44872 | 100 |
unfolding R_def residue_ring_def by auto |
31719 | 101 |
|
102 |
lemma res_one_eq: "\<one> = 1" |
|
44872 | 103 |
unfolding R_def residue_ring_def units_of_def by auto |
31719 | 104 |
|
60527 | 105 |
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}" |
65066 | 106 |
using m_gt_one |
107 |
unfolding Units_def R_def residue_ring_def |
|
31719 | 108 |
apply auto |
60527 | 109 |
apply (subgoal_tac "x \<noteq> 0") |
31719 | 110 |
apply auto |
55352 | 111 |
apply (metis invertible_coprime_int) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
112 |
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
|
113 |
apply (auto simp add: cong_int_def mult.commute) |
41541 | 114 |
done |
31719 | 115 |
|
116 |
lemma res_neg_eq: "\<ominus> x = (- x) mod m" |
|
65066 | 117 |
using m_gt_one unfolding R_def a_inv_def m_inv_def residue_ring_def |
118 |
apply simp |
|
31719 | 119 |
apply (rule the_equality) |
65066 | 120 |
apply (simp add: mod_add_right_eq) |
121 |
apply (simp add: add.commute mod_add_right_eq) |
|
122 |
apply (metis add.right_neutral minus_add_cancel mod_add_right_eq mod_pos_pos_trivial) |
|
41541 | 123 |
done |
31719 | 124 |
|
44872 | 125 |
lemma finite [iff]: "finite (carrier R)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
126 |
by (simp add: res_carrier_eq) |
31719 | 127 |
|
44872 | 128 |
lemma finite_Units [iff]: "finite (Units R)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
129 |
by (simp add: finite_ring_finite_units) |
31719 | 130 |
|
60527 | 131 |
text \<open> |
63167 | 132 |
The function \<open>a \<mapsto> a mod m\<close> maps the integers to the |
60527 | 133 |
residue classes. The following lemmas show that this mapping |
134 |
respects addition and multiplication on the integers. |
|
135 |
\<close> |
|
31719 | 136 |
|
60527 | 137 |
lemma mod_in_carrier [iff]: "a mod m \<in> carrier R" |
138 |
unfolding res_carrier_eq |
|
139 |
using insert m_gt_one by auto |
|
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 |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64282
diff
changeset
|
143 |
by (auto simp add: mod_simps) |
31719 | 144 |
|
145 |
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
|
55352 | 146 |
unfolding R_def residue_ring_def |
64593
50c715579715
reoriented congruence rules in non-explosive direction
haftmann
parents:
64282
diff
changeset
|
147 |
by (auto simp add: mod_simps) |
31719 | 148 |
|
149 |
lemma zero_cong: "\<zero> = 0" |
|
44872 | 150 |
unfolding R_def residue_ring_def by auto |
31719 | 151 |
|
152 |
lemma one_cong: "\<one> = 1 mod m" |
|
44872 | 153 |
using m_gt_one unfolding R_def residue_ring_def by auto |
31719 | 154 |
|
60527 | 155 |
(* FIXME revise algebra library to use 1? *) |
31719 | 156 |
lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
65066 | 157 |
using m_gt_one |
31719 | 158 |
apply (induct n) |
41541 | 159 |
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
|
160 |
apply (metis mult.commute mult_cong) |
41541 | 161 |
done |
31719 | 162 |
|
163 |
lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m" |
|
55352 | 164 |
by (metis mod_minus_eq res_neg_eq) |
31719 | 165 |
|
60528 | 166 |
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 | 167 |
by (induct set: finite) (auto simp: one_cong mult_cong) |
31719 | 168 |
|
60528 | 169 |
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 | 170 |
by (induct set: finite) (auto simp: zero_cong add_cong) |
31719 | 171 |
|
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
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
|
176 |
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
|
177 |
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
|
178 |
next |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
179 |
case False |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
180 |
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
|
181 |
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
|
182 |
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
|
183 |
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
|
184 |
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
|
185 |
qed |
31719 | 186 |
|
60528 | 187 |
lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)" |
31719 | 188 |
unfolding cong_int_def by auto |
189 |
||
190 |
||
60528 | 191 |
text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close> |
31719 | 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 |
||
60527 | 195 |
text \<open>Other useful facts about the residue ring.\<close> |
31719 | 196 |
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" |
197 |
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
|
198 |
apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff |
60528 | 199 |
zero_neq_one zmod_zminus1_eq_if) |
41541 | 200 |
done |
31719 | 201 |
|
202 |
end |
|
203 |
||
204 |
||
60527 | 205 |
subsection \<open>Prime residues\<close> |
31719 | 206 |
|
207 |
locale residues_prime = |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
208 |
fixes p :: nat and R (structure) |
31719 | 209 |
assumes p_prime [intro]: "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
210 |
defines "R \<equiv> residue_ring (int p)" |
31719 | 211 |
|
212 |
sublocale residues_prime < residues p |
|
65066 | 213 |
unfolding R_def residues_def |
31719 | 214 |
using p_prime apply auto |
62348 | 215 |
apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) |
41541 | 216 |
done |
31719 | 217 |
|
44872 | 218 |
context residues_prime |
219 |
begin |
|
31719 | 220 |
|
221 |
lemma is_field: "field R" |
|
65066 | 222 |
proof - |
223 |
have "\<And>x. \<lbrakk>gcd x (int p) \<noteq> 1; 0 \<le> x; x < int p\<rbrakk> \<Longrightarrow> x = 0" |
|
224 |
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) |
|
225 |
then show ?thesis |
|
226 |
apply (intro cring.field_intro2 cring) |
|
44872 | 227 |
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) |
65066 | 228 |
done |
229 |
qed |
|
31719 | 230 |
|
231 |
lemma res_prime_units_eq: "Units R = {1..p - 1}" |
|
232 |
apply (subst res_units_eq) |
|
233 |
apply auto |
|
62348 | 234 |
apply (subst gcd.commute) |
55352 | 235 |
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) |
41541 | 236 |
done |
31719 | 237 |
|
238 |
end |
|
239 |
||
240 |
sublocale residues_prime < field |
|
241 |
by (rule is_field) |
|
242 |
||
243 |
||
60527 | 244 |
section \<open>Test cases: Euler's theorem and Wilson's theorem\<close> |
31719 | 245 |
|
60527 | 246 |
subsection \<open>Euler's theorem\<close> |
31719 | 247 |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
248 |
lemma (in residues) totient_eq: |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
249 |
"totient (nat m) = card (Units R)" |
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
250 |
proof - |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
251 |
have *: "inj_on nat (Units R)" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
252 |
by (rule inj_onI) (auto simp add: res_units_eq) |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
253 |
define m' where "m' = nat m" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
254 |
from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
255 |
from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
256 |
unfolding res_units_eq |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
257 |
by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
258 |
hence "Units R = int ` totatives m'" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
259 |
hence "totatives m' = nat ` Units R" by (simp add: image_image) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
260 |
then have "card (totatives (nat m)) = card (nat ` Units R)" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
261 |
by (simp add: m'_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
262 |
also have "\<dots> = card (Units R)" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
263 |
using * card_image [of nat "Units R"] by auto |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
264 |
finally show ?thesis by (simp add: totient_def) |
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
265 |
qed |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
266 |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
267 |
lemma (in residues_prime) totient_eq: "totient p = p - 1" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
268 |
using totient_eq by (simp add: res_prime_units_eq) |
31719 | 269 |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
270 |
lemma (in residues) euler_theorem: |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
271 |
assumes "coprime a m" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
272 |
shows "[a ^ totient (nat m) = 1] (mod m)" |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
273 |
proof - |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
274 |
have "a ^ totient (nat m) mod m = 1 mod m" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
275 |
by (metis assms finite_Units m_gt_one mod_in_res_units one_cong totient_eq pow_cong units_power_order_eq_one) |
65066 | 276 |
then show ?thesis |
277 |
using res_eq_to_cong by blast |
|
31719 | 278 |
qed |
279 |
||
280 |
lemma euler_theorem: |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
281 |
fixes a m :: nat |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
282 |
assumes "coprime a m" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
283 |
shows "[a ^ totient m = 1] (mod m)" |
60527 | 284 |
proof (cases "m = 0 | m = 1") |
285 |
case True |
|
44872 | 286 |
then show ?thesis by auto |
31719 | 287 |
next |
60527 | 288 |
case False |
41541 | 289 |
with assms show ?thesis |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
290 |
using residues.euler_theorem [of "int m" "int a"] transfer_int_nat_cong |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
291 |
by (auto simp add: residues_def transfer_int_nat_gcd(1)) force |
31719 | 292 |
qed |
293 |
||
294 |
lemma fermat_theorem: |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
295 |
fixes p a :: nat |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
296 |
assumes "prime p" and "\<not> p dvd a" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
297 |
shows "[a ^ (p - 1) = 1] (mod p)" |
31719 | 298 |
proof - |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
299 |
from assms prime_imp_coprime [of p a] have "coprime a p" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
300 |
by (auto simp add: ac_simps) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
301 |
then have "[a ^ totient p = 1] (mod p)" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
302 |
by (rule euler_theorem) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
303 |
also have "totient p = p - 1" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
304 |
by (rule totient_prime) (rule assms) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
65416
diff
changeset
|
305 |
finally show ?thesis . |
31719 | 306 |
qed |
307 |
||
308 |
||
60526 | 309 |
subsection \<open>Wilson's theorem\<close> |
31719 | 310 |
|
60527 | 311 |
lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow> |
312 |
{x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}" |
|
31719 | 313 |
apply auto |
55352 | 314 |
apply (metis Units_inv_inv)+ |
41541 | 315 |
done |
31719 | 316 |
|
317 |
lemma (in residues_prime) wilson_theorem1: |
|
318 |
assumes a: "p > 2" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
319 |
shows "[fact (p - 1) = (-1::int)] (mod p)" |
31719 | 320 |
proof - |
60527 | 321 |
let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}" |
322 |
have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs" |
|
31719 | 323 |
by auto |
60527 | 324 |
have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)" |
31732 | 325 |
apply (subst UR) |
31719 | 326 |
apply (subst finprod_Un_disjoint) |
55352 | 327 |
apply (auto intro: funcsetI) |
60527 | 328 |
using inv_one apply auto[1] |
329 |
using inv_eq_neg_one_eq apply auto |
|
31719 | 330 |
done |
60527 | 331 |
also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" |
31719 | 332 |
apply (subst finprod_insert) |
333 |
apply auto |
|
334 |
apply (frule one_eq_neg_one) |
|
60527 | 335 |
using a apply force |
31719 | 336 |
done |
60527 | 337 |
also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))" |
338 |
apply (subst finprod_Union_disjoint) |
|
339 |
apply auto |
|
55352 | 340 |
apply (metis Units_inv_inv)+ |
31719 | 341 |
done |
342 |
also have "\<dots> = \<one>" |
|
60527 | 343 |
apply (rule finprod_one) |
344 |
apply auto |
|
345 |
apply (subst finprod_insert) |
|
346 |
apply auto |
|
55352 | 347 |
apply (metis inv_eq_self) |
31719 | 348 |
done |
60527 | 349 |
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" |
31719 | 350 |
by simp |
60527 | 351 |
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" |
65066 | 352 |
by (rule finprod_cong') (auto simp: res_units_eq) |
60527 | 353 |
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" |
65066 | 354 |
by (rule prod_cong) auto |
31719 | 355 |
also have "\<dots> = fact (p - 1) mod p" |
64272 | 356 |
apply (simp add: fact_prod) |
65066 | 357 |
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
|
358 |
apply (subst res_prime_units_eq) |
64272 | 359 |
apply (simp add: int_prod zmod_int prod_int_eq) |
31719 | 360 |
done |
60527 | 361 |
finally have "fact (p - 1) mod p = \<ominus> \<one>" . |
362 |
then show ?thesis |
|
60528 | 363 |
by (metis of_nat_fact Divides.transfer_int_nat_functions(2) |
364 |
cong_int_def res_neg_eq res_one_eq) |
|
31719 | 365 |
qed |
366 |
||
55352 | 367 |
lemma wilson_theorem: |
60527 | 368 |
assumes "prime p" |
369 |
shows "[fact (p - 1) = - 1] (mod p)" |
|
55352 | 370 |
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
|
371 |
case True |
55352 | 372 |
then show ?thesis |
64272 | 373 |
by (simp add: cong_int_def fact_prod) |
55352 | 374 |
next |
375 |
case False |
|
376 |
then show ?thesis |
|
377 |
using assms prime_ge_2_nat |
|
378 |
by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) |
|
379 |
qed |
|
31719 | 380 |
|
66304 | 381 |
text \<open> |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
382 |
This result can be transferred to the multiplicative group of |
66304 | 383 |
$\mathbb{Z}/p\mathbb{Z}$ for $p$ prime.\<close> |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
384 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
385 |
lemma mod_nat_int_pow_eq: |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
386 |
fixes n :: nat and p a :: int |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
387 |
assumes "a \<ge> 0" "p \<ge> 0" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
388 |
shows "(nat a ^ n) mod (nat p) = nat ((a ^ n) mod p)" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
389 |
using assms |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
390 |
by (simp add: int_one_le_iff_zero_less nat_mod_distrib order_less_imp_le nat_power_eq[symmetric]) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
391 |
|
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
392 |
theorem residue_prime_mult_group_has_gen : |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
393 |
fixes p :: nat |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
394 |
assumes prime_p : "prime p" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
395 |
shows "\<exists>a \<in> {1 .. p - 1}. {1 .. p - 1} = {a^i mod p|i . i \<in> UNIV}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
396 |
proof - |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
397 |
have "p\<ge>2" using prime_gt_1_nat[OF prime_p] by simp |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
398 |
interpret R:residues_prime "p" "residue_ring p" unfolding residues_prime_def |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
399 |
by (simp add: prime_p) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
400 |
have car: "carrier (residue_ring (int p)) - {\<zero>\<^bsub>residue_ring (int p)\<^esub>} = {1 .. int p - 1}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
401 |
by (auto simp add: R.zero_cong R.res_carrier_eq) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
402 |
obtain a where a:"a \<in> {1 .. int p - 1}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
403 |
and a_gen:"{1 .. int p - 1} = {a(^)\<^bsub>residue_ring (int p)\<^esub>i|i::nat . i \<in> UNIV}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
404 |
apply atomize_elim using field.finite_field_mult_group_has_gen[OF R.is_field] |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
405 |
by (auto simp add: car[symmetric] carrier_mult_of) |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
406 |
{ fix x fix i :: nat assume x: "x \<in> {1 .. int p - 1}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
407 |
hence "x (^)\<^bsub>residue_ring (int p)\<^esub> i = x ^ i mod (int p)" using R.pow_cong[of x i] by auto} |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
408 |
note * = this |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
409 |
have **:"nat ` {1 .. int p - 1} = {1 .. p - 1}" (is "?L = ?R") |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
410 |
proof |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
411 |
{ fix n assume n: "n \<in> ?L" |
66304 | 412 |
then have "n \<in> ?R" using \<open>p\<ge>2\<close> by force |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
413 |
} thus "?L \<subseteq> ?R" by blast |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
414 |
{ fix n assume n: "n \<in> ?R" |
66304 | 415 |
then have "n \<in> ?L" using \<open>p\<ge>2\<close> Set_Interval.transfer_nat_int_set_functions(2) by fastforce |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
416 |
} thus "?R \<subseteq> ?L" by blast |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
417 |
qed |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
418 |
have "nat ` {a^i mod (int p) | i::nat. i \<in> UNIV} = {nat a^i mod p | i . i \<in> UNIV}" (is "?L = ?R") |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
419 |
proof |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
420 |
{ fix x assume x: "x \<in> ?L" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
421 |
then obtain i where i:"x = nat (a^i mod (int p))" by blast |
66304 | 422 |
hence "x = nat a ^ i mod p" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
423 |
hence "x \<in> ?R" using i by blast |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
424 |
} thus "?L \<subseteq> ?R" by blast |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
425 |
{ fix x assume x: "x \<in> ?R" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
426 |
then obtain i where i:"x = nat a^i mod p" by blast |
66304 | 427 |
hence "x \<in> ?L" using mod_nat_int_pow_eq[of a "int p" i] a \<open>p\<ge>2\<close> by auto |
65416
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
428 |
} thus "?R \<subseteq> ?L" by blast |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
429 |
qed |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
430 |
hence "{1 .. p - 1} = {nat a^i mod p | i. i \<in> UNIV}" |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
431 |
using * a a_gen ** by presburger |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
432 |
moreover |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
433 |
have "nat a \<in> {1 .. p - 1}" using a by force |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
434 |
ultimately show ?thesis .. |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
435 |
qed |
f707dbcf11e3
more approproiate placement of theories MiscAlgebra and Multiplicate_Group
haftmann
parents:
65066
diff
changeset
|
436 |
|
31719 | 437 |
end |