1 (* Title: HOL/Old_Number_Theory/EulerFermat.thy |
1 (* Title: HOL/Old_Number_Theory/EulerFermat.thy |
2 Author: Thomas M. Rasmussen |
2 Author: Thomas M. Rasmussen |
3 Copyright 2000 University of Cambridge |
3 Copyright 2000 University of Cambridge |
4 *) |
4 *) |
5 |
5 |
6 section {* Fermat's Little Theorem extended to Euler's Totient function *} |
6 section \<open>Fermat's Little Theorem extended to Euler's Totient function\<close> |
7 |
7 |
8 theory EulerFermat |
8 theory EulerFermat |
9 imports BijectionRel IntFact |
9 imports BijectionRel IntFact |
10 begin |
10 begin |
11 |
11 |
12 text {* |
12 text \<open> |
13 Fermat's Little Theorem extended to Euler's Totient function. More |
13 Fermat's Little Theorem extended to Euler's Totient function. More |
14 abstract approach than Boyer-Moore (which seems necessary to achieve |
14 abstract approach than Boyer-Moore (which seems necessary to achieve |
15 the extended version). |
15 the extended version). |
16 *} |
16 \<close> |
17 |
17 |
18 |
18 |
19 subsection {* Definitions and lemmas *} |
19 subsection \<open>Definitions and lemmas\<close> |
20 |
20 |
21 inductive_set RsetR :: "int => int set set" for m :: int |
21 inductive_set RsetR :: "int => int set set" for m :: int |
22 where |
22 where |
23 empty [simp]: "{} \<in> RsetR m" |
23 empty [simp]: "{} \<in> RsetR m" |
24 | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==> |
24 | insert: "A \<in> RsetR m ==> zgcd a m = 1 ==> |
52 |
52 |
53 definition zcongm :: "int => int => int => bool" |
53 definition zcongm :: "int => int => int => bool" |
54 where "zcongm m = (\<lambda>a b. zcong a b m)" |
54 where "zcongm m = (\<lambda>a b. zcong a b m)" |
55 |
55 |
56 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
56 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
57 -- {* LCP: not sure why this lemma is needed now *} |
57 -- \<open>LCP: not sure why this lemma is needed now\<close> |
58 by (auto simp add: abs_if) |
58 by (auto simp add: abs_if) |
59 |
59 |
60 |
60 |
61 text {* \medskip @{text norRRset} *} |
61 text \<open>\medskip @{text norRRset}\<close> |
62 |
62 |
63 declare BnorRset.simps [simp del] |
63 declare BnorRset.simps [simp del] |
64 |
64 |
65 lemma BnorRset_induct: |
65 lemma BnorRset_induct: |
66 assumes "!!a m. P {} a m" |
66 assumes "!!a m. P {} a m" |
144 apply (rule_tac [4] zgcd_zcong_zgcd) |
144 apply (rule_tac [4] zgcd_zcong_zgcd) |
145 apply (simp_all (no_asm_use) add: zcong_sym) |
145 apply (simp_all (no_asm_use) add: zcong_sym) |
146 done |
146 done |
147 |
147 |
148 |
148 |
149 text {* \medskip @{term noXRRset} *} |
149 text \<open>\medskip @{term noXRRset}\<close> |
150 |
150 |
151 lemma RRset_gcd [rule_format]: |
151 lemma RRset_gcd [rule_format]: |
152 "is_RRset A m ==> a \<in> A --> zgcd a m = 1" |
152 "is_RRset A m ==> a \<in> A --> zgcd a m = 1" |
153 apply (unfold is_RRset_def) |
153 apply (unfold is_RRset_def) |
154 apply (rule RsetR.induct, auto) |
154 apply (rule RsetR.induct, auto) |
247 lemma Bnor_prod_power [rule_format]: |
247 lemma Bnor_prod_power [rule_format]: |
248 "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) = |
248 "x \<noteq> 0 ==> a < m --> \<Prod>((\<lambda>a. a * x) ` BnorRset a m) = |
249 \<Prod>(BnorRset a m) * x^card (BnorRset a m)" |
249 \<Prod>(BnorRset a m) * x^card (BnorRset a m)" |
250 apply (induct a m rule: BnorRset_induct) |
250 apply (induct a m rule: BnorRset_induct) |
251 prefer 2 |
251 prefer 2 |
252 apply (simplesubst BnorRset.simps) --{*multiple redexes*} |
252 apply (simplesubst BnorRset.simps) --\<open>multiple redexes\<close> |
253 apply (unfold Let_def, auto) |
253 apply (unfold Let_def, auto) |
254 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
254 apply (simp add: Bnor_fin Bnor_mem_zle_swap) |
255 apply (subst setprod.insert) |
255 apply (subst setprod.insert) |
256 apply (rule_tac [2] Bnor_prod_power_aux) |
256 apply (rule_tac [2] Bnor_prod_power_aux) |
257 apply (unfold inj_on_def) |
257 apply (unfold inj_on_def) |
258 apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap) |
258 apply (simp_all add: ac_simps Bnor_fin Bnor_mem_zle_swap) |
259 done |
259 done |
260 |
260 |
261 |
261 |
262 subsection {* Fermat *} |
262 subsection \<open>Fermat\<close> |
263 |
263 |
264 lemma bijzcong_zcong_prod: |
264 lemma bijzcong_zcong_prod: |
265 "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" |
265 "(A, B) \<in> bijR (zcongm m) ==> [\<Prod>A = \<Prod>B] (mod m)" |
266 apply (unfold zcongm_def) |
266 apply (unfold zcongm_def) |
267 apply (erule bijR.induct) |
267 apply (erule bijR.induct) |