# HG changeset patch
# User haftmann
# Date 1510425668 0
# Node ID e7e54a0b9197aa002dcdcafef8588a76d7613767
# Parent  1e29e2666a158f136671e442647f6c8de52a9041
dedicated definition for coprimality

diff -r 1e29e2666a15 -r e7e54a0b9197 NEWS
--- a/NEWS	Sat Nov 11 18:33:35 2017 +0000
+++ b/NEWS	Sat Nov 11 18:41:08 2017 +0000
@@ -89,7 +89,10 @@
 * Class linordered_semiring_1 covers zero_less_one also, ruling out
 pathologic instances. Minor INCOMPATIBILITY.
 
-* Removed nat-int transfer machinery.  Rare INCOMPATIBILITY.
+* Removed nat-int transfer machinery. Rare INCOMPATIBILITY.
+
+* Predicate coprime is now a real definition, not a mere
+abbreviation. INCOMPATIBILITY.
 
 
 *** System ***
diff -r 1e29e2666a15 -r e7e54a0b9197 src/Doc/Corec/Corec.thy
--- a/src/Doc/Corec/Corec.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/Doc/Corec/Corec.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -334,9 +334,9 @@
           primes m (n + 1))"
       apply (relation "measure (\<lambda>(m, n).
         if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
-       apply (auto simp: mod_Suc intro: Suc_lessI)
-       apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
-      by (metis diff_less_mono2 lessI mod_less_divisor)
+       apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+      apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+      done
 
 text \<open>
 \noindent
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Algebra/Multiplicative_Group.thy
--- a/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Algebra/Multiplicative_Group.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -139,7 +139,7 @@
 
 (* Deviates from the definition given in the library in number theory *)
 definition phi' :: "nat => nat"
-  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}"
+  where "phi' m = card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}"
 
 notation (latex output)
   phi' ("\<phi> _")
@@ -148,8 +148,8 @@
   assumes "m > 0"
   shows "phi' m > 0"
 proof -
-  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1}" using assms by simp
-  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> gcd x m = 1} > 0" by (auto simp: card_gt_0_iff)
+  have "1 \<in> {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m}" using assms by simp
+  hence "card {x. 1 \<le> x \<and> x \<le> m \<and> coprime x m} > 0" by (auto simp: card_gt_0_iff)
   thus ?thesis unfolding phi'_def by simp
 qed
 
@@ -232,7 +232,7 @@
           by (simp add: gcd_mult_distrib_nat q ac_simps)
         hence "n div gcd (a * n div d) n = d*n div (d*(n div d))" using a by simp
         hence "a * n div d \<in> ?F"
