src/HOL/Algebra/Multiplicative_Group.thy
 changeset 67051 e7e54a0b9197 parent 66500 ba94aeb02fbc child 67226 ec32cdaab97b
```     1.1 --- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:33:35 2017 +0000
1.2 +++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:41:08 2017 +0000
1.3 @@ -139,7 +139,7 @@
1.4
1.5  (* Deviates from the definition given in the library in number theory *)
1.6  definition phi' :: "nat => nat"
1.7 -  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
1.8 +  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
1.9
1.10  notation (latex output)
1.11    phi' ("\<phi> _")
1.12 @@ -148,8 +148,8 @@
1.13    assumes "m > 0"
1.14    shows "phi' m > 0"
1.15  proof -
1.16 -  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
1.17 -  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
1.18 +  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
1.19 +  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
1.20    thus ?thesis unfolding phi'_def by simp
1.21  qed
1.22
1.23 @@ -232,7 +232,7 @@
1.24            by (simp add: gcd_mult_distrib_nat q ac_simps)
1.25          hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
1.26          hence "a * n div d \<in> ?F"
1.27 -          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
1.28 +          using ge_1 le_n by (fastforce simp add: `d dvd n`)
1.29        } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
1.30        { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
1.31          hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
1.32 @@ -256,7 +256,7 @@
1.33      proof
1.34        fix m assume m: "m \<in> ?R"
1.35        thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
1.36 -        by (simp add: dvd_mult_div_cancel)
1.37 +        by simp
1.38      qed
1.39    qed fastforce
1.40    finally show ?thesis by force
1.41 @@ -329,7 +329,7 @@
1.42  lemma ord_min:
1.43    assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
1.44  proof -
1.45 -  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
1.46 +  define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
1.47    have fin: "finite Ord" by (auto simp: Ord_def)
1.48    have in_ord: "ord a \<in> Ord"
1.49      using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
1.50 @@ -411,7 +411,7 @@
1.51    show "?R \<subseteq> ?L" by blast
1.52    { fix y assume "y \<in> ?L"
1.53      then obtain x::nat where x:"y = a(^)x" by auto
1.54 -    def r \<equiv> "x mod ord a"
1.55 +    define r where "r = x mod ord a"
1.56      then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
1.57      hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
1.58        using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
1.59 @@ -427,7 +427,7 @@
1.60    assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
1.61    shows "ord a dvd k"
1.62  proof -
1.63 -  def r \<equiv> "k mod ord a"
1.64 +  define r where "r = k mod ord a"
1.65    then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
1.66    hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
1.67        using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
1.68 @@ -486,15 +486,16 @@
1.69      proof -
1.70        have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
1.71          using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
1.72 -      thus ?thesis by (simp add: gcd.commute)
1.73 +      thus ?thesis by (simp add: ac_simps)
1.74      qed
1.75      have dvd_d:"(ord a div gcd n (ord a)) dvd d"
1.76      proof -
1.77        have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
1.78          by (metis dvd_triv_right mult.commute)
1.79        hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
1.80 -        by (simp add:  mult.commute)
1.81 -      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
1.82 +        by (simp add: mult.commute)
1.83 +      then show ?thesis
1.84 +        using cp by (simp add: coprime_dvd_mult_left_iff)
1.85      qed
1.86      have "d > 0" using d_elem by simp
1.87      hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
1.88 @@ -744,7 +745,8 @@
1.89    shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
1.90  proof
1.91    assume A: ?L then show ?R
1.92 -    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
1.93 +    using assms ord_ge_1 [OF assms]
1.94 +    by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)
1.95  next
1.96    assume ?R then show ?L
1.97      using ord_pow_dvd_ord_elem[OF assms, of k] by auto
```