More material on totient function
authoreberlm <eberlm@in.tum.de>
Thu May 04 16:49:29 2017 +0200 (2017-05-04)
changeset 65726f5d64d094efe
parent 65720 c5b19f997214
child 65727 33368a2296aa
More material on totient function
src/HOL/Number_Theory/Pocklington.thy
src/HOL/Number_Theory/Residues.thy
src/HOL/Number_Theory/Totient.thy
     1.1 --- a/src/HOL/Number_Theory/Pocklington.thy	Thu May 04 15:15:07 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Pocklington.thy	Thu May 04 16:49:29 2017 +0200
     1.3 @@ -144,7 +144,7 @@
     1.4    assumes n: "n \<ge> 2" and an: "[a ^ (n - 1) = 1] (mod n)"
     1.5    and nm: "\<forall>m. 0 < m \<and> m < n - 1 \<longrightarrow> \<not> [a ^ m = 1] (mod n)"
     1.6    shows "prime n"
     1.7 -using \<open>n \<ge> 2\<close> proof (rule totient_prime)
     1.8 +proof (rule totient_imp_prime)
     1.9    show "totient n = n - 1"
    1.10    proof (rule ccontr)
    1.11      have "[a ^ totient n = 1] (mod n)"
    1.12 @@ -152,11 +152,11 @@
    1.13          (use n an in auto)
    1.14      moreover assume "totient n \<noteq> n - 1"
    1.15      then have "totient n > 0 \<and> totient n < n - 1"
    1.16 -      using \<open>n \<ge> 2\<close> by (simp add: order_less_le)
    1.17 +      using \<open>n \<ge> 2\<close> and totient_less[of n] by simp
    1.18      ultimately show False
    1.19        using nm by auto
    1.20    qed
    1.21 -qed
    1.22 +qed (insert n, auto)
    1.23  
    1.24  lemma nat_exists_least_iff: "(\<exists>(n::nat). P n) \<longleftrightarrow> (\<exists>n. P n \<and> (\<forall>m < n. \<not> P m))"
    1.25    by (metis ex_least_nat_le not_less0)
    1.26 @@ -527,7 +527,7 @@
    1.27        by auto}
    1.28    hence d1: "d = 1" by blast
    1.29    hence o: "ord p (a^r) = q" using d by simp
    1.30 -  from pp prime_totient [of p]
    1.31 +  from pp totient_prime [of p]
    1.32    have totient_eq: "totient p = p - 1" by simp
    1.33    {fix d assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
    1.34      from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
     2.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu May 04 15:15:07 2017 +0100
     2.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu May 04 16:49:29 2017 +0200
     2.3 @@ -31,7 +31,7 @@
     2.4  where
     2.5    "residue_ring m =
     2.6      \<lparr>carrier = {0..m - 1},
     2.7 -     mult = \<lambda>x y. (x * y) mod m,
     2.8 +     monoid.mult = \<lambda>x y. (x * y) mod m,
     2.9       one = 1,
    2.10       zero = 0,
    2.11       add = \<lambda>x y. (x + y) mod m\<rparr>"
    2.12 @@ -247,18 +247,22 @@
    2.13  
    2.14  lemma (in residues) totient_eq:
    2.15    "totient (nat m) = card (Units R)"
    2.16 +  thm R_def
    2.17  proof -
    2.18    have *: "inj_on nat (Units R)"
    2.19      by (rule inj_onI) (auto simp add: res_units_eq)
    2.20 -  have "totatives (nat m) = nat ` Units R"
    2.21 -    by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1))
    2.22 -      (smt One_nat_def image_def mem_Collect_eq nat_0 nat_eq_iff nat_less_iff of_nat_1 transfer_int_nat_gcd(1))
    2.23 +  define m' where "m' = nat m"
    2.24 +  from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
    2.25 +  from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
    2.26 +    unfolding res_units_eq
    2.27 +    by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
    2.28 +  hence "Units R = int ` totatives m'" by blast
    2.29 +  hence "totatives m' = nat ` Units R" by (simp add: image_image)
    2.30    then have "card (totatives (nat m)) = card (nat ` Units R)"
    2.31 -    by simp
    2.32 +    by (simp add: m'_def)
    2.33    also have "\<dots> = card (Units R)"
    2.34      using * card_image [of nat "Units R"] by auto
    2.35 -  finally show ?thesis
    2.36 -    by simp
    2.37 +  finally show ?thesis by (simp add: totient_def)
    2.38  qed
    2.39  
    2.40  lemma (in residues_prime) totient_eq: "totient p = p - 1"
    2.41 @@ -298,7 +302,7 @@
    2.42    then have "[a ^ totient p = 1] (mod p)"
    2.43       by (rule euler_theorem)
    2.44    also have "totient p = p - 1"
    2.45 -    by (rule prime_totient) (rule assms)
    2.46 +    by (rule totient_prime) (rule assms)
    2.47    finally show ?thesis .
    2.48  qed
    2.49  
     3.1 --- a/src/HOL/Number_Theory/Totient.thy	Thu May 04 15:15:07 2017 +0100
     3.2 +++ b/src/HOL/Number_Theory/Totient.thy	Thu May 04 16:49:29 2017 +0200
     3.3 @@ -1,164 +1,515 @@
     3.4  (*  Title:      HOL/Number_Theory/Totient.thy
     3.5      Author:     Jeremy Avigad
     3.6      Author:     Florian Haftmann
     3.7 +    Author:     Manuel Eberl
     3.8  *)
     3.9  
    3.10  section \<open>Fundamental facts about Euler's totient function\<close>
    3.11  
    3.12  theory Totient
    3.13  imports
    3.14 +  Complex_Main
    3.15    "~~/src/HOL/Computational_Algebra/Primes"
    3.16 +  "~~/src/HOL/Number_Theory/Cong"
    3.17  begin
    3.18 -
    3.19 -definition totatives :: "nat \<Rightarrow> nat set"
    3.20 -  where "totatives n = {m. 0 < m \<and> m < n \<and> coprime m n}"
    3.21 -
    3.22 -lemma in_totatives_iff [simp]:
    3.23 -  "m \<in> totatives n \<longleftrightarrow> 0 < m \<and> m < n \<and> coprime m n"
    3.24 +  
    3.25 +definition totatives :: "nat \<Rightarrow> nat set" where
    3.26 +  "totatives n = {k \<in> {0<..n}. coprime k n}"
    3.27 +  
    3.28 +lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
    3.29 +  by (simp add: totatives_def)
    3.30 +  
    3.31 +lemma totatives_code [code]: "totatives n = Set.filter (\<lambda>k. coprime k n) {0<..n}"
    3.32 +  by (simp add: totatives_def Set.filter_def)
    3.33 +  
    3.34 +lemma finite_totatives [simp]: "finite (totatives n)"
    3.35    by (simp add: totatives_def)
    3.36 -
    3.37 -lemma finite_totatives [simp]:
    3.38 -  "finite (totatives n)"
    3.39 -  by (simp add: totatives_def)
    3.40 -
    3.41 -lemma totatives_subset:
    3.42 -  "totatives n \<subseteq> {1..<n}"
    3.43 -  by auto
    3.44 +    
    3.45 +lemma totatives_subset: "totatives n \<subseteq> {0<..n}"
    3.46 +  by (auto simp: totatives_def)
    3.47 +    
    3.48 +lemma zero_not_in_totatives [simp]: "0 \<notin> totatives n"
    3.49 +  by (auto simp: totatives_def)
    3.50 +    
    3.51 +lemma totatives_le: "x \<in> totatives n \<Longrightarrow> x \<le> n"
    3.52 +  by (auto simp: totatives_def)
    3.53 +    
    3.54 +lemma totatives_less: 
    3.55 +  assumes "x \<in> totatives n" "n > 1"
    3.56 +  shows   "x < n"
    3.57 +proof -
    3.58 +  from assms have "x \<noteq> n" by (auto simp: totatives_def)
    3.59 +  with totatives_le[OF assms(1)] show ?thesis by simp
    3.60 +qed
    3.61  
    3.62 -lemma totatives_subset_Suc_0 [simp]:
    3.63 -  "totatives n \<subseteq> {Suc 0..<n}"
    3.64 -  using totatives_subset [of n] by simp
    3.65 +lemma totatives_0 [simp]: "totatives 0 = {}"
    3.66 +  by (auto simp: totatives_def)
    3.67  
    3.68 -lemma totatives_0 [simp]:
    3.69 -  "totatives 0 = {}"
    3.70 -  using totatives_subset [of 0] by simp
    3.71 +lemma totatives_1 [simp]: "totatives 1 = {Suc 0}"
    3.72 +  by (auto simp: totatives_def)
    3.73  
    3.74 -lemma totatives_1 [simp]:
    3.75 -  "totatives 1 = {}"
    3.76 -  using totatives_subset [of 1] by simp
    3.77 +lemma totatives_Suc_0 [simp]: "totatives (Suc 0) = {Suc 0}"
    3.78 +  by (auto simp: totatives_def)
    3.79  
    3.80 -lemma totatives_Suc_0 [simp]:
    3.81 -  "totatives (Suc 0) = {}"
    3.82 -  using totatives_1 by simp
    3.83 +lemma one_in_totatives [simp]: "n > 0 \<Longrightarrow> Suc 0 \<in> totatives n"
    3.84 +  by (auto simp: totatives_def)
    3.85  
    3.86 -lemma one_in_totatives:
    3.87 -  assumes "n \<ge> 2"
    3.88 -  shows "1 \<in> totatives n"
    3.89 -  using assms by simp
    3.90 -
    3.91 +lemma totatives_eq_empty_iff [simp]: "totatives n = {} \<longleftrightarrow> n = 0"
    3.92 +  using one_in_totatives[of n] by (auto simp del: one_in_totatives)
    3.93 +    
    3.94  lemma minus_one_in_totatives:
    3.95    assumes "n \<ge> 2"
    3.96    shows "n - 1 \<in> totatives n"
    3.97 -  using assms coprime_minus_one_nat [of n] by simp
    3.98 +  using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
    3.99  
   3.100 -lemma totatives_eq_empty_iff [simp]:
   3.101 -  "totatives n = {} \<longleftrightarrow> n \<in> {0, 1}"
   3.102 +lemma totatives_prime_power_Suc:
   3.103 +  assumes "prime p"
   3.104 +  shows   "totatives (p ^ Suc n) = {0<..p^Suc n} - (\<lambda>m. p * m) ` {0<..p^n}"
   3.105 +proof safe
   3.106 +  fix m assume m: "p * m \<in> totatives (p ^ Suc n)" and m: "m \<in> {0<..p^n}"
   3.107 +  thus False using assms by (auto simp: totatives_def gcd_mult_left)
   3.108 +next
   3.109 +  fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
   3.110 +  from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
   3.111 +  hence "coprime k (p ^ Suc n)"
   3.112 +    using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
   3.113 +  with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
   3.114 +qed (auto simp: totatives_def)
   3.115 +
   3.116 +lemma totatives_prime: "prime p \<Longrightarrow> totatives p = {0<..<p}"
   3.117 +  using totatives_prime_power_Suc[of p 0] by fastforce
   3.118 +
   3.119 +lemma bij_betw_totatives:
   3.120 +  assumes "m1 > 1" "m2 > 1" "coprime m1 m2"
   3.121 +  shows   "bij_betw (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2)) 
   3.122 +             (totatives m1 \<times> totatives m2)"
   3.123 +  unfolding bij_betw_def
   3.124  proof
   3.125 -  assume "totatives n = {}"
   3.126 -  show "n \<in> {0, 1}"
   3.127 -  proof (rule ccontr)
   3.128 -    assume "n \<notin> {0, 1}"
   3.129 -    then have "n \<ge> 2"
   3.130 -      by simp
   3.131 -    then have "1 \<in> totatives n"
   3.132 -      by (rule one_in_totatives)
   3.133 -    with \<open>totatives n = {}\<close> show False
   3.134 -      by simp
   3.135 +  show "inj_on (\<lambda>x. (x mod m1, x mod m2)) (totatives (m1 * m2))"
   3.136 +  proof (intro inj_onI, clarify)
   3.137 +    fix x y assume xy: "x \<in> totatives (m1 * m2)" "y \<in> totatives (m1 * m2)"
   3.138 +                       "x mod m1 = y mod m1" "x mod m2 = y mod m2"
   3.139 +    have ex: "\<exists>!z. z < m1 * m2 \<and> [z = x] (mod m1) \<and> [z = x] (mod m2)"
   3.140 +      by (rule binary_chinese_remainder_unique_nat) (insert assms, simp_all)
   3.141 +    have "x < m1 * m2 \<and> [x = x] (mod m1) \<and> [x = x] (mod m2)"
   3.142 +         "y < m1 * m2 \<and> [y = x] (mod m1) \<and> [y = x] (mod m2)"
   3.143 +      using xy assms by (simp_all add: totatives_less one_less_mult cong_nat_def)
   3.144 +    from this[THEN the1_equality[OF ex]] show "x = y" by simp
   3.145 +  qed
   3.146 +next
   3.147 +  show "(\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1 * m2) = totatives m1 \<times> totatives m2"
   3.148 +  proof safe
   3.149 +    fix x assume "x \<in> totatives (m1 * m2)"
   3.150 +    with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
   3.151 +      by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
   3.152 +  next
   3.153 +    fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
   3.154 +    with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
   3.155 +    with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
   3.156 +      where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_nat_def)
   3.157 +    from x ab assms(3) have "x \<in> totatives (m1 * m2)"
   3.158 +      by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
   3.159 +    with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   3.160 +  qed
   3.161 +qed
   3.162 +
   3.163 +lemma bij_betw_totatives_gcd_eq:
   3.164 +  fixes n d :: nat
   3.165 +  assumes "d dvd n" "n > 0"
   3.166 +  shows   "bij_betw (\<lambda>k. k * d) (totatives (n div d)) {k\<in>{0<..n}. gcd k n = d}"
   3.167 +  unfolding bij_betw_def
   3.168 +proof
   3.169 +  show "inj_on (\<lambda>k. k * d) (totatives (n div d))"
   3.170 +    by (auto simp: inj_on_def)
   3.171 +next
   3.172 +  show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
   3.173 +  proof (intro equalityI subsetI, goal_cases)
   3.174 +    case (1 k)
   3.175 +    thus ?case using assms
   3.176 +      by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
   3.177 +                                 gcd_mult_right gcd.commute)
   3.178 +  next
   3.179 +    case (2 k)
   3.180 +    hence "d dvd k" by auto
   3.181 +    then obtain l where k: "k = l * d" by (elim dvdE) auto
   3.182 +    from 2 and assms show ?case unfolding k
   3.183 +      by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d] 
   3.184 +                                    gcd_mult_right elim!: dvdE)
   3.185    qed
   3.186 -qed auto
   3.187 +qed
   3.188 +
   3.189 +
   3.190 +
   3.191 +definition totient :: "nat \<Rightarrow> nat" where
   3.192 +  "totient n = card (totatives n)"
   3.193 +  
   3.194 +primrec totient_naive :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat" where
   3.195 +  "totient_naive 0 acc n = acc"
   3.196 +| "totient_naive (Suc k) acc n =
   3.197 +     (if coprime (Suc k) n then totient_naive k (acc + 1) n else totient_naive k acc n)"
   3.198 +  
   3.199 +lemma totient_naive:
   3.200 +  "totient_naive k acc n = card {x \<in> {0<..k}. coprime x n} + acc"
   3.201 +proof (induction k arbitrary: acc)
   3.202 +  case (Suc k acc)
   3.203 +  have "totient_naive (Suc k) acc n = 
   3.204 +          (if coprime (Suc k) n then 1 else 0) + card {x \<in> {0<..k}. coprime x n} + acc"
   3.205 +    using Suc by simp
   3.206 +  also have "(if coprime (Suc k) n then 1 else 0) = 
   3.207 +               card (if coprime (Suc k) n then {Suc k} else {})" by auto
   3.208 +  also have "\<dots> + card {x \<in> {0<..k}. coprime x n} =
   3.209 +               card ((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n})"
   3.210 +    by (intro card_Un_disjoint [symmetric]) auto
   3.211 +  also have "((if coprime (Suc k) n then {Suc k} else {}) \<union> {x \<in> {0<..k}. coprime x n}) =
   3.212 +               {x \<in> {0<..Suc k}. coprime x n}" by (auto elim: le_SucE)
   3.213 +  finally show ?case .
   3.214 +qed simp_all
   3.215 +  
   3.216 +lemma totient_code_naive [code]: "totient n = totient_naive n 0 n"
   3.217 +  by (subst totient_naive) (simp add: totient_def totatives_def)
   3.218  
   3.219 -lemma prime_totatives:
   3.220 -  assumes "prime p"
   3.221 -  shows "totatives p = {1..<p}"
   3.222 -proof
   3.223 -  show "{1..<p} \<subseteq> totatives p"
   3.224 -  proof
   3.225 -    fix n
   3.226 -    assume "n \<in> {1..<p}"
   3.227 -    with nat_dvd_not_less have "\<not> p dvd n"
   3.228 -      by auto
   3.229 -    with assms prime_imp_coprime [of p n] have "coprime p n"
   3.230 -      by simp
   3.231 -    with \<open>n \<in> {1..<p}\<close> show "n \<in> totatives p"
   3.232 -      by (auto simp add: totatives_def ac_simps)
   3.233 -  qed
   3.234 +lemma totient_le: "totient n \<le> n"
   3.235 +proof -
   3.236 +  have "card (totatives n) \<le> card {0<..n}"
   3.237 +    by (intro card_mono) (auto simp: totatives_def)
   3.238 +  thus ?thesis by (simp add: totient_def)
   3.239 +qed
   3.240 +  
   3.241 +lemma totient_less: 
   3.242 +  assumes "n > 1"
   3.243 +  shows   "totient n < n"
   3.244 +proof -
   3.245 +  from assms have "card (totatives n) \<le> card {0<..<n}"
   3.246 +    using totatives_less[of _ n] totatives_subset[of n] by (intro card_mono) auto
   3.247 +  with assms show ?thesis by (simp add: totient_def)
   3.248 +qed    
   3.249 +
   3.250 +lemma totient_0 [simp]: "totient 0 = 0"
   3.251 +  by (simp add: totient_def)
   3.252 +
   3.253 +lemma totient_Suc_0 [simp]: "totient (Suc 0) = Suc 0"
   3.254 +  by (simp add: totient_def)
   3.255 +
   3.256 +lemma totient_1 [simp]: "totient 1 = Suc 0"
   3.257 +  by simp
   3.258 +
   3.259 +lemma totient_0_iff [simp]: "totient n = 0 \<longleftrightarrow> n = 0"
   3.260 +  by (auto simp: totient_def)
   3.261 +
   3.262 +lemma totient_gt_0_iff [simp]: "totient n > 0 \<longleftrightarrow> n > 0"
   3.263 +  by (auto intro: Nat.gr0I)
   3.264 +
   3.265 +lemma card_gcd_eq_totient:
   3.266 +  "n > 0 \<Longrightarrow> d dvd n \<Longrightarrow> card {k\<in>{0<..n}. gcd k n = d} = totient (n div d)"
   3.267 +  unfolding totient_def by (rule sym, rule bij_betw_same_card[OF bij_betw_totatives_gcd_eq])
   3.268 +  
   3.269 +lemma totient_divisor_sum: "(\<Sum>d | d dvd n. totient d) = n"
   3.270 +proof (cases "n = 0")
   3.271 +  case False
   3.272 +  hence "n > 0" by simp
   3.273 +  define A where "A = (\<lambda>d. {k\<in>{0<..n}. gcd k n = d})"
   3.274 +  have *: "card (A d) = totient (n div d)" if d: "d dvd n" for d
   3.275 +    using \<open>n > 0\<close> and d unfolding A_def by (rule card_gcd_eq_totient)  
   3.276 +  have "n = card {1..n}" by simp
   3.277 +  also have "{1..n} = (\<Union>d\<in>{d. d dvd n}. A d)" by safe (auto simp: A_def)
   3.278 +  also have "card \<dots> = (\<Sum>d | d dvd n. card (A d))"
   3.279 +    using \<open>n > 0\<close> by (intro card_UN_disjoint) (auto simp: A_def)
   3.280 +  also have "\<dots> = (\<Sum>d | d dvd n. totient (n div d))" by (intro sum.cong refl *) auto
   3.281 +  also have "\<dots> = (\<Sum>d | d dvd n. totient d)" using \<open>n > 0\<close>
   3.282 +    by (intro sum.reindex_bij_witness[of _ "op div n" "op div n"]) (auto elim: dvdE)
   3.283 +  finally show ?thesis ..
   3.284  qed auto
   3.285  
   3.286 -lemma totatives_prime:
   3.287 -  assumes "p \<ge> 2" and "totatives p = {1..<p}"
   3.288 -  shows "prime p"
   3.289 -proof (rule ccontr)
   3.290 -  from \<open>2 \<le> p\<close> have "1 < p"
   3.291 -    by simp
   3.292 -  moreover assume "\<not> prime p"
   3.293 -  ultimately obtain n where "1 < n" "n < p" "n dvd p"
   3.294 -    by (auto simp add: prime_nat_iff)
   3.295 -      (metis Suc_lessD Suc_lessI dvd_imp_le dvd_pos_nat le_neq_implies_less)
   3.296 -  then have "n \<in> {1..<p}"
   3.297 -    by simp
   3.298 -  with assms have "n \<in> totatives p"
   3.299 -    by simp
   3.300 -  then have "coprime n p"
   3.301 -    by simp
   3.302 -  with \<open>1 < n\<close> \<open>n dvd p\<close> show False
   3.303 -    by simp
   3.304 +lemma totient_mult_coprime:
   3.305 +  assumes "coprime m n"
   3.306 +  shows   "totient (m * n) = totient m * totient n"
   3.307 +proof (cases "m > 1 \<and> n > 1")
   3.308 +  case True
   3.309 +  hence mn: "m > 1" "n > 1" by simp_all
   3.310 +  have "totient (m * n) = card (totatives (m * n))" by (simp add: totient_def)
   3.311 +  also have "\<dots> = card (totatives m \<times> totatives n)"
   3.312 +    using bij_betw_totatives [OF mn \<open>coprime m n\<close>] by (rule bij_betw_same_card)
   3.313 +  also have "\<dots> = totient m * totient n" by (simp add: totient_def)
   3.314 +  finally show ?thesis .
   3.315 +next
   3.316 +  case False
   3.317 +  with assms show ?thesis by (cases m; cases n) auto
   3.318  qed
   3.319  
   3.320 -definition totient :: "nat \<Rightarrow> nat"
   3.321 -  where "totient = card \<circ> totatives"
   3.322 -
   3.323 -lemma card_totatives [simp]:
   3.324 -  "card (totatives n) = totient n"
   3.325 -  by (simp add: totient_def)
   3.326 -
   3.327 -lemma totient_0 [simp]:
   3.328 -  "totient 0 = 0"
   3.329 -  by (simp add: totient_def)
   3.330 -
   3.331 -lemma totient_1 [simp]:
   3.332 -  "totient 1 = 0"
   3.333 -  by (simp add: totient_def)
   3.334 -
   3.335 -lemma totient_Suc_0 [simp]:
   3.336 -  "totient (Suc 0) = 0"
   3.337 -  using totient_1 by simp
   3.338 -  
   3.339 -lemma prime_totient:
   3.340 +lemma totient_prime_power_Suc:
   3.341    assumes "prime p"
   3.342 -  shows "totient p = p - 1"
   3.343 -  using assms prime_totatives
   3.344 -  by (simp add: totient_def)
   3.345 -
   3.346 -lemma totient_eq_0_iff [simp]:
   3.347 -  "totient n = 0 \<longleftrightarrow> n \<in> {0, 1}"
   3.348 -  by (simp only: totient_def comp_def card_eq_0_iff) auto
   3.349 -
   3.350 -lemma totient_noneq_0_iff [simp]:
   3.351 -  "totient n > 0 \<longleftrightarrow> 2 \<le> n"
   3.352 +  shows   "totient (p ^ Suc n) = p ^ n * (p - 1)"
   3.353  proof -
   3.354 -  have "totient n > 0 \<longleftrightarrow> totient n \<noteq> 0"
   3.355 -    by blast
   3.356 -  also have "\<dots> \<longleftrightarrow> 2 \<le> n"
   3.357 -    by auto
   3.358 +  from assms have "totient (p ^ Suc n) = card ({0<..p ^ Suc n} - op * p ` {0<..p ^ n})"
   3.359 +    unfolding totient_def by (subst totatives_prime_power_Suc) simp_all
   3.360 +  also from assms have "\<dots> = p ^ Suc n - card (op * p ` {0<..p^n})"
   3.361 +    by (subst card_Diff_subset) (auto intro: prime_gt_0_nat)
   3.362 +  also from assms have "card (op * p ` {0<..p^n}) = p ^ n"
   3.363 +    by (subst card_image) (auto simp: inj_on_def)
   3.364 +  also have "p ^ Suc n - p ^ n = p ^ n * (p - 1)" by (simp add: algebra_simps)
   3.365    finally show ?thesis .
   3.366  qed
   3.367  
   3.368 -lemma totient_less_eq:
   3.369 -  "totient n \<le> n - 1"
   3.370 -  using card_mono [of "{1..<n}" "totatives n"] by auto
   3.371 +lemma totient_prime_power:
   3.372 +  assumes "prime p" "n > 0"
   3.373 +  shows   "totient (p ^ n) = p ^ (n - 1) * (p - 1)"
   3.374 +  using totient_prime_power_Suc[of p "n - 1"] assms by simp
   3.375  
   3.376 -lemma totient_less_eq_Suc_0 [simp]:
   3.377 -  "totient n \<le> n - Suc 0"
   3.378 -  using totient_less_eq [of n] by simp
   3.379 +lemma totient_imp_prime:
   3.380 +  assumes "totient p = p - 1" "p > 0"
   3.381 +  shows   "prime p"
   3.382 +proof (cases "p = 1")
   3.383 +  case True
   3.384 +  with assms show ?thesis by auto
   3.385 +next
   3.386 +  case False
   3.387 +  with assms have p: "p > 1" by simp
   3.388 +  have "x \<in> {0<..<p}" if "x \<in> totatives p" for x
   3.389 +    using that and p by (cases "x = p") (auto simp: totatives_def)
   3.390 +  with assms have *: "totatives p = {0<..<p}"
   3.391 +    by (intro card_subset_eq) (auto simp: totient_def)
   3.392 +  have **: False if "x \<noteq> 1" "x \<noteq> p" "x dvd p" for x
   3.393 +  proof -
   3.394 +    from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
   3.395 +    from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
   3.396 +    from that and nz have "\<not>coprime x p" by auto
   3.397 +    hence "x \<notin> totatives p" by (simp add: totatives_def)
   3.398 +    also note *
   3.399 +    finally show False using that and le by auto
   3.400 +  qed
   3.401 +  hence "(\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)" by blast
   3.402 +  with p show ?thesis by (subst prime_nat_iff) (auto dest: **)
   3.403 +qed
   3.404 +    
   3.405 +lemma totient_prime:
   3.406 +  assumes "prime p"
   3.407 +  shows   "totient p = p - 1"
   3.408 +  using totient_prime_power_Suc[of p 0] assms by simp
   3.409 +
   3.410 +lemma totient_2 [simp]: "totient 2 = 1"
   3.411 +  and totient_3 [simp]: "totient 3 = 2"
   3.412 +  and totient_5 [simp]: "totient 5 = 4"
   3.413 +  and totient_7 [simp]: "totient 7 = 6"
   3.414 +  by (subst totient_prime; simp)+
   3.415 +    
   3.416 +lemma totient_4 [simp]: "totient 4 = 2"
   3.417 +  and totient_8 [simp]: "totient 8 = 4"
   3.418 +  and totient_9 [simp]: "totient 9 = 6"
   3.419 +  using totient_prime_power[of 2 2] totient_prime_power[of 2 3] totient_prime_power[of 3 2] 
   3.420 +  by simp_all
   3.421 +    
   3.422 +lemma totient_6 [simp]: "totient 6 = 2"
   3.423 +  using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)    
   3.424  
   3.425 -lemma totient_prime:
   3.426 -  assumes "2 \<le> p" "totient p = p - 1"
   3.427 -  shows "prime p"
   3.428 -proof -
   3.429 -  have "totatives p = {1..<p}"
   3.430 -    by (rule card_subset_eq) (simp_all add: assms)
   3.431 -  with assms show ?thesis
   3.432 -    by (auto intro: totatives_prime)
   3.433 +lemma totient_even:
   3.434 +  assumes "n > 2"
   3.435 +  shows   "even (totient n)"
   3.436 +proof (cases "\<exists>p. prime p \<and> p \<noteq> 2 \<and> p dvd n")
   3.437 +  case True
   3.438 +  then obtain p where p: "prime p" "p \<noteq> 2" "p dvd n" by auto
   3.439 +  from \<open>p \<noteq> 2\<close> have "p = 0 \<or> p = 1 \<or> p > 2" by auto
   3.440 +  with p(1) have "odd p" using prime_odd_nat[of p] by auto
   3.441 +  define k where "k = multiplicity p n"
   3.442 +  from p assms have k_pos: "k > 0" unfolding k_def by (subst multiplicity_gt_zero_iff) auto
   3.443 +  have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
   3.444 +  then obtain m where m: "n = p ^ k * m" by (elim dvdE)
   3.445 +  with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
   3.446 +  from k_def m_pos p have "\<not>p dvd m"
   3.447 +    by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib 
   3.448 +                          prime_elem_multiplicity_eq_zero_iff)
   3.449 +  hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
   3.450 +  thus ?thesis using p k_pos \<open>odd p\<close> 
   3.451 +    by (auto simp add: m totient_mult_coprime totient_prime_power)
   3.452 +next
   3.453 +  case False
   3.454 +  from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
   3.455 +    by (intro Primes.prime_factorization_nat) auto
   3.456 +  also from False have "\<dots> = (\<Prod>p\<in>prime_factors n. if p = 2 then 2 ^ multiplicity 2 n else 1)"
   3.457 +    by (intro prod.cong refl) auto
   3.458 +  also have "\<dots> = 2 ^ multiplicity 2 n" 
   3.459 +    by (subst prod.delta[OF finite_set_mset]) (auto simp: prime_factors_multiplicity)
   3.460 +  finally have n: "n = 2 ^ multiplicity 2 n" .
   3.461 +  have "multiplicity 2 n = 0 \<or> multiplicity 2 n = 1 \<or> multiplicity 2 n > 1" by force
   3.462 +  with n assms have "multiplicity 2 n > 1" by auto
   3.463 +  thus ?thesis by (subst n) (simp add: totient_prime_power)
   3.464 +qed
   3.465 +
   3.466 +lemma totient_prod_coprime:
   3.467 +  assumes "pairwise_coprime (f ` A)" "inj_on f A"
   3.468 +  shows   "totient (prod f A) = prod (\<lambda>x. totient (f x)) A"
   3.469 +  using assms
   3.470 +proof (induction A rule: infinite_finite_induct)
   3.471 +  case (insert x A)
   3.472 +  from insert.prems and insert.hyps have *: "coprime (prod f A) (f x)"
   3.473 +    by (intro prod_coprime[OF pairwise_coprimeD[OF insert.prems(1)]]) (auto simp: inj_on_def)
   3.474 +  from insert.hyps have "prod f (insert x A) = prod f A * f x" by simp
   3.475 +  also have "totient \<dots> = totient (prod f A) * totient (f x)"
   3.476 +    using insert.hyps insert.prems by (intro totient_mult_coprime *)
   3.477 +  also have "totient (prod f A) = (\<Prod>x\<in>A. totient (f x))" 
   3.478 +    using insert.prems by (intro insert.IH) (auto dest: pairwise_coprime_subset)
   3.479 +  also from insert.hyps have "\<dots> * totient (f x) = (\<Prod>x\<in>insert x A. totient (f x))" by simp
   3.480 +  finally show ?case .
   3.481 +qed simp_all
   3.482 +
   3.483 +(* TODO Move *)
   3.484 +lemma prime_power_eq_imp_eq:
   3.485 +  fixes p q :: "'a :: factorial_semiring"
   3.486 +  assumes "prime p" "prime q" "m > 0"
   3.487 +  assumes "p ^ m = q ^ n"
   3.488 +  shows   "p = q"
   3.489 +proof (rule ccontr)
   3.490 +  assume pq: "p \<noteq> q"
   3.491 +  from assms have "m = multiplicity p (p ^ m)" 
   3.492 +    by (subst multiplicity_prime_power) auto
   3.493 +  also note \<open>p ^ m = q ^ n\<close>
   3.494 +  also from assms pq have "multiplicity p (q ^ n) = 0"
   3.495 +    by (subst multiplicity_distinct_prime_power) auto
   3.496 +  finally show False using \<open>m > 0\<close> by simp
   3.497  qed
   3.498  
   3.499 +lemma totient_formula1:
   3.500 +  assumes "n > 0"
   3.501 +  shows   "totient n = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))"
   3.502 +proof -
   3.503 +  from assms have "n = (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n)"
   3.504 +    by (rule prime_factorization_nat)
   3.505 +  also have "totient \<dots> = (\<Prod>x\<in>prime_factors n. totient (x ^ multiplicity x n))"
   3.506 +  proof (rule totient_prod_coprime)
   3.507 +    show "pairwise_coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
   3.508 +    proof (standard, clarify, goal_cases)
   3.509 +      fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
   3.510 +                     "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
   3.511 +      thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
   3.512 +        by (intro coprime_exp2 primes_coprime[of p q]) auto
   3.513 +    qed
   3.514 +  next
   3.515 +    show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
   3.516 +    proof
   3.517 +      fix p q assume pq: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
   3.518 +                         "p ^ multiplicity p n = q ^ multiplicity q n"
   3.519 +      from assms and pq have "prime p" "prime q" "multiplicity p n > 0" 
   3.520 +        by (simp_all add: prime_factors_multiplicity)
   3.521 +      from prime_power_eq_imp_eq[OF this pq(3)] show "p = q" .
   3.522 +    qed
   3.523 +  qed
   3.524 +  also have "\<dots> = (\<Prod>p\<in>prime_factors n. p ^ (multiplicity p n - 1) * (p - 1))"
   3.525 +    by (intro prod.cong refl totient_prime_power) (auto simp: prime_factors_multiplicity)
   3.526 +  finally show ?thesis .
   3.527 +qed
   3.528 +
   3.529 +lemma totient_dvd:
   3.530 +  assumes "m dvd n"
   3.531 +  shows   "totient m dvd totient n"
   3.532 +proof (cases "m = 0 \<or> n = 0")
   3.533 +  case False
   3.534 +  let ?M = "\<lambda>p m :: nat. multiplicity p m - 1"
   3.535 +  have "(\<Prod>p\<in>prime_factors m. p ^ ?M p m * (p - 1)) dvd
   3.536 +          (\<Prod>p\<in>prime_factors n. p ^ ?M p n * (p - 1))" using assms False
   3.537 +    by (intro prod_dvd_prod_subset2 mult_dvd_mono dvd_refl le_imp_power_dvd diff_le_mono
   3.538 +              dvd_prime_factors dvd_imp_multiplicity_le) auto
   3.539 +  with False show ?thesis by (simp add: totient_formula1)
   3.540 +qed (insert assms, auto)
   3.541 +  
   3.542 +lemma totient_dvd_mono:
   3.543 +  assumes "m dvd n" "n > 0"
   3.544 +  shows   "totient m \<le> totient n"
   3.545 +  by (cases "m = 0") (insert assms, auto intro: dvd_imp_le totient_dvd)
   3.546 +
   3.547 +(* TODO Move *)
   3.548 +lemma prime_factors_power: "n > 0 \<Longrightarrow> prime_factors (x ^ n) = prime_factors x"
   3.549 +  by (cases "x = 0"; cases "n = 0")
   3.550 +     (auto simp: prime_factors_multiplicity prime_elem_multiplicity_power_distrib zero_power)
   3.551 +
   3.552 +lemma totient_formula2:
   3.553 +  "real (totient n) = real n * (\<Prod>p\<in>prime_factors n. 1 - 1 / real p)"
   3.554 +proof (cases "n = 0")
   3.555 +  case False
   3.556 +  have "real (totient n) = (\<Prod>p\<in>prime_factors n. real
   3.557 +          (p ^ (multiplicity p n - 1) * (p - 1)))" 
   3.558 +    using False by (subst totient_formula1) simp_all
   3.559 +  also have "\<dots> = (\<Prod>p\<in>prime_factors n. real (p ^ multiplicity p n) * (1 - 1 / real p))"
   3.560 +    by (intro prod.cong refl) (auto simp add: field_simps prime_factors_multiplicity 
   3.561 +          prime_ge_Suc_0_nat of_nat_diff power_Suc [symmetric] simp del: power_Suc)
   3.562 +  also have "\<dots> = real (\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) * 
   3.563 +                    (\<Prod>p\<in>prime_factors n. 1 - 1 / real p)" by (subst prod.distrib) auto
   3.564 +  also have "(\<Prod>p\<in>prime_factors n. p ^ multiplicity p n) = n"
   3.565 +    using False by (intro Primes.prime_factorization_nat [symmetric]) auto
   3.566 +  finally show ?thesis .
   3.567 +qed auto
   3.568 +
   3.569 +lemma totient_gcd: "totient (a * b) * totient (gcd a b) = totient a * totient b * gcd a b"
   3.570 +proof (cases "a = 0 \<or> b = 0")
   3.571 +  case False
   3.572 +  let ?P = "prime_factors :: nat \<Rightarrow> nat set"
   3.573 +  have "real (totient a * totient b * gcd a b) = real (a * b * gcd a b) *
   3.574 +          ((\<Prod>p\<in>?P a. 1 - 1 / real p) * (\<Prod>p\<in>?P b. 1 - 1 / real p))"
   3.575 +    by (simp add: totient_formula2)
   3.576 +  also have "?P a = (?P a - ?P b) \<union> (?P a \<inter> ?P b)" by auto
   3.577 +  also have "(\<Prod>p\<in>\<dots>. 1 - 1 / real p) = 
   3.578 +                 (\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)"
   3.579 +    by (rule prod.union_disjoint) blast+
   3.580 +  also have "\<dots> * (\<Prod>p\<in>?P b. 1 - 1 / real p) = (\<Prod>p\<in>?P a - ?P b. 1 - 1 / real p) * 
   3.581 +               (\<Prod>p\<in>?P b. 1 - 1 / real p) * (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)" (is "_ = ?A * _")
   3.582 +    by (simp only: mult_ac)
   3.583 +  also have "?A = (\<Prod>p\<in>?P a - ?P b \<union> ?P b. 1 - 1 / real p)"
   3.584 +    by (rule prod.union_disjoint [symmetric]) blast+
   3.585 +  also have "?P a - ?P b \<union> ?P b = ?P a \<union> ?P b" by blast
   3.586 +  also have "real (a * b * gcd a b) * ((\<Prod>p\<in>\<dots>. 1 - 1 / real p) * 
   3.587 +                 (\<Prod>p\<in>?P a \<inter> ?P b. 1 - 1 / real p)) = real (totient (a * b) * totient (gcd a b))"
   3.588 +    using False by (simp add: totient_formula2 prime_factors_product prime_factorization_gcd)
   3.589 +  finally show ?thesis by (simp only: of_nat_eq_iff)
   3.590 +qed auto
   3.591 +  
   3.592 +lemma totient_mult: "totient (a * b) = totient a * totient b * gcd a b div totient (gcd a b)"
   3.593 +  by (subst totient_gcd [symmetric]) simp
   3.594 +
   3.595 +lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
   3.596 +  using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
   3.597 +
   3.598 +(* TODO Move *)
   3.599 +lemma gcd_2_odd:
   3.600 +  assumes "odd (n::nat)"
   3.601 +  shows   "gcd n 2 = 1"
   3.602 +proof -
   3.603 +  from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
   3.604 +  have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
   3.605 +  thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
   3.606 +qed
   3.607 +
   3.608 +lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
   3.609 +  by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
   3.610 +
   3.611 +lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
   3.612 +proof (induction m arbitrary: n)
   3.613 +  case (Suc m n)
   3.614 +  have "totient (n ^ Suc (Suc m)) = totient (n * n ^ Suc m)" by simp
   3.615 +  also have "\<dots> = n ^ Suc m * totient n"
   3.616 +    using Suc.IH by (subst totient_mult) simp
   3.617 +  finally show ?case .
   3.618 +qed simp_all
   3.619 +  
   3.620 +lemma totient_power: "m > 0 \<Longrightarrow> totient (n ^ m) = n ^ (m - 1) * totient n"
   3.621 +  using totient_power_Suc[of n "m - 1"] by (cases m) simp_all
   3.622 +
   3.623 +lemma totient_gcd_lcm: "totient (gcd a b) * totient (lcm a b) = totient a * totient b"
   3.624 +proof (cases "a = 0 \<or> b = 0")
   3.625 +  case False
   3.626 +  let ?P = "prime_factors :: nat \<Rightarrow> nat set" and ?f = "\<lambda>p::nat. 1 - 1 / real p"
   3.627 +  have "real (totient (gcd a b) * totient (lcm a b)) = real (gcd a b * lcm a b) * 
   3.628 +          (prod ?f (?P a \<inter> ?P b) * prod ?f (?P a \<union> ?P b))"
   3.629 +    using False unfolding of_nat_mult 
   3.630 +    by (simp add: totient_formula2 prime_factorization_gcd prime_factorization_lcm)
   3.631 +  also have "gcd a b * lcm a b = a * b" by simp
   3.632 +  also have "?P a \<union> ?P b = (?P a - ?P a \<inter> ?P b) \<union> ?P b" by blast
   3.633 +  also have "prod ?f \<dots> = prod ?f (?P a - ?P a \<inter> ?P b) * prod ?f (?P b)"
   3.634 +    by (rule prod.union_disjoint) blast+
   3.635 +  also have "prod ?f (?P a \<inter> ?P b) * \<dots> = 
   3.636 +               prod ?f (?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b)) * prod ?f (?P b)"
   3.637 +    by (subst prod.union_disjoint) auto
   3.638 +  also have "?P a \<inter> ?P b \<union> (?P a - ?P a \<inter> ?P b) = ?P a" by blast
   3.639 +  also have "real (a * b) * (prod ?f (?P a) * prod ?f (?P b)) = real (totient a * totient b)"
   3.640 +    using False by (simp add: totient_formula2)
   3.641 +  finally show ?thesis by (simp only: of_nat_eq_iff)
   3.642 +qed auto    
   3.643 +
   3.644  end