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
```