|
1 (* Title: HOL/Number_Theory/Totient.thy |
|
2 Author: Jeremy Avigad |
|
3 Author: Florian Haftmann |
|
4 *) |
|
5 |
|
6 section \<open>Fundamental facts about Euler's totient function\<close> |
|
7 |
|
8 theory Totient |
|
9 imports |
|
10 "~~/src/HOL/Computational_Algebra/Primes" |
|
11 begin |
|
12 |
|
13 definition totatives :: "nat \<Rightarrow> nat set" |
|
14 where "totatives n = {m. 0 < m \<and> m < n \<and> coprime m n}" |
|
15 |
|
16 lemma in_totatives_iff [simp]: |
|
17 "m \<in> totatives n \<longleftrightarrow> 0 < m \<and> m < n \<and> coprime m n" |
|
18 by (simp add: totatives_def) |
|
19 |
|
20 lemma finite_totatives [simp]: |
|
21 "finite (totatives n)" |
|
22 by (simp add: totatives_def) |
|
23 |
|
24 lemma totatives_subset: |
|
25 "totatives n \<subseteq> {1..<n}" |
|
26 by auto |
|
27 |
|
28 lemma totatives_subset_Suc_0 [simp]: |
|
29 "totatives n \<subseteq> {Suc 0..<n}" |
|
30 using totatives_subset [of n] by simp |
|
31 |
|
32 lemma totatives_0 [simp]: |
|
33 "totatives 0 = {}" |
|
34 using totatives_subset [of 0] by simp |
|
35 |
|
36 lemma totatives_1 [simp]: |
|
37 "totatives 1 = {}" |
|
38 using totatives_subset [of 1] by simp |
|
39 |
|
40 lemma totatives_Suc_0 [simp]: |
|
41 "totatives (Suc 0) = {}" |
|
42 using totatives_1 by simp |
|
43 |
|
44 lemma one_in_totatives: |
|
45 assumes "n \<ge> 2" |
|
46 shows "1 \<in> totatives n" |
|
47 using assms by simp |
|
48 |
|
49 lemma minus_one_in_totatives: |
|
50 assumes "n \<ge> 2" |
|
51 shows "n - 1 \<in> totatives n" |
|
52 using assms coprime_minus_one_nat [of n] by simp |
|
53 |
|
54 lemma totatives_eq_empty_iff [simp]: |
|
55 "totatives n = {} \<longleftrightarrow> n \<in> {0, 1}" |
|
56 proof |
|
57 assume "totatives n = {}" |
|
58 show "n \<in> {0, 1}" |
|
59 proof (rule ccontr) |
|
60 assume "n \<notin> {0, 1}" |
|
61 then have "n \<ge> 2" |
|
62 by simp |
|
63 then have "1 \<in> totatives n" |
|
64 by (rule one_in_totatives) |
|
65 with \<open>totatives n = {}\<close> show False |
|
66 by simp |
|
67 qed |
|
68 qed auto |
|
69 |
|
70 lemma prime_totatives: |
|
71 assumes "prime p" |
|
72 shows "totatives p = {1..<p}" |
|
73 proof |
|
74 show "{1..<p} \<subseteq> totatives p" |
|
75 proof |
|
76 fix n |
|
77 assume "n \<in> {1..<p}" |
|
78 with nat_dvd_not_less have "\<not> p dvd n" |
|
79 by auto |
|
80 with assms prime_imp_coprime [of p n] have "coprime p n" |
|
81 by simp |
|
82 with \<open>n \<in> {1..<p}\<close> show "n \<in> totatives p" |
|
83 by (auto simp add: totatives_def ac_simps) |
|
84 qed |
|
85 qed auto |
|
86 |
|
87 lemma totatives_prime: |
|
88 assumes "p \<ge> 2" and "totatives p = {1..<p}" |
|
89 shows "prime p" |
|
90 proof (rule ccontr) |
|
91 from \<open>2 \<le> p\<close> have "1 < p" |
|
92 by simp |
|
93 moreover assume "\<not> prime p" |
|
94 ultimately obtain n where "1 < n" "n < p" "n dvd p" |
|
95 by (auto simp add: prime_nat_iff) |
|
96 (metis Suc_lessD Suc_lessI dvd_imp_le dvd_pos_nat le_neq_implies_less) |
|
97 then have "n \<in> {1..<p}" |
|
98 by simp |
|
99 with assms have "n \<in> totatives p" |
|
100 by simp |
|
101 then have "coprime n p" |
|
102 by simp |
|
103 with \<open>1 < n\<close> \<open>n dvd p\<close> show False |
|
104 by simp |
|
105 qed |
|
106 |
|
107 definition totient :: "nat \<Rightarrow> nat" |
|
108 where "totient = card \<circ> totatives" |
|
109 |
|
110 lemma card_totatives [simp]: |
|
111 "card (totatives n) = totient n" |
|
112 by (simp add: totient_def) |
|
113 |
|
114 lemma totient_0 [simp]: |
|
115 "totient 0 = 0" |
|
116 by (simp add: totient_def) |
|
117 |
|
118 lemma totient_1 [simp]: |
|
119 "totient 1 = 0" |
|
120 by (simp add: totient_def) |
|
121 |
|
122 lemma totient_Suc_0 [simp]: |
|
123 "totient (Suc 0) = 0" |
|
124 using totient_1 by simp |
|
125 |
|
126 lemma prime_totient: |
|
127 assumes "prime p" |
|
128 shows "totient p = p - 1" |
|
129 using assms prime_totatives |
|
130 by (simp add: totient_def) |
|
131 |
|
132 lemma totient_eq_0_iff [simp]: |
|
133 "totient n = 0 \<longleftrightarrow> n \<in> {0, 1}" |
|
134 by (simp only: totient_def comp_def card_eq_0_iff) auto |
|
135 |
|
136 lemma totient_noneq_0_iff [simp]: |
|
137 "totient n > 0 \<longleftrightarrow> 2 \<le> n" |
|
138 proof - |
|
139 have "totient n > 0 \<longleftrightarrow> totient n \<noteq> 0" |
|
140 by blast |
|
141 also have "\<dots> \<longleftrightarrow> 2 \<le> n" |
|
142 by auto |
|
143 finally show ?thesis . |
|
144 qed |
|
145 |
|
146 lemma totient_less_eq: |
|
147 "totient n \<le> n - 1" |
|
148 using card_mono [of "{1..<n}" "totatives n"] by auto |
|
149 |
|
150 lemma totient_less_eq_Suc_0 [simp]: |
|
151 "totient n \<le> n - Suc 0" |
|
152 using totient_less_eq [of n] by simp |
|
153 |
|
154 lemma totient_prime: |
|
155 assumes "2 \<le> p" "totient p = p - 1" |
|
156 shows "prime p" |
|
157 proof - |
|
158 have "totatives p = {1..<p}" |
|
159 by (rule card_subset_eq) (simp_all add: assms) |
|
160 with assms show ?thesis |
|
161 by (auto intro: totatives_prime) |
|
162 qed |
|
163 |
|
164 end |