1 (* Title: HOL/NumberTheory/EulerFermat.thy |
1 (* Title: HOL/NumberTheory/EulerFermat.thy |
2 ID: $Id$ |
2 ID: $Id$ |
3 Author: Thomas M. Rasmussen |
3 Author: Thomas M. Rasmussen |
4 Copyright 2000 University of Cambridge |
4 Copyright 2000 University of Cambridge |
5 |
|
6 Changes by Jeremy Avigad, 2003/02/21: |
|
7 repaired proof of Bnor_prime (removed use of zprime_def) |
|
8 *) |
5 *) |
9 |
6 |
10 header {* Fermat's Little Theorem extended to Euler's Totient function *} |
7 header {* Fermat's Little Theorem extended to Euler's Totient function *} |
11 |
8 |
12 theory EulerFermat imports BijectionRel IntFact begin |
9 theory EulerFermat imports BijectionRel IntFact begin |
58 zcongm :: "int => int => int => bool" |
55 zcongm :: "int => int => int => bool" |
59 "zcongm m == \<lambda>a b. zcong a b m" |
56 "zcongm m == \<lambda>a b. zcong a b m" |
60 |
57 |
61 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
58 lemma abs_eq_1_iff [iff]: "(abs z = (1::int)) = (z = 1 \<or> z = -1)" |
62 -- {* LCP: not sure why this lemma is needed now *} |
59 -- {* LCP: not sure why this lemma is needed now *} |
63 by (auto simp add: abs_if) |
60 by (auto simp add: abs_if) |
64 |
61 |
65 |
62 |
66 text {* \medskip @{text norRRset} *} |
63 text {* \medskip @{text norRRset} *} |
67 |
64 |
68 declare BnorRset.simps [simp del] |
65 declare BnorRset.simps [simp del] |
69 |
66 |
70 lemma BnorRset_induct: |
67 lemma BnorRset_induct: |
71 "(!!a m. P {} a m) ==> |
68 assumes "!!a m. P {} a m" |
72 (!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m |
69 and "!!a m. 0 < (a::int) ==> P (BnorRset (a - 1, m::int)) (a - 1) m |
73 ==> P (BnorRset(a,m)) a m) |
70 ==> P (BnorRset(a,m)) a m" |
74 ==> P (BnorRset(u,v)) u v" |
71 shows "P (BnorRset(u,v)) u v" |
75 proof - |
72 apply (rule BnorRset.induct) |
76 case rule_context |
73 apply safe |
77 show ?thesis |
74 apply (case_tac [2] "0 < a") |
78 apply (rule BnorRset.induct, safe) |
75 apply (rule_tac [2] prems) |
79 apply (case_tac [2] "0 < a") |
76 apply simp_all |
80 apply (rule_tac [2] rule_context, simp_all) |
77 apply (simp_all add: BnorRset.simps prems) |
81 apply (simp_all add: BnorRset.simps rule_context) |
78 done |
82 done |
79 |
83 qed |
80 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) \<longrightarrow> b \<le> a" |
84 |
81 apply (induct a m rule: BnorRset_induct) |
85 lemma Bnor_mem_zle [rule_format]: "b \<in> BnorRset (a, m) --> b \<le> a" |
82 apply simp |
86 apply (induct a m rule: BnorRset_induct) |
83 apply (subst BnorRset.simps) |
87 prefer 2 |
|
88 apply (subst BnorRset.simps) |
|
89 apply (unfold Let_def, auto) |
84 apply (unfold Let_def, auto) |
90 done |
85 done |
91 |
86 |
92 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)" |
87 lemma Bnor_mem_zle_swap: "a < b ==> b \<notin> BnorRset (a, m)" |
93 by (auto dest: Bnor_mem_zle) |
88 by (auto dest: Bnor_mem_zle) |
94 |
89 |
95 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b" |
90 lemma Bnor_mem_zg [rule_format]: "b \<in> BnorRset (a, m) --> 0 < b" |
96 apply (induct a m rule: BnorRset_induct) |
91 apply (induct a m rule: BnorRset_induct) |
97 prefer 2 |
92 prefer 2 |
98 apply (subst BnorRset.simps) |
93 apply (subst BnorRset.simps) |
208 RRset2norRR_correct [THEN conjunct1, standard] |
203 RRset2norRR_correct [THEN conjunct1, standard] |
209 lemmas RRset2norRR_correct2 = |
204 lemmas RRset2norRR_correct2 = |
210 RRset2norRR_correct [THEN conjunct2, standard] |
205 RRset2norRR_correct [THEN conjunct2, standard] |
211 |
206 |
212 lemma RsetR_fin: "A \<in> RsetR m ==> finite A" |
207 lemma RsetR_fin: "A \<in> RsetR m ==> finite A" |
213 by (erule RsetR.induct, auto) |
208 by (induct set: RsetR) auto |
214 |
209 |
215 lemma RRset_zcong_eq [rule_format]: |
210 lemma RRset_zcong_eq [rule_format]: |
216 "1 < m ==> |
211 "1 < m ==> |
217 is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b" |
212 is_RRset A m ==> [a = b] (mod m) ==> a \<in> A --> b \<in> A --> a = b" |
218 apply (unfold is_RRset_def) |
213 apply (unfold is_RRset_def) |