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