src/HOL/Number_Theory/Residues.thy
changeset 67051 e7e54a0b9197
parent 66954 0230af0f3c59
child 67091 1393c2340eec
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:33:35 2017 +0000
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:41:08 2017 +0000
     1.3 @@ -106,13 +106,9 @@
     1.4  
     1.5  lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
     1.6    using m_gt_one
     1.7 -  unfolding Units_def R_def residue_ring_def
     1.8 -  apply auto
     1.9 -    apply (subgoal_tac "x \<noteq> 0")
    1.10 -     apply auto
    1.11 -   apply (metis invertible_coprime_int)
    1.12 +  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
    1.13    apply (subst (asm) coprime_iff_invertible'_int)
    1.14 -   apply (auto simp add: cong_def mult.commute)
    1.15 +   apply (auto simp add: cong_def)
    1.16    done
    1.17  
    1.18  lemma res_neg_eq: "\<ominus> x = (- x) mod m"
    1.19 @@ -220,6 +216,22 @@
    1.20  context residues_prime
    1.21  begin
    1.22  
    1.23 +lemma p_coprime_left:
    1.24 +  "coprime p a \<longleftrightarrow> \<not> p dvd a"
    1.25 +  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
    1.26 +
    1.27 +lemma p_coprime_right:
    1.28 +  "coprime a p  \<longleftrightarrow> \<not> p dvd a"
    1.29 +  using p_coprime_left [of a] by (simp add: ac_simps)
    1.30 +
    1.31 +lemma p_coprime_left_int:
    1.32 +  "coprime (int p) a \<longleftrightarrow> \<not> int p dvd a"
    1.33 +  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
    1.34 +
    1.35 +lemma p_coprime_right_int:
    1.36 +  "coprime a (int p) \<longleftrightarrow> \<not> int p dvd a"
    1.37 +  using p_coprime_left_int [of a] by (simp add: ac_simps)
    1.38 +
    1.39  lemma is_field: "field R"
    1.40  proof -
    1.41    have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
    1.42 @@ -231,9 +243,7 @@
    1.43  
    1.44  lemma res_prime_units_eq: "Units R = {1..p - 1}"
    1.45    apply (subst res_units_eq)
    1.46 -  apply auto
    1.47 -  apply (subst gcd.commute)
    1.48 -  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
    1.49 +  apply (auto simp add: p_coprime_right_int zdvd_not_zless)
    1.50    done
    1.51  
    1.52  end
    1.53 @@ -246,26 +256,27 @@
    1.54  
    1.55  subsection \<open>Euler's theorem\<close>
    1.56  
    1.57 -lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
    1.58 +lemma (in residues) totatives_eq:
    1.59 +  "totatives (nat m) = nat ` Units R"
    1.60  proof -
    1.61 +  from m_gt_one have "\<bar>m\<bar> > 1"
    1.62 +    by simp
    1.63 +  then have "totatives (nat \<bar>m\<bar>) = nat ` abs ` Units R"
    1.64 +    by (auto simp add: totatives_def res_units_eq image_iff le_less)
    1.65 +      (use m_gt_one zless_nat_eq_int_zless in force)
    1.66 +  moreover have "\<bar>m\<bar> = m" "abs ` Units R = Units R"
    1.67 +    using m_gt_one by (auto simp add: res_units_eq image_iff)
    1.68 +  ultimately show ?thesis
    1.69 +    by simp
    1.70 +qed
    1.71 +
    1.72 +lemma (in residues) totient_eq:
    1.73 +  "totient (nat m) = card (Units R)"
    1.74 +proof  -
    1.75    have *: "inj_on nat (Units R)"
    1.76      by (rule inj_onI) (auto simp add: res_units_eq)
    1.77 -  define m' where "m' = nat m"
    1.78 -  from m_gt_one have "m = int m'" "m' > 1"
    1.79 -    by (simp_all add: m'_def)
    1.80 -  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
    1.81 -    unfolding res_units_eq
    1.82 -    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
    1.83 -  then have "Units R = int ` totatives m'"
    1.84 -    by blast
    1.85 -  then have "totatives m' = nat ` Units R"
    1.86 -    by (simp add: image_image)
    1.87 -  then have "card (totatives (nat m)) = card (nat ` Units R)"
    1.88 -    by (simp add: m'_def)
    1.89 -  also have "\<dots> = card (Units R)"
    1.90 -    using * card_image [of nat "Units R"] by auto
    1.91 -  finally show ?thesis
    1.92 -    by (simp add: totient_def)
    1.93 +  then show ?thesis
    1.94 +    by (simp add: totient_def totatives_eq card_image)
    1.95  qed
    1.96  
    1.97  lemma (in residues_prime) totient_eq: "totient p = p - 1"