author | wenzelm |
Tue, 01 Aug 2017 22:19:37 +0200 | |
changeset 66305 | 7454317f883c |
parent 65726 | f5d64d094efe |
child 66453 | cc19f7ca2ed6 |
permissions | -rw-r--r-- |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
1 |
(* Title: HOL/Number_Theory/Totient.thy |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
2 |
Author: Jeremy Avigad |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
3 |
Author: Florian Haftmann |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
4 |
Author: Manuel Eberl |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
5 |
*) |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
6 |
|
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
7 |
section \<open>Fundamental facts about Euler's totient function\<close> |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
8 |
|
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
9 |
theory Totient |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
10 |
imports |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
11 |
Complex_Main |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
12 |
"~~/src/HOL/Computational_Algebra/Primes" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
13 |
"~~/src/HOL/Number_Theory/Cong" |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
14 |
begin |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
15 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
16 |
definition totatives :: "nat \<Rightarrow> nat set" where |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
17 |
"totatives n = {k \<in> {0<..n}. coprime k n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
18 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
19 |
lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
20 |
by (simp add: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
21 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
22 |
lemma totatives_code [code]: "totatives n = Set.filter (\<lambda>k. coprime k n) {0<..n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
23 |
by (simp add: totatives_def Set.filter_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
24 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
25 |
lemma finite_totatives [simp]: "finite (totatives n)" |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
26 |
by (simp add: totatives_def) |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
27 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
28 |
lemma totatives_subset: "totatives n \<subseteq> {0<..n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
29 |
by (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
30 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
31 |
lemma zero_not_in_totatives [simp]: "0 \<notin> totatives n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
32 |
by (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
33 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
34 |
lemma totatives_le: "x \<in> totatives n \<Longrightarrow> x \<le> n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
35 |
by (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
36 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
37 |
lemma totatives_less: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
38 |
assumes "x \<in> totatives n" "n > 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
39 |
shows "x < n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
40 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
41 |
from assms have "x \<noteq> n" by (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
42 |
with totatives_le[OF assms(1)] show ?thesis by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
43 |
qed |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
44 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
45 |
lemma totatives_0 [simp]: "totatives 0 = {}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
46 |
by (auto simp: totatives_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
47 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
48 |
lemma totatives_1 [simp]: "totatives 1 = {Suc 0}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
49 |
by (auto simp: totatives_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
50 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
51 |
lemma totatives_Suc_0 [simp]: "totatives (Suc 0) = {Suc 0}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
52 |
by (auto simp: totatives_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
53 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
54 |
lemma one_in_totatives [simp]: "n > 0 \<Longrightarrow> Suc 0 \<in> totatives n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
55 |
by (auto simp: totatives_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
56 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
57 |
lemma totatives_eq_empty_iff [simp]: "totatives n = {} \<longleftrightarrow> n = 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
58 |
using one_in_totatives[of n] by (auto simp del: one_in_totatives) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
59 |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
60 |
lemma minus_one_in_totatives: |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
61 |
assumes "n \<ge> 2" |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
62 |
shows "n - 1 \<in> totatives n" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
63 |
using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
64 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
65 |
lemma totatives_prime_power_Suc: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
66 |
assumes "prime p" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
67 |
shows "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m) ` {0<..p^n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
68 |
proof safe |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
69 |
fix m assume m: "p * m \<in> totatives (p ^ Suc n)" and m: "m \<in> {0<..p^n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
70 |
thus False using assms by (auto simp: totatives_def gcd_mult_left) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
71 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
72 |
fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
73 |
from k have "\<not>(p dvd k)" by (auto elim!: dvdE) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
74 |
hence "coprime k (p ^ Suc n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
75 |
using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
76 |
with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
77 |
qed (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
78 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
79 |
lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
80 |
using totatives_prime_power_Suc[of p 0] by fastforce |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
81 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
82 |
lemma bij_betw_totatives: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
83 |
assumes "m1 > 1" "m2 > 1" "coprime m1 m2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
84 |
shows "bij_betw (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2)) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
85 |
(totatives m1 \<times> totatives m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
86 |
unfolding bij_betw_def |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
87 |
proof |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
88 |
show "inj_on (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
89 |
proof (intro inj_onI, clarify) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
90 |
fix x y assume xy: "x \<in> totatives (m1 * m2)" "y \<in> totatives (m1 * m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
91 |
"x mod m1 = y mod m1" "x mod m2 = y mod m2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
92 |
have ex: "\<exists>!z. z < m1 * m2 \<and> [z = x] (mod m1) \<and> [z = x] (mod m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
93 |
by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
94 |
have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
95 |
"y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
96 |
using xy assms by (simp_all add: totatives_less one_less_mult cong_nat_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
97 |
from this[THEN the1_equality[OF ex]] show "x = y" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
98 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
99 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
100 |
show "(\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1 * m2) = totatives m1 \<times> totatives m2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
101 |
proof safe |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
102 |
fix x assume "x \<in> totatives (m1 * m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
103 |
with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
104 |
by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
105 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
106 |
fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
107 |
with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
108 |
with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
109 |
where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_nat_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
110 |
from x ab assms(3) have "x \<in> totatives (m1 * m2)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
111 |
by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
112 |
with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
113 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
114 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
115 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
116 |
lemma bij_betw_totatives_gcd_eq: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
117 |
fixes n d :: nat |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
118 |
assumes "d dvd n" "n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
119 |
shows "bij_betw (\<lambda>k. k * d) (totatives (n div d)) {k\<in>{0<..n}. gcd k n = d}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
120 |
unfolding bij_betw_def |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
121 |
proof |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
122 |
show "inj_on (\<lambda>k. k * d) (totatives (n div d))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
123 |
by (auto simp: inj_on_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
124 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
125 |
show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
126 |
proof (intro equalityI subsetI, goal_cases) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
127 |
case (1 k) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
128 |
thus ?case using assms |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
129 |
by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d] |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
130 |
gcd_mult_right gcd.commute) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
131 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
132 |
case (2 k) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
133 |
hence "d dvd k" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
134 |
then obtain l where k: "k = l * d" by (elim dvdE) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
135 |
from 2 and assms show ?case unfolding k |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
136 |
by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d] |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
137 |
gcd_mult_right elim!: dvdE) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
138 |
qed |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
139 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
140 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
141 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
142 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
143 |
definition totient :: "nat \<Rightarrow> nat" where |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
144 |
"totient n = card (totatives n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
145 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
146 |
primrec totient_naive :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
147 |
"totient_naive 0 acc n = acc" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
148 |
| "totient_naive (Suc k) acc n = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
149 |
(if coprime (Suc k) n then totient_naive k (acc + 1) n else totient_naive k acc n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
150 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
151 |
lemma totient_naive: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
152 |
"totient_naive k acc n = card {x \<in> {0<..k}. coprime x n} + acc" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
153 |
proof (induction k arbitrary: acc) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
154 |
case (Suc k acc) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
155 |
have "totient_naive (Suc k) acc n = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
156 |
(if coprime (Suc k) n then 1 else 0) + card {x \<in> {0<..k}. coprime x n} + acc" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
157 |
using Suc by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
158 |
also have "(if coprime (Suc k) n then 1 else 0) = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
159 |
card (if coprime (Suc k) n then {Suc k} else {})" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
160 |
also have "\<dots> + card {x \<in> {0<..k}. coprime x n} = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
161 |
card ((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n})" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
162 |
by (intro card_Un_disjoint [symmetric]) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
163 |
also have "((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n}) = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
164 |
{x \<in> {0<..Suc k}. coprime x n}" by (auto elim: le_SucE) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
165 |
finally show ?case . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
166 |
qed simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
167 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
168 |
lemma totient_code_naive [code]: "totient n = totient_naive n 0 n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
169 |
by (subst totient_naive) (simp add: totient_def totatives_def) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
170 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
171 |
lemma totient_le: "totient n \<le> n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
172 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
173 |
have "card (totatives n) \<le> card {0<..n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
174 |
by (intro card_mono) (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
175 |
thus ?thesis by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
176 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
177 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
178 |
lemma totient_less: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
179 |
assumes "n > 1" |
66305 | 180 |
shows "totient n < n" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
181 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
182 |
from assms have "card (totatives n) \<le> card {0<..<n}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
183 |
using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
184 |
with assms show ?thesis by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
185 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
186 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
187 |
lemma totient_0 [simp]: "totient 0 = 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
188 |
by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
189 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
190 |
lemma totient_Suc_0 [simp]: "totient (Suc 0) = Suc 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
191 |
by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
192 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
193 |
lemma totient_1 [simp]: "totient 1 = Suc 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
194 |
by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
195 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
196 |
lemma totient_0_iff [simp]: "totient n = 0 \<longleftrightarrow> n = 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
197 |
by (auto simp: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
198 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
199 |
lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
200 |
by (auto intro: Nat.gr0I) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
201 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
202 |
lemma card_gcd_eq_totient: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
203 |
"n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
204 |
unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq]) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
205 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
206 |
lemma totient_divisor_sum: "(\<Sum>d | d dvd n. totient d) = n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
207 |
proof (cases "n = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
208 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
209 |
hence "n > 0" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
210 |
define A where "A = (\<lambda>d. {k\<in>{0<..n}. gcd k n = d})" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
211 |
have *: "card (A d) = totient (n div d)" if d: "d dvd n" for d |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
212 |
using \<open>n > 0\<close> and d unfolding A_def by (rule card_gcd_eq_totient) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
213 |
have "n = card {1..n}" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
214 |
also have "{1..n} = (\<Union>d\<in>{d. d dvd n}. A d)" by safe (auto simp: A_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
215 |
also have "card \<dots> = (\<Sum>d | d dvd n. card (A d))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
216 |
using \<open>n > 0\<close> by (intro card_UN_disjoint) (auto simp: A_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
217 |
also have "\<dots> = (\<Sum>d | d dvd n. totient (n div d))" by (intro sum.cong refl *) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
218 |
also have "\<dots> = (\<Sum>d | d dvd n. totient d)" using \<open>n > 0\<close> |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
219 |
by (intro sum.reindex_bij_witness[of _ "op div n" "op div n"]) (auto elim: dvdE) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
220 |
finally show ?thesis .. |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
221 |
qed auto |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
222 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
223 |
lemma totient_mult_coprime: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
224 |
assumes "coprime m n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
225 |
shows "totient (m * n) = totient m * totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
226 |
proof (cases "m > 1 \<and> n > 1") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
227 |
case True |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
228 |
hence mn: "m > 1" "n > 1" by simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
229 |
have "totient (m * n) = card (totatives (m * n))" by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
230 |
also have "\<dots> = card (totatives m \<times> totatives n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
231 |
using bij_betw_totatives [OF mn \<open>coprime m n\<close>] by (rule bij_betw_same_card) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
232 |
also have "\<dots> = totient m * totient n" by (simp add: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
233 |
finally show ?thesis . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
234 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
235 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
236 |
with assms show ?thesis by (cases m; cases n) auto |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
237 |
qed |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
238 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
239 |
lemma totient_prime_power_Suc: |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
240 |
assumes "prime p" |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
241 |
shows "totient (p ^ Suc n) = p ^ n * (p - 1)" |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
242 |
proof - |
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
243 |
from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - op * p ` {0<..p ^ n})" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
244 |
unfolding totient_def by (subst totatives_prime_power_Suc) simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
245 |
also from assms have "\<dots> = p ^ Suc n - card (op * p ` {0<..p^n})" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
246 |
by (subst card_Diff_subset) (auto intro: prime_gt_0_nat) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
247 |
also from assms have "card (op * p ` {0<..p^n}) = p ^ n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
248 |
by (subst card_image) (auto simp: inj_on_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
249 |
also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
250 |
finally show ?thesis . |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
251 |
qed |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
252 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
253 |
lemma totient_prime_power: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
254 |
assumes "prime p" "n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
255 |
shows "totient (p ^ n) = p ^ (n - 1) * (p - 1)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
256 |
using totient_prime_power_Suc[of p "n - 1"] assms by simp |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
257 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
258 |
lemma totient_imp_prime: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
259 |
assumes "totient p = p - 1" "p > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
260 |
shows "prime p" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
261 |
proof (cases "p = 1") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
262 |
case True |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
263 |
with assms show ?thesis by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
264 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
265 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
266 |
with assms have p: "p > 1" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
267 |
have "x \<in> {0<..<p}" if "x \<in> totatives p" for x |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
268 |
using that and p by (cases "x = p") (auto simp: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
269 |
with assms have *: "totatives p = {0<..<p}" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
270 |
by (intro card_subset_eq) (auto simp: totient_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
271 |
have **: False if "x \<noteq> 1" "x \<noteq> p" "x dvd p" for x |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
272 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
273 |
from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
274 |
from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
275 |
from that and nz have "\<not>coprime x p" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
276 |
hence "x \<notin> totatives p" by (simp add: totatives_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
277 |
also note * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
278 |
finally show False using that and le by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
279 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
280 |
hence "(\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
281 |
with p show ?thesis by (subst prime_nat_iff) (auto dest: **) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
282 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
283 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
284 |
lemma totient_prime: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
285 |
assumes "prime p" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
286 |
shows "totient p = p - 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
287 |
using totient_prime_power_Suc[of p 0] assms by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
288 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
289 |
lemma totient_2 [simp]: "totient 2 = 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
290 |
and totient_3 [simp]: "totient 3 = 2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
291 |
and totient_5 [simp]: "totient 5 = 4" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
292 |
and totient_7 [simp]: "totient 7 = 6" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
293 |
by (subst totient_prime; simp)+ |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
294 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
295 |
lemma totient_4 [simp]: "totient 4 = 2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
296 |
and totient_8 [simp]: "totient 8 = 4" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
297 |
and totient_9 [simp]: "totient 9 = 6" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
298 |
using totient_prime_power[of 2 2] totient_prime_power[of 2 3] totient_prime_power[of 3 2] |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
299 |
by simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
300 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
301 |
lemma totient_6 [simp]: "totient 6 = 2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
302 |
using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat) |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
303 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
304 |
lemma totient_even: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
305 |
assumes "n > 2" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
306 |
shows "even (totient n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
307 |
proof (cases "\<exists>p. prime p \<and> p \<noteq> 2 \<and> p dvd n") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
308 |
case True |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
309 |
then obtain p where p: "prime p" "p \<noteq> 2" "p dvd n" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
310 |
from \<open>p \<noteq> 2\<close> have "p = 0 \<or> p = 1 \<or> p > 2" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
311 |
with p(1) have "odd p" using prime_odd_nat[of p] by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
312 |
define k where "k = multiplicity p n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
313 |
from p assms have k_pos: "k > 0" unfolding k_def by (subst multiplicity_gt_zero_iff) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
314 |
have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
315 |
then obtain m where m: "n = p ^ k * m" by (elim dvdE) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
316 |
with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
317 |
from k_def m_pos p have "\<not>p dvd m" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
318 |
by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
319 |
prime_elem_multiplicity_eq_zero_iff) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
320 |
hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)]) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
321 |
thus ?thesis using p k_pos \<open>odd p\<close> |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
322 |
by (auto simp add: m totient_mult_coprime totient_prime_power) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
323 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
324 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
325 |
from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
326 |
by (intro Primes.prime_factorization_nat) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
327 |
also from False have "\<dots> = (\<Prod>p\<in>prime_factors n. if p = 2 then 2 ^ multiplicity 2 n else 1)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
328 |
by (intro prod.cong refl) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
329 |
also have "\<dots> = 2 ^ multiplicity 2 n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
330 |
by (subst prod.delta[OF finite_set_mset]) (auto simp: prime_factors_multiplicity) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
331 |
finally have n: "n = 2 ^ multiplicity 2 n" . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
332 |
have "multiplicity 2 n = 0 \<or> multiplicity 2 n = 1 \<or> multiplicity 2 n > 1" by force |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
333 |
with n assms have "multiplicity 2 n > 1" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
334 |
thus ?thesis by (subst n) (simp add: totient_prime_power) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
335 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
336 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
337 |
lemma totient_prod_coprime: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
338 |
assumes "pairwise_coprime (f ` A)" "inj_on f A" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
339 |
shows "totient (prod f A) = prod (\<lambda>x. totient (f x)) A" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
340 |
using assms |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
341 |
proof (induction A rule: infinite_finite_induct) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
342 |
case (insert x A) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
343 |
from insert.prems and insert.hyps have *: "coprime (prod f A) (f x)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
344 |
by (intro prod_coprime[OF pairwise_coprimeD[OF insert.prems(1)]]) (auto simp: inj_on_def) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
345 |
from insert.hyps have "prod f (insert x A) = prod f A * f x" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
346 |
also have "totient \<dots> = totient (prod f A) * totient (f x)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
347 |
using insert.hyps insert.prems by (intro totient_mult_coprime *) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
348 |
also have "totient (prod f A) = (\<Prod>x\<in>A. totient (f x))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
349 |
using insert.prems by (intro insert.IH) (auto dest: pairwise_coprime_subset) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
350 |
also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>x\<in>insert x A. totient (f x))" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
351 |
finally show ?case . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
352 |
qed simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
353 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
354 |
(* TODO Move *) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
355 |
lemma prime_power_eq_imp_eq: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
356 |
fixes p q :: "'a :: factorial_semiring" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
357 |
assumes "prime p" "prime q" "m > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
358 |
assumes "p ^ m = q ^ n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
359 |
shows "p = q" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
360 |
proof (rule ccontr) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
361 |
assume pq: "p \<noteq> q" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
362 |
from assms have "m = multiplicity p (p ^ m)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
363 |
by (subst multiplicity_prime_power) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
364 |
also note \<open>p ^ m = q ^ n\<close> |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
365 |
also from assms pq have "multiplicity p (q ^ n) = 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
366 |
by (subst multiplicity_distinct_prime_power) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
367 |
finally show False using \<open>m > 0\<close> by simp |
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
368 |
qed |
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
369 |
|
65726
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
370 |
lemma totient_formula1: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
371 |
assumes "n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
372 |
shows "totient n = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
373 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
374 |
from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
375 |
by (rule prime_factorization_nat) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
376 |
also have "totient \<dots> = (\<Prod>x\<in>prime_factors n. totient (x ^ multiplicity x n))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
377 |
proof (rule totient_prod_coprime) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
378 |
show "pairwise_coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
379 |
proof (standard, clarify, goal_cases) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
380 |
fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
381 |
"p ^ multiplicity p n \<noteq> q ^ multiplicity q n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
382 |
thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
383 |
by (intro coprime_exp2 primes_coprime[of p q]) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
384 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
385 |
next |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
386 |
show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
387 |
proof |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
388 |
fix p q assume pq: "p \<in># prime_factorization n" "q \<in># prime_factorization n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
389 |
"p ^ multiplicity p n = q ^ multiplicity q n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
390 |
from assms and pq have "prime p" "prime q" "multiplicity p n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
391 |
by (simp_all add: prime_factors_multiplicity) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
392 |
from prime_power_eq_imp_eq[OF this pq(3)] show "p = q" . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
393 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
394 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
395 |
also have "\<dots> = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
396 |
by (intro prod.cong refl totient_prime_power) (auto simp: prime_factors_multiplicity) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
397 |
finally show ?thesis . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
398 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
399 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
400 |
lemma totient_dvd: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
401 |
assumes "m dvd n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
402 |
shows "totient m dvd totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
403 |
proof (cases "m = 0 \<or> n = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
404 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
405 |
let ?M = "\<lambda>p m :: nat. multiplicity p m - 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
406 |
have "(\<Prod>p\<in>prime_factors m. p ^ ?M p m * (p - 1)) dvd |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
407 |
(\<Prod>p\<in>prime_factors n. p ^ ?M p n * (p - 1))" using assms False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
408 |
by (intro prod_dvd_prod_subset2 mult_dvd_mono dvd_refl le_imp_power_dvd diff_le_mono |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
409 |
dvd_prime_factors dvd_imp_multiplicity_le) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
410 |
with False show ?thesis by (simp add: totient_formula1) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
411 |
qed (insert assms, auto) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
412 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
413 |
lemma totient_dvd_mono: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
414 |
assumes "m dvd n" "n > 0" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
415 |
shows "totient m \<le> totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
416 |
by (cases "m = 0") (insert assms, auto intro: dvd_imp_le totient_dvd) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
417 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
418 |
(* TODO Move *) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
419 |
lemma prime_factors_power: "n > 0 \<Longrightarrow> prime_factors (x ^ n) = prime_factors x" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
420 |
by (cases "x = 0"; cases "n = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
421 |
(auto simp: prime_factors_multiplicity prime_elem_multiplicity_power_distrib zero_power) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
422 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
423 |
lemma totient_formula2: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
424 |
"real (totient n) = real n * (\<Prod>p\<in>prime_factors n. 1 - 1 / real p)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
425 |
proof (cases "n = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
426 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
427 |
have "real (totient n) = (\<Prod>p\<in>prime_factors n. real |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
428 |
(p ^ (multiplicity p n - 1) * (p - 1)))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
429 |
using False by (subst totient_formula1) simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
430 |
also have "\<dots> = (\<Prod>p\<in>prime_factors n. real (p ^ multiplicity p n) * (1 - 1 / real p))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
431 |
by (intro prod.cong refl) (auto simp add: field_simps prime_factors_multiplicity |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
432 |
prime_ge_Suc_0_nat of_nat_diff power_Suc [symmetric] simp del: power_Suc) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
433 |
also have "\<dots> = real (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
434 |
(\<Prod>p\<in>prime_factors n. 1 - 1 / real p)" by (subst prod.distrib) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
435 |
also have "(\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
436 |
using False by (intro Primes.prime_factorization_nat [symmetric]) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
437 |
finally show ?thesis . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
438 |
qed auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
439 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
440 |
lemma totient_gcd: "totient (a * b) * totient (gcd a b) = totient a * totient b * gcd a b" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
441 |
proof (cases "a = 0 \<or> b = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
442 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
443 |
let ?P = "prime_factors :: nat \<Rightarrow> nat set" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
444 |
have "real (totient a * totient b * gcd a b) = real (a * b * gcd a b) * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
445 |
((\<Prod>p\<in>?P a. 1 - 1 / real p) * (\<Prod>p\<in>?P b. 1 - 1 / real p))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
446 |
by (simp add: totient_formula2) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
447 |
also have "?P a = (?P a - ?P b) \<union> (?P a \<inter> ?P b)" by auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
448 |
also have "(\<Prod>p\<in>\<dots>. 1 - 1 / real p) = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
449 |
(\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
450 |
by (rule prod.union_disjoint) blast+ |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
451 |
also have "\<dots> * (\<Prod>p\<in>?P b. 1 - 1 / real p) = (\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
452 |
(\<Prod>p\<in>?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)" (is "_ = ?A * _") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
453 |
by (simp only: mult_ac) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
454 |
also have "?A = (\<Prod>p\<in>?P a - ?P b \<union> ?P b. 1 - 1 / real p)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
455 |
by (rule prod.union_disjoint [symmetric]) blast+ |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
456 |
also have "?P a - ?P b \<union> ?P b = ?P a \<union> ?P b" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
457 |
also have "real (a * b * gcd a b) * ((\<Prod>p\<in>\<dots>. 1 - 1 / real p) * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
458 |
(\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)) = real (totient (a * b) * totient (gcd a b))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
459 |
using False by (simp add: totient_formula2 prime_factors_product prime_factorization_gcd) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
460 |
finally show ?thesis by (simp only: of_nat_eq_iff) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
461 |
qed auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
462 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
463 |
lemma totient_mult: "totient (a * b) = totient a * totient b * gcd a b div totient (gcd a b)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
464 |
by (subst totient_gcd [symmetric]) simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
465 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
466 |
lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
467 |
using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
468 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
469 |
(* TODO Move *) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
470 |
lemma gcd_2_odd: |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
471 |
assumes "odd (n::nat)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
472 |
shows "gcd n 2 = 1" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
473 |
proof - |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
474 |
from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
475 |
have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
476 |
thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
477 |
qed |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
478 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
479 |
lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
480 |
by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
481 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
482 |
lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
483 |
proof (induction m arbitrary: n) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
484 |
case (Suc m n) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
485 |
have "totient (n ^ Suc (Suc m)) = totient (n * n ^ Suc m)" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
486 |
also have "\<dots> = n ^ Suc m * totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
487 |
using Suc.IH by (subst totient_mult) simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
488 |
finally show ?case . |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
489 |
qed simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
490 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
491 |
lemma totient_power: "m > 0 \<Longrightarrow> totient (n ^ m) = n ^ (m - 1) * totient n" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
492 |
using totient_power_Suc[of n "m - 1"] by (cases m) simp_all |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
493 |
|
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
494 |
lemma totient_gcd_lcm: "totient (gcd a b) * totient (lcm a b) = totient a * totient b" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
495 |
proof (cases "a = 0 \<or> b = 0") |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
496 |
case False |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
497 |
let ?P = "prime_factors :: nat \<Rightarrow> nat set" and ?f = "\<lambda>p::nat. 1 - 1 / real p" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
498 |
have "real (totient (gcd a b) * totient (lcm a b)) = real (gcd a b * lcm a b) * |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
499 |
(prod ?f (?P a \<inter> ?P b) * prod ?f (?P a \<union> ?P b))" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
500 |
using False unfolding of_nat_mult |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
501 |
by (simp add: totient_formula2 prime_factorization_gcd prime_factorization_lcm) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
502 |
also have "gcd a b * lcm a b = a * b" by simp |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
503 |
also have "?P a \<union> ?P b = (?P a - ?P a \<inter> ?P b) \<union> ?P b" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
504 |
also have "prod ?f \<dots> = prod ?f (?P a - ?P a \<inter> ?P b) * prod ?f (?P b)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
505 |
by (rule prod.union_disjoint) blast+ |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
506 |
also have "prod ?f (?P a \<inter> ?P b) * \<dots> = |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
507 |
prod ?f (?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b)) * prod ?f (?P b)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
508 |
by (subst prod.union_disjoint) auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
509 |
also have "?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b) = ?P a" by blast |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
510 |
also have "real (a * b) * (prod ?f (?P a) * prod ?f (?P b)) = real (totient a * totient b)" |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
511 |
using False by (simp add: totient_formula2) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
512 |
finally show ?thesis by (simp only: of_nat_eq_iff) |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
513 |
qed auto |
f5d64d094efe
More material on totient function
eberlm <eberlm@in.tum.de>
parents:
65465
diff
changeset
|
514 |
|
65465
067210a08a22
more fundamental euler's totient function on nat rather than int;
haftmann
parents:
diff
changeset
|
515 |
end |