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