src/HOL/Number_Theory/Residues.thy
changeset 65726 f5d64d094efe
parent 65465 067210a08a22
child 65899 ab7d8c999531
     1.1 --- a/src/HOL/Number_Theory/Residues.thy	Thu May 04 15:15:07 2017 +0100
     1.2 +++ b/src/HOL/Number_Theory/Residues.thy	Thu May 04 16:49:29 2017 +0200
     1.3 @@ -31,7 +31,7 @@
     1.4  where
     1.5    "residue_ring m =
     1.6      \<lparr>carrier = {0..m - 1},
     1.7 -     mult = \<lambda>x y. (x * y) mod m,
     1.8 +     monoid.mult = \<lambda>x y. (x * y) mod m,
     1.9       one = 1,
    1.10       zero = 0,
    1.11       add = \<lambda>x y. (x + y) mod m\<rparr>"
    1.12 @@ -247,18 +247,22 @@
    1.13  
    1.14  lemma (in residues) totient_eq:
    1.15    "totient (nat m) = card (Units R)"
    1.16 +  thm R_def
    1.17  proof -
    1.18    have *: "inj_on nat (Units R)"
    1.19      by (rule inj_onI) (auto simp add: res_units_eq)
    1.20 -  have "totatives (nat m) = nat ` Units R"
    1.21 -    by (auto simp add: res_units_eq totatives_def transfer_nat_int_gcd(1))
    1.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))
    1.23 +  define m' where "m' = nat m"
    1.24 +  from m_gt_one have m: "m = int m'" "m' > 1" by (simp_all add: m'_def)
    1.25 +  from m have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
    1.26 +    unfolding res_units_eq
    1.27 +    by (cases x; cases "x = m") (auto simp: totatives_def transfer_int_nat_gcd)
    1.28 +  hence "Units R = int ` totatives m'" by blast
    1.29 +  hence "totatives m' = nat ` Units R" by (simp add: image_image)
    1.30    then have "card (totatives (nat m)) = card (nat ` Units R)"
    1.31 -    by simp
    1.32 +    by (simp add: m'_def)
    1.33    also have "\<dots> = card (Units R)"
    1.34      using * card_image [of nat "Units R"] by auto
    1.35 -  finally show ?thesis
    1.36 -    by simp
    1.37 +  finally show ?thesis by (simp add: totient_def)
    1.38  qed
    1.39  
    1.40  lemma (in residues_prime) totient_eq: "totient p = p - 1"
    1.41 @@ -298,7 +302,7 @@
    1.42    then have "[a ^ totient p = 1] (mod p)"
    1.43       by (rule euler_theorem)
    1.44    also have "totient p = p - 1"
    1.45 -    by (rule prime_totient) (rule assms)
    1.46 +    by (rule totient_prime) (rule assms)
    1.47    finally show ?thesis .
    1.48  qed
    1.49