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)