author | eberlm <eberlm@in.tum.de> |
Thu, 21 Jul 2016 10:06:04 +0200 | |
changeset 63534 | 523b488b15c9 |
parent 63417 | c184ec919c70 |
child 63537 | 831816778409 |
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 |
|
59667
651ea265d568
Removal of the file HOL/Number_Theory/Binomial!! And class field_char_0 now declared in Int.thy
paulson <lp15@cam.ac.uk>
parents:
58889
diff
changeset
|
11 |
imports UniqueFactorization MiscAlgebra |
31719 | 12 |
begin |
13 |
||
60527 | 14 |
subsection \<open>A locale for residue rings\<close> |
31719 | 15 |
|
60527 | 16 |
definition residue_ring :: "int \<Rightarrow> int ring" |
60528 | 17 |
where |
60527 | 18 |
"residue_ring m = |
19 |
\<lparr>carrier = {0..m - 1}, |
|
20 |
mult = \<lambda>x y. (x * y) mod m, |
|
21 |
one = 1, |
|
22 |
zero = 0, |
|
23 |
add = \<lambda>x y. (x + y) mod m\<rparr>" |
|
31719 | 24 |
|
25 |
locale residues = |
|
26 |
fixes m :: int and R (structure) |
|
27 |
assumes m_gt_one: "m > 1" |
|
60527 | 28 |
defines "R \<equiv> residue_ring m" |
44872 | 29 |
begin |
31719 | 30 |
|
31 |
lemma abelian_group: "abelian_group R" |
|
32 |
apply (insert m_gt_one) |
|
33 |
apply (rule abelian_groupI) |
|
34 |
apply (unfold R_def residue_ring_def) |
|
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
35 |
apply (auto simp add: mod_add_right_eq [symmetric] ac_simps) |
31719 | 36 |
apply (case_tac "x = 0") |
37 |
apply force |
|
38 |
apply (subgoal_tac "(x + (m - x)) mod m = 0") |
|
39 |
apply (erule bexI) |
|
40 |
apply auto |
|
41541 | 41 |
done |
31719 | 42 |
|
43 |
lemma comm_monoid: "comm_monoid R" |
|
44 |
apply (insert m_gt_one) |
|
45 |
apply (unfold R_def residue_ring_def) |
|
46 |
apply (rule comm_monoidI) |
|
47 |
apply auto |
|
48 |
apply (subgoal_tac "x * y mod m * z mod m = z * (x * y mod m) mod m") |
|
49 |
apply (erule ssubst) |
|
47163 | 50 |
apply (subst mod_mult_right_eq [symmetric])+ |
57514
bdc2c6b40bf2
prefer ac_simps collections over separate name bindings for add and mult
haftmann
parents:
57512
diff
changeset
|
51 |
apply (simp_all only: ac_simps) |
41541 | 52 |
done |
31719 | 53 |
|
54 |
lemma cring: "cring R" |
|
55 |
apply (rule cringI) |
|
56 |
apply (rule abelian_group) |
|
57 |
apply (rule comm_monoid) |
|
58 |
apply (unfold R_def residue_ring_def, auto) |
|
59 |
apply (subst mod_add_eq [symmetric]) |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset
|
60 |
apply (subst mult.commute) |
47163 | 61 |
apply (subst mod_mult_right_eq [symmetric]) |
36350 | 62 |
apply (simp add: field_simps) |
41541 | 63 |
done |
31719 | 64 |
|
65 |
end |
|
66 |
||
67 |
sublocale residues < cring |
|
68 |
by (rule cring) |
|
69 |
||
70 |
||
41541 | 71 |
context residues |
72 |
begin |
|
31719 | 73 |
|
60527 | 74 |
text \<open> |
75 |
These lemmas translate back and forth between internal and |
|
76 |
external concepts. |
|
77 |
\<close> |
|
31719 | 78 |
|
79 |
lemma res_carrier_eq: "carrier R = {0..m - 1}" |
|
44872 | 80 |
unfolding R_def residue_ring_def by auto |
31719 | 81 |
|
82 |
lemma res_add_eq: "x \<oplus> y = (x + y) mod m" |
|
44872 | 83 |
unfolding R_def residue_ring_def by auto |
31719 | 84 |
|
85 |
lemma res_mult_eq: "x \<otimes> y = (x * y) mod m" |
|
44872 | 86 |
unfolding R_def residue_ring_def by auto |
31719 | 87 |
|
88 |
lemma res_zero_eq: "\<zero> = 0" |
|
44872 | 89 |
unfolding R_def residue_ring_def by auto |
31719 | 90 |
|
91 |
lemma res_one_eq: "\<one> = 1" |
|
44872 | 92 |
unfolding R_def residue_ring_def units_of_def by auto |
31719 | 93 |
|
60527 | 94 |
lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}" |
31719 | 95 |
apply (insert m_gt_one) |
96 |
apply (unfold Units_def R_def residue_ring_def) |
|
97 |
apply auto |
|
60527 | 98 |
apply (subgoal_tac "x \<noteq> 0") |
31719 | 99 |
apply auto |
55352 | 100 |
apply (metis invertible_coprime_int) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
101 |
apply (subst (asm) coprime_iff_invertible'_int) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset
|
102 |
apply (auto simp add: cong_int_def mult.commute) |
41541 | 103 |
done |
31719 | 104 |
|
105 |
lemma res_neg_eq: "\<ominus> x = (- x) mod m" |
|
106 |
apply (insert m_gt_one) |
|
107 |
apply (unfold R_def a_inv_def m_inv_def residue_ring_def) |
|
108 |
apply auto |
|
109 |
apply (rule the_equality) |
|
110 |
apply auto |
|
111 |
apply (subst mod_add_right_eq [symmetric]) |
|
112 |
apply auto |
|
113 |
apply (subst mod_add_left_eq [symmetric]) |
|
114 |
apply auto |
|
115 |
apply (subgoal_tac "y mod m = - x mod m") |
|
116 |
apply simp |
|
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset
|
117 |
apply (metis minus_add_cancel mod_mult_self1 mult.commute) |
41541 | 118 |
done |
31719 | 119 |
|
44872 | 120 |
lemma finite [iff]: "finite (carrier R)" |
60527 | 121 |
by (subst res_carrier_eq) auto |
31719 | 122 |
|
44872 | 123 |
lemma finite_Units [iff]: "finite (Units R)" |
50027
7747a9f4c358
adjusting proofs as the set_comprehension_pointfree simproc breaks some existing proofs
bulwahn
parents:
47163
diff
changeset
|
124 |
by (subst res_units_eq) auto |
31719 | 125 |
|
60527 | 126 |
text \<open> |
63167 | 127 |
The function \<open>a \<mapsto> a mod m\<close> maps the integers to the |
60527 | 128 |
residue classes. The following lemmas show that this mapping |
129 |
respects addition and multiplication on the integers. |
|
130 |
\<close> |
|
31719 | 131 |
|
60527 | 132 |
lemma mod_in_carrier [iff]: "a mod m \<in> carrier R" |
133 |
unfolding res_carrier_eq |
|
134 |
using insert m_gt_one by auto |
|
31719 | 135 |
|
136 |
lemma add_cong: "(x mod m) \<oplus> (y mod m) = (x + y) mod m" |
|
44872 | 137 |
unfolding R_def residue_ring_def |
138 |
apply auto |
|
139 |
apply presburger |
|
140 |
done |
|
31719 | 141 |
|
142 |
lemma mult_cong: "(x mod m) \<otimes> (y mod m) = (x * y) mod m" |
|
55352 | 143 |
unfolding R_def residue_ring_def |
144 |
by auto (metis mod_mult_eq) |
|
31719 | 145 |
|
146 |
lemma zero_cong: "\<zero> = 0" |
|
44872 | 147 |
unfolding R_def residue_ring_def by auto |
31719 | 148 |
|
149 |
lemma one_cong: "\<one> = 1 mod m" |
|
44872 | 150 |
using m_gt_one unfolding R_def residue_ring_def by auto |
31719 | 151 |
|
60527 | 152 |
(* FIXME revise algebra library to use 1? *) |
31719 | 153 |
lemma pow_cong: "(x mod m) (^) n = x^n mod m" |
154 |
apply (insert m_gt_one) |
|
155 |
apply (induct n) |
|
41541 | 156 |
apply (auto simp add: nat_pow_def one_cong) |
57512
cc97b347b301
reduced name variants for assoc and commute on plus and mult
haftmann
parents:
55352
diff
changeset
|
157 |
apply (metis mult.commute mult_cong) |
41541 | 158 |
done |
31719 | 159 |
|
160 |
lemma neg_cong: "\<ominus> (x mod m) = (- x) mod m" |
|
55352 | 161 |
by (metis mod_minus_eq res_neg_eq) |
31719 | 162 |
|
60528 | 163 |
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 | 164 |
by (induct set: finite) (auto simp: one_cong mult_cong) |
31719 | 165 |
|
60528 | 166 |
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 | 167 |
by (induct set: finite) (auto simp: zero_cong add_cong) |
31719 | 168 |
|
60688
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
169 |
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
|
170 |
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
|
171 |
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
|
172 |
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
|
173 |
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
|
174 |
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
|
175 |
next |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
176 |
case False |
01488b559910
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead
haftmann
parents:
60528
diff
changeset
|
177 |
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
|
178 |
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
|
179 |
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
|
180 |
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
|
181 |
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
|
182 |
qed |
31719 | 183 |
|
60528 | 184 |
lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)" |
31719 | 185 |
unfolding cong_int_def by auto |
186 |
||
187 |
||
60528 | 188 |
text \<open>Simplifying with these will translate a ring equation in R to a congruence.\<close> |
31719 | 189 |
lemmas res_to_cong_simps = add_cong mult_cong pow_cong one_cong |
190 |
prod_cong sum_cong neg_cong res_eq_to_cong |
|
191 |
||
60527 | 192 |
text \<open>Other useful facts about the residue ring.\<close> |
31719 | 193 |
lemma one_eq_neg_one: "\<one> = \<ominus> \<one> \<Longrightarrow> m = 2" |
194 |
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
|
195 |
apply (metis add.commute add_diff_cancel mod_mod_trivial one_add_one uminus_add_conv_diff |
60528 | 196 |
zero_neq_one zmod_zminus1_eq_if) |
41541 | 197 |
done |
31719 | 198 |
|
199 |
end |
|
200 |
||
201 |
||
60527 | 202 |
subsection \<open>Prime residues\<close> |
31719 | 203 |
|
204 |
locale residues_prime = |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
205 |
fixes p :: nat and R (structure) |
31719 | 206 |
assumes p_prime [intro]: "prime p" |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
207 |
defines "R \<equiv> residue_ring (int p)" |
31719 | 208 |
|
209 |
sublocale residues_prime < residues p |
|
210 |
apply (unfold R_def residues_def) |
|
211 |
using p_prime apply auto |
|
62348 | 212 |
apply (metis (full_types) of_nat_1 of_nat_less_iff prime_gt_1_nat) |
41541 | 213 |
done |
31719 | 214 |
|
44872 | 215 |
context residues_prime |
216 |
begin |
|
31719 | 217 |
|
218 |
lemma is_field: "field R" |
|
219 |
apply (rule cring.field_intro2) |
|
220 |
apply (rule cring) |
|
44872 | 221 |
apply (auto simp add: res_carrier_eq res_one_eq res_zero_eq res_units_eq) |
31719 | 222 |
apply (rule classical) |
223 |
apply (erule notE) |
|
62348 | 224 |
apply (subst gcd.commute) |
31952
40501bb2d57c
renamed lemmas: nat_xyz/int_xyz -> xyz_nat/xyz_int
nipkow
parents:
31798
diff
changeset
|
225 |
apply (rule prime_imp_coprime_int) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
226 |
apply (simp add: p_prime) |
31719 | 227 |
apply (rule notI) |
228 |
apply (frule zdvd_imp_le) |
|
229 |
apply auto |
|
41541 | 230 |
done |
31719 | 231 |
|
232 |
lemma res_prime_units_eq: "Units R = {1..p - 1}" |
|
233 |
apply (subst res_units_eq) |
|
234 |
apply auto |
|
62348 | 235 |
apply (subst gcd.commute) |
55352 | 236 |
apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless) |
41541 | 237 |
done |
31719 | 238 |
|
239 |
end |
|
240 |
||
241 |
sublocale residues_prime < field |
|
242 |
by (rule is_field) |
|
243 |
||
244 |
||
60527 | 245 |
section \<open>Test cases: Euler's theorem and Wilson's theorem\<close> |
31719 | 246 |
|
60527 | 247 |
subsection \<open>Euler's theorem\<close> |
31719 | 248 |
|
60527 | 249 |
text \<open>The definition of the phi function.\<close> |
31719 | 250 |
|
60527 | 251 |
definition phi :: "int \<Rightarrow> nat" |
252 |
where "phi m = card {x. 0 < x \<and> x < m \<and> gcd x m = 1}" |
|
31719 | 253 |
|
60527 | 254 |
lemma phi_def_nat: "phi m = card {x. 0 < x \<and> x < nat m \<and> gcd x (nat m) = 1}" |
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
255 |
apply (simp add: phi_def) |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
256 |
apply (rule bij_betw_same_card [of nat]) |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
257 |
apply (auto simp add: inj_on_def bij_betw_def image_def) |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
258 |
apply (metis dual_order.irrefl dual_order.strict_trans leI nat_1 transfer_nat_int_gcd(1)) |
62348 | 259 |
apply (metis One_nat_def of_nat_0 of_nat_1 of_nat_less_0_iff int_nat_eq nat_int |
260 |
transfer_int_nat_gcd(1) of_nat_less_iff) |
|
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
261 |
done |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
262 |
|
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
263 |
lemma prime_phi: |
60527 | 264 |
assumes "2 \<le> p" "phi p = p - 1" |
265 |
shows "prime p" |
|
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
266 |
proof - |
60528 | 267 |
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
|
268 |
using assms unfolding phi_def_nat |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
269 |
by (intro card_seteq) fastforce+ |
60528 | 270 |
have False if **: "1 < x" "x < p" and "x dvd p" for x :: nat |
60527 | 271 |
proof - |
60528 | 272 |
from * have cop: "x \<in> {1..p - 1} \<Longrightarrow> coprime x p" |
273 |
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
|
274 |
have "coprime x p" |
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
275 |
apply (rule cop) |
60528 | 276 |
using ** apply auto |
55261
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
277 |
done |
60527 | 278 |
with \<open>x dvd p\<close> \<open>1 < x\<close> show ?thesis |
279 |
by auto |
|
280 |
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
|
281 |
then show ?thesis |
60526 | 282 |
using \<open>2 \<le> p\<close> |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
283 |
by (simp add: is_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
|
284 |
(metis One_nat_def dvd_pos_nat nat_dvd_not_less nat_neq_iff not_gr0 |
55352 | 285 |
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
|
286 |
qed |
ad3604df6bc6
new lemmas involving phi from Lehmer AFP entry
paulson <lp15@cam.ac.uk>
parents:
55242
diff
changeset
|
287 |
|
31719 | 288 |
lemma phi_zero [simp]: "phi 0 = 0" |
60527 | 289 |
unfolding phi_def |
44872 | 290 |
(* Auto hangs here. Once again, where is the simplification rule |
60527 | 291 |
1 \<equiv> Suc 0 coming from? *) |
31719 | 292 |
apply (auto simp add: card_eq_0_iff) |
293 |
(* Add card_eq_0_iff as a simp rule? delete card_empty_imp? *) |
|
41541 | 294 |
done |
31719 | 295 |
|
296 |
lemma phi_one [simp]: "phi 1 = 0" |
|
44872 | 297 |
by (auto simp add: phi_def card_eq_0_iff) |
31719 | 298 |
|
60527 | 299 |
lemma (in residues) phi_eq: "phi m = card (Units R)" |
31719 | 300 |
by (simp add: phi_def res_units_eq) |
301 |
||
44872 | 302 |
lemma (in residues) euler_theorem1: |
31719 | 303 |
assumes a: "gcd a m = 1" |
304 |
shows "[a^phi m = 1] (mod m)" |
|
305 |
proof - |
|
60527 | 306 |
from a m_gt_one have [simp]: "a mod m \<in> Units R" |
31719 | 307 |
by (intro mod_in_res_units) |
308 |
from phi_eq have "(a mod m) (^) (phi m) = (a mod m) (^) (card (Units R))" |
|
309 |
by simp |
|
44872 | 310 |
also have "\<dots> = \<one>" |
60527 | 311 |
by (intro units_power_order_eq_one) auto |
31719 | 312 |
finally show ?thesis |
313 |
by (simp add: res_to_cong_simps) |
|
314 |
qed |
|
315 |
||
316 |
(* In fact, there is a two line proof! |
|
317 |
||
44872 | 318 |
lemma (in residues) euler_theorem1: |
31719 | 319 |
assumes a: "gcd a m = 1" |
320 |
shows "[a^phi m = 1] (mod m)" |
|
321 |
proof - |
|
322 |
have "(a mod m) (^) (phi m) = \<one>" |
|
323 |
by (simp add: phi_eq units_power_order_eq_one a m_gt_one) |
|
44872 | 324 |
then show ?thesis |
31719 | 325 |
by (simp add: res_to_cong_simps) |
326 |
qed |
|
327 |
||
328 |
*) |
|
329 |
||
63167 | 330 |
text \<open>Outside the locale, we can relax the restriction \<open>m > 1\<close>.\<close> |
31719 | 331 |
lemma euler_theorem: |
60527 | 332 |
assumes "m \<ge> 0" |
333 |
and "gcd a m = 1" |
|
31719 | 334 |
shows "[a^phi m = 1] (mod m)" |
60527 | 335 |
proof (cases "m = 0 | m = 1") |
336 |
case True |
|
44872 | 337 |
then show ?thesis by auto |
31719 | 338 |
next |
60527 | 339 |
case False |
41541 | 340 |
with assms show ?thesis |
31719 | 341 |
by (intro residues.euler_theorem1, unfold residues_def, auto) |
342 |
qed |
|
343 |
||
60527 | 344 |
lemma (in residues_prime) phi_prime: "phi p = nat p - 1" |
31719 | 345 |
apply (subst phi_eq) |
346 |
apply (subst res_prime_units_eq) |
|
347 |
apply auto |
|
41541 | 348 |
done |
31719 | 349 |
|
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
350 |
lemma phi_prime: "prime (int p) \<Longrightarrow> phi p = nat p - 1" |
31719 | 351 |
apply (rule residues_prime.phi_prime) |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
352 |
apply simp |
31719 | 353 |
apply (erule residues_prime.intro) |
41541 | 354 |
done |
31719 | 355 |
|
356 |
lemma fermat_theorem: |
|
60527 | 357 |
fixes a :: int |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
358 |
assumes "prime (int p)" |
60527 | 359 |
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
|
360 |
shows "[a^(p - 1) = 1] (mod p)" |
31719 | 361 |
proof - |
60527 | 362 |
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
|
363 |
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
|
364 |
simp: gcd.commute[of _ "int p"]) |
31719 | 365 |
also have "phi p = nat p - 1" |
60527 | 366 |
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
|
367 |
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
|
368 |
by (metis nat_int) |
31719 | 369 |
qed |
370 |
||
55227
653de351d21c
version of Fermat's Theorem for type nat
paulson <lp15@cam.ac.uk>
parents:
55172
diff
changeset
|
371 |
lemma fermat_theorem_nat: |
63534
523b488b15c9
Overhaul of prime/multiplicity/prime_factors
eberlm <eberlm@in.tum.de>
parents:
63417
diff
changeset
|
372 |
assumes "prime (int p)" and "\<not> p dvd a" |
60527 | 373 |
shows "[a ^ (p - 1) = 1] (mod p)" |
374 |
using fermat_theorem [of p a] assms |
|
62348 | 375 |
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
|
376 |
|
31719 | 377 |
|
60526 | 378 |
subsection \<open>Wilson's theorem\<close> |
31719 | 379 |
|
60527 | 380 |
lemma (in field) inv_pair_lemma: "x \<in> Units R \<Longrightarrow> y \<in> Units R \<Longrightarrow> |
381 |
{x, inv x} \<noteq> {y, inv y} \<Longrightarrow> {x, inv x} \<inter> {y, inv y} = {}" |
|
31719 | 382 |
apply auto |
55352 | 383 |
apply (metis Units_inv_inv)+ |
41541 | 384 |
done |
31719 | 385 |
|
386 |
lemma (in residues_prime) wilson_theorem1: |
|
387 |
assumes a: "p > 2" |
|
59730
b7c394c7a619
The factorial function, "fact", now has type "nat => 'a"
paulson <lp15@cam.ac.uk>
parents:
59667
diff
changeset
|
388 |
shows "[fact (p - 1) = (-1::int)] (mod p)" |
31719 | 389 |
proof - |
60527 | 390 |
let ?Inverse_Pairs = "{{x, inv x}| x. x \<in> Units R - {\<one>, \<ominus> \<one>}}" |
391 |
have UR: "Units R = {\<one>, \<ominus> \<one>} \<union> \<Union>?Inverse_Pairs" |
|
31719 | 392 |
by auto |
60527 | 393 |
have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) \<otimes> (\<Otimes>i\<in>\<Union>?Inverse_Pairs. i)" |
31732 | 394 |
apply (subst UR) |
31719 | 395 |
apply (subst finprod_Un_disjoint) |
55352 | 396 |
apply (auto intro: funcsetI) |
60527 | 397 |
using inv_one apply auto[1] |
398 |
using inv_eq_neg_one_eq apply auto |
|
31719 | 399 |
done |
60527 | 400 |
also have "(\<Otimes>i\<in>{\<one>, \<ominus> \<one>}. i) = \<ominus> \<one>" |
31719 | 401 |
apply (subst finprod_insert) |
402 |
apply auto |
|
403 |
apply (frule one_eq_neg_one) |
|
60527 | 404 |
using a apply force |
31719 | 405 |
done |
60527 | 406 |
also have "(\<Otimes>i\<in>(\<Union>?Inverse_Pairs). i) = (\<Otimes>A\<in>?Inverse_Pairs. (\<Otimes>y\<in>A. y))" |
407 |
apply (subst finprod_Union_disjoint) |
|
408 |
apply auto |
|
55352 | 409 |
apply (metis Units_inv_inv)+ |
31719 | 410 |
done |
411 |
also have "\<dots> = \<one>" |
|
60527 | 412 |
apply (rule finprod_one) |
413 |
apply auto |
|
414 |
apply (subst finprod_insert) |
|
415 |
apply auto |
|
55352 | 416 |
apply (metis inv_eq_self) |
31719 | 417 |
done |
60527 | 418 |
finally have "(\<Otimes>i\<in>Units R. i) = \<ominus> \<one>" |
31719 | 419 |
by simp |
60527 | 420 |
also have "(\<Otimes>i\<in>Units R. i) = (\<Otimes>i\<in>Units R. i mod p)" |
31719 | 421 |
apply (rule finprod_cong') |
60527 | 422 |
apply auto |
31719 | 423 |
apply (subst (asm) res_prime_units_eq) |
424 |
apply auto |
|
425 |
done |
|
60527 | 426 |
also have "\<dots> = (\<Prod>i\<in>Units R. i) mod p" |
31719 | 427 |
apply (rule prod_cong) |
428 |
apply auto |
|
429 |
done |
|
430 |
also have "\<dots> = fact (p - 1) mod p" |
|
63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63167
diff
changeset
|
431 |
apply (simp add: fact_setprod) |
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
|
432 |
apply (insert assms) |
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55227
diff
changeset
|
433 |
apply (subst res_prime_units_eq) |
413ec965f95d
Number_Theory: prime is no longer overloaded, but only for nat. Automatic coercion to int enabled.
paulson <lp15@cam.ac.uk>
parents:
55227
diff
changeset
|
434 |
apply (simp add: int_setprod zmod_int setprod_int_eq) |
31719 | 435 |
done |
60527 | 436 |
finally have "fact (p - 1) mod p = \<ominus> \<one>" . |
437 |
then show ?thesis |
|
60528 | 438 |
by (metis of_nat_fact Divides.transfer_int_nat_functions(2) |
439 |
cong_int_def res_neg_eq res_one_eq) |
|
31719 | 440 |
qed |
441 |
||
55352 | 442 |
lemma wilson_theorem: |
60527 | 443 |
assumes "prime p" |
444 |
shows "[fact (p - 1) = - 1] (mod p)" |
|
55352 | 445 |
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
|
446 |
case True |
55352 | 447 |
then show ?thesis |
63417
c184ec919c70
more lemmas to emphasize {0::nat..(<)n} as canonical representation of intervals on nat
haftmann
parents:
63167
diff
changeset
|
448 |
by (simp add: cong_int_def fact_setprod) |
55352 | 449 |
next |
450 |
case False |
|
451 |
then show ?thesis |
|
452 |
using assms prime_ge_2_nat |
|
453 |
by (metis residues_prime.wilson_theorem1 residues_prime.intro le_eq_less_or_eq) |
|
454 |
qed |
|
31719 | 455 |
|
456 |
end |