|
1 (* Author: Thomas M. Rasmussen |
|
2 Copyright 2000 University of Cambridge |
|
3 *) |
|
4 |
|
5 header {* Fermat's Little Theorem extended to Euler's Totient function *} |
|
6 |
|
7 theory EulerFermat |
|
8 imports BijectionRel IntFact |
|
9 begin |
|
10 |
|
11 text {* |
|
12 Fermat's Little Theorem extended to Euler's Totient function. More |
|
13 abstract approach than Boyer-Moore (which seems necessary to achieve |
|
14 the extended version). |
|
15 *} |
|
16 |
|
17 |
|
18 subsection {* Definitions and lemmas *} |
|
19 |
|
20 inductive_set |
|
21 RsetR :: "int => int set set" |
|
22 for m :: int |
|
23 where |
|
24 empty [simp]: "{} \<in> RsetR m" |
|
25 | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==> |
|
26 \<forall>a'. a' \<in> A --> \<not> zcong a a' m ==> insert a A \<in> RsetR m" |
|
27 |
|
28 consts |
|
29 BnorRset :: "int * int => int set" |
|
30 |
|
31 recdef BnorRset |
|
32 "measure ((\<lambda>(a, m). nat a) :: int * int => nat)" |
|
33 "BnorRset (a, m) = |
|
34 (if 0 < a then |
|
35 let na = BnorRset (a - 1, m) |
|
36 in (if zgcd a m = 1 then insert a na else na) |
|
37 else {})" |
|
38 |
|
39 definition |
|
40 norRRset :: "int => int set" where |
|
41 "norRRset m = BnorRset (m - 1, m)" |
|
42 |
|
43 definition |
|
44 noXRRset :: "int => int => int set" where |
|
45 "noXRRset m x = (\<lambda>a. a * x) ` norRRset m" |
|
46 |
|
47 definition |
|
48 phi :: "int => nat" where |
|
49 "phi m = card (norRRset m)" |
|
50 |
|
51 definition |
|
52 is_RRset :: "int set => int => bool" where |
|
53 "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)" |
|
54 |
|
55 definition |
|
56 RRset2norRR :: "int set => int => int => int" where |
|
57 "RRset2norRR A m a = |
|
58 (if 1 < m \<and> is_RRset A m \<and> a \<in> A then |
|
59 SOME b. zcong a b m \<and> b \<in> norRRset m |
|
60 else 0)" |
|
61 |
|
62 definition |
|
63 zcongm :: "int => int => int => bool" where |
|
64 "zcongm m = (\<lambda>a b. zcong a b m)" |
|
65 |
|
66 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
|
67 -- {* LCP: not sure why this lemma is needed now *} |
|
68 by (auto simp add: abs_if) |
|
69 |
|
70 |
|
71 text {* \medskip @{text norRRset} *} |
|
72 |
|
73 declare BnorRset.simps [simp del] |
|
74 |
|
75 lemma BnorRset_induct: |
|
76 assumes "!!a m. P {} a m" |
|
77 and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m |
|
78 ==> P (BnorRset(a,m)) a m" |
|
79 shows "P (BnorRset(u,v)) u v" |
|
80 apply (rule BnorRset.induct) |
|
81 apply safe |
|
82 apply (case_tac [2] "0 < a") |
|
83 apply (rule_tac [2] prems) |
|
84 apply simp_all |
|
85 apply (simp_all add: BnorRset.simps prems) |
|
86 done |
|
87 |
|
88 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a" |
|
89 apply (induct a m rule: BnorRset_induct) |
|
90 apply simp |
|
91 apply (subst BnorRset.simps) |
|
92 apply (unfold Let_def, auto) |
|
93 done |
|
94 |
|
95 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)" |
|
96 by (auto dest: Bnor_mem_zle) |
|
97 |
|
98 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b" |
|
99 apply (induct a m rule: BnorRset_induct) |
|
100 prefer 2 |
|
101 apply (subst BnorRset.simps) |
|
102 apply (unfold Let_def, auto) |
|
103 done |
|
104 |
|
105 lemma Bnor_mem_if [rule_format]: |
|
106 "zgcd b m = 1 --> 0 < b --> b \<le> a --> b \<in> BnorRset (a, m)" |
|
107 apply (induct a m rule: BnorRset.induct, auto) |
|
108 apply (subst BnorRset.simps) |
|
109 defer |
|
110 apply (subst BnorRset.simps) |
|
111 apply (unfold Let_def, auto) |
|
112 done |
|
113 |
|
114 lemma Bnor_in_RsetR [rule_format]: "a < m --> BnorRset (a, m) \<in> RsetR m" |
|
115 apply (induct a m rule: BnorRset_induct, simp) |
|
116 apply (subst BnorRset.simps) |
|
117 apply (unfold Let_def, auto) |
|
118 apply (rule RsetR.insert) |
|
119 apply (rule_tac [3] allI) |
|
120 apply (rule_tac [3] impI) |
|
121 apply (rule_tac [3] zcong_not) |
|
122 apply (subgoal_tac [6] "a' \<le> a - 1") |
|
123 apply (rule_tac [7] Bnor_mem_zle) |
|
124 apply (rule_tac [5] Bnor_mem_zg, auto) |
|
125 done |
|
126 |
|
127 lemma Bnor_fin: "finite (BnorRset (a, m))" |
|
128 apply (induct a m rule: BnorRset_induct) |
|
129 prefer 2 |
|
130 apply (subst BnorRset.simps) |
|
131 apply (unfold Let_def, auto) |
|
132 done |
|
133 |
|
134 lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)" |
|
135 apply auto |
|
136 done |
|
137 |
|
138 lemma norR_mem_unique: |
|
139 "1 < m ==> |
|
140 zgcd a m = 1 ==> \<exists>!b. [a = b] (mod m) \<and> b \<in> norRRset m" |
|
141 apply (unfold norRRset_def) |
|
142 apply (cut_tac a = a and m = m in zcong_zless_unique, auto) |
|
143 apply (rule_tac [2] m = m in zcong_zless_imp_eq) |
|
144 apply (auto intro: Bnor_mem_zle Bnor_mem_zg zcong_trans |
|
145 order_less_imp_le norR_mem_unique_aux simp add: zcong_sym) |
|
146 apply (rule_tac x = b in exI, safe) |
|
147 apply (rule Bnor_mem_if) |
|
148 apply (case_tac [2] "b = 0") |
|
149 apply (auto intro: order_less_le [THEN iffD2]) |
|
150 prefer 2 |
|
151 apply (simp only: zcong_def) |
|
152 apply (subgoal_tac "zgcd a m = m") |
|
153 prefer 2 |
|
154 apply (subst zdvd_iff_zgcd [symmetric]) |
|
155 apply (rule_tac [4] zgcd_zcong_zgcd) |
|
156 apply (simp_all add: zcong_sym) |
|
157 done |
|
158 |
|
159 |
|
160 text {* \medskip @{term noXRRset} *} |
|
161 |
|
162 lemma RRset_gcd [rule_format]: |
|
163 "is_RRset A m ==> a \<in> A --> zgcd a m = 1" |
|
164 apply (unfold is_RRset_def) |
|
165 apply (rule RsetR.induct [where P="%A. a \<in> A --> zgcd a m = 1"], auto) |
|
166 done |
|
167 |
|
168 lemma RsetR_zmult_mono: |
|
169 "A \<in> RsetR m ==> |
|
170 0 < m ==> zgcd x m = 1 ==> (\<lambda>a. a * x) ` A \<in> RsetR m" |
|
171 apply (erule RsetR.induct, simp_all) |
|
172 apply (rule RsetR.insert, auto) |
|
173 apply (blast intro: zgcd_zgcd_zmult) |
|
174 apply (simp add: zcong_cancel) |
|
175 done |
|
176 |
|
177 lemma card_nor_eq_noX: |
|
178 "0 < m ==> |
|
179 zgcd x m = 1 ==> card (noXRRset m x) = card (norRRset m)" |
|
180 apply (unfold norRRset_def noXRRset_def) |
|
181 apply (rule card_image) |
|
182 apply (auto simp add: inj_on_def Bnor_fin) |
|
183 apply (simp add: BnorRset.simps) |
|
184 done |
|
185 |
|
186 lemma noX_is_RRset: |
|
187 "0 < m ==> zgcd x m = 1 ==> is_RRset (noXRRset m x) m" |
|
188 apply (unfold is_RRset_def phi_def) |
|
189 apply (auto simp add: card_nor_eq_noX) |
|
190 apply (unfold noXRRset_def norRRset_def) |
|
191 apply (rule RsetR_zmult_mono) |
|
192 apply (rule Bnor_in_RsetR, simp_all) |
|
193 done |
|
194 |
|
195 lemma aux_some: |
|
196 "1 < m ==> is_RRset A m ==> a \<in> A |
|
197 ==> zcong a (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) m \<and> |
|
198 (SOME b. [a = b] (mod m) \<and> b \<in> norRRset m) \<in> norRRset m" |
|
199 apply (rule norR_mem_unique [THEN ex1_implies_ex, THEN someI_ex]) |
|
200 apply (rule_tac [2] RRset_gcd, simp_all) |
|
201 done |
|
202 |
|
203 lemma RRset2norRR_correct: |
|
204 "1 < m ==> is_RRset A m ==> a \<in> A ==> |
|
205 [a = RRset2norRR A m a] (mod m) \<and> RRset2norRR A m a \<in> norRRset m" |
|
206 apply (unfold RRset2norRR_def, simp) |
|
207 apply (rule aux_some, simp_all) |
|
208 done |
|
209 |
|
210 lemmas RRset2norRR_correct1 = |
|
211 RRset2norRR_correct [THEN conjunct1, standard] |
|
212 lemmas RRset2norRR_correct2 = |
|
213 RRset2norRR_correct [THEN conjunct2, standard] |
|
214 |
|
215 lemma RsetR_fin: "A \<in> RsetR m ==> finite A" |
|
216 by (induct set: RsetR) auto |
|
217 |
|
218 lemma RRset_zcong_eq [rule_format]: |
|
219 "1 < m ==> |
|
220 is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b" |
|
221 apply (unfold is_RRset_def) |
|
222 apply (rule RsetR.induct [where P="%A. a \<in> A --> b \<in> A --> a = b"]) |
|
223 apply (auto simp add: zcong_sym) |
|
224 done |
|
225 |
|
226 lemma aux: |
|
227 "P (SOME a. P a) ==> Q (SOME a. Q a) ==> |
|
228 (SOME a. P a) = (SOME a. Q a) ==> \<exists>a. P a \<and> Q a" |
|
229 apply auto |
|
230 done |
|
231 |
|
232 lemma RRset2norRR_inj: |
|
233 "1 < m ==> is_RRset A m ==> inj_on (RRset2norRR A m) A" |
|
234 apply (unfold RRset2norRR_def inj_on_def, auto) |
|
235 apply (subgoal_tac "\<exists>b. ([x = b] (mod m) \<and> b \<in> norRRset m) \<and> |
|
236 ([y = b] (mod m) \<and> b \<in> norRRset m)") |
|
237 apply (rule_tac [2] aux) |
|
238 apply (rule_tac [3] aux_some) |
|
239 apply (rule_tac [2] aux_some) |
|
240 apply (rule RRset_zcong_eq, auto) |
|
241 apply (rule_tac b = b in zcong_trans) |
|
242 apply (simp_all add: zcong_sym) |
|
243 done |
|
244 |
|
245 lemma RRset2norRR_eq_norR: |
|
246 "1 < m ==> is_RRset A m ==> RRset2norRR A m ` A = norRRset m" |
|
247 apply (rule card_seteq) |
|
248 prefer 3 |
|
249 apply (subst card_image) |
|
250 apply (rule_tac RRset2norRR_inj, auto) |
|
251 apply (rule_tac [3] RRset2norRR_correct2, auto) |
|
252 apply (unfold is_RRset_def phi_def norRRset_def) |
|
253 apply (auto simp add: Bnor_fin) |
|
254 done |
|
255 |
|
256 |
|
257 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A" |
|
258 by (unfold inj_on_def, auto) |
|
259 |
|
260 lemma Bnor_prod_power [rule_format]: |
|
261 "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset (a, m)) = |
|
262 \<Prod>(BnorRset(a, m)) * x^card (BnorRset (a, m))" |
|
263 apply (induct a m rule: BnorRset_induct) |
|
264 prefer 2 |
|
265 apply (simplesubst BnorRset.simps) --{*multiple redexes*} |
|
266 apply (unfold Let_def, auto) |
|
267 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
|
268 apply (subst setprod_insert) |
|
269 apply (rule_tac [2] Bnor_prod_power_aux) |
|
270 apply (unfold inj_on_def) |
|
271 apply (simp_all add: zmult_ac Bnor_fin finite_imageI |
|
272 Bnor_mem_zle_swap) |
|
273 done |
|
274 |
|
275 |
|
276 subsection {* Fermat *} |
|
277 |
|
278 lemma bijzcong_zcong_prod: |
|
279 "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" |
|
280 apply (unfold zcongm_def) |
|
281 apply (erule bijR.induct) |
|
282 apply (subgoal_tac [2] "a \<notin> A \<and> b \<notin> B \<and> finite A \<and> finite B") |
|
283 apply (auto intro: fin_bijRl fin_bijRr zcong_zmult) |
|
284 done |
|
285 |
|
286 lemma Bnor_prod_zgcd [rule_format]: |
|
287 "a < m --> zgcd (\<Prod>(BnorRset(a, m))) m = 1" |
|
288 apply (induct a m rule: BnorRset_induct) |
|
289 prefer 2 |
|
290 apply (subst BnorRset.simps) |
|
291 apply (unfold Let_def, auto) |
|
292 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
|
293 apply (blast intro: zgcd_zgcd_zmult) |
|
294 done |
|
295 |
|
296 theorem Euler_Fermat: |
|
297 "0 < m ==> zgcd x m = 1 ==> [x^(phi m) = 1] (mod m)" |
|
298 apply (unfold norRRset_def phi_def) |
|
299 apply (case_tac "x = 0") |
|
300 apply (case_tac [2] "m = 1") |
|
301 apply (rule_tac [3] iffD1) |
|
302 apply (rule_tac [3] k = "\<Prod>(BnorRset(m - 1, m))" |
|
303 in zcong_cancel2) |
|
304 prefer 5 |
|
305 apply (subst Bnor_prod_power [symmetric]) |
|
306 apply (rule_tac [7] Bnor_prod_zgcd, simp_all) |
|
307 apply (rule bijzcong_zcong_prod) |
|
308 apply (fold norRRset_def noXRRset_def) |
|
309 apply (subst RRset2norRR_eq_norR [symmetric]) |
|
310 apply (rule_tac [3] inj_func_bijR, auto) |
|
311 apply (unfold zcongm_def) |
|
312 apply (rule_tac [2] RRset2norRR_correct1) |
|
313 apply (rule_tac [5] RRset2norRR_inj) |
|
314 apply (auto intro: order_less_le [THEN iffD2] |
|
315 simp add: noX_is_RRset) |
|
316 apply (unfold noXRRset_def norRRset_def) |
|
317 apply (rule finite_imageI) |
|
318 apply (rule Bnor_fin) |
|
319 done |
|
320 |
|
321 lemma Bnor_prime: |
|
322 "\<lbrakk> zprime p; a < p \<rbrakk> \<Longrightarrow> card (BnorRset (a, p)) = nat a" |
|
323 apply (induct a p rule: BnorRset.induct) |
|
324 apply (subst BnorRset.simps) |
|
325 apply (unfold Let_def, auto simp add:zless_zprime_imp_zrelprime) |
|
326 apply (subgoal_tac "finite (BnorRset (a - 1,m))") |
|
327 apply (subgoal_tac "a ~: BnorRset (a - 1,m)") |
|
328 apply (auto simp add: card_insert_disjoint Suc_nat_eq_nat_zadd1) |
|
329 apply (frule Bnor_mem_zle, arith) |
|
330 apply (frule Bnor_fin) |
|
331 done |
|
332 |
|
333 lemma phi_prime: "zprime p ==> phi p = nat (p - 1)" |
|
334 apply (unfold phi_def norRRset_def) |
|
335 apply (rule Bnor_prime, auto) |
|
336 done |
|
337 |
|
338 theorem Little_Fermat: |
|
339 "zprime p ==> \<not> p dvd x ==> [x^(nat (p - 1)) = 1] (mod p)" |
|
340 apply (subst phi_prime [symmetric]) |
|
341 apply (rule_tac [2] Euler_Fermat) |
|
342 apply (erule_tac [3] zprime_imp_zrelprime) |
|
343 apply (unfold zprime_def, auto) |
|
344 done |
|
345 |
|
346 end |