src/HOL/Number_Theory/Totient.thy
 changeset 67051 e7e54a0b9197 parent 66888 930abfdf8727 child 67118 ccab07d1196c
```     1.1 --- a/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -15,7 +15,7 @@
1.4
1.5  definition totatives :: "nat \<Rightarrow> nat set" where
1.6    "totatives n = {k \<in> {0<..n}. coprime k n}"
1.7 -
1.8 +
1.9  lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
1.10    by (simp add: totatives_def)
1.11
1.12 @@ -60,7 +60,7 @@
1.13  lemma minus_one_in_totatives:
1.14    assumes "n \<ge> 2"
1.15    shows "n - 1 \<in> totatives n"
1.16 -  using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
1.17 +  using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
1.18
1.19  lemma totatives_prime_power_Suc:
1.20    assumes "prime p"
1.21 @@ -72,7 +72,8 @@
1.22    fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
1.23    from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
1.24    hence "coprime k (p ^ Suc n)"
1.25 -    using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
1.26 +    using prime_imp_coprime [OF assms, of k]
1.27 +    by (cases "n > 0") (auto simp add: ac_simps)
1.28    with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
1.29  qed (auto simp: totatives_def)
1.30
1.31 @@ -101,14 +102,15 @@
1.32    proof safe
1.33      fix x assume "x \<in> totatives (m1 * m2)"
1.34      with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
1.35 -      by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
1.36 +      using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
1.37 +      by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
1.38    next
1.39      fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
1.40      with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
1.41      with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
1.42        where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
1.43      from x ab assms(3) have "x \<in> totatives (m1 * m2)"
1.44 -      by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
1.45 +      by (auto intro: ccontr simp add: in_totatives_iff)
1.46      with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
1.47    qed
1.48  qed
1.49 @@ -125,21 +127,18 @@
1.50    show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
1.51    proof (intro equalityI subsetI, goal_cases)
1.52      case (1 k)
1.53 -    thus ?case using assms
1.54 -      by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
1.55 -                                 gcd_mult_right gcd.commute)
1.56 +    then show ?case using assms
1.57 +      by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
1.58    next
1.59      case (2 k)
1.60      hence "d dvd k" by auto
1.61      then obtain l where k: "k = l * d" by (elim dvdE) auto
1.62 -    from 2 and assms show ?case unfolding k
1.63 -      by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d]
1.64 -                                    gcd_mult_right elim!: dvdE)
1.65 +    from 2 assms show ?case
1.66 +      using gcd_mult_right [of _ d l]
1.67 +      by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
1.68    qed
1.69  qed
1.70
1.71 -
1.72 -
1.73  definition totient :: "nat \<Rightarrow> nat" where
1.74    "totient n = card (totatives n)"
1.75
1.76 @@ -272,7 +271,8 @@
1.77    proof -
1.78      from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
1.79      from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
1.80 -    from that and nz have "\<not>coprime x p" by auto
1.81 +    from that and nz have "\<not>coprime x p"
1.82 +      by (auto elim: dvdE)
1.83      hence "x \<notin> totatives p" by (simp add: totatives_def)
1.84      also note *
1.85      finally show False using that and le by auto
1.86 @@ -299,7 +299,8 @@
1.87    by simp_all
1.88
1.89  lemma totient_6 [simp]: "totient 6 = 2"
1.90 -  using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)
1.91 +  using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
1.92 +  by simp
1.93
1.94  lemma totient_even:
1.95    assumes "n > 2"
1.96 @@ -314,11 +315,14 @@
1.97    have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
1.98    then obtain m where m: "n = p ^ k * m" by (elim dvdE)
1.99    with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
1.100 -  from k_def m_pos p have "\<not>p dvd m"
1.101 +  from k_def m_pos p have "\<not> p dvd m"
1.102      by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib
1.103                            prime_elem_multiplicity_eq_zero_iff)
1.104 -  hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
1.105 -  thus ?thesis using p k_pos \<open>odd p\<close>
1.106 +  with \<open>prime p\<close> have "coprime p m"
1.107 +    by (rule prime_imp_coprime)
1.108 +  with \<open>k > 0\<close> have "coprime (p ^ k) m"
1.109 +    by simp
1.110 +  then show ?thesis using p k_pos \<open>odd p\<close>
1.111      by (auto simp add: m totient_mult_coprime totient_prime_power)
1.112  next
1.113    case False
1.114 @@ -341,7 +345,7 @@
1.115  proof (induction A rule: infinite_finite_induct)
1.116    case (insert x A)
1.117    have *: "coprime (prod f A) (f x)"
1.118 -  proof (rule prod_coprime)
1.119 +  proof (rule prod_coprime_left)
1.120      fix y
1.121      assume "y \<in> A"
1.122      with \<open>x \<notin> A\<close> have "y \<noteq> x"
1.123 @@ -388,10 +392,12 @@
1.124    proof (rule totient_prod_coprime)
1.125      show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
1.126      proof (rule pairwiseI, clarify)
1.127 -      fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n"
1.128 +      fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n"
1.129                       "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
1.130 -      thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
1.131 -        by (intro coprime_exp2 primes_coprime[of p q]) auto
1.132 +      then have "multiplicity p n > 0" "multiplicity q n > 0"
1.133 +        by (simp_all add: prime_factors_multiplicity)
1.134 +      with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
1.135 +        by auto
1.136      qed
1.137    next
1.138      show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
1.139 @@ -475,20 +481,22 @@
1.140    by (subst totient_gcd [symmetric]) simp
1.141
1.142  lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
1.143 -  using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
1.144 +  by (fact of_nat_eq_1_iff)
1.145
1.146  (* TODO Move *)
1.147 -lemma gcd_2_odd:
1.148 +lemma odd_imp_coprime_nat:
1.149    assumes "odd (n::nat)"
1.150 -  shows   "gcd n 2 = 1"
1.151 +  shows   "coprime n 2"
1.152  proof -
1.153    from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
1.154 -  have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
1.155 -  thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
1.156 +  have "coprime (Suc (2 * k)) (2 * k)"
1.157 +    by (fact coprime_Suc_left_nat)
1.158 +  then show ?thesis using n
1.159 +    by simp
1.160  qed
1.161
1.162  lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
1.163 -  by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
1.164 +  by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
1.165
1.166  lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
1.167  proof (induction m arbitrary: n)
```