src/HOL/Old_Number_Theory/EulerFermat.thy
 author haftmann Fri Nov 27 08:41:10 2009 +0100 (2009-11-27) changeset 33963 977b94b64905 parent 32960 69916a850301 child 35440 bdf8ad377877 permissions -rw-r--r--
renamed former datatype.ML to datatype_data.ML; datatype.ML provides uniform view on datatype.ML and datatype_rep_proofs.ML
1 (*  Author:     Thomas M. Rasmussen
2     Copyright   2000  University of Cambridge
3 *)
5 header {* Fermat's Little Theorem extended to Euler's Totient function *}
7 theory EulerFermat
8 imports BijectionRel IntFact
9 begin
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 *}
18 subsection {* Definitions and lemmas *}
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"
28 consts
29   BnorRset :: "int * int => int set"
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 {})"
39 definition
40   norRRset :: "int => int set" where
41   "norRRset m = BnorRset (m - 1, m)"
43 definition
44   noXRRset :: "int => int => int set" where
45   "noXRRset m x = (\<lambda>a. a * x) ` norRRset m"
47 definition
48   phi :: "int => nat" where
49   "phi m = card (norRRset m)"
51 definition
52   is_RRset :: "int set => int => bool" where
53   "is_RRset A m = (A \<in> RsetR m \<and> card A = phi m)"
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)"
62 definition
63   zcongm :: "int => int => int => bool" where
64   "zcongm m = (\<lambda>a b. zcong a b m)"
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)
71 text {* \medskip @{text norRRset} *}
73 declare BnorRset.simps [simp del]
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
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
95 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)"
96   by (auto dest: Bnor_mem_zle)
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
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
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
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
134 lemma norR_mem_unique_aux: "a \<le> b - 1 ==> a < (b::int)"
135   apply auto
136   done
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
160 text {* \medskip @{term noXRRset} *}
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
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
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
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
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
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
210 lemmas RRset2norRR_correct1 =
211   RRset2norRR_correct [THEN conjunct1, standard]
212 lemmas RRset2norRR_correct2 =
213   RRset2norRR_correct [THEN conjunct2, standard]
215 lemma RsetR_fin: "A \<in> RsetR m ==> finite A"
216   by (induct set: RsetR) auto
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
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
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
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
257 lemma Bnor_prod_power_aux: "a \<notin> A ==> inj f ==> f a \<notin> f ` A"
258 by (unfold inj_on_def, auto)
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
276 subsection {* Fermat *}
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
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
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
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
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
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
346 end