-          using ge_1 le_n by (fastforce simp add: `d dvd n` dvd_mult_div_cancel)
+          using ge_1 le_n by (fastforce simp add: `d dvd n`)
       } thus "(\<lambda>a. a*n div d) ` ?RF \<subseteq> ?F" by blast
       { fix m l assume A: "m \<in> ?F" "l \<in> ?F" "m div gcd m n = l div gcd l n"
         hence "gcd m n = gcd l n" using dvd_div_eq_2[OF assms] by fastforce
@@ -256,7 +256,7 @@
     proof
       fix m assume m: "m \<in> ?R"
       thus "m \<in> ?L" using dvd_triv_right[of "n div gcd m n" "gcd m n"]
-        by (simp add: dvd_mult_div_cancel)
+        by simp
     qed
   qed fastforce
   finally show ?thesis by force
@@ -329,7 +329,7 @@
 lemma ord_min:
   assumes  "finite (carrier G)" "1 \<le> d" "a \<in> carrier G" "a (^) d = \<one>" shows "ord a \<le> d"
 proof -
-  def Ord \<equiv> "{d \<in> {1..order G}. a (^) d = \<one>}"
+  define Ord where "Ord = {d \<in> {1..order G}. a (^) d = \<one>}"
   have fin: "finite Ord" by (auto simp: Ord_def)
   have in_ord: "ord a \<in> Ord"
     using assms pow_ord_eq_1 ord_ge_1 ord_le_group_order by (auto simp: Ord_def)
@@ -411,7 +411,7 @@
   show "?R \<subseteq> ?L" by blast
   { fix y assume "y \<in> ?L"
     then obtain x::nat where x:"y = a(^)x" by auto
-    def r \<equiv> "x mod ord a"
+    define r where "r = x mod ord a"
     then obtain q where q:"x = q * ord a + r" using mod_eqD by atomize_elim presburger
     hence "y = (a(^)ord a)(^)q \<otimes> a(^)r"
       using x assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -427,7 +427,7 @@
   assumes "finite (carrier G)" "a \<in> carrier G" "a (^) k = \<one>"
   shows "ord a dvd k"
 proof -
-  def r \<equiv> "k mod ord a"
+  define r where "r = k mod ord a"
   then obtain q where q:"k = q*ord a + r" using mod_eqD by atomize_elim presburger
   hence "a(^)k = (a(^)ord a)(^)q \<otimes> a(^)r"
       using assms by (simp add: mult.commute nat_pow_mult nat_pow_pow)
@@ -486,15 +486,16 @@
     proof -
       have "coprime (n div gcd n (ord a)) (ord a div gcd n (ord a))"
         using div_gcd_coprime[of n "ord a"] ge_1 by fastforce
-      thus ?thesis by (simp add: gcd.commute)
+      thus ?thesis by (simp add: ac_simps)
     qed
     have dvd_d:"(ord a div gcd n (ord a)) dvd d"
     proof -
       have "ord a div gcd n (ord a) dvd (n div gcd n (ord a)) * d" using prod_eq
         by (metis dvd_triv_right mult.commute)
       hence "ord a div gcd n (ord a) dvd d * (n div gcd n (ord a))"
-        by (simp add:  mult.commute)
-      thus ?thesis using coprime_dvd_mult[OF cp, of d] by fastforce
+        by (simp add: mult.commute)
+      then show ?thesis
+        using cp by (simp add: coprime_dvd_mult_left_iff)
     qed
     have "d > 0" using d_elem by simp
     hence "ord a div gcd n (ord a) \<le> d" using dvd_d by (simp add : Nat.dvd_imp_le)
@@ -744,7 +745,8 @@
   shows pow_ord_eq_ord_iff: "group.ord G (a (^) k) = ord a \<longleftrightarrow> coprime k (ord a)" (is "?L \<longleftrightarrow> ?R")
 proof
   assume A: ?L then show ?R
-    using assms ord_ge_1[OF assms] by (auto simp: nat_div_eq ord_pow_dvd_ord_elem)
+    using assms ord_ge_1 [OF assms]
+    by (auto simp: nat_div_eq ord_pow_dvd_ord_elem coprime_iff_gcd_eq_1)
 next
   assume ?R then show ?L
     using ord_pow_dvd_ord_elem[OF assms, of k] by auto
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Factorial_Ring.thy
--- a/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Factorial_Ring.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -13,12 +13,6 @@
 
 subsection \<open>Irreducible and prime elements\<close>
 
-(* TODO: Move ? *)
-lemma (in semiring_gcd) prod_coprime' [rule_format]: 
-    "(\<forall>i\<in>A. gcd a (f i) = 1) \<longrightarrow> gcd a (\<Prod>i\<in>A. f i) = 1"
-  using prod_coprime[of A f a] by (simp add: gcd.commute)
-
-
 context comm_semiring_1
 begin
 
@@ -583,7 +577,7 @@
 end
 
 
-subsection \<open>In a semiring with GCD, each irreducible element is a prime elements\<close>
+subsection \<open>In a semiring with GCD, each irreducible element is a prime element\<close>
 
 context semiring_gcd
 begin
@@ -620,23 +614,26 @@
   using assms by (simp add: prime_elem_imp_coprime)
 
 lemma prime_elem_imp_power_coprime:
-  "prime_elem p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
-  by (auto intro!: coprime_exp dest: prime_elem_imp_coprime simp: gcd.commute)
+  "prime_elem p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (cases "m > 0") (auto dest: prime_elem_imp_coprime simp add: ac_simps)
 
 lemma prime_imp_power_coprime:
-  "prime p \<Longrightarrow> \<not>p dvd a \<Longrightarrow> coprime a (p ^ m)"
-  by (simp add: prime_elem_imp_power_coprime)
+  "prime p \<Longrightarrow> \<not> p dvd a \<Longrightarrow> coprime a (p ^ m)"
+  by (rule prime_elem_imp_power_coprime) simp_all
 
 lemma prime_elem_divprod_pow:
   assumes p: "prime_elem p" and ab: "coprime a b" and pab: "p^n dvd a * b"
   shows   "p^n dvd a \<or> p^n dvd b"
   using assms
 proof -
-  from ab p have "\<not>p dvd a \<or> \<not>p dvd b"
-    by (auto simp: coprime prime_elem_def)
-  with p have "coprime (p^n) a \<or> coprime (p^n) b"
-    by (auto intro: prime_elem_imp_coprime coprime_exp_left)
-  with pab show ?thesis by (auto intro: coprime_dvd_mult simp: mult_ac)
+  from p have "\<not> is_unit p"
+    by simp
+  with ab p have "\<not> p dvd a \<or> \<not> p dvd b"
+    using not_coprimeI by blast
+  with p have "coprime (p ^ n) a \<or> coprime (p ^ n) b"
+    by (auto dest: prime_elem_imp_power_coprime simp add: ac_simps)
+  with pab show ?thesis
+    by (auto simp add: coprime_dvd_mult_left_iff coprime_dvd_mult_right_iff)
 qed
 
 lemma primes_coprime:
@@ -1524,6 +1521,27 @@
     with assms[of P] assms[of Q] PQ show "P = Q" by simp
 qed
 
+lemma divides_primepow:
+  assumes "prime p" and "a dvd p ^ n"
+  obtains m where "m \<le> n" and "normalize a = p ^ m"
+proof -
+  from assms have "a \<noteq> 0"
+    by auto
+  with assms
+  have "prod_mset (prime_factorization a) dvd prod_mset (prime_factorization (p ^ n))"
+    by (simp add: prod_mset_prime_factorization)
+  then have "prime_factorization a \<subseteq># prime_factorization (p ^ n)"
+    by (simp add: in_prime_factors_imp_prime prod_mset_dvd_prod_mset_primes_iff)
+  with assms have "prime_factorization a \<subseteq># replicate_mset n p"
+    by (simp add: prime_factorization_prime_power)
+  then obtain m where "m \<le> n" and "prime_factorization a = replicate_mset m p"
+    by (rule msubseteq_replicate_msetE)
+  then have "prod_mset (prime_factorization a) = prod_mset (replicate_mset m p)"
+    by simp
+  with \<open>a \<noteq> 0\<close> have "normalize a = p ^ m"
+    by (simp add: prod_mset_prime_factorization)
+  with \<open>m \<le> n\<close> show thesis ..
+qed
 
 
 subsection \<open>GCD and LCM computation with unique factorizations\<close>
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Normalized_Fraction.thy
--- a/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Normalized_Fraction.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -16,6 +16,15 @@
   "normalize_quot = 
      (\<lambda>(a,b). if b = 0 then (0,1) else let d = gcd a b * unit_factor b in (a div d, b div d))" 
 
+lemma normalize_quot_zero [simp]:
+  "normalize_quot (a, 0) = (0, 1)"
+  by (simp add: normalize_quot_def)
+
+lemma normalize_quot_proj [simp]:
+  "fst (normalize_quot (a, b)) = a div (gcd a b * unit_factor b)"
+  "snd (normalize_quot (a, b)) = normalize b div gcd a b" if "b \<noteq> 0"
+  using that by (simp_all add: normalize_quot_def Let_def mult.commute [of _ "unit_factor b"] dvd_div_mult2_eq mult_unit_dvd_iff')
+
 definition normalized_fracts :: "('a :: {ring_gcd,idom_divide} \<times> 'a) set" where
   "normalized_fracts = {(a,b). coprime a b \<and> unit_factor b = 1}"
   
@@ -61,8 +70,8 @@
   
 lemma coprime_normalize_quot:
   "coprime (fst (normalize_quot x)) (snd (normalize_quot x))"
-  by (simp add: normalize_quot_def case_prod_unfold Let_def
-        div_mult_unit2 gcd_div_unit1 gcd_div_unit2 div_gcd_coprime)
+  by (simp add: normalize_quot_def case_prod_unfold div_mult_unit2)
+    (metis coprime_mult_self_right_iff div_gcd_coprime unit_div_mult_self unit_factor_is_unit)
 
 lemma normalize_quot_in_normalized_fracts [simp]: "normalize_quot x \<in> normalized_fracts"
   by (simp add: normalized_fracts_def coprime_normalize_quot case_prod_unfold)
@@ -203,15 +212,26 @@
      and  "g \<equiv> fst (normalize_quot (c, b))" and "h \<equiv> snd (normalize_quot (c, b))"
   shows   "normalize_quot (a * c, b * d) = (e * g, f * h)"
 proof (rule normalize_quotI)
+  from assms have "gcd a b = 1" "gcd c d = 1"
+    by simp_all
   from assms have "b \<noteq> 0" "d \<noteq> 0" by auto
-  from normalize_quotE[OF \<open>b \<noteq> 0\<close>, of c] guess k . note k = this [folded assms]
-  from normalize_quotE[OF \<open>d \<noteq> 0\<close>, of a] guess l . note l = this [folded assms]
-  from k l show "a * c * (f * h) = b * d * (e * g)" by (simp_all)
+  with assms have "normalize b = b" "normalize d = d"
+    by (auto intro: normalize_unit_factor_eqI)
+  from normalize_quotE [OF \<open>b \<noteq> 0\<close>, of c] guess k .
+  note k = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+  from normalize_quotE [OF \<open>d \<noteq> 0\<close>, of a] guess l .
+  note l = this [folded \<open>gcd a b = 1\<close> \<open>gcd c d = 1\<close> assms(3) assms(4)]
+  from k l show "a * c * (f * h) = b * d * (e * g)"
+    by (metis e_def f_def g_def h_def mult.commute mult.left_commute)
   from assms have [simp]: "unit_factor f = 1" "unit_factor h = 1"
     by simp_all
   from assms have "coprime e f" "coprime g h" by (simp_all add: coprime_normalize_quot)
-  with k l assms(1,2) show "(e * g, f * h) \<in> normalized_fracts"
-    by (simp add: normalized_fracts_def unit_factor_mult coprime_mul_eq coprime_mul_eq')
+  with k l assms(1,2) \<open>b \<noteq> 0\<close> \<open>d \<noteq> 0\<close> \<open>unit_factor b = 1\<close> \<open>unit_factor d = 1\<close>
+    \<open>normalize b = b\<close> \<open>normalize d = d\<close>
+  show "(e * g, f * h) \<in> normalized_fracts"
+    by (simp add: normalized_fracts_def unit_factor_mult e_def f_def g_def h_def
+      coprime_normalize_quot dvd_unit_factor_div unit_factor_gcd)
+      (metis coprime_mult_left_iff coprime_mult_right_iff)
 qed (insert assms(3,4), auto)
 
 lemma normalize_quot_mult:
@@ -230,8 +250,8 @@
      (let (a,b) = quot_of_fract x; (c,d) = quot_of_fract y;
           (e,f) = normalize_quot (a,d); (g,h) = normalize_quot (c,b)
       in  (e*g, f*h))"
-  by transfer (simp_all add: Let_def case_prod_unfold normalize_quot_mult_coprime [symmetric]
-                 coprime_normalize_quot normalize_quot_mult [symmetric])
+  by transfer
+     (simp add: split_def Let_def coprime_normalize_quot normalize_quot_mult normalize_quot_mult_coprime)
   
 lemma normalize_quot_0 [simp]: 
     "normalize_quot (0, x) = (0, 1)" "normalize_quot (x, 0) = (0, 1)"
@@ -254,7 +274,9 @@
     by (simp add: div_unit_factor [symmetric] unit_div_mult_swap mult_ac del: div_unit_factor)
   have "coprime a' b'" by (simp add: a'_def b'_def coprime_normalize_quot)
   thus "(b' div unit_factor a', a' div unit_factor a') \<in> normalized_fracts"
-    using assms(1,2) d by (auto simp: normalized_fracts_def gcd_div_unit1 gcd_div_unit2 gcd.commute)
+    using assms(1,2) d
+    by (auto simp: normalized_fracts_def ac_simps)
+      (metis gcd.normalize_left_idem gcd_div_unit2 is_unit_gcd unit_factor_is_unit)
 qed fact+
   
 lemma quot_of_fract_inverse:
@@ -274,12 +296,19 @@
   shows "normalize_quot (x div u, y) = (x' div u, y')"
 proof (cases "y = 0")
   case False
-  from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
-  from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
-  with False d \<open>is_unit u\<close> show ?thesis
-    by (intro normalize_quotI)
-       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
-          gcd_div_unit1)
+  define v where "v = 1 div u"
+  with \<open>is_unit u\<close> have "is_unit v" and u: "\<And>a. a div u = a * v"
+    by simp_all
+  from \<open>is_unit v\<close> have "coprime v = top"
+    by (simp add: fun_eq_iff is_unit_left_imp_coprime)
+  from normalize_quotE[OF False, of x] guess d .
+  note d = this[folded assms(2,3)]
+  from assms have "coprime x' y'" "unit_factor y' = 1"
+    by (simp_all add: coprime_normalize_quot)
+  with d \<open>coprime v = top\<close> have "normalize_quot (x * v, y) = (x' * v, y')"
+    by (auto simp: normalized_fracts_def intro: normalize_quotI)
+  then show ?thesis
+    by (simp add: u)
 qed (simp_all add: assms)
 
 lemma normalize_quot_div_unit_right:
@@ -291,10 +320,8 @@
   case False
   from normalize_quotE[OF this, of x] guess d . note d = this[folded assms(2,3)]
   from assms have "coprime x' y'" "unit_factor y' = 1" by (simp_all add: coprime_normalize_quot)
-  with False d \<open>is_unit u\<close> show ?thesis
-    by (intro normalize_quotI)
-       (auto simp: normalized_fracts_def unit_div_mult_swap unit_div_commute unit_div_cancel
-          gcd_mult_unit1 unit_div_eq_0_iff mult.assoc [symmetric])
+  with d \<open>is_unit u\<close> show ?thesis
+    by (auto simp add: normalized_fracts_def is_unit_left_imp_coprime unit_div_eq_0_iff intro: normalize_quotI)
 qed (simp_all add: assms)
 
 lemma normalize_quot_normalize_left:
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Nth_Powers.thy
--- a/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Nth_Powers.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -111,9 +111,10 @@
     ultimately show "n dvd multiplicity p a"
       by (auto simp: not_dvd_imp_multiplicity_0)
   qed
-  from A[of a b] assms show "is_nth_power n a" by (cases "n = 0") simp_all
-  from A[of b a] assms show "is_nth_power n b" 
-    by (cases "n = 0") (simp_all add: gcd.commute mult.commute)
+  from A [of a b] assms show "is_nth_power n a"
+    by (cases "n = 0") simp_all
+  from A [of b a] assms show "is_nth_power n b"
+    by (cases "n = 0") (simp_all add: ac_simps)
 qed
     
 lemma is_nth_power_mult_coprime_nat_iff:
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Polynomial_Factorial.thy
--- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -171,7 +171,7 @@
   hence "fract_poly (smult a q) = fract_poly (smult b p)" by (simp del: fract_poly_eq_iff)
   hence "smult b p = smult a q" by (simp only: fract_poly_eq_iff)
   moreover have "c = to_fract a / to_fract b" "coprime b a" "normalize b = b"
-    by (simp_all add: a_def b_def coprime_quot_of_fract gcd.commute
+    by (simp_all add: a_def b_def coprime_quot_of_fract [of c] ac_simps
           normalize_snd_quot_of_fract Fract_conv_to_fract [symmetric])
   ultimately show ?thesis by (intro that[of a b])
 qed
@@ -513,9 +513,12 @@
    from fract_poly_smult_eqE[OF this] guess a b . note ab = this
    hence "content (smult a p) = content (smult b (q' * r'))" by (simp only:)
    with ab(4) have a: "a = normalize b" by (simp add: content_mult q r)
-   hence "normalize b = gcd a b" by simp
-   also from ab(3) have "\<dots> = 1" .
-   finally have "a = 1" "is_unit b" by (simp_all add: a normalize_1_iff)
+   then have "normalize b = gcd a b"
+     by simp
+   with \<open>coprime a b\<close> have "normalize b = 1"
+     by simp
+   then have "a = 1" "is_unit b"
+     by (simp_all add: a normalize_1_iff)
    
    note eq
    also from ab(1) \<open>a = 1\<close> have "cr * cg = to_fract b" by simp
@@ -676,7 +679,8 @@
     from fract_poly_smult_eqE[OF eq] guess a b . note ab = this
     from ab(2) have "content (smult a p) = content (smult b e)" by (simp only: )
     with assms content_e have "a = normalize b" by (simp add: ab(4))
-    with ab have ab': "a = 1" "is_unit b" by (simp_all add: normalize_1_iff)
+    with ab have ab': "a = 1" "is_unit b"
+      by (simp_all add: normalize_1_iff)
     with ab ab' have "c' = to_fract b" by auto
     from this and \<open>is_unit b\<close> show ?thesis by (rule that)
   qed
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Primes.thy
--- a/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Primes.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -245,9 +245,9 @@
   using prime_power_cancel [OF assms] assms by auto
 
 lemma prime_power_canonical:
-  fixes m::nat
+  fixes m :: nat
   assumes "prime p" "m > 0"
-  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p^k"
+  shows "\<exists>k n. \<not> p dvd n \<and> m = n * p ^ k"
 using \<open>m > 0\<close>
 proof (induction m rule: less_induct)
   case (less m)
@@ -381,9 +381,9 @@
 
 (* TODO: Generalise? *)
 lemma prime_power_mult_nat:
-  fixes p::nat
+  fixes p :: nat
   assumes p: "prime p" and xy: "x * y = p ^ k"
-  shows "\<exists>i j. x = p ^i \<and> y = p^ j"
+  shows "\<exists>i j. x = p ^ i \<and> y = p^ j"
 using xy
 proof(induct k arbitrary: x y)
   case 0 thus ?case apply simp by (rule exI[where x="0"], simp)
@@ -429,25 +429,10 @@
 qed
 
 lemma divides_primepow_nat:
-  fixes p::nat
+  fixes p :: nat
   assumes p: "prime p"
-  shows "d dvd p^k \<longleftrightarrow> (\<exists> i. i \<le> k \<and> d = p ^i)"
-proof
-  assume H: "d dvd p^k" then obtain e where e: "d*e = p^k"
-    unfolding dvd_def  apply (auto simp add: mult.commute) by blast
-  from prime_power_mult_nat[OF p e] obtain i j where ij: "d = p^i" "e=p^j" by blast
-  from e ij have "p^(i + j) = p^k" by (simp add: power_add)
-  hence "i + j = k" using p prime_gt_1_nat power_inject_exp[of p "i+j" k] by simp
-  hence "i \<le> k" by arith
-  with ij(1) show "\<exists>i\<le>k. d = p ^ i" by blast
-next
-  {fix i assume H: "i \<le> k" "d = p^i"
-    then obtain j where j: "k = i + j"
-      by (metis le_add_diff_inverse)
-    hence "p^k = p^j*d" using H(2) by (simp add: power_add)
-    hence "d dvd p^k" unfolding dvd_def by auto}
-  thus "\<exists>i\<le>k. d = p ^ i \<Longrightarrow> d dvd p ^ k" by blast
-qed
+  shows "d dvd p ^ k \<longleftrightarrow> (\<exists>i\<le>k. d = p ^ i)"
+  using assms divides_primepow [of p d k] by (auto intro: le_imp_power_dvd)
 
 
 subsection \<open>Chinese Remainder Theorem Variants\<close>
@@ -481,8 +466,8 @@
   from bezout_add_strong_nat[OF a, of b] bezout_add_strong_nat[OF b, of a]
   obtain d1 x1 y1 d2 x2 y2 where dxy1: "d1 dvd a" "d1 dvd b" "a * x1 = b * y1 + d1"
     and dxy2: "d2 dvd b" "d2 dvd a" "b * x2 = a * y2 + d2" by blast
-  then have d12: "d1 = 1" "d2 =1"
-    by (metis ab coprime_nat)+
+  then have d12: "d1 = 1" "d2 = 1"
+    using ab coprime_common_divisor_nat [of a b] by blast+
   let ?x = "v * a * x1 + u * b * x2"
   let ?q1 = "v * x1 + u * y2"
   let ?q2 = "v * y1 + u * x2"
@@ -497,14 +482,14 @@
 lemma coprime_bezout_strong:
   fixes a::nat assumes "coprime a b"  "b \<noteq> 1"
   shows "\<exists>x y. a * x = b * y + 1"
-by (metis assms bezout_nat gcd_nat.left_neutral)
+  by (metis add.commute add.right_neutral assms(1) assms(2) chinese_remainder coprime_1_left coprime_1_right coprime_crossproduct_nat mult.commute mult.right_neutral mult_cancel_left)
 
 lemma bezout_prime:
   assumes p: "prime p" and pa: "\<not> p dvd a"
   shows "\<exists>x y. a*x = Suc (p*y)"
 proof -
   have ap: "coprime a p"
-    by (metis gcd.commute p pa prime_imp_coprime)
+    using coprime_commute p pa prime_imp_coprime by auto
   moreover from p have "p \<noteq> 1" by auto
   ultimately have "\<exists>x y. a * x = p * y + 1"
     by (rule coprime_bezout_strong)
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Computational_Algebra/Squarefree.thy
--- a/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Computational_Algebra/Squarefree.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -116,13 +116,16 @@
   show ?thesis unfolding squarefree_factorial_semiring'[OF nz]
   proof
     fix p assume p: "p \<in> prime_factors (a * b)"
-    {
+    with nz have "prime p"
+      by (simp add: prime_factors_dvd)
+    have "\<not> (p dvd a \<and> p dvd b)"
+    proof
       assume "p dvd a \<and> p dvd b"
-      hence "p dvd gcd a b" by simp
-      also have "gcd a b = 1" by fact
-      finally have False using nz using p by (auto simp: prime_factors_dvd)
-    }
-    hence "\<not>(p dvd a \<and> p dvd b)" by blast
+      with \<open>coprime a b\<close> have "is_unit p"
+        by (auto intro: coprime_common_divisor)
+      with \<open>prime p\<close> show False
+        by simp
+    qed
     moreover from p have "p dvd a \<or> p dvd b" using nz 
       by (auto simp: prime_factors_dvd prime_dvd_mult_iff)
     ultimately show "multiplicity p (a * b) = 1" using nz p assms(2,3)
@@ -138,7 +141,7 @@
   shows   "squarefree (prod f A)"
   using assms 
   by (induction A rule: infinite_finite_induct) 
-     (auto intro!: squarefree_mult_coprime prod_coprime')
+     (auto intro!: squarefree_mult_coprime prod_coprime_right)
 
 lemma squarefree_powerD: "m > 0 \<Longrightarrow> squarefree (n ^ m) \<Longrightarrow> squarefree n"
   by (cases m) (auto dest: squarefree_multD)
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Corec_Examples/Paper_Examples.thy
--- a/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Corec_Examples/Paper_Examples.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -96,9 +96,9 @@
 where "primes m n =
   (if (m = 0 \<and> n > 1) \<or> coprime m n then n \<lhd> primes (m * n) (n + 1) else primes m (n + 1))"
 apply (relation "measure (\<lambda>(m, n). if n = 0 then 1 else if coprime m n then 0 else m - n mod m)")
-apply (auto simp: mod_Suc intro: Suc_lessI )
-apply (metis One_nat_def coprime_Suc_nat gcd.commute gcd_red_nat)
-by (metis diff_less_mono2 lessI mod_less_divisor)
+   apply (auto simp: mod_Suc diff_less_mono2 intro: Suc_lessI elim!: not_coprimeE)
+   apply (metis dvd_1_iff_1 dvd_eq_mod_eq_0 mod_0 mod_Suc mod_Suc_eq mod_mod_cancel)
+  done
 
 corec facC :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> nat stream"
 where "facC n a i = (if i = 0 then a \<lhd> facC (n + 1) 1 (n + 1) else facC n (a * i) (i - 1))"
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Decision_Procs/Rat_Pair.thy
--- a/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Decision_Procs/Rat_Pair.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -51,7 +51,8 @@
     from dvd_mult_div_cancel[OF gdvd(1)] dvd_mult_div_cancel[OF gdvd(2)] ab
     have nz': "?a' \<noteq> 0" "?b' \<noteq> 0" by - (rule notI, simp)+
     from ab have stupid: "a \<noteq> 0 \<or> b \<noteq> 0" by arith
-    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1" .
+    from div_gcd_coprime[OF stupid] have gp1: "?g' = 1"
+      by simp
     from ab consider "b < 0" | "b > 0" by arith
     then show ?thesis
     proof cases
@@ -198,6 +199,8 @@
     from \<open>a \<noteq> 0\<close> \<open>a' \<noteq> 0\<close> na nb
     have gcd1: "gcd a b = 1" "gcd b a = 1" "gcd a' b' = 1" "gcd b' a' = 1"
       by (simp_all add: x y isnormNum_def add: gcd.commute)
+    then have "coprime a b" "coprime b a" "coprime a' b'" "coprime b' a'"
+      by (simp_all add: coprime_iff_gcd_eq_1)
     from eq have raw_dvd: "a dvd a' * b" "b dvd b' * a" "a' dvd a * b'" "b' dvd b * a'"
       apply -
       apply algebra
@@ -205,11 +208,11 @@
       apply simp
       apply algebra
       done
-    from zdvd_antisym_abs[OF coprime_dvd_mult[OF gcd1(2) raw_dvd(2)]
-        coprime_dvd_mult[OF gcd1(4) raw_dvd(4)]]
-      have eq1: "b = b'" using pos by arith
-      with eq have "a = a'" using pos by simp
-      with eq1 show ?thesis by (simp add: x y)
+    then have eq1: "b = b'"
+      using pos \<open>coprime b a\<close> \<open>coprime b' a'\<close>
+      by (auto simp add: coprime_dvd_mult_left_iff intro: associated_eqI)
+    with eq have "a = a'" using pos by simp
+    with \<open>b = b'\<close> show ?thesis by (simp add: x y)
   qed
   show ?lhs if ?rhs
     using that by simp
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Euclidean_Division.thy
--- a/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Euclidean_Division.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -125,6 +125,15 @@
   "a mod b = 0" if "is_unit b"
   using that by (simp add: mod_eq_0_iff_dvd unit_imp_dvd)
 
+lemma coprime_mod_left_iff [simp]:
+  "coprime (a mod b) b \<longleftrightarrow> coprime a b" if "b \<noteq> 0"
+  by (rule; rule coprimeI)
+    (use that in \<open>auto dest!: dvd_mod_imp_dvd coprime_common_divisor simp add: dvd_mod_iff\<close>)
+
+lemma coprime_mod_right_iff [simp]:
+  "coprime a (b mod a) \<longleftrightarrow> coprime a b" if "a \<noteq> 0"
+  using that coprime_mod_left_iff [of a b] by (simp add: ac_simps)
+
 end
 
 class euclidean_ring = idom_modulo + euclidean_semiring
@@ -533,6 +542,10 @@
   with that show thesis .
 qed
 
+lemma invertible_coprime:
+  "coprime a c" if "a * b mod c = 1"
+  by (rule coprimeI) (use that dvd_mod_iff [of _ c "a * b"] in auto)
+
 end
 
   
@@ -772,6 +785,18 @@
 
 end
 
+lemma coprime_Suc_0_left [simp]:
+  "coprime (Suc 0) n"
+  using coprime_1_left [of n] by simp
+
+lemma coprime_Suc_0_right [simp]:
+  "coprime n (Suc 0)"
+  using coprime_1_right [of n] by simp
+
+lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+  for a b :: nat
+  by (drule coprime_common_divisor [of _ _ x]) simp_all
+
 instantiation nat :: unique_euclidean_semiring
 begin
 
@@ -1422,6 +1447,64 @@
 
 end
 
+lemma coprime_int_iff [simp]:
+  "coprime (int m) (int n) \<longleftrightarrow> coprime m n" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  show ?Q
+  proof (rule coprimeI)
+    fix q
+    assume "q dvd m" "q dvd n"
+    then have "int q dvd int m" "int q dvd int n"
+      by (simp_all add: zdvd_int)
+    with \<open>?P\<close> have "is_unit (int q)"
+      by (rule coprime_common_divisor)
+    then show "is_unit q"
+      by simp
+  qed
+next
+  assume ?Q
+  show ?P
+  proof (rule coprimeI)
+    fix k
+    assume "k dvd int m" "k dvd int n"
+    then have "nat \<bar>k\<bar> dvd m" "nat \<bar>k\<bar> dvd n"
+      by (simp_all add: zdvd_int)
+    with \<open>?Q\<close> have "is_unit (nat \<bar>k\<bar>)"
+      by (rule coprime_common_divisor)
+    then show "is_unit k"
+      by simp
+  qed
+qed
+
+lemma coprime_abs_left_iff [simp]:
+  "coprime \<bar>k\<bar> l \<longleftrightarrow> coprime k l" for k l :: int
+  using coprime_normalize_left_iff [of k l] by simp
+
+lemma coprime_abs_right_iff [simp]:
+  "coprime k \<bar>l\<bar> \<longleftrightarrow> coprime k l" for k l :: int
+  using coprime_abs_left_iff [of l k] by (simp add: ac_simps)
+
+lemma coprime_nat_abs_left_iff [simp]:
+  "coprime (nat \<bar>k\<bar>) n \<longleftrightarrow> coprime k (int n)"
+proof -
+  define m where "m = nat \<bar>k\<bar>"
+  then have "\<bar>k\<bar> = int m"
+    by simp
+  moreover have "coprime k (int n) \<longleftrightarrow> coprime \<bar>k\<bar> (int n)"
+    by simp
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma coprime_nat_abs_right_iff [simp]:
+  "coprime n (nat \<bar>k\<bar>) \<longleftrightarrow> coprime (int n) k"
+  using coprime_nat_abs_left_iff [of k n] by (simp add: ac_simps)
+
+lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
+  for a b :: int
+  by (drule coprime_common_divisor [of _ _ x]) simp_all
+
 instantiation int :: idom_modulo
 begin
 
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/GCD.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -142,12 +142,6 @@
 class gcd = zero + one + dvd +
   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
-begin
-
-abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-  where "coprime x y \<equiv> gcd x y = 1"
-
-end
 
 class Gcd = gcd +
   fixes Gcd :: "'a set \<Rightarrow> 'a"
@@ -243,7 +237,8 @@
     by simp
 qed
 
-lemma is_unit_gcd [simp]: "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+lemma is_unit_gcd_iff [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> gcd a b = 1"
   by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
 
 sublocale gcd: abel_semigroup gcd
@@ -279,7 +274,7 @@
   show "gcd (normalize a) b = gcd a b" for a b
     using gcd_dvd1 [of "normalize a" b]
     by (auto intro: associated_eqI)
-  show "coprime 1 a" for a
+  show "gcd 1 a = 1" for a
     by (rule associated_eqI) simp_all
 qed simp_all
 
@@ -292,12 +287,6 @@
 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   by (fact gcd.right_idem)
 
-lemma coprime_1_left: "coprime 1 a"
-  by (fact gcd.bottom_left_bottom)
-
-lemma coprime_1_right: "coprime a 1"
-  by (fact gcd.bottom_right_bottom)
-
 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
 proof (cases "c = 0")
   case True
@@ -634,70 +623,6 @@
     by (rule dvd_trans)
 qed
 
-lemma coprime_dvd_mult:
-  assumes "coprime a b" and "a dvd c * b"
-  shows "a dvd c"
-proof (cases "c = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have unit: "is_unit (unit_factor c)"
-    by simp
-  from \<open>coprime a b\<close> mult_gcd_left [of c a b]
-  have "gcd (c * a) (c * b) * unit_factor c = c"
-    by (simp add: ac_simps)
-  moreover from \<open>a dvd c * b\<close> have "a dvd gcd (c * a) (c * b) * unit_factor c"
-    by (simp add: dvd_mult_unit_iff unit)
-  ultimately show ?thesis
-    by simp
-qed
-
-lemma coprime_dvd_mult_iff: "coprime a c \<Longrightarrow> a dvd b * c \<longleftrightarrow> a dvd b"
-  by (auto intro: coprime_dvd_mult)
-
-lemma gcd_mult_cancel: "coprime c b \<Longrightarrow> gcd (c * a) b = gcd a b"
-  apply (rule associated_eqI)
-     apply (rule gcd_greatest)
-      apply (rule_tac b = c in coprime_dvd_mult)
-       apply (simp add: gcd.assoc)
-       apply (simp_all add: ac_simps)
-  done
-
-lemma coprime_crossproduct:
-  fixes a b c d :: 'a
-  assumes "coprime a d" and "coprime b c"
-  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
-    normalize a = normalize b \<and> normalize c = normalize d"
-    (is "?lhs \<longleftrightarrow> ?rhs")
-proof
-  assume ?rhs
-  then show ?lhs by simp
-next
-  assume ?lhs
-  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
-    by (auto intro: dvdI dest: sym)
-  with \<open>coprime a d\<close> have "a dvd b"
-    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
-    by (auto intro: dvdI dest: sym)
-  with \<open>coprime b c\<close> have "b dvd a"
-    by (simp add: coprime_dvd_mult_iff normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
-    by (auto intro: dvdI dest: sym simp add: mult.commute)
-  with \<open>coprime b c\<close> have "c dvd d"
-    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
-  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
-    by (auto intro: dvdI dest: sym simp add: mult.commute)
-  with \<open>coprime a d\<close> have "d dvd c"
-    by (simp add: coprime_dvd_mult_iff gcd.commute normalize_mult [symmetric])
-  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
-    by (rule associatedI)
-  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
-    by (rule associatedI)
-  ultimately show ?rhs ..
-qed
-
 lemma gcd_add1 [simp]: "gcd (m + n) n = gcd m n"
   by (rule gcdI [symmetric]) (simp_all add: dvd_add_left_iff)
 
@@ -707,285 +632,6 @@
 lemma gcd_add_mult: "gcd m (k * m + n) = gcd m n"
   by (rule gcdI [symmetric]) (simp_all add: dvd_add_right_iff)
 
-lemma coprimeI: "(\<And>l. l dvd a \<Longrightarrow> l dvd b \<Longrightarrow> l dvd 1) \<Longrightarrow> gcd a b = 1"
-  by (rule sym, rule gcdI) simp_all
-
-lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
-  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
-
-lemma div_gcd_coprime:
-  assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
-  shows "coprime (a div gcd a b) (b div gcd a b)"
-proof -
-  let ?g = "gcd a b"
-  let ?a' = "a div ?g"
-  let ?b' = "b div ?g"
-  let ?g' = "gcd ?a' ?b'"
-  have dvdg: "?g dvd a" "?g dvd b"
-    by simp_all
-  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
-    by simp_all
-  from dvdg dvdg' obtain ka kb ka' kb' where
-    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
-    unfolding dvd_def by blast
-  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
-    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
-  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
-    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
-  have "?g \<noteq> 0"
-    using nz by simp
-  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  ultimately show ?thesis
-    using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
-qed
-
-lemma divides_mult:
-  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
-  shows "a * b dvd c"
-proof -
-  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
-  with \<open>a dvd c\<close> have "a dvd b' * b"
-    by (simp add: ac_simps)
-  with \<open>coprime a b\<close> have "a dvd b'"
-    by (simp add: coprime_dvd_mult_iff)
-  then obtain a' where "b' = a * a'" ..
-  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
-    by (simp add: ac_simps)
-  then show ?thesis ..
-qed
-
-lemma coprime_lmult:
-  assumes dab: "gcd d (a * b) = 1"
-  shows "gcd d a = 1"
-proof (rule coprimeI)
-  fix l
-  assume "l dvd d" and "l dvd a"
-  then have "l dvd a * b"
-    by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1"
-    by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_rmult:
-  assumes dab: "gcd d (a * b) = 1"
-  shows "gcd d b = 1"
-proof (rule coprimeI)
-  fix l
-  assume "l dvd d" and "l dvd b"
-  then have "l dvd a * b"
-    by simp
-  with \<open>l dvd d\<close> and dab show "l dvd 1"
-    by (auto intro: gcd_greatest)
-qed
-
-lemma coprime_mult:
-  assumes "coprime d a"
-    and "coprime d b"
-  shows "coprime d (a * b)"
-  apply (subst gcd.commute)
-  using assms(1) apply (subst gcd_mult_cancel)
-   apply (subst gcd.commute)
-   apply assumption
-  apply (subst gcd.commute)
-  apply (rule assms(2))
-  done
-
-lemma coprime_mul_eq: "gcd d (a * b) = 1 \<longleftrightarrow> gcd d a = 1 \<and> gcd d b = 1"
-  using coprime_rmult[of d a b] coprime_lmult[of d a b] coprime_mult[of d a b]
-  by blast
-
-lemma coprime_mul_eq':
-  "coprime (a * b) d \<longleftrightarrow> coprime a d \<and> coprime b d"
-  using coprime_mul_eq [of d a b] by (simp add: gcd.commute)
-
-lemma gcd_coprime:
-  assumes c: "gcd a b \<noteq> 0"
-    and a: "a = a' * gcd a b"
-    and b: "b = b' * gcd a b"
-  shows "gcd a' b' = 1"
-proof -
-  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
-    by simp
-  with div_gcd_coprime have "gcd (a div gcd a b) (b div gcd a b) = 1" .
-  also from assms have "a div gcd a b = a'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
-  also from assms have "b div gcd a b = b'"
-    using dvd_div_eq_mult local.gcd_dvd1 by blast
-  finally show ?thesis .
-qed
-
-lemma coprime_power:
-  assumes "0 < n"
-  shows "gcd a (b ^ n) = 1 \<longleftrightarrow> gcd a b = 1"
-  using assms
-proof (induct n)
-  case 0
-  then show ?case by simp
-next
-  case (Suc n)
-  then show ?case
-    by (cases n) (simp_all add: coprime_mul_eq)
-qed
-
-lemma gcd_coprime_exists:
-  assumes "gcd a b \<noteq> 0"
-  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> gcd a' b' = 1"
-  apply (rule_tac x = "a div gcd a b" in exI)
-  apply (rule_tac x = "b div gcd a b" in exI)
-  using assms
-  apply (auto intro: div_gcd_coprime)
-  done
-
-lemma coprime_exp: "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
-  by (induct n) (simp_all add: coprime_mult)
-
-lemma coprime_exp_left: "coprime a b \<Longrightarrow> coprime (a ^ n) b"
-  by (induct n) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_exp2:
-  assumes "coprime a b"
-  shows "coprime (a ^ n) (b ^ m)"
-proof (rule coprime_exp_left)
-  from assms show "coprime a (b ^ m)"
-    by (induct m) (simp_all add: gcd_mult_cancel gcd.commute [of a])
-qed
-
-lemma gcd_exp: "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
-proof (cases "a = 0 \<and> b = 0")
-  case True
-  then show ?thesis
-    by (cases n) simp_all
-next
-  case False
-  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
-    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
-  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
-    by simp
-  also note gcd_mult_distrib
-  also have "unit_factor (gcd a b ^ n) = 1"
-    using False by (auto simp add: unit_factor_power unit_factor_gcd)
-  also have "(gcd a b)^n * (a div gcd a b)^n = a^n"
-    apply (subst ac_simps)
-    apply (subst div_power)
-     apply simp
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply simp
-    done
-  also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
-    apply (subst ac_simps)
-    apply (subst div_power)
-     apply simp
-    apply (rule dvd_div_mult_self)
-    apply (rule dvd_power_same)
-    apply simp
-    done
-  finally show ?thesis by simp
-qed
-
-lemma coprime_common_divisor: "gcd a b = 1 \<Longrightarrow> a dvd a \<Longrightarrow> a dvd b \<Longrightarrow> is_unit a"
-  apply (subgoal_tac "a dvd gcd a b")
-   apply simp
-  apply (erule (1) gcd_greatest)
-  done
-
-lemma division_decomp:
-  assumes "a dvd b * c"
-  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
-proof (cases "gcd a b = 0")
-  case True
-  then have "a = 0 \<and> b = 0"
-    by simp
-  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
-    by simp
-  then show ?thesis by blast
-next
-  case False
-  let ?d = "gcd a b"
-  from gcd_coprime_exists [OF False]
-    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
-    by blast
-  from ab'(1) have "a' dvd a"
-    unfolding dvd_def by blast
-  with assms have "a' dvd b * c"
-    using dvd_trans [of a' a "b * c"] by simp
-  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
-    by simp
-  then have "?d * a' dvd ?d * (b' * c)"
-    by (simp add: mult_ac)
-  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
-    by simp
-  with coprime_dvd_mult[OF ab'(3)] have "a' dvd c"
-    by (subst (asm) ac_simps) blast
-  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
-    by (simp add: mult_ac)
-  then show ?thesis by blast
-qed
-
-lemma pow_divs_pow:
-  assumes ab: "a ^ n dvd b ^ n" and n: "n \<noteq> 0"
-  shows "a dvd b"
-proof (cases "gcd a b = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  let ?d = "gcd a b"
-  from n obtain m where m: "n = Suc m"
-    by (cases n) simp_all
-  from False have zn: "?d ^ n \<noteq> 0"
-    by (rule power_not_zero)
-  from gcd_coprime_exists [OF False]
-  obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "gcd a' b' = 1"
-    by blast
-  from ab have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
-    by (simp add: ab'(1,2)[symmetric])
-  then have "?d^n * a'^n dvd ?d^n * b'^n"
-    by (simp only: power_mult_distrib ac_simps)
-  with zn have "a'^n dvd b'^n"
-    by simp
-  then have "a' dvd b'^n"
-    using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
-  then have "a' dvd b'^m * b'"
-    by (simp add: m ac_simps)
-  with coprime_dvd_mult[OF coprime_exp[OF ab'(3), of m]]
-  have "a' dvd b'" by (subst (asm) ac_simps) blast
-  then have "a' * ?d dvd b' * ?d"
-    by (rule mult_dvd_mono) simp
-  with ab'(1,2) show ?thesis
-    by simp
-qed
-
-lemma pow_divs_eq [simp]: "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
-  by (auto intro: pow_divs_pow dvd_power_same)
-
-lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
-  by (subst add_commute) simp
-
-lemma prod_coprime [rule_format]: "(\<forall>i\<in>A. gcd (f i) a = 1) \<longrightarrow> gcd (\<Prod>i\<in>A. f i) a = 1"
-  by (induct A rule: infinite_finite_induct) (auto simp add: gcd_mult_cancel)
-
-lemma prod_list_coprime: "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (prod_list xs) y"
-  by (induct xs) (simp_all add: gcd_mult_cancel)
-
-lemma coprime_divisors:
-  assumes "d dvd a" "e dvd b" "gcd a b = 1"
-  shows "gcd d e = 1"
-proof -
-  from assms obtain k l where "a = d * k" "b = e * l"
-    unfolding dvd_def by blast
-  with assms have "gcd (d * k) (e * l) = 1"
-    by simp
-  then have "gcd (d * k) e = 1"
-    by (rule coprime_lmult)
-  also have "gcd (d * k) e = gcd e (d * k)"
-    by (simp add: ac_simps)
-  finally have "gcd e d = 1"
-    by (rule coprime_lmult)
-  then show ?thesis
-    by (simp add: ac_simps)
-qed
-
 lemma lcm_gcd_prod: "lcm a b * gcd a b = normalize (a * b)"
   by (simp add: lcm_gcd)
 
@@ -1006,9 +652,6 @@
   "a dvd d \<and> b dvd d \<and> normalize d = d \<and> (\<forall>e. a dvd e \<and> b dvd e \<longrightarrow> d dvd e) \<longleftrightarrow> d = lcm a b"
   by rule (auto intro: lcmI simp: lcm_least lcm_eq_0_iff)
 
-lemma lcm_coprime: "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
-  by (subst lcm_gcd) simp
-
 lemma lcm_proj1_if_dvd: "b dvd a \<Longrightarrow> lcm a b = normalize a"
   apply (cases "a = 0")
    apply simp
@@ -1058,7 +701,7 @@
 qed
 
 lemma dvd_productE:
-  assumes "p dvd (a * b)"
+  assumes "p dvd a * b"
   obtains x y where "p = x * y" "x dvd a" "y dvd b"
 proof (cases "a = 0")
   case True
@@ -1076,32 +719,11 @@
   ultimately show ?thesis by (rule that)
 qed
 
-lemma coprime_crossproduct':
-  fixes a b c d
-  assumes "b \<noteq> 0"
-  assumes unit_factors: "unit_factor b = unit_factor d"
-  assumes coprime: "coprime a b" "coprime c d"
-  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
-proof safe
-  assume eq: "a * d = b * c"
-  hence "normalize a * normalize d = normalize c * normalize b"
-    by (simp only: normalize_mult [symmetric] mult_ac)
-  with coprime have "normalize b = normalize d"
-    by (subst (asm) coprime_crossproduct) simp_all
-  from this and unit_factors show "b = d"
-    by (rule normalize_unit_factor_eqI)
-  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
-  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
-qed (simp_all add: mult_ac)
-
 end
 
 class ring_gcd = comm_ring_1 + semiring_gcd
 begin
 
-lemma coprime_minus_one: "coprime (n - 1) n"
-  using coprime_plus_one[of "n - 1"] by (simp add: gcd.commute)
-
 lemma gcd_neg1 [simp]: "gcd (-a) b = gcd a b"
   by (rule sym, rule gcdI) (simp_all add: gcd_greatest)
 
@@ -1471,36 +1093,6 @@
 lemma Lcm_2 [simp]: "Lcm {a, b} = lcm a b"
   by simp
 
-lemma Lcm_coprime:
-  assumes "finite A"
-    and "A \<noteq> {}"
-    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1"
-  shows "Lcm A = normalize (\<Prod>A)"
-  using assms
-proof (induct rule: finite_ne_induct)
-  case singleton
-  then show ?case by simp
-next
-  case (insert a A)
-  have "Lcm (insert a A) = lcm a (Lcm A)"
-    by simp
-  also from insert have "Lcm A = normalize (\<Prod>A)"
-    by blast
-  also have "lcm a \<dots> = lcm a (\<Prod>A)"
-    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
-  also from insert have "gcd a (\<Prod>A) = 1"
-    by (subst gcd.commute, intro prod_coprime) auto
-  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
-    by (simp add: lcm_coprime)
-  finally show ?case .
-qed
-
-lemma Lcm_coprime':
-  "card A \<noteq> 0 \<Longrightarrow>
-    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> gcd a b = 1) \<Longrightarrow>
-    Lcm A = normalize (\<Prod>A)"
-  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
-
 lemma Gcd_1: "1 \<in> A \<Longrightarrow> Gcd A = 1"
   by (auto intro!: Gcd_eq_1_I)
 
@@ -1677,6 +1269,465 @@
 
 end
 
+
+subsection \<open>Coprimality\<close>
+
+context semiring_gcd
+begin
+
+lemma coprime_imp_gcd_eq_1 [simp]:
+  "gcd a b = 1" if "coprime a b"
+proof -
+  define t r s where "t = gcd a b" and "r = a div t" and "s = b div t"
+  then have "a = t * r" and "b = t * s"
+    by simp_all
+  with that have "coprime (t * r) (t * s)"
+    by simp
+  then show ?thesis
+    by (simp add: t_def)
+qed
+
+lemma gcd_eq_1_imp_coprime:
+  "coprime a b" if "gcd a b = 1"
+proof (rule coprimeI)
+  fix c
+  assume "c dvd a" and "c dvd b"
+  then have "c dvd gcd a b"
+    by (rule gcd_greatest)
+  with that show "is_unit c"
+    by simp
+qed
+
+lemma coprime_iff_gcd_eq_1 [presburger, code]:
+  "coprime a b \<longleftrightarrow> gcd a b = 1"
+  by rule (simp_all add: gcd_eq_1_imp_coprime)
+
+lemma is_unit_gcd [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+  by (simp add: coprime_iff_gcd_eq_1)
+
+lemma coprime_add_one_left [simp]: "coprime (a + 1) a"
+  by (simp add: gcd_eq_1_imp_coprime ac_simps)
+
+lemma coprime_add_one_right [simp]: "coprime a (a + 1)"
+  using coprime_add_one_left [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_left_iff [simp]:
+  "coprime (a * b) c \<longleftrightarrow> coprime a c \<and> coprime b c"
+proof
+  assume "coprime (a * b) c"
+  with coprime_common_divisor [of "a * b" c]
+  have *: "is_unit d" if "d dvd a * b" and "d dvd c" for d
+    using that by blast
+  have "coprime a c"
+    by (rule coprimeI, rule *) simp_all
+  moreover have "coprime b c"
+    by (rule coprimeI, rule *) simp_all
+  ultimately show "coprime a c \<and> coprime b c" ..
+next
+  assume "coprime a c \<and> coprime b c"
+  then have "coprime a c" "coprime b c"
+    by simp_all
+  show "coprime (a * b) c"
+  proof (rule coprimeI)
+    fix d
+    assume "d dvd a * b"
+    then obtain r s where d: "d = r * s" "r dvd a" "s dvd b"
+      by (rule dvd_productE)
+    assume "d dvd c"
+    with d have "r * s dvd c"
+      by simp
+    then have "r dvd c" "s dvd c"
+      by (auto intro: dvd_mult_left dvd_mult_right)
+    from \<open>coprime a c\<close> \<open>r dvd a\<close> \<open>r dvd c\<close>
+    have "is_unit r"
+      by (rule coprime_common_divisor)
+    moreover from \<open>coprime b c\<close> \<open>s dvd b\<close> \<open>s dvd c\<close>
+    have "is_unit s"
+      by (rule coprime_common_divisor)
+    ultimately show "is_unit d"
+      by (simp add: d is_unit_mult_iff)
+  qed
+qed
+
+lemma coprime_mult_right_iff [simp]:
+  "coprime c (a * b) \<longleftrightarrow> coprime c a \<and> coprime c b"
+  using coprime_mult_left_iff [of a b c] by (simp add: ac_simps)
+
+lemma coprime_power_left_iff [simp]:
+  "coprime (a ^ n) b \<longleftrightarrow> coprime a b \<or> n = 0"
+proof (cases "n = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  then have "n > 0"
+    by simp
+  then show ?thesis
+    by (induction n rule: nat_induct_non_zero) simp_all
+qed
+
+lemma coprime_power_right_iff [simp]:
+  "coprime a (b ^ n) \<longleftrightarrow> coprime a b \<or> n = 0"
+  using coprime_power_left_iff [of b n a] by (simp add: ac_simps)
+
+lemma prod_coprime_left:
+  "coprime (\<Prod>i\<in>A. f i) a" if "\<And>i. i \<in> A \<Longrightarrow> coprime (f i) a"
+  using that by (induct A rule: infinite_finite_induct) simp_all
+
+lemma prod_coprime_right:
+  "coprime a (\<Prod>i\<in>A. f i)" if "\<And>i. i \<in> A \<Longrightarrow> coprime a (f i)"
+  using that prod_coprime_left [of A f a] by (simp add: ac_simps)
+
+lemma prod_list_coprime_left:
+  "coprime (prod_list xs) a" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime x a"
+  using that by (induct xs) simp_all
+
+lemma prod_list_coprime_right:
+  "coprime a (prod_list xs)" if "\<And>x. x \<in> set xs \<Longrightarrow> coprime a x"
+  using that prod_list_coprime_left [of xs a] by (simp add: ac_simps)
+
+lemma coprime_dvd_mult_left_iff:
+  "a dvd b * c \<longleftrightarrow> a dvd b" if "coprime a c"
+proof
+  assume "a dvd b"
+  then show "a dvd b * c"
+    by simp
+next
+  assume "a dvd b * c"
+  show "a dvd b"
+  proof (cases "b = 0")
+    case True
+    then show ?thesis
+      by simp
+  next
+    case False
+    then have unit: "is_unit (unit_factor b)"
+      by simp
+    from \<open>coprime a c\<close> mult_gcd_left [of b a c]
+    have "gcd (b * a) (b * c) * unit_factor b = b"
+      by (simp add: ac_simps)
+    moreover from \<open>a dvd b * c\<close>
+    have "a dvd gcd (b * a) (b * c) * unit_factor b"
+      by (simp add: dvd_mult_unit_iff unit)
+    ultimately show ?thesis
+      by simp
+  qed
+qed
+
+lemma coprime_dvd_mult_right_iff:
+  "a dvd c * b \<longleftrightarrow> a dvd b" if "coprime a c"
+  using that coprime_dvd_mult_left_iff [of a c b] by (simp add: ac_simps)
+
+lemma divides_mult:
+  "a * b dvd c" if "a dvd c" and "b dvd c" and "coprime a b"
+proof -
+  from \<open>b dvd c\<close> obtain b' where "c = b * b'" ..
+  with \<open>a dvd c\<close> have "a dvd b' * b"
+    by (simp add: ac_simps)
+  with \<open>coprime a b\<close> have "a dvd b'"
+    by (simp add: coprime_dvd_mult_left_iff)
+  then obtain a' where "b' = a * a'" ..
+  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
+    by (simp add: ac_simps)
+  then show ?thesis ..
+qed
+
+lemma div_gcd_coprime:
+  assumes "a \<noteq> 0 \<or> b \<noteq> 0"
+  shows "coprime (a div gcd a b) (b div gcd a b)"
+proof -
+  let ?g = "gcd a b"
+  let ?a' = "a div ?g"
+  let ?b' = "b div ?g"
+  let ?g' = "gcd ?a' ?b'"
+  have dvdg: "?g dvd a" "?g dvd b"
+    by simp_all
+  have dvdg': "?g' dvd ?a'" "?g' dvd ?b'"
+    by simp_all
+  from dvdg dvdg' obtain ka kb ka' kb' where
+    kab: "a = ?g * ka" "b = ?g * kb" "?a' = ?g' * ka'" "?b' = ?g' * kb'"
+    unfolding dvd_def by blast
+  from this [symmetric] have "?g * ?a' = (?g * ?g') * ka'" "?g * ?b' = (?g * ?g') * kb'"
+    by (simp_all add: mult.assoc mult.left_commute [of "gcd a b"])
+  then have dvdgg':"?g * ?g' dvd a" "?g* ?g' dvd b"
+    by (auto simp add: dvd_mult_div_cancel [OF dvdg(1)] dvd_mult_div_cancel [OF dvdg(2)] dvd_def)
+  have "?g \<noteq> 0"
+    using assms by simp
+  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  ultimately show ?thesis
+    using dvd_times_left_cancel_iff [of "gcd a b" _ 1]
+    by simp (simp only: coprime_iff_gcd_eq_1)
+qed
+
+lemma gcd_coprime:
+  assumes c: "gcd a b \<noteq> 0"
+    and a: "a = a' * gcd a b"
+    and b: "b = b' * gcd a b"
+  shows "coprime a' b'"
+proof -
+  from c have "a \<noteq> 0 \<or> b \<noteq> 0"
+    by simp
+  with div_gcd_coprime have "coprime (a div gcd a b) (b div gcd a b)" .
+  also from assms have "a div gcd a b = a'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
+  also from assms have "b div gcd a b = b'"
+    using dvd_div_eq_mult local.gcd_dvd1 by blast
+  finally show ?thesis .
+qed
+
+lemma gcd_coprime_exists:
+  assumes "gcd a b \<noteq> 0"
+  shows "\<exists>a' b'. a = a' * gcd a b \<and> b = b' * gcd a b \<and> coprime a' b'"
+  apply (rule_tac x = "a div gcd a b" in exI)
+  apply (rule_tac x = "b div gcd a b" in exI)
+  using assms
+  apply (auto intro: div_gcd_coprime)
+  done
+
+lemma pow_divides_pow_iff [simp]:
+  "a ^ n dvd b ^ n \<longleftrightarrow> a dvd b" if "n > 0"
+proof (cases "gcd a b = 0")
+  case True
+  then show ?thesis
+    by simp
+next
+  case False
+  show ?thesis
+  proof
+    let ?d = "gcd a b"
+    from \<open>n > 0\<close> obtain m where m: "n = Suc m"
+      by (cases n) simp_all
+    from False have zn: "?d ^ n \<noteq> 0"
+      by (rule power_not_zero)
+    from gcd_coprime_exists [OF False]
+    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+      by blast
+    assume "a ^ n dvd b ^ n"
+    then have "(a' * ?d) ^ n dvd (b' * ?d) ^ n"
+      by (simp add: ab'(1,2)[symmetric])
+    then have "?d^n * a'^n dvd ?d^n * b'^n"
+      by (simp only: power_mult_distrib ac_simps)
+    with zn have "a' ^ n dvd b' ^ n"
+      by simp
+    then have "a' dvd b' ^ n"
+      using dvd_trans[of a' "a'^n" "b'^n"] by (simp add: m)
+    then have "a' dvd b' ^ m * b'"
+      by (simp add: m ac_simps)
+    moreover have "coprime a' (b' ^ n)"
+      using \<open>coprime a' b'\<close> by simp
+    then have "a' dvd b'"
+      using \<open>a' dvd b' ^ n\<close> coprime_dvd_mult_left_iff dvd_mult by blast
+    then have "a' * ?d dvd b' * ?d"
+      by (rule mult_dvd_mono) simp
+    with ab'(1,2) show "a dvd b"
+      by simp
+  next
+    assume "a dvd b"
+    with \<open>n > 0\<close> show "a ^ n dvd b ^ n"
+      by (induction rule: nat_induct_non_zero)
+        (simp_all add: mult_dvd_mono)
+  qed
+qed
+
+lemma coprime_crossproduct:
+  fixes a b c d :: 'a
+  assumes "coprime a d" and "coprime b c"
+  shows "normalize a * normalize c = normalize b * normalize d \<longleftrightarrow>
+    normalize a = normalize b \<and> normalize c = normalize d"
+    (is "?lhs \<longleftrightarrow> ?rhs")
+proof
+  assume ?rhs
+  then show ?lhs by simp
+next
+  assume ?lhs
+  from \<open>?lhs\<close> have "normalize a dvd normalize b * normalize d"
+    by (auto intro: dvdI dest: sym)
+  with \<open>coprime a d\<close> have "a dvd b"
+    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize b dvd normalize a * normalize c"
+    by (auto intro: dvdI dest: sym)
+  with \<open>coprime b c\<close> have "b dvd a"
+    by (simp add: coprime_dvd_mult_left_iff normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize c dvd normalize d * normalize b"
+    by (auto intro: dvdI dest: sym simp add: mult.commute)
+  with \<open>coprime b c\<close> have "c dvd d"
+    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+  from \<open>?lhs\<close> have "normalize d dvd normalize c * normalize a"
+    by (auto intro: dvdI dest: sym simp add: mult.commute)
+  with \<open>coprime a d\<close> have "d dvd c"
+    by (simp add: coprime_dvd_mult_left_iff coprime_commute normalize_mult [symmetric])
+  from \<open>a dvd b\<close> \<open>b dvd a\<close> have "normalize a = normalize b"
+    by (rule associatedI)
+  moreover from \<open>c dvd d\<close> \<open>d dvd c\<close> have "normalize c = normalize d"
+    by (rule associatedI)
+  ultimately show ?rhs ..
+qed
+
+lemma coprime_crossproduct':
+  fixes a b c d
+  assumes "b \<noteq> 0"
+  assumes unit_factors: "unit_factor b = unit_factor d"
+  assumes coprime: "coprime a b" "coprime c d"
+  shows "a * d = b * c \<longleftrightarrow> a = c \<and> b = d"
+proof safe
+  assume eq: "a * d = b * c"
+  hence "normalize a * normalize d = normalize c * normalize b"
+    by (simp only: normalize_mult [symmetric] mult_ac)
+  with coprime have "normalize b = normalize d"
+    by (subst (asm) coprime_crossproduct) simp_all
+  from this and unit_factors show "b = d"
+    by (rule normalize_unit_factor_eqI)
+  from eq have "a * d = c * d" by (simp only: \<open>b = d\<close> mult_ac)
+  with \<open>b \<noteq> 0\<close> \<open>b = d\<close> show "a = c" by simp
+qed (simp_all add: mult_ac)
+
+lemma gcd_mult_left_left_cancel:
+  "gcd (c * a) b = gcd a b" if "coprime b c"
+proof -
+  have "coprime (gcd b (a * c)) c"
+    by (rule coprimeI) (auto intro: that coprime_common_divisor)
+  then have "gcd b (a * c) dvd a"
+    using coprime_dvd_mult_left_iff [of "gcd b (a * c)" c a]
+    by simp
+  then show ?thesis
+    by (auto intro: associated_eqI simp add: ac_simps)
+qed
+
+lemma gcd_mult_left_right_cancel:
+  "gcd (a * c) b = gcd a b" if "coprime b c"
+  using that gcd_mult_left_left_cancel [of b c a]
+  by (simp add: ac_simps)
+
+lemma gcd_mult_right_left_cancel:
+  "gcd a (c * b) = gcd a b" if "coprime a c"
+  using that gcd_mult_left_left_cancel [of a c b]
+  by (simp add: ac_simps)
+
+lemma gcd_mult_right_right_cancel:
+  "gcd a (b * c) = gcd a b" if "coprime a c"
+  using that gcd_mult_right_left_cancel [of a c b]
+  by (simp add: ac_simps)
+
+lemma gcd_exp [simp]:
+  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0 \<or> n = 0")
+  case True
+  then show ?thesis
+    by (cases n) simp_all
+next
+  case False
+  then have "coprime (a div gcd a b) (b div gcd a b)" and "n > 0"
+    by (auto intro: div_gcd_coprime)
+  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by simp
+  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by simp
+  then have "gcd a b ^ n = gcd a b ^ n * \<dots>"
+    by simp
+  also note gcd_mult_distrib
+  also have "unit_factor (gcd a b ^ n) = 1"
+    using False by (auto simp add: unit_factor_power unit_factor_gcd)
+  also have "(gcd a b) ^ n * (a div gcd a b) ^ n = a ^ n"
+    by (simp add: ac_simps div_power dvd_power_same)
+  also have "(gcd a b) ^ n * (b div gcd a b) ^ n = b ^ n"
+    by (simp add: ac_simps div_power dvd_power_same)
+  finally show ?thesis by simp
+qed
+
+lemma division_decomp:
+  assumes "a dvd b * c"
+  shows "\<exists>b' c'. a = b' * c' \<and> b' dvd b \<and> c' dvd c"
+proof (cases "gcd a b = 0")
+  case True
+  then have "a = 0 \<and> b = 0"
+    by simp
+  then have "a = 0 * c \<and> 0 dvd b \<and> c dvd c"
+    by simp
+  then show ?thesis by blast
+next
+  case False
+  let ?d = "gcd a b"
+  from gcd_coprime_exists [OF False]
+    obtain a' b' where ab': "a = a' * ?d" "b = b' * ?d" "coprime a' b'"
+    by blast
+  from ab'(1) have "a' dvd a" ..
+  with assms have "a' dvd b * c"
+    using dvd_trans [of a' a "b * c"] by simp
+  from assms ab'(1,2) have "a' * ?d dvd (b' * ?d) * c"
+    by simp
+  then have "?d * a' dvd ?d * (b' * c)"
+    by (simp add: mult_ac)
+  with \<open>?d \<noteq> 0\<close> have "a' dvd b' * c"
+    by simp
+  then have "a' dvd c"
+    using \<open>coprime a' b'\<close> by (simp add: coprime_dvd_mult_right_iff)
+  with ab'(1) have "a = ?d * a' \<and> ?d dvd b \<and> a' dvd c"
+    by (simp add: ac_simps)
+  then show ?thesis by blast
+qed
+
+lemma lcm_coprime: "coprime a b \<Longrightarrow> lcm a b = normalize (a * b)"
+  by (subst lcm_gcd) simp
+
+end
+
+context ring_gcd
+begin
+
+lemma coprime_minus_left_iff [simp]:
+  "coprime (- a) b \<longleftrightarrow> coprime a b"
+  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_minus_right_iff [simp]:
+  "coprime a (- b) \<longleftrightarrow> coprime a b"
+  using coprime_minus_left_iff [of b a] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left [simp]: "coprime (a - 1) a"
+  using coprime_add_one_right [of "a - 1"] by simp
+
+lemma coprime_doff_one_right [simp]: "coprime a (a - 1)"
+  using coprime_diff_one_left [of a] by (simp add: ac_simps)
+
+end
+
+context semiring_Gcd
+begin
+
+lemma Lcm_coprime:
+  assumes "finite A"
+    and "A \<noteq> {}"
+    and "\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b"
+  shows "Lcm A = normalize (\<Prod>A)"
+  using assms
+proof (induct rule: finite_ne_induct)
+  case singleton
+  then show ?case by simp
+next
+  case (insert a A)
+  have "Lcm (insert a A) = lcm a (Lcm A)"
+    by simp
+  also from insert have "Lcm A = normalize (\<Prod>A)"
+    by blast
+  also have "lcm a \<dots> = lcm a (\<Prod>A)"
+    by (cases "\<Prod>A = 0") (simp_all add: lcm_div_unit2)
+  also from insert have "coprime a (\<Prod>A)"
+    by (subst coprime_commute, intro prod_coprime_left) auto
+  with insert have "lcm a (\<Prod>A) = normalize (\<Prod>(insert a A))"
+    by (simp add: lcm_coprime)
+  finally show ?case .
+qed
+
+lemma Lcm_coprime':
+  "card A \<noteq> 0 \<Longrightarrow>
+    (\<And>a b. a \<in> A \<Longrightarrow> b \<in> A \<Longrightarrow> a \<noteq> b \<Longrightarrow> coprime a b) \<Longrightarrow>
+    Lcm A = normalize (\<Prod>A)"
+  by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
+
+end
+
+
 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
 
 instantiation nat :: gcd
@@ -1716,9 +1767,6 @@
    apply simp_all
   done
 
-
-text \<open>Specific to \<open>int\<close>.\<close>
-
 lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
   by (simp add: gcd_int_def)
 
@@ -1949,19 +1997,6 @@
   for k m n :: int
   by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
 
-lemma coprime_crossproduct_nat:
-  fixes a b c d :: nat
-  assumes "coprime a d" and "coprime b c"
-  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
-  using assms coprime_crossproduct [of a d b c] by simp
-
-lemma coprime_crossproduct_int:
-  fixes a b c d :: int
-  assumes "coprime a d" and "coprime b c"
-  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
-  using assms coprime_crossproduct [of a d b c] by simp
-
-
 text \<open>\medskip Addition laws.\<close>
 
 (* TODO: add the other variations? *)
@@ -2064,53 +2099,33 @@
   for k l :: int
   by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
 
-
-subsection \<open>Coprimality\<close>
-
-lemma coprime_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
-  for a b :: nat
-  using coprime [of a b] by simp
-
-lemma coprime_Suc_0_nat: "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
-  for a b :: nat
-  using coprime_nat by simp
-
-lemma coprime_int: "coprime a b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
-  for a b :: int
-  using gcd_unique_int [of 1 a b]
-  apply clarsimp
-  apply (erule subst)
-  apply (rule iffI)
-   apply force
-  using abs_dvd_iff abs_ge_zero apply blast
-  done
-
-lemma pow_divides_eq_nat [simp]: "n > 0 \<Longrightarrow> a^n dvd b^n \<longleftrightarrow> a dvd b"
-  for a b n :: nat
-  using pow_divs_eq[of n] by simp
-
-lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
-  using coprime_plus_one[of n] by simp
-
-lemma coprime_minus_one_nat: "n \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
-  for n :: nat
-  using coprime_Suc_nat [of "n - 1"] gcd.commute [of "n - 1" n] by auto
-
-lemma coprime_common_divisor_nat: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
-  for a b :: nat
-  by (metis gcd_greatest_iff nat_dvd_1_iff_1)
-
-lemma coprime_common_divisor_int: "coprime a b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> \<bar>x\<bar> = 1"
-  for a b :: int
-  using gcd_greatest_iff [of x a b] by auto
-
-lemma invertible_coprime_nat: "x * y mod m = 1 \<Longrightarrow> coprime x m"
-  for m x y :: nat
-  by (metis coprime_lmult gcd_1_nat gcd.commute gcd_red_nat)
-
-lemma invertible_coprime_int: "x * y mod m = 1 \<Longrightarrow> coprime x m"
-  for m x y :: int
-  by (metis coprime_lmult gcd_1_int gcd.commute gcd_red_int)
+lemma coprime_Suc_left_nat [simp]:
+  "coprime (Suc n) n"
+  using coprime_add_one_left [of n] by simp
+
+lemma coprime_Suc_right_nat [simp]:
+  "coprime n (Suc n)"
+  using coprime_Suc_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_diff_one_left_nat [simp]:
+  "coprime (n - 1) n" if "n > 0" for n :: nat
+  using that coprime_Suc_right_nat [of "n - 1"] by simp
+
+lemma coprime_diff_one_right_nat [simp]:
+  "coprime n (n - 1)" if "n > 0" for n :: nat
+  using that coprime_diff_one_left_nat [of n] by (simp add: ac_simps)
+
+lemma coprime_crossproduct_nat:
+  fixes a b c d :: nat
+  assumes "coprime a d" and "coprime b c"
+  shows "a * c = b * d \<longleftrightarrow> a = b \<and> c = d"
+  using assms coprime_crossproduct [of a d b c] by simp
+
+lemma coprime_crossproduct_int:
+  fixes a b c d :: int
+  assumes "coprime a d" and "coprime b c"
+  shows "\<bar>a\<bar> * \<bar>c\<bar> = \<bar>b\<bar> * \<bar>d\<bar> \<longleftrightarrow> \<bar>a\<bar> = \<bar>b\<bar> \<and> \<bar>c\<bar> = \<bar>d\<bar>"
+  using assms coprime_crossproduct [of a d b c] by simp
 
 
 subsection \<open>Bezout's theorem\<close>
@@ -2742,14 +2757,6 @@
   for i m n :: int
   by (fact dvd_lcmI2)
 
-lemma coprime_exp2_nat [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
-  for a b :: nat
-  by (fact coprime_exp2)
-
-lemma coprime_exp2_int [intro]: "coprime a b \<Longrightarrow> coprime (a^n) (b^m)"
-  for a b :: int
-  by (fact coprime_exp2)
-
 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
 lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Isar_Examples/Fibonacci.thy
--- a/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Isar_Examples/Fibonacci.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -21,10 +21,6 @@
 text_raw \<open>\<^footnote>\<open>Isar version by Gertrud Bauer. Original tactic script by Larry
   Paulson. A few proofs of laws taken from @{cite "Concrete-Math"}.\<close>\<close>
 
-
-declare One_nat_def [simp]
-
-
 subsection \<open>Fibonacci numbers\<close>
 
 fun fib :: "nat \<Rightarrow> nat"
@@ -65,12 +61,13 @@
   finally show "?P (n + 2)" .
 qed
 
-lemma gcd_fib_Suc_eq_1: "gcd (fib n) (fib (n + 1)) = 1"
+lemma coprime_fib_Suc: "coprime (fib n) (fib (n + 1))"
   (is "?P n")
 proof (induct n rule: fib_induct)
   show "?P 0" by simp
   show "?P 1" by simp
   fix n
+  assume P: "coprime (fib (n + 1)) (fib (n + 1 + 1))"
   have "fib (n + 2 + 1) = fib (n + 1) + fib (n + 2)"
     by simp
   also have "\<dots> = fib (n + 2) + fib (n + 1)"
@@ -79,8 +76,10 @@
     by (rule gcd_add2)
   also have "\<dots> = gcd (fib (n + 1)) (fib (n + 1 + 1))"
     by (simp add: gcd.commute)
-  also assume "\<dots> = 1"
-  finally show "?P (n + 2)" .
+  also have "\<dots> = 1"
+    using P by simp
+  finally show "?P (n + 2)"
+    by (simp add: coprime_iff_gcd_eq_1)
 qed
 
 lemma gcd_mult_add: "(0::nat) < n \<Longrightarrow> gcd (n * k + m) n = gcd m n"
@@ -106,7 +105,8 @@
   also have "gcd \<dots> (fib (k + 1)) = gcd (fib k * fib n) (fib (k + 1))"
     by (simp add: gcd_mult_add)
   also have "\<dots> = gcd (fib n) (fib (k + 1))"
-    by (simp only: gcd_fib_Suc_eq_1 gcd_mult_cancel)
+    using coprime_fib_Suc [of k] gcd_mult_left_right_cancel [of "fib (k + 1)" "fib k" "fib n"]
+    by (simp add: ac_simps)
   also have "\<dots> = gcd (fib m) (fib n)"
     using Suc by (simp add: gcd.commute)
   finally show ?thesis .
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Library/Multiset.thy
--- a/src/HOL/Library/Multiset.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Library/Multiset.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -2155,6 +2155,42 @@
   "image_mset f (replicate_mset n a) = replicate_mset n (f a)"
   by (induct n) simp_all
 
+lemma replicate_mset_msubseteq_iff:
+  "replicate_mset m a \<subseteq># replicate_mset n b \<longleftrightarrow> m = 0 \<or> a = b \<and> m \<le> n"
+  by (cases m)
+    (auto simp add: insert_subset_eq_iff count_le_replicate_mset_subset_eq [symmetric])
+
+lemma msubseteq_replicate_msetE:
+  assumes "A \<subseteq># replicate_mset n a"
+  obtains m where "m \<le> n" and "A = replicate_mset m a"
+proof (cases "n = 0")
+  case True
+  with assms that show thesis
+    by simp
+next
+  case False
+  from assms have "set_mset A \<subseteq> set_mset (replicate_mset n a)"
+    by (rule set_mset_mono)
+  with False have "set_mset A \<subseteq> {a}"
+    by simp
+  then have "\<exists>m. A = replicate_mset m a"
+  proof (induction A)
+    case empty
+    then show ?case
+      by simp
+  next
+    case (add b A)
+    then obtain m where "A = replicate_mset m a"
+      by auto
+    with add.prems show ?case
+      by (auto intro: exI [of _ "Suc m"])
+  qed
+  then obtain m where A: "A = replicate_mset m a" ..
+  with assms have "m \<le> n"
+    by (auto simp add: replicate_mset_msubseteq_iff)
+  then show thesis using A ..
+qed
+
 
 subsection \<open>Big operators\<close>
 
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Map.thy
--- a/src/HOL/Map.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Map.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -782,6 +782,20 @@
   with * \<open>x = (k, v)\<close> show ?case by simp
 qed
 
+lemma eq_key_imp_eq_value:
+  "v1 = v2"
+  if "distinct (map fst xs)" "(k, v1) \<in> set xs" "(k, v2) \<in> set xs"
+proof -
+  from that have "inj_on fst (set xs)"
+    by (simp add: distinct_map)
+  moreover have "fst (k, v1) = fst (k, v2)"
+    by simp
+  ultimately have "(k, v1) = (k, v2)"
+    by (rule inj_onD) (fact that)+
+  then show ?thesis
+    by simp
+qed
+
 lemma map_of_inject_set:
   assumes distinct: "distinct (map fst xs)" "distinct (map fst ys)"
   shows "map_of xs = map_of ys \<longleftrightarrow> set xs = set ys" (is "?lhs \<longleftrightarrow> ?rhs")
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Nitpick.thy
--- a/src/HOL/Nitpick.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Nitpick.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -137,7 +137,7 @@
   by (simp only: lcm_nat_def Nitpick.nat_lcm_def gcd_eq_nitpick_gcd)
 
 definition Frac :: "int \<times> int \<Rightarrow> bool" where
-  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> gcd a b = 1"
+  "Frac \<equiv> \<lambda>(a, b). b > 0 \<and> coprime a b"
 
 consts
   Abs_Frac :: "int \<times> int \<Rightarrow> 'a"
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Cong.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -229,7 +229,8 @@
 lemma cong_mult_rcancel_int:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
   if "coprime k m" for a k m :: int
-  by (metis that cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
+  using that by (simp add: cong_altdef_int)
+    (metis coprime_commute coprime_dvd_mult_right_iff mult.commute right_diff_distrib') 
 
 lemma cong_mult_rcancel_nat:
   "[a * k = b * k] (mod m) \<longleftrightarrow> [a = b] (mod m)"
@@ -242,7 +243,7 @@
   also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar> * k"
     by (simp add: abs_mult nat_times_as_int)
   also have "\<dots> \<longleftrightarrow> m dvd nat \<bar>int a - int b\<bar>"
-    by (rule coprime_dvd_mult_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
+    by (rule coprime_dvd_mult_left_iff) (use \<open>coprime k m\<close> in \<open>simp add: ac_simps\<close>)
   also have "\<dots> \<longleftrightarrow> [a = b] (mod m)"
     by (simp add: cong_altdef_nat')
   finally show ?thesis .
@@ -320,11 +321,11 @@
 
 lemma cong_imp_coprime_nat: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   for a b :: nat
-  by (auto simp add: cong_gcd_eq_nat)
+  by (auto simp add: cong_gcd_eq_nat coprime_iff_gcd_eq_1)
 
 lemma cong_imp_coprime_int: "[a = b] (mod m) \<Longrightarrow> coprime a m \<Longrightarrow> coprime b m"
   for a b :: int
-  by (auto simp add: cong_gcd_eq_int)
+  by (auto simp add: cong_gcd_eq_int coprime_iff_gcd_eq_1)
 
 lemma cong_cong_mod_nat: "[a = b] (mod m) \<longleftrightarrow> [a mod m = b mod m] (mod m)"
   for a b :: nat
@@ -490,36 +491,24 @@
 qed
 
 lemma cong_solve_coprime_nat:
-  fixes a :: nat
-  assumes "coprime a n"
-  shows "\<exists>x. [a * x = 1] (mod n)"
-proof (cases "a = 0")
-  case True
-  with assms show ?thesis
-    by (simp add: cong_0_1_nat') 
-next
-  case False
-  with assms show ?thesis
-    by (metis cong_solve_nat)
-qed
+  "\<exists>x. [a * x = Suc 0] (mod n)" if "coprime a n"
+  using that cong_solve_nat [of a n] by (cases "a = 0") simp_all
 
-lemma cong_solve_coprime_int: "coprime (a::int) n \<Longrightarrow> \<exists>x. [a * x = 1] (mod n)"
-  apply (cases "a = 0")
-   apply auto
-   apply (cases "n \<ge> 0")
-    apply auto
-  apply (metis cong_solve_int)
-  done
+lemma cong_solve_coprime_int:
+  "\<exists>x. [a * x = 1] (mod n)" if "coprime a n" for a n x :: int
+  using that cong_solve_int [of a n] by (cases "a = 0")
+    (auto simp add: zabs_def split: if_splits)
 
 lemma coprime_iff_invertible_nat:
-  "m > 0 \<Longrightarrow> coprime a m = (\<exists>x. [a * x = Suc 0] (mod m))"
-  by (metis One_nat_def cong_gcd_eq_nat cong_solve_coprime_nat coprime_lmult gcd.commute gcd_Suc_0)
+  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = Suc 0] (mod m))"
+  by (auto intro: cong_solve_coprime_nat)
+    (use cong_imp_coprime_nat cong_sym coprime_Suc_0_left coprime_mult_left_iff in blast)
 
-lemma coprime_iff_invertible_int: "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
+lemma coprime_iff_invertible_int:
+  "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. [a * x = 1] (mod m))"
   for m :: int
-  apply (auto intro: cong_solve_coprime_int)
-  using cong_gcd_eq_int coprime_mul_eq' apply fastforce
-  done
+  by (auto intro: cong_solve_coprime_int)
+    (meson cong_imp_coprime_int cong_sym coprime_1_left coprime_mult_left_iff)
 
 lemma coprime_iff_invertible'_nat:
   "m > 0 \<Longrightarrow> coprime a m \<longleftrightarrow> (\<exists>x. 0 \<le> x \<and> x < m \<and> [a * x = Suc 0] (mod m))"
@@ -554,16 +543,16 @@
     and "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   using that apply (induct A rule: infinite_finite_induct)
     apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+  apply (metis coprime_cong_mult_nat prod_coprime_right)
   done
 
-lemma cong_cong_prod_coprime_int [rule_format]:
+lemma cong_cong_prod_coprime_int:
   "[x = y] (mod (\<Prod>i\<in>A. m i))" if
     "(\<forall>i\<in>A. [(x::int) = y] (mod m i))"
     "(\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j)))"
   using that apply (induct A rule: infinite_finite_induct)
-  apply auto
-  apply (metis coprime_cong_mult_int gcd.commute prod_coprime)
+    apply auto
+  apply (metis coprime_cong_mult_int prod_coprime_right)
   done
 
 lemma binary_chinese_remainder_aux_nat:
@@ -574,7 +563,7 @@
   from cong_solve_coprime_nat [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
     by auto
   from a have b: "coprime m2 m1"
-    by (subst gcd.commute)
+    by (simp add: ac_simps)
   from cong_solve_coprime_nat [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
@@ -593,7 +582,7 @@
   from cong_solve_coprime_int [OF a] obtain x1 where 1: "[m1 * x1 = 1] (mod m2)"
     by auto
   from a have b: "coprime m2 m1"
-    by (subst gcd.commute)
+    by (simp add: ac_simps)
   from cong_solve_coprime_int [OF b] obtain x2 where 2: "[m2 * x2 = 1] (mod m1)"
     by auto
   have "[m1 * x1 = 0] (mod m1)"
@@ -730,8 +719,8 @@
   fix i
   assume "i \<in> A"
   with cop have "coprime (\<Prod>j \<in> A - {i}. m j) (m i)"
-    by (intro prod_coprime) auto
-  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
+    by (intro prod_coprime_left) auto
+  then have "\<exists>x. [(\<Prod>j \<in> A - {i}. m j) * x = Suc 0] (mod m i)"
     by (elim cong_solve_coprime_nat)
   then obtain x where "[(\<Prod>j \<in> A - {i}. m j) * x = 1] (mod m i)"
     by auto
@@ -789,8 +778,8 @@
   if "\<forall>i\<in>A. (\<forall>j\<in>A. i \<noteq> j \<longrightarrow> coprime (m i) (m j))"
     and "\<forall>i\<in>A. [x = y] (mod m i)" for x y :: nat
   using that apply (induct A rule: infinite_finite_induct)
-  apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute prod_coprime)
+    apply auto
+  apply (metis coprime_cong_mult_nat prod_coprime_right)
   done
 
 lemma chinese_remainder_unique_nat:
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Euler_Criterion.thy
--- a/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Euler_Criterion.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -65,7 +65,7 @@
 proof -
   have "~ p dvd x" using assms zdvd_not_zless S1_def by auto
   hence co_xp: "coprime x p" using p_prime prime_imp_coprime_int[of p x] 
-    by (simp add: gcd.commute)
+    by (simp add: ac_simps)
   then obtain y' where y': "[x * y' = 1] (mod p)" using cong_solve_coprime_int by blast
   moreover define y where "y = y' * a mod p"
   ultimately have "[x * y = a] (mod p)" using mod_mult_right_eq[of x "y' * a" p]
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Fib.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -87,17 +87,34 @@
 
 lemma coprime_fib_Suc_nat: "coprime (fib n) (fib (Suc n))"
   apply (induct n rule: fib.induct)
-  apply auto
-  apply (metis gcd_add1 add.commute)
+    apply (simp_all add: coprime_iff_gcd_eq_1 algebra_simps)
+  apply (simp add: add.assoc [symmetric])
   done
 
-lemma gcd_fib_add: "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
-  apply (simp add: gcd.commute [of "fib m"])
-  apply (cases m)
-  apply (auto simp add: fib_add)
-  apply (metis gcd.commute mult.commute coprime_fib_Suc_nat
-    gcd_add_mult gcd_mult_cancel gcd.commute)
-  done
+lemma gcd_fib_add:
+  "gcd (fib m) (fib (n + m)) = gcd (fib m) (fib n)"
+proof (cases m)
+  case 0
+  then show ?thesis
+    by simp
+next
+  case (Suc q)
+  from coprime_fib_Suc_nat [of q]
+  have "coprime (fib (Suc q)) (fib q)"
+    by (simp add: ac_simps)
+  have "gcd (fib q) (fib (Suc q)) = Suc 0"
+    using coprime_fib_Suc_nat [of q] by simp
+  then have *: "gcd (fib n * fib q) (fib n * fib (Suc q)) = fib n"
+    by (simp add: gcd_mult_distrib_nat [symmetric])
+  moreover have "gcd (fib (Suc q)) (fib n * fib q + fib (Suc n) * fib (Suc q)) =
+    gcd (fib (Suc q)) (fib n * fib q)"
+    using gcd_add_mult [of "fib (Suc q)"] by (simp add: ac_simps)
+  moreover have "gcd (fib (Suc q)) (fib n * fib (Suc q)) = fib (Suc q)"
+    by simp
+  ultimately show ?thesis
+    using Suc \<open>coprime (fib (Suc q)) (fib q)\<close>
+    by (auto simp add: fib_add algebra_simps gcd_mult_right_right_cancel)
+qed
 
 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
   by (simp add: gcd_fib_add [symmetric, of _ "n-m"])
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Gauss.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -115,8 +115,9 @@
   proof -
     from p_a_relprime have "\<not> p dvd a"
       by (simp add: cong_altdef_int)
-    with p_prime have "coprime a (int p)"
-      by (subst gcd.commute, intro prime_imp_coprime) auto
+    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+    have "coprime a (int p)"
+      by (simp_all add: zdvd_int ac_simps)
     with a cong_mult_rcancel_int [of a "int p" x y] have "[x = y] (mod p)"
       by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -149,8 +150,9 @@
       using cong_def by blast
     from p_a_relprime have "\<not>p dvd a"
       by (simp add: cong_altdef_int)
-    with p_prime have "coprime a (int p)"
-      by (subst gcd.commute, intro prime_imp_coprime) auto
+    with p_prime prime_imp_coprime [of _ "nat \<bar>a\<bar>"]
+    have "coprime a (int p)"
+      by (simp_all add: zdvd_int ac_simps)  
     with a' cong_mult_rcancel_int [of a "int p" x y]
     have "[x = y] (mod p)" by simp
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
@@ -219,13 +221,16 @@
   by (auto simp add: D_def C_def B_def A_def)
 
 lemma all_A_relprime:
-  assumes "x \<in> A"
-  shows "gcd x p = 1"
-  using p_prime A_ncong_p [OF assms]
-  by (auto simp: cong_altdef_int gcd.commute[of _ "int p"] intro!: prime_imp_coprime)
-
-lemma A_prod_relprime: "gcd (prod id A) p = 1"
-  by (metis id_def all_A_relprime prod_coprime)
+  "coprime x p" if "x \<in> A"
+proof -
+  from A_ncong_p [OF that] have "\<not> int p dvd x"
+    by (simp add: cong_altdef_int)
+  with p_prime show ?thesis
+    by (metis (no_types) coprime_commute prime_imp_coprime prime_nat_int_transfer)
+qed
+  
+lemma A_prod_relprime: "coprime (prod id A) p"
+  by (auto intro: prod_coprime_left all_A_relprime)
 
 
 subsection \<open>Relationships Between Gauss Sets\<close>
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Pocklington.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -11,18 +11,11 @@
 subsection \<open>Lemmas about previously defined terms\<close>
 
 lemma prime_nat_iff'': "prime (p::nat) \<longleftrightarrow> p \<noteq> 0 \<and> p \<noteq> 1 \<and> (\<forall>m. 0 < m \<and> m < p \<longrightarrow> coprime p m)"
-  unfolding prime_nat_iff
-proof safe
-  fix m
-  assume p: "p > 0" "p \<noteq> 1"
-    and m: "m dvd p" "m \<noteq> p"
-    and *: "\<forall>m. m > 0 \<and> m < p \<longrightarrow> coprime p m"
-  from p m have "m \<noteq> 0" by (intro notI) auto
-  moreover from p m have "m < p" by (auto dest: dvd_imp_le)
-  ultimately have "coprime p m"
-    using * by blast
-  with m show "m = 1" by simp
-qed (auto simp: prime_nat_iff simp del: One_nat_def intro!: prime_imp_coprime dest: dvd_imp_le)
+  apply (auto simp add: prime_nat_iff)
+   apply (rule coprimeI)
+   apply (auto dest: nat_dvd_not_less simp add: ac_simps)
+  apply (metis One_nat_def dvd_1_iff_1 dvd_pos_nat gcd_nat.order_iff is_unit_gcd linorder_neqE_nat nat_dvd_not_less)
+  done
 
 lemma finite_number_segment: "card { m. 0 < m \<and> m < n } = n - 1"
 proof -
@@ -46,7 +39,7 @@
   from bezout_add_strong_nat [OF this]
   obtain d x y where dxy: "d dvd a" "d dvd n" "a * x = n * y + d" by blast
   from dxy(1,2) have d1: "d = 1"
-    by (metis assms coprime_nat)
+    using assms coprime_common_divisor [of a n d] by simp
   with dxy(3) have "a * x * b = (n * y + 1) * b"
     by simp
   then have "a * (x * b) = n * (y * b) + b"
@@ -94,9 +87,9 @@
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = a] (mod p)"
 proof -
   from pa have ap: "coprime a p"
-    by (metis gcd.commute)
-  have px: "coprime x p"
-    by (metis gcd.commute p prime_nat_iff'' x0 xp)
+    by (simp add: ac_simps)
+  from x0 xp p have px: "coprime x p"
+    by (auto simp add: prime_nat_iff'' ac_simps)
   obtain y where y: "y < p" "[x * y = a] (mod p)" "\<forall>z. z < p \<and> [x * z = a] (mod p) \<longrightarrow> z = y"
     by (metis cong_solve_unique neq0_conv p prime_gt_0_nat px)
   have "y \<noteq> 0"
@@ -104,8 +97,8 @@
     assume "y = 0"
     with y(2) have "p dvd a"
       using cong_dvd_iff by auto
-    then show False
-      by (metis gcd_nat.absorb1 not_prime_1 p pa)
+    with not_prime_1 p pa show False
+      by (auto simp add: gcd_nat.order_iff)
   qed
   with y show ?thesis
     by blast
@@ -128,9 +121,9 @@
   obtain x where x: "x < a * b" "[x = m] (mod a)" "[x = n] (mod b)" "\<forall>y. ?P y \<longrightarrow> y = x"
     by blast
   from ma nb x have "coprime x a" "coprime x b"
-    by (metis cong_gcd_eq_nat)+
+    using cong_imp_coprime_nat cong_sym by blast+
   then have "coprime x (a*b)"
-    by (metis coprime_mul_eq)
+    by simp
   with x show ?thesis
     by blast
 qed
@@ -164,7 +157,8 @@
       from dvd_mod_iff[OF d(2), of "a^m"] dam am1 show ?thesis
         by simp
     qed
-    then show ?thesis by blast
+    then show ?thesis
+      by (auto intro: coprimeI)
   qed
 qed
 
@@ -216,8 +210,8 @@
   from mod_less_divisor[of n 1] n01 have onen: "1 mod n = 1"
     by simp
   from lucas_coprime_lemma[OF n01(3) an1] cong_imp_coprime_nat an1
-  have an: "coprime a n" "coprime (a^(n - 1)) n"
-    by (auto simp add: coprime_exp gcd.commute)
+  have an: "coprime a n" "coprime (a ^ (n - 1)) n"
+    using \<open>n \<ge> 2\<close> by simp_all
   have False if H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
   proof -
     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
@@ -229,7 +223,7 @@
       let ?y = "a^ ((n - 1) div m * m)"
       note mdeq = div_mult_mod_eq[of "(n - 1)" m]
       have yn: "coprime ?y n"
-        by (metis an(1) coprime_exp gcd.commute)
+        using an(1) by (cases "(n - Suc 0) div m * m = 0") auto
       have "?y mod n = (a^m)^((n - 1) div m) mod n"
         by (simp add: algebra_simps power_mult)
       also have "\<dots> = (a^m mod n)^((n - 1) div m) mod n"
@@ -359,9 +353,11 @@
     next
       case (Suc d')
       then have d0: "d \<noteq> 0" by simp
-      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
+      from prem obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1"
+        by (auto elim: not_coprimeE) 
       from \<open>?lhs\<close> obtain q1 q2 where q12: "a ^ d + n * q1 = 1 + n * q2"
-        by (metis prem d0 gcd.commute lucas_coprime_lemma)
+        using prem d0 lucas_coprime_lemma
+        by (auto elim: not_coprimeE simp add: ac_simps)
       then have "a ^ d + n * q1 - n * q2 = 1" by simp
       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2 Suc p have "p dvd 1"
         by metis
@@ -398,8 +394,10 @@
   qed
 qed
 
-lemma order_divides_totient: "ord n a dvd totient n" if "coprime n a"
-  by (metis euler_theorem gcd.commute ord_divides that)
+lemma order_divides_totient:
+  "ord n a dvd totient n" if "coprime n a"
+  using that euler_theorem [of a n]
+  by (simp add: ord_divides [symmetric] ac_simps)
 
 lemma order_divides_expdiff:
   fixes n::nat and a::nat assumes na: "coprime n a"
@@ -412,11 +410,11 @@
     from na ed have "\<exists>c. d = e + c" by presburger
     then obtain c where c: "d = e + c" ..
     from na have an: "coprime a n"
-      by (metis gcd.commute)
-    have aen: "coprime (a^e) n"
-      by (metis coprime_exp gcd.commute na)
-    have acn: "coprime (a^c) n"
-      by (metis coprime_exp gcd.commute na)
+      by (simp add: ac_simps)
+    then have aen: "coprime (a ^ e) n"
+      by (cases "e > 0") simp_all
+    from an have acn: "coprime (a ^ c) n"
+      by (cases "c > 0") simp_all
     from c have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
       by simp
     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
@@ -620,8 +618,9 @@
       by (metis cong_to_1_nat exps)
     from nqr s s' have "(n - 1) div P = ord p (a^r) * t*r"
       using P0 by simp
-    with caP have "coprime (a^(ord p (a^r) * t*r) - 1) n" by simp
-    with p01 pn pd0 coprime_common_divisor_nat show False
+    with caP have "coprime (a ^ (ord p (a ^ r) * t * r) - 1) n"
+      by simp
+    with p01 pn pd0 coprime_common_divisor [of _ n p] show False
       by auto
   qed
   with d have o: "ord p (a^r) = q" by simp
@@ -632,12 +631,14 @@
     assume d: "d dvd p" "d dvd a" "d \<noteq> 1"
     from pp[unfolded prime_nat_iff] d have dp: "d = p" by blast
     from n have "n \<noteq> 0" by simp
-    then have False using d dp pn
-      by auto (metis One_nat_def Suc_pred an dvd_1_iff_1 gcd_greatest_iff lucas_coprime_lemma)
+    then have False using d dp pn an
+      by auto (metis One_nat_def Suc_lessI
+        \<open>1 < p \<and> (\<forall>m. m dvd p \<longrightarrow> m = 1 \<or> m = p)\<close> \<open>a ^ (q * r) = p * l * k + 1\<close> add_diff_cancel_left' dvd_diff_nat dvd_power dvd_triv_left gcd_nat.trans nat_dvd_not_less nqr zero_less_diff zero_less_one) 
   }
-  then have cpa: "coprime p a" by auto
-  have arp: "coprime (a^r) p"
-    by (metis coprime_exp cpa gcd.commute)
+  then have cpa: "coprime p a"
+    by (auto intro: coprimeI)
+  then have arp: "coprime (a ^ r) p"
+    by (cases "r > 0") (simp_all add: ac_simps)
   from euler_theorem [OF arp, simplified ord_divides] o totient_eq have "q dvd (p - 1)"
     by simp
   then obtain d where d:"p - 1 = q * d"
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Residues.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -106,13 +106,9 @@
 
 lemma res_units_eq: "Units R = {x. 0 < x \<and> x < m \<and> coprime x m}"
   using m_gt_one
-  unfolding Units_def R_def residue_ring_def
-  apply auto
-    apply (subgoal_tac "x \<noteq> 0")
-     apply auto
-   apply (metis invertible_coprime_int)
+  apply (auto simp add: Units_def R_def residue_ring_def ac_simps invertible_coprime intro: ccontr)
   apply (subst (asm) coprime_iff_invertible'_int)
-   apply (auto simp add: cong_def mult.commute)
+   apply (auto simp add: cong_def)
   done
 
 lemma res_neg_eq: "\<ominus> x = (- x) mod m"
@@ -220,6 +216,22 @@
 context residues_prime
 begin
 
+lemma p_coprime_left:
+  "coprime p a \<longleftrightarrow> \<not> p dvd a"
+  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right:
+  "coprime a p  \<longleftrightarrow> \<not> p dvd a"
+  using p_coprime_left [of a] by (simp add: ac_simps)
+
+lemma p_coprime_left_int:
+  "coprime (int p) a \<longleftrightarrow> \<not> int p dvd a"
+  using p_prime by (auto intro: prime_imp_coprime dest: coprime_common_divisor)
+
+lemma p_coprime_right_int:
+  "coprime a (int p) \<longleftrightarrow> \<not> int p dvd a"
+  using p_coprime_left_int [of a] by (simp add: ac_simps)
+
 lemma is_field: "field R"
 proof -
   have "0 < x \<Longrightarrow> x < int p \<Longrightarrow> coprime (int p) x" for x
@@ -231,9 +243,7 @@
 
 lemma res_prime_units_eq: "Units R = {1..p - 1}"
   apply (subst res_units_eq)
-  apply auto
-  apply (subst gcd.commute)
-  apply (auto simp add: p_prime prime_imp_coprime_int zdvd_not_zless)
+  apply (auto simp add: p_coprime_right_int zdvd_not_zless)
   done
 
 end
@@ -246,26 +256,27 @@
 
 subsection \<open>Euler's theorem\<close>
 
-lemma (in residues) totient_eq: "totient (nat m) = card (Units R)"
+lemma (in residues) totatives_eq:
+  "totatives (nat m) = nat ` Units R"
 proof -
+  from m_gt_one have "\<bar>m\<bar> > 1"
+    by simp
+  then have "totatives (nat \<bar>m\<bar>) = nat ` abs ` Units R"
+    by (auto simp add: totatives_def res_units_eq image_iff le_less)
+      (use m_gt_one zless_nat_eq_int_zless in force)
+  moreover have "\<bar>m\<bar> = m" "abs ` Units R = Units R"
+    using m_gt_one by (auto simp add: res_units_eq image_iff)
+  ultimately show ?thesis
+    by simp
+qed
+
+lemma (in residues) totient_eq:
+  "totient (nat m) = card (Units R)"
+proof  -
   have *: "inj_on nat (Units R)"
     by (rule inj_onI) (auto simp add: res_units_eq)
-  define m' where "m' = nat m"
-  from m_gt_one have "m = int m'" "m' > 1"
-    by (simp_all add: m'_def)
-  then have "x \<in> Units R \<longleftrightarrow> x \<in> int ` totatives m'" for x
-    unfolding res_units_eq
-    by (cases x; cases "x = m") (auto simp: totatives_def gcd_int_def)
-  then have "Units R = int ` totatives m'"
-    by blast
-  then have "totatives m' = nat ` Units R"
-    by (simp add: image_image)
-  then have "card (totatives (nat m)) = card (nat ` Units R)"
-    by (simp add: m'_def)
-  also have "\<dots> = card (Units R)"
-    using * card_image [of nat "Units R"] by auto
-  finally show ?thesis
-    by (simp add: totient_def)
+  then show ?thesis
+    by (simp add: totient_def totatives_eq card_image)
 qed
 
 lemma (in residues_prime) totient_eq: "totient p = p - 1"
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Number_Theory/Totient.thy
--- a/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Number_Theory/Totient.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -15,7 +15,7 @@
   
 definition totatives :: "nat \<Rightarrow> nat set" where
   "totatives n = {k \<in> {0<..n}. coprime k n}"
-  
+
 lemma in_totatives_iff: "k \<in> totatives n \<longleftrightarrow> k > 0 \<and> k \<le> n \<and> coprime k n"
   by (simp add: totatives_def)
   
@@ -60,7 +60,7 @@
 lemma minus_one_in_totatives:
   assumes "n \<ge> 2"
   shows "n - 1 \<in> totatives n"
-  using assms coprime_minus_one_nat [of n] by (simp add: in_totatives_iff)
+  using assms coprime_diff_one_left_nat [of n] by (simp add: in_totatives_iff)
 
 lemma totatives_prime_power_Suc:
   assumes "prime p"
@@ -72,7 +72,8 @@
   fix k assume k: "k \<in> {0<..p^Suc n}" "k \<notin> (\<lambda>m. p * m) ` {0<..p^n}"
   from k have "\<not>(p dvd k)" by (auto elim!: dvdE)
   hence "coprime k (p ^ Suc n)"
-    using prime_imp_coprime[OF assms, of k] by (intro coprime_exp) (simp_all add: gcd.commute)
+    using prime_imp_coprime [OF assms, of k]
+    by (cases "n > 0") (auto simp add: ac_simps)
   with k show "k \<in> totatives (p ^ Suc n)" by (simp add: totatives_def)
 qed (auto simp: totatives_def)
 
@@ -101,14 +102,15 @@
   proof safe
     fix x assume "x \<in> totatives (m1 * m2)"
     with assms show "x mod m1 \<in> totatives m1" "x mod m2 \<in> totatives m2"
-      by (auto simp: totatives_def coprime_mul_eq not_le simp del: One_nat_def intro!: Nat.gr0I)
+      using coprime_common_divisor [of x m1 m1] coprime_common_divisor [of x m2 m2]
+      by (auto simp add: in_totatives_iff mod_greater_zero_iff_not_dvd)
   next
     fix a b assume ab: "a \<in> totatives m1" "b \<in> totatives m2"
     with assms have ab': "a < m1" "b < m2" by (auto simp: totatives_less)
     with binary_chinese_remainder_unique_nat[OF assms(3), of a b] obtain x
       where x: "x < m1 * m2" "x mod m1 = a" "x mod m2 = b" by (auto simp: cong_def)
     from x ab assms(3) have "x \<in> totatives (m1 * m2)"
-      by (auto simp: totatives_def coprime_mul_eq simp del: One_nat_def intro!: Nat.gr0I)
+      by (auto intro: ccontr simp add: in_totatives_iff)
     with x show "(a, b) \<in> (\<lambda>x. (x mod m1, x mod m2)) ` totatives (m1*m2)" by blast
   qed
 qed
@@ -125,21 +127,18 @@
   show "(\<lambda>k. k * d) ` totatives (n div d) = {k\<in>{0<..n}. gcd k n = d}"
   proof (intro equalityI subsetI, goal_cases)
     case (1 k)
-    thus ?case using assms
-      by (auto elim!: dvdE simp: inj_on_def totatives_def mult.commute[of d]
-                                 gcd_mult_right gcd.commute)
+    then show ?case using assms
+      by (auto elim: dvdE simp add: in_totatives_iff ac_simps gcd_mult_right)
   next
     case (2 k)
     hence "d dvd k" by auto
     then obtain l where k: "k = l * d" by (elim dvdE) auto
-    from 2 and assms show ?case unfolding k
-      by (intro imageI) (auto simp: totatives_def gcd.commute mult.commute[of d] 
-                                    gcd_mult_right elim!: dvdE)
+    from 2 assms show ?case
+      using gcd_mult_right [of _ d l]
+      by (auto intro: gcd_eq_1_imp_coprime elim!: dvdE simp add: k image_iff in_totatives_iff ac_simps)
   qed
 qed
 
-
-
 definition totient :: "nat \<Rightarrow> nat" where
   "totient n = card (totatives n)"
   
@@ -272,7 +271,8 @@
   proof -
     from that have nz: "x \<noteq> 0" by (auto intro!: Nat.gr0I)
     from that and p have le: "x \<le> p" by (intro dvd_imp_le) auto
-    from that and nz have "\<not>coprime x p" by auto
+    from that and nz have "\<not>coprime x p"
+      by (auto elim: dvdE)
     hence "x \<notin> totatives p" by (simp add: totatives_def)
     also note *
     finally show False using that and le by auto
@@ -299,7 +299,8 @@
   by simp_all
     
 lemma totient_6 [simp]: "totient 6 = 2"
-  using totient_mult_coprime[of 2 3] by (simp add: gcd_non_0_nat)    
+  using totient_mult_coprime [of 2 3] coprime_add_one_right [of 2]
+  by simp
 
 lemma totient_even:
   assumes "n > 2"
@@ -314,11 +315,14 @@
   have "p ^ k dvd n" unfolding k_def by (simp add: multiplicity_dvd)
   then obtain m where m: "n = p ^ k * m" by (elim dvdE)
   with assms have m_pos: "m > 0" by (auto intro!: Nat.gr0I)
-  from k_def m_pos p have "\<not>p dvd m"
+  from k_def m_pos p have "\<not> p dvd m"
     by (subst (asm) m) (auto intro!: Nat.gr0I simp: prime_elem_multiplicity_mult_distrib 
                           prime_elem_multiplicity_eq_zero_iff)
-  hence "coprime (p ^ k) m" by (intro coprime_exp_left prime_imp_coprime[OF p(1)])
-  thus ?thesis using p k_pos \<open>odd p\<close> 
+  with \<open>prime p\<close> have "coprime p m"
+    by (rule prime_imp_coprime)
+  with \<open>k > 0\<close> have "coprime (p ^ k) m"
+    by simp
+  then show ?thesis using p k_pos \<open>odd p\<close> 
     by (auto simp add: m totient_mult_coprime totient_prime_power)
 next
   case False
@@ -341,7 +345,7 @@
 proof (induction A rule: infinite_finite_induct)
   case (insert x A)
   have *: "coprime (prod f A) (f x)"
-  proof (rule prod_coprime)
+  proof (rule prod_coprime_left)
     fix y
     assume "y \<in> A"
     with \<open>x \<notin> A\<close> have "y \<noteq> x"
@@ -388,10 +392,12 @@
   proof (rule totient_prod_coprime)
     show "pairwise coprime ((\<lambda>p. p ^ multiplicity p n) ` prime_factors n)"
     proof (rule pairwiseI, clarify)
-      fix p q assume "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
+      fix p q assume *: "p \<in># prime_factorization n" "q \<in># prime_factorization n" 
                      "p ^ multiplicity p n \<noteq> q ^ multiplicity q n"
-      thus "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
-        by (intro coprime_exp2 primes_coprime[of p q]) auto
+      then have "multiplicity p n > 0" "multiplicity q n > 0"
+        by (simp_all add: prime_factors_multiplicity)
+      with * primes_coprime [of p q] show "coprime (p ^ multiplicity p n) (q ^ multiplicity q n)"
+        by auto
     qed
   next
     show "inj_on (\<lambda>p. p ^ multiplicity p n) (prime_factors n)"
@@ -475,20 +481,22 @@
   by (subst totient_gcd [symmetric]) simp
 
 lemma of_nat_eq_1_iff: "of_nat x = (1 :: 'a :: {semiring_1, semiring_char_0}) \<longleftrightarrow> x = 1"
-  using of_nat_eq_iff[of x 1] by (simp del: of_nat_eq_iff)
+  by (fact of_nat_eq_1_iff)
 
 (* TODO Move *)
-lemma gcd_2_odd:
+lemma odd_imp_coprime_nat:
   assumes "odd (n::nat)"
-  shows   "gcd n 2 = 1"
+  shows   "coprime n 2"
 proof -
   from assms obtain k where n: "n = Suc (2 * k)" by (auto elim!: oddE)
-  have "coprime (Suc (2 * k)) (2 * k)" by (rule coprime_Suc_nat)
-  thus ?thesis using n by (subst (asm) coprime_mul_eq) simp_all
+  have "coprime (Suc (2 * k)) (2 * k)"
+    by (fact coprime_Suc_left_nat)
+  then show ?thesis using n
+    by simp
 qed
 
 lemma totient_double: "totient (2 * n) = (if even n then 2 * totient n else totient n)"
-  by (subst totient_mult) (auto simp: gcd.commute[of 2] gcd_2_odd)
+  by (simp add: totient_mult ac_simps odd_imp_coprime_nat)
 
 lemma totient_power_Suc: "totient (n ^ Suc m) = n ^ m * totient n"
 proof (induction m arbitrary: n)
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Parity.thy
--- a/src/HOL/Parity.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Parity.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -318,6 +318,38 @@
   using mult_div_mod_eq [of 2 a]
   by (simp add: even_iff_mod_2_eq_zero)
 
+lemma coprime_left_2_iff_odd [simp]:
+  "coprime 2 a \<longleftrightarrow> odd a"
+proof
+  assume "odd a"
+  show "coprime 2 a"
+  proof (rule coprimeI)
+    fix b
+    assume "b dvd 2" "b dvd a"
+    then have "b dvd a mod 2"
+      by (auto intro: dvd_mod)
+    with \<open>odd a\<close> show "is_unit b"
+      by (simp add: mod_2_eq_odd)
+  qed
+next
+  assume "coprime 2 a"
+  show "odd a"
+  proof (rule notI)
+    assume "even a"
+    then obtain b where "a = 2 * b" ..
+    with \<open>coprime 2 a\<close> have "coprime 2 (2 * b)"
+      by simp
+    moreover have "\<not> coprime 2 (2 * b)"
+      by (rule not_coprimeI [of 2]) simp_all
+    ultimately show False
+      by blast
+  qed
+qed
+
+lemma coprime_right_2_iff_odd [simp]:
+  "coprime a 2 \<longleftrightarrow> odd a"
+  using coprime_left_2_iff_odd [of a] by (simp add: ac_simps)
+
 end
 
 class ring_parity = ring + semiring_parity
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Rat.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -999,7 +999,7 @@
 proof (cases p)
   case (Fract a b)
   then show ?thesis
-    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
+    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract ac_simps)
 qed
 
 lemma rat_divide_code [code abstract]:
@@ -1008,9 +1008,10 @@
      in normalize (a * d, c * b))"
   by (cases p, cases q) (simp add: quotient_of_Fract)
 
-lemma rat_abs_code [code abstract]: "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
+lemma rat_abs_code [code abstract]:
+  "quotient_of \<bar>p\<bar> = (let (a, b) = quotient_of p in (\<bar>a\<bar>, b))"
   by (cases p) (simp add: quotient_of_Fract)
-
+  
 lemma rat_sgn_code [code abstract]: "quotient_of (sgn p) = (sgn (fst (quotient_of p)), 1)"
 proof (cases p)
   case (Fract a b)
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Real.thy
--- a/src/HOL/Real.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Real.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -1245,7 +1245,7 @@
 
 lemma Rats_abs_nat_div_natE:
   assumes "x \<in> \<rat>"
-  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "gcd m n = 1"
+  obtains m n :: nat where "n \<noteq> 0" and "\<bar>x\<bar> = real m / real n" and "coprime m n"
 proof -
   from \<open>x \<in> \<rat>\<close> obtain i :: int and n :: nat where "n \<noteq> 0" and "x = real_of_int i / real n"
     by (auto simp add: Rats_eq_int_div_nat)
@@ -1281,6 +1281,8 @@
     with gcd_k gcd_l have "?gcd * ?gcd' = ?gcd" by simp
     with gcd show ?thesis by auto
   qed
+  then have "coprime ?k ?l"
+    by (simp only: coprime_iff_gcd_eq_1)
   ultimately show ?thesis ..
 qed
 
@@ -1415,8 +1417,6 @@
   for m :: nat
   by (metis not_le real_of_nat_less_numeral_iff)
 
-declare of_int_floor_le [simp]  (* FIXME duplicate!? *)
-
 lemma of_int_floor_cancel [simp]: "of_int \<lfloor>x\<rfloor> = x \<longleftrightarrow> (\<exists>n::int. x = of_int n)"
   by (metis floor_of_int)
 
@@ -1424,7 +1424,7 @@
   by linarith
 
 lemma floor_eq2: "real_of_int n \<le> x \<Longrightarrow> x < real_of_int n + 1 \<Longrightarrow> \<lfloor>x\<rfloor> = n"
-  by linarith
+  by (fact floor_unique)
 
 lemma floor_eq3: "real n < x \<Longrightarrow> x < real (Suc n) \<Longrightarrow> nat \<lfloor>x\<rfloor> = n"
   by linarith
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Rings.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -1161,6 +1161,108 @@
   "is_unit c \<Longrightarrow> b dvd a \<Longrightarrow> a div (b * c) = a div b div c"
   by (rule dvd_div_mult2_eq) (simp_all add: mult_unit_dvd_iff)
 
+
+text \<open>Coprimality\<close>
+
+definition coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  where "coprime a b \<longleftrightarrow> (\<forall>c. c dvd a \<longrightarrow> c dvd b \<longrightarrow> is_unit c)"
+
+lemma coprimeI:
+  assumes "\<And>c. c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> is_unit c"
+  shows "coprime a b"
+  using assms by (auto simp: coprime_def)
+
+lemma not_coprimeI:
+  assumes "c dvd a" and "c dvd b" and "\<not> is_unit c"
+  shows "\<not> coprime a b"
+  using assms by (auto simp: coprime_def)
+
+lemma coprime_common_divisor:
+  "is_unit c" if "coprime a b" and "c dvd a" and "c dvd b"
+  using that by (auto simp: coprime_def)
+
+lemma not_coprimeE:
+  assumes "\<not> coprime a b"
+  obtains c where "c dvd a" and "c dvd b" and "\<not> is_unit c"
+  using assms by (auto simp: coprime_def)
+
+lemma coprime_imp_coprime:
+  "coprime a b" if "coprime c d"
+    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd c"
+    and "\<And>e. \<not> is_unit e \<Longrightarrow> e dvd a \<Longrightarrow> e dvd b \<Longrightarrow> e dvd d"
+proof (rule coprimeI)
+  fix e
+  assume "e dvd a" and "e dvd b"
+  with that have "e dvd c" and "e dvd d"
+    by (auto intro: dvd_trans)
+  with \<open>coprime c d\<close> show "is_unit e"
+    by (rule coprime_common_divisor)
+qed
+
+lemma coprime_divisors:
+  "coprime a b" if "a dvd c" "b dvd d" and "coprime c d"
+using \<open>coprime c d\<close> proof (rule coprime_imp_coprime)
+  fix e
+  assume "e dvd a" then show "e dvd c"
+    using \<open>a dvd c\<close> by (rule dvd_trans)
+  assume "e dvd b" then show "e dvd d"
+    using \<open>b dvd d\<close> by (rule dvd_trans)
+qed
+
+lemma coprime_self [simp]:
+  "coprime a a \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  then show ?Q
+    by (rule coprime_common_divisor) simp_all
+next
+  assume ?Q
+  show ?P
+    by (rule coprimeI) (erule dvd_unit_imp_unit, rule \<open>?Q\<close>)
+qed
+
+lemma coprime_commute [ac_simps]:
+  "coprime b a \<longleftrightarrow> coprime a b"
+  unfolding coprime_def by auto
+
+lemma is_unit_left_imp_coprime:
+  "coprime a b" if "is_unit a"
+proof (rule coprimeI)
+  fix c
+  assume "c dvd a"
+  with that show "is_unit c"
+    by (auto intro: dvd_unit_imp_unit)
+qed
+
+lemma is_unit_right_imp_coprime:
+  "coprime a b" if "is_unit b"
+  using that is_unit_left_imp_coprime [of b a] by (simp add: ac_simps)
+
+lemma coprime_1_left [simp]:
+  "coprime 1 a"
+  by (rule coprimeI)
+
+lemma coprime_1_right [simp]:
+  "coprime a 1"
+  by (rule coprimeI)
+
+lemma coprime_0_left_iff [simp]:
+  "coprime 0 a \<longleftrightarrow> is_unit a"
+  by (auto intro: coprimeI dvd_unit_imp_unit coprime_common_divisor [of 0 a a])
+
+lemma coprime_0_right_iff [simp]:
+  "coprime a 0 \<longleftrightarrow> is_unit a"
+  using coprime_0_left_iff [of a] by (simp add: ac_simps)
+
+lemma coprime_mult_self_left_iff [simp]:
+  "coprime (c * a) (c * b) \<longleftrightarrow> is_unit c \<and> coprime a b"
+  by (auto intro: coprime_common_divisor)
+    (rule coprimeI, auto intro: coprime_common_divisor simp add: dvd_mult_unit_iff')+
+
+lemma coprime_mult_self_right_iff [simp]:
+  "coprime (a * c) (b * c) \<longleftrightarrow> is_unit c \<and> coprime a b"
+  using coprime_mult_self_left_iff [of c a b] by (simp add: ac_simps)
+
 end
 
 class unit_factor =
@@ -1430,6 +1532,14 @@
   shows "is_unit a \<longleftrightarrow> a = 1"
   using assms by (cases "a = 0") (auto dest: is_unit_normalize)
 
+lemma coprime_normalize_left_iff [simp]:
+  "coprime (normalize a) b \<longleftrightarrow> coprime a b"
+  by (rule; rule coprimeI) (auto intro: coprime_common_divisor)
+
+lemma coprime_normalize_right_iff [simp]:
+  "coprime a (normalize b) \<longleftrightarrow> coprime a b"
+  using coprime_normalize_left_iff [of b a] by (simp add: ac_simps)
+
 text \<open>
   We avoid an explicit definition of associated elements but prefer explicit
   normalisation instead. In theory we could define an abbreviation like @{prop
@@ -2435,8 +2545,8 @@
 subclass ordered_ring_abs
   by standard (auto simp: abs_if not_less mult_less_0_iff)
 
-lemma abs_mult_self [simp]: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
-  by (simp add: abs_if)
+lemma abs_mult_self: "\<bar>a\<bar> * \<bar>a\<bar> = a * a"
+  by (fact abs_mult_self_eq)
 
 lemma abs_mult_less:
   assumes ac: "\<bar>a\<bar> < c"
diff -r 1e29e2666a15 -r e7e54a0b9197 src/HOL/Set.thy
--- a/src/HOL/Set.thy	Sat Nov 11 18:33:35 2017 +0000
+++ b/src/HOL/Set.thy	Sat Nov 11 18:41:08 2017 +0000
@@ -1874,6 +1874,11 @@
 lemma pairwise_mono: "\<lbrakk>pairwise P A; \<And>x y. P x y \<Longrightarrow> Q x y\<rbrakk> \<Longrightarrow> pairwise Q A"
   by (auto simp: pairwise_def)
 
+lemma pairwise_imageI:
+  "pairwise P (f ` A)"
+  if "\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> f x \<noteq> f y \<Longrightarrow> P (f x) (f y)"
+  using that by (auto intro: pairwiseI)
+
 lemma pairwise_image: "pairwise r (f ` s) \<longleftrightarrow> pairwise (\<lambda>x y. (f x \<noteq> f y) \<longrightarrow> r (f x) (f y)) s"
   by (force simp: pairwise_def)