# HG changeset patch
# User haftmann
# Date 1436356901 -7200
# Node ID 01488b5599104f0207aebd1965c9b7ceec4f0c59
# Parent  33dbbcb6a8a30656748217feff42931009f80489
avoid explicit definition of the relation of associated elements in a ring -- prefer explicit normalization instead

diff -r 33dbbcb6a8a3 -r 01488b559910 NEWS
--- a/NEWS	Wed Jul 08 14:01:40 2015 +0200
+++ b/NEWS	Wed Jul 08 14:01:41 2015 +0200
@@ -186,11 +186,19 @@
 * Tightened specification of class semiring_no_zero_divisors.  Slight
 INCOMPATIBILITY.
 
-* Class algebraic_semidom introduced common algebraic notions of
-integral (semi)domains like units and associated elements.  Although
+* Class algebraic_semidom introduces common algebraic notions of
+integral (semi)domains, particularly units.  Although
 logically subsumed by fields, is is not a super class of these
 in order not to burden fields with notions that are trivial there.
-INCOMPATIBILITY.
+
+* Class normalization_semidom specifies canonical representants
+for equivalence classes of associated elements in an integral
+(semi)domain.  This formalizes associated elements as well.
+
+* Abstract specification of gcd/lcm operations in classes semiring_gcd,
+semiring_Gcd, semiring_Lcd.  Minor INCOMPATIBILITY: facts gcd_nat.commute
+and gcd_int.commute are subsumed by gcd.commute, as well as gcd_nat.assoc
+and gcd_int.assoc by gcd.assoc.
 
 * Former constants Fields.divide (_ / _) and Divides.div (_ div _)
 are logically unified to Rings.divide in syntactic type class
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Equiv_Relations.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -523,20 +523,6 @@
   "equivp R \<Longrightarrow> R x y \<Longrightarrow> R y z \<Longrightarrow> R x z"
   by (erule equivpE, erule transpE)
 
-
-subsection \<open>Prominent examples\<close>
-
-lemma equivp_associated:
-  "equivp associated"
-proof (rule equivpI)
-  show "reflp associated"
-    by (rule reflpI) simp
-  show "symp associated"
-    by (rule sympI) (simp add: associated_sym)
-  show "transp associated"
-    by (rule transpI) (fact associated_trans)
-qed
-
 hide_const (open) proj
 
 end
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -74,16 +74,6 @@
 
 end
 
-context algebraic_semidom
-begin
-
-lemma associated_1 [simp]:
-  "associated 1 a \<longleftrightarrow> is_unit a"
-  "associated a 1 \<longleftrightarrow> is_unit a"
-  by (auto simp add: associated_def)
-
-end
-
 declare One_nat_def [simp del]
 
 subsection {* GCD and LCM definitions *}
@@ -116,29 +106,11 @@
 
 lemma gcd_0_left [simp]:
   "gcd 0 a = normalize a"
-proof (rule associated_eqI)
-  show "associated (gcd 0 a) (normalize a)"
-    by (auto intro!: associatedI gcd_greatest)
-  show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0"
-  proof -
-    from that have "unit_factor (normalize (gcd 0 a)) = 1"
-      by (rule unit_factor_normalize)
-    then show ?thesis by simp
-  qed
-qed simp
+  by (rule associated_eqI) simp_all
 
 lemma gcd_0_right [simp]:
   "gcd a 0 = normalize a"
-proof (rule associated_eqI)
-  show "associated (gcd a 0) (normalize a)"
-    by (auto intro!: associatedI gcd_greatest)
-  show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0"
-  proof -
-    from that have "unit_factor (normalize (gcd a 0)) = 1"
-      by (rule unit_factor_normalize)
-    then show ?thesis by simp
-  qed
-qed simp
+  by (rule associated_eqI) simp_all
   
 lemma gcd_eq_0_iff [simp]:
   "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
@@ -169,7 +141,7 @@
 proof
   fix a b c
   show "gcd a b = gcd b a"
-    by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd)
+    by (rule associated_eqI) simp_all
   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
     by (rule dvd_trans) simp
   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
@@ -182,10 +154,8 @@
     by (rule dvd_trans) simp
   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
     by (auto intro!: gcd_greatest)
-  from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))"
-    by (rule associatedI)
-  then show "gcd (gcd a b) c = gcd a (gcd b c)"
-    by (rule associated_eqI) (simp_all add: unit_factor_gcd)
+  from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
+    by (rule associated_eqI) simp_all
 qed
 
 lemma gcd_self [simp]:
@@ -193,15 +163,13 @@
 proof -
   have "a dvd gcd a a"
     by (rule gcd_greatest) simp_all
-  then have "associated (gcd a a) (normalize a)"
-    by (auto intro: associatedI)
   then show ?thesis
-    by (auto intro: associated_eqI simp add: unit_factor_gcd)
+    by (auto intro: associated_eqI)
 qed
     
 lemma coprime_1_left [simp]:
   "coprime 1 a"
-  by (rule associated_eqI) (simp_all add: unit_factor_gcd)
+  by (rule associated_eqI) simp_all
 
 lemma coprime_1_right [simp]:
   "coprime a 1"
@@ -218,7 +186,7 @@
   moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
-    by - (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd)
+    by (auto intro: associated_eqI)
   then show ?thesis by (simp add: normalize_mult)
 qed
 
@@ -318,14 +286,15 @@
   fix a b c
   show "lcm a b = lcm b a"
     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
-  have "associated (lcm (lcm a b) c) (lcm a (lcm b c))"
-    by (auto intro!: associatedI lcm_least
+  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
+    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
+    by (auto intro: lcm_least
       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   then show "lcm (lcm a b) c = lcm a (lcm b c)"
-    by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff)
+    by (rule associated_eqI) simp_all
 qed
 
 lemma lcm_self [simp]:
@@ -333,10 +302,8 @@
 proof -
   have "lcm a a dvd a"
     by (rule lcm_least) simp_all
-  then have "associated (lcm a a) (normalize a)"
-    by (auto intro: associatedI)
   then show ?thesis
-    by (rule associated_eqI) (auto simp add: unit_factor_lcm)
+    by (auto intro: associated_eqI)
 qed
 
 lemma gcd_mult_lcm [simp]:
@@ -471,10 +438,8 @@
       ultimately show ?thesis by (blast intro: dvd_trans)
     qed
   qed
-  ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
-    by (rule associatedI)
-  then show ?thesis
-    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
+  ultimately show ?thesis
+    by (auto intro: associated_eqI)
 qed
 
 lemma dvd_Gcd: -- \<open>FIXME remove\<close>
@@ -507,10 +472,10 @@
     ultimately show "Gcd (normalize ` A) dvd a"
       by simp
   qed
-  then have "associated (Gcd (normalize ` A)) (Gcd A)"
-    by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
+  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
+    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   then show ?thesis
-    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
+    by (auto intro: associated_eqI)
 qed
 
 lemma Lcm_least:
@@ -604,10 +569,8 @@
       ultimately show ?thesis by (blast intro: dvd_trans)
     qed
   qed
-  ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))"
-    by (rule associatedI)
-  then show "lcm a (Lcm A) = Lcm (insert a A)"
-    by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff)
+  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
+    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
 qed
   
 lemma Lcm_set [code_unfold]:
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Library/Poly_Deriv.thy
--- a/src/HOL/Library/Poly_Deriv.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -182,11 +182,21 @@
 qed
 
 lemma order_decomp:
-     "p \<noteq> 0
-      ==> \<exists>q. p = [:-a, 1:] ^ (order a p) * q &
-                ~([:-a, 1:] dvd q)"
-apply (drule order [where a=a])
-by (metis dvdE dvd_mult_cancel_left power_Suc2)
+  assumes "p \<noteq> 0"
+  shows "\<exists>q. p = [:- a, 1:] ^ order a p * q \<and> \<not> [:- a, 1:] dvd q"
+proof -
+  from assms have A: "[:- a, 1:] ^ order a p dvd p"
+    and B: "\<not> [:- a, 1:] ^ Suc (order a p) dvd p" by (auto dest: order)
+  from A obtain q where C: "p = [:- a, 1:] ^ order a p * q" ..
+  with B have "\<not> [:- a, 1:] ^ Suc (order a p) dvd [:- a, 1:] ^ order a p * q"
+    by simp
+  then have "\<not> [:- a, 1:] ^ order a p * [:- a, 1:] dvd [:- a, 1:] ^ order a p * q"
+    by simp
+  then have D: "\<not> [:- a, 1:] dvd q"
+    using idom_class.dvd_mult_cancel_left [of "[:- a, 1:] ^ order a p" "[:- a, 1:]" q]
+    by auto
+  from C D show ?thesis by blast
+qed
 
 lemma order_pderiv: "[| pderiv p \<noteq> 0; order a p \<noteq> 0 |]
       ==> (order a p = Suc (order a (pderiv p)))"
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -267,7 +267,7 @@
 
 lemma cong_mult_rcancel_int:
     "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
-  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd_int.commute)
+  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute)
 
 lemma cong_mult_rcancel_nat:
     "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
@@ -528,15 +528,15 @@
   done
 
 lemma coprime_iff_invertible_nat: "m > 0 \<Longrightarrow> coprime a m = (EX x. [a * x = Suc 0] (mod m))"
-  apply (auto intro: cong_solve_coprime_nat simp: One_nat_def)
+  apply (auto intro: cong_solve_coprime_nat)
   apply (metis cong_Suc_0_nat cong_solve_nat gcd_nat.left_neutral)
   apply (metis One_nat_def cong_gcd_eq_nat coprime_lmult_nat 
-      gcd_lcm_complete_lattice_nat.inf_bot_right gcd_nat.commute)
+      gcd_lcm_complete_lattice_nat.inf_bot_right gcd.commute)
   done
 
 lemma coprime_iff_invertible_int: "m > (0::int) \<Longrightarrow> coprime a m = (EX x. [a * x = 1] (mod m))"
   apply (auto intro: cong_solve_coprime_int)
-  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd_int.commute gcd_red_int)
+  apply (metis cong_int_def coprime_mul_eq_int gcd_1_int gcd.commute gcd_red_int)
   done
 
 lemma coprime_iff_invertible'_nat: "m > 0 \<Longrightarrow> coprime a m =
@@ -571,7 +571,7 @@
       [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
+  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
   done
 
 lemma cong_cong_setprod_coprime_int [rule_format]: "finite A \<Longrightarrow>
@@ -580,7 +580,7 @@
       [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis coprime_cong_mult_int gcd_int.commute setprod_coprime_int)
+  apply (metis coprime_cong_mult_int gcd.commute setprod_coprime_int)
   done
 
 lemma binary_chinese_remainder_aux_nat:
@@ -827,7 +827,7 @@
          [x = y] (mod (PROD i:A. m i))"
   apply (induct set: finite)
   apply auto
-  apply (metis One_nat_def coprime_cong_mult_nat gcd_nat.commute setprod_coprime_nat)
+  apply (metis One_nat_def coprime_cong_mult_nat gcd.commute setprod_coprime_nat)
   done
 
 lemma chinese_remainder_unique_nat:
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -228,16 +228,15 @@
   "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
   by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
 
-lemma unit_factor_gcd [simp]:
-  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)" (is "?f a b = ?g a b")
-  by (induct a b rule: gcd_eucl_induct)
-    (auto simp add: gcd_0 gcd_non_0)
+lemma normalize_gcd [simp]:
+  "normalize (gcd a b) = gcd a b"
+  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_0 gcd_non_0)
 
 lemma gcdI:
   assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
-    and "unit_factor c = (if c = 0 then 0 else 1)"
+    and "normalize c = c"
   shows "c = gcd a b"
-  by (rule associated_eqI) (auto simp: assms associated_def intro: gcd_greatest)
+  by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
 
 sublocale gcd!: abel_semigroup gcd
 proof
@@ -251,10 +250,10 @@
     moreover have "gcd (gcd a b) c dvd c" by simp
     ultimately show "gcd (gcd a b) c dvd gcd b c"
       by (rule gcd_greatest)
-    show "unit_factor (gcd (gcd a b) c) =  (if gcd (gcd a b) c = 0 then 0 else 1)"
+    show "normalize (gcd (gcd a b) c) = gcd (gcd a b) c"
       by auto
     fix l assume "l dvd a" and "l dvd gcd b c"
-    with dvd_trans[OF _ gcd_dvd1] and dvd_trans[OF _ gcd_dvd2]
+    with dvd_trans [OF _ gcd_dvd1] and dvd_trans [OF _ gcd_dvd2]
       have "l dvd b" and "l dvd c" by blast+
     with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
       by (intro gcd_greatest)
@@ -266,9 +265,9 @@
 qed
 
 lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
-    unit_factor d = (if d = 0 then 0 else 1) \<and>
+    normalize d = d \<and>
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
-  by (rule, auto intro: gcdI simp: gcd_greatest)
+  by rule (auto intro: gcdI simp: gcd_greatest)
 
 lemma gcd_dvd_prod: "gcd a b dvd k * b"
   using mult_dvd_mono [of 1] by auto
@@ -378,10 +377,9 @@
 
 lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   apply (rule gcdI)
+  apply simp_all
   apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
-  apply (rule gcd_dvd2)
   apply (rule gcd_greatest, simp add: unit_simps, assumption)
-  apply (subst unit_factor_gcd, simp add: gcd_0)
   done
 
 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
@@ -461,7 +459,7 @@
   with A show "gcd a b dvd c" by (rule dvd_trans)
   have "gcd c d dvd d" by simp
   with A show "gcd a b dvd d" by (rule dvd_trans)
-  show "unit_factor (gcd a b) = (if gcd a b = 0 then 0 else 1)"
+  show "normalize (gcd a b) = gcd a b"
     by simp
   fix l assume "l dvd c" and "l dvd d"
   hence "l dvd gcd c d" by (rule gcd_greatest)
@@ -484,22 +482,27 @@
 
 lemma coprime_crossproduct:
   assumes [simp]: "gcd a d = 1" "gcd b c = 1"
-  shows "associated (a * c) (b * d) \<longleftrightarrow> associated a b \<and> associated c d" (is "?lhs \<longleftrightarrow> ?rhs")
+  shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
+    (is "?lhs \<longleftrightarrow> ?rhs")
 proof
-  assume ?rhs then show ?lhs unfolding associated_def by (fast intro: mult_dvd_mono)
+  assume ?rhs
+  then have "a dvd b" "b dvd a" "c dvd d" "d dvd c" by (simp_all add: associated_iff_dvd)
+  then have "a * c dvd b * d" "b * d dvd a * c" by (fast intro: mult_dvd_mono)+
+  then show ?lhs by (simp add: associated_iff_dvd)
 next
   assume ?lhs
-  from \<open>?lhs\<close> have "a dvd b * d" unfolding associated_def by (metis dvd_mult_left) 
+  then have dvd: "a * c dvd b * d" "b * d dvd a * c" by (simp_all add: associated_iff_dvd)
+  then have "a dvd b * d" by (metis dvd_mult_left) 
   hence "a dvd b" by (simp add: coprime_dvd_mult_iff)
-  moreover from \<open>?lhs\<close> have "b dvd a * c" unfolding associated_def by (metis dvd_mult_left) 
+  moreover from dvd have "b dvd a * c" by (metis dvd_mult_left) 
   hence "b dvd a" by (simp add: coprime_dvd_mult_iff)
-  moreover from \<open>?lhs\<close> have "c dvd d * b" 
-    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
+  moreover from dvd have "c dvd d * b" 
+    by (auto dest: dvd_mult_right simp add: ac_simps)
   hence "c dvd d" by (simp add: coprime_dvd_mult_iff gcd.commute)
-  moreover from \<open>?lhs\<close> have "d dvd c * a"
-    unfolding associated_def by (auto dest: dvd_mult_right simp add: ac_simps)
+  moreover from dvd have "d dvd c * a"
+    by (auto dest: dvd_mult_right simp add: ac_simps)
   hence "d dvd c" by (simp add: coprime_dvd_mult_iff gcd.commute)
-  ultimately show ?rhs unfolding associated_def by simp
+  ultimately show ?rhs by (simp add: associated_iff_dvd)
 qed
 
 lemma gcd_add1 [simp]:
@@ -616,19 +619,29 @@
   apply assumption
   done
 
+lemma lcm_gcd:
+  "lcm a b = normalize (a * b) div gcd a b"
+  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
+
+subclass semiring_gcd
+  apply standard
+  using gcd_right_idem
+  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
+  done
+
 lemma gcd_exp:
-  "gcd (a^n) (b^n) = (gcd a b) ^ n"
+  "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
 proof (cases "a = 0 \<and> b = 0")
-  assume "a = 0 \<and> b = 0"
-  then show ?thesis by (cases n, simp_all add: gcd_0_left)
+  case True
+  then show ?thesis by (cases n) simp_all
 next
-  assume A: "\<not>(a = 0 \<and> b = 0)"
-  hence "1 = gcd ((a div gcd a b)^n) ((b div gcd a b)^n)"
-    using div_gcd_coprime by (subst sym, auto simp: div_gcd_coprime)
-  hence "(gcd a b) ^ n = (gcd a b) ^ n * ..." by simp
+  case False
+  then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    using div_gcd_coprime by (subst sym) (auto simp: div_gcd_coprime)
+  then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
   also note gcd_mult_distrib
-  also have "unit_factor ((gcd a b)^n) = 1"
-    by (simp add: unit_factor_power A)
+  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 (subst ac_simps, subst div_power, simp, rule dvd_div_mult_self, rule dvd_power_same, simp)
   also have "(gcd a b)^n * (b div gcd a b)^n = b^n"
@@ -749,16 +762,6 @@
     by (simp add: ac_simps)
 qed
 
-lemma lcm_gcd:
-  "lcm a b = normalize (a * b) div gcd a b"
-  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
-
-subclass semiring_gcd
-  apply standard
-  using gcd_right_idem
-  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
-  done
-
 lemma lcm_gcd_prod:
   "lcm a b * gcd a b = normalize (a * b)"
   by (simp add: lcm_gcd)
@@ -783,9 +786,9 @@
 
 lemma lcmI:
   assumes "a dvd c" and "b dvd c" and "\<And>d. a dvd d \<Longrightarrow> b dvd d \<Longrightarrow> c dvd d"
-    and "unit_factor c = (if c = 0 then 0 else 1)"
+    and "normalize c = c"
   shows "c = lcm a b"
-  by (rule associated_eqI) (auto simp: assms intro: associatedI lcm_least)
+  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
 
 sublocale lcm!: abel_semigroup lcm ..
 
@@ -823,9 +826,9 @@
 
 lemma lcm_unique:
   "a dvd d \<and> b dvd d \<and> 
-  unit_factor d = (if d = 0 then 0 else 1) \<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_zero)
+  by rule (auto intro: lcmI simp: lcm_least lcm_zero)
 
 lemma dvd_lcm_I1 [simp]:
   "k dvd m \<Longrightarrow> k dvd lcm m n"
@@ -906,7 +909,7 @@
   apply (rule dvd_trans[of _ "b * a"], simp, rule lcm_dvd1)
   apply (rule lcm_dvd2)
   apply (rule lcm_least, simp add: unit_simps, assumption)
-  apply (subst unit_factor_lcm, simp add: lcm_zero)
+  apply simp
   done
 
 lemma lcm_mult_unit2:
@@ -1035,12 +1038,19 @@
 
 lemma normalize_Lcm [simp]:
   "normalize (Lcm A) = Lcm A"
-  by (cases "Lcm A = 0") (auto intro: associated_eqI)
+proof (cases "Lcm A = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "unit_factor (Lcm A) * normalize (Lcm A) = Lcm A"
+    by (fact unit_factor_mult_normalize)
+  with False show ?thesis by simp
+qed
 
 lemma LcmI:
   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
-    and "unit_factor b = (if b = 0 then 0 else 1)" shows "b = Lcm A"
-  by (rule associated_eqI) (auto simp: assms associated_def intro: Lcm_least)
+    and "normalize b = b" shows "b = Lcm A"
+  by (rule associated_eqI) (auto simp: assms intro: Lcm_least)
 
 lemma Lcm_subset:
   "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
@@ -1204,16 +1214,23 @@
 
 lemma normalize_Gcd [simp]:
   "normalize (Gcd A) = Gcd A"
-  by (cases "Gcd A = 0") (auto intro: associated_eqI)
+proof (cases "Gcd A = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A"
+    by (fact unit_factor_mult_normalize)
+  with False show ?thesis by simp
+qed
 
 subclass semiring_Gcd
   by standard (simp_all add: Gcd_greatest)
 
 lemma GcdI:
   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
-    and "unit_factor b = (if b = 0 then 0 else 1)"
+    and "normalize b = b"
   shows "b = Gcd A"
-  by (rule associated_eqI) (auto simp: assms associated_def intro: Gcd_greatest)
+  by (rule associated_eqI) (auto simp: assms intro: Gcd_greatest)
 
 lemma Lcm_Gcd:
   "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Fib.thy
--- a/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -67,7 +67,7 @@
   apply (cases m)
   apply (auto simp add: fib_add)
   apply (metis gcd_commute_nat mult.commute coprime_fib_Suc_nat
-    gcd_add_mult_nat gcd_mult_cancel_nat gcd_nat.commute)
+    gcd_add_mult_nat gcd_mult_cancel_nat gcd.commute)
   done
 
 lemma gcd_fib_diff: "m \<le> n \<Longrightarrow> gcd (fib m) (fib (n - m)) = gcd (fib m) (fib n)"
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Gauss.thy
--- a/src/HOL/Number_Theory/Gauss.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -112,7 +112,7 @@
     from a p_a_relprime p_prime a_nonzero cong_mult_rcancel_int [of _ a x y]
     have "[x = y](mod p)"
       by (metis monoid_mult_class.mult.left_neutral cong_dvd_modulus_int cong_mult_rcancel_int 
-                cong_mult_self_int gcd_int.commute prime_imp_coprime_int)
+                cong_mult_self_int gcd.commute prime_imp_coprime_int)
     with cong_less_imp_eq_int [of x y p] p_minus_one_l
         order_le_less_trans [of x "(int p - 1) div 2" p]
         order_le_less_trans [of y "(int p - 1) div 2" p] 
@@ -202,7 +202,7 @@
 
 lemma all_A_relprime: assumes "x \<in> A" shows "gcd x p = 1"
   using p_prime A_ncong_p [OF assms]
-  by (simp add: cong_altdef_int) (metis gcd_int.commute prime_imp_coprime_int)
+  by (simp add: cong_altdef_int) (metis gcd.commute prime_imp_coprime_int)
 
 lemma A_prod_relprime: "gcd (setprod id A) p = 1"
   by (metis id_def all_A_relprime setprod_coprime_int)
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Pocklington.thy
--- a/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -98,9 +98,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_nat.commute) 
+    by (metis gcd.commute) 
   have px:"coprime x p"
-    by (metis gcd_nat.commute p prime x0 xp)
+    by (metis gcd.commute p prime x0 xp)
   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)
   {assume y0: "y = 0"
@@ -114,7 +114,7 @@
 lemma cong_unique_inverse_prime:
   assumes p: "prime p" and x0: "0 < x" and xp: "x < p"
   shows "\<exists>!y. 0 < y \<and> y < p \<and> [x * y = 1] (mod p)"
-by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd_nat.commute assms) 
+by (metis cong_solve_unique_nontrivial gcd_lcm_complete_lattice_nat.inf_bot_left gcd.commute assms) 
 
 lemma chinese_remainder_coprime_unique:
   fixes a::nat 
@@ -157,7 +157,7 @@
     by auto
   also have "... \<le> card {x. 0 < x \<and> x < n \<and> coprime x n}"
     apply (rule card_mono) using assms
-    by auto (metis dual_order.antisym gcd_1_int gcd_int.commute int_one_le_iff_zero_less)
+    by auto (metis dual_order.antisym gcd_1_int gcd.commute int_one_le_iff_zero_less)
   also have "... = phi n"
     by (simp add: phi_def)
   finally show ?thesis .
@@ -242,7 +242,7 @@
   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_nat gcd_nat.commute)
+    by (auto simp add: coprime_exp_nat gcd.commute)
   {assume H0: "\<exists>m. 0 < m \<and> m < n - 1 \<and> [a ^ m = 1] (mod n)" (is "EX m. ?P m")
     from H0[unfolded nat_exists_least_iff[of ?P]] obtain m where
       m: "0 < m" "m < n - 1" "[a ^ m = 1] (mod n)" "\<forall>k <m. \<not>?P k" by blast
@@ -251,7 +251,7 @@
       let ?y = "a^ ((n - 1) div m * m)"
       note mdeq = mod_div_equality[of "(n - 1)" m]
       have yn: "coprime ?y n"
-        by (metis an(1) coprime_exp_nat gcd_nat.commute)
+        by (metis an(1) coprime_exp_nat gcd.commute)
       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"
@@ -310,7 +310,7 @@
   moreover
   {assume "n\<noteq>0 \<and> n\<noteq>1" hence n2:"n \<ge> 2" by arith
     from assms have na': "coprime a n"
-      by (metis gcd_nat.commute)
+      by (metis gcd.commute)
     from phi_lowerbound_1_nat[OF n2] euler_theorem_nat [OF na']
     have ex: "\<exists>m>0. ?P m" by - (rule exI[where x="phi n"], auto) }
   ultimately have ex: "\<exists>m>0. ?P m" by blast
@@ -367,7 +367,7 @@
       obtain p where p: "p dvd n" "p dvd a" "p \<noteq> 1" by auto
       from lh
       obtain q1 q2 where q12:"a ^ d + n * q1 = 1 + n * q2"
-        by (metis H d0 gcd_nat.commute lucas_coprime_lemma) 
+        by (metis H d0 gcd.commute lucas_coprime_lemma) 
       hence "a ^ d + n * q1 - n * q2 = 1" by simp
       with dvd_diff_nat [OF dvd_add [OF divides_rexp]]  dvd_mult2  d' p
       have "p dvd 1"
@@ -404,7 +404,7 @@
 
 lemma order_divides_phi: 
   fixes n::nat shows "coprime n a \<Longrightarrow> ord n a dvd phi n"
-  by (metis ord_divides euler_theorem_nat gcd_nat.commute)
+  by (metis ord_divides euler_theorem_nat gcd.commute)
 
 lemma order_divides_expdiff:
   fixes n::nat and a::nat assumes na: "coprime n a"
@@ -415,11 +415,11 @@
     hence "\<exists>c. d = e + c" by presburger
     then obtain c where c: "d = e + c" by presburger
     from na have an: "coprime a n"
-      by (metis gcd_nat.commute)
+      by (metis gcd.commute)
     have aen: "coprime (a^e) n"
-      by (metis coprime_exp_nat gcd_nat.commute na)      
+      by (metis coprime_exp_nat gcd.commute na)      
     have acn: "coprime (a^c) n"
-      by (metis coprime_exp_nat gcd_nat.commute na) 
+      by (metis coprime_exp_nat gcd.commute na) 
     have "[a^d = a^e] (mod n) \<longleftrightarrow> [a^(e + c) = a^(e + 0)] (mod n)"
       using c by simp
     also have "\<dots> \<longleftrightarrow> [a^e* a^c = a^e *a^0] (mod n)" by (simp add: power_add)
@@ -588,7 +588,7 @@
            gcd_lcm_complete_lattice_nat.top_greatest pn)} 
   hence cpa: "coprime p a" by auto
   have arp: "coprime (a^r) p"
-    by (metis coprime_exp_nat cpa gcd_nat.commute) 
+    by (metis coprime_exp_nat cpa gcd.commute) 
   from euler_theorem_nat[OF arp, simplified ord_divides] o phip
   have "q dvd (p - 1)" by simp
   then obtain d where d:"p - 1 = q * d" 
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Primes.thy
--- a/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -44,7 +44,7 @@
 
 lemma prime_odd_nat: "prime p \<Longrightarrow> p > 2 \<Longrightarrow> odd p"
   apply (auto simp add: prime_nat_def even_iff_mod_2_eq_zero dvd_eq_mod_eq_0)
-  apply (metis dvd_eq_mod_eq_0 even_Suc even_iff_mod_2_eq_zero mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
+  apply (metis dvd_eq_mod_eq_0 even_Suc mod_by_1 nat_dvd_not_less not_mod_2_eq_0_eq_1 zero_less_numeral)
   done
 
 (* FIXME Is there a better way to handle these, rather than making them elim rules? *)
@@ -159,11 +159,11 @@
 
 
 lemma prime_imp_power_coprime_nat: "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
-  by (metis coprime_exp_nat gcd_nat.commute prime_imp_coprime_nat)
+  by (metis coprime_exp_nat gcd.commute prime_imp_coprime_nat)
 
 lemma prime_imp_power_coprime_int:
   fixes a::int shows "prime p \<Longrightarrow> ~ p dvd a \<Longrightarrow> coprime a (p^m)"
-  by (metis coprime_exp_int gcd_int.commute prime_imp_coprime_int)
+  by (metis coprime_exp_int gcd.commute prime_imp_coprime_int)
 
 lemma primes_coprime_nat: "prime p \<Longrightarrow> prime q \<Longrightarrow> p \<noteq> q \<Longrightarrow> coprime p q"
   by (metis gcd_nat.absorb1 gcd_nat.absorb2 prime_imp_coprime_nat)
@@ -375,7 +375,7 @@
 lemma bezout_gcd_nat:
   fixes a::nat shows "\<exists>x y. a * x - b * y = gcd a b \<or> b * x - a * y = gcd a b"
   using bezout_nat[of a b]
-by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd_nat.commute
+by (metis bezout_nat diff_add_inverse gcd_add_mult_nat gcd.commute
   gcd_nat.right_neutral mult_0)
 
 lemma gcd_bezout_sum_nat:
@@ -423,7 +423,7 @@
   shows "\<exists>x y. a*x = Suc (p*y)"
 proof-
   have ap: "coprime a p"
-    by (metis gcd_nat.commute p pa prime_imp_coprime_nat)
+    by (metis gcd.commute p pa prime_imp_coprime_nat)
   from coprime_bezout_strong[OF ap] show ?thesis
     by (metis Suc_eq_plus1 gcd_lcm_complete_lattice_nat.bot.extremum pa)
 qed
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Number_Theory/Residues.thy
--- a/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -166,15 +166,20 @@
 lemma (in residues) sum_cong: "finite A \<Longrightarrow> (\<Oplus>i\<in>A. (f i) mod m) = (\<Sum>i\<in>A. f i) mod m"
   by (induct set: finite) (auto simp: zero_cong add_cong)
 
-lemma mod_in_res_units [simp]: "1 < m \<Longrightarrow> coprime a m \<Longrightarrow> a mod m \<in> Units R"
-  apply (subst res_units_eq)
-  apply auto
-  apply (insert pos_mod_sign [of m a])
-  apply (subgoal_tac "a mod m \<noteq> 0")
-  apply arith
-  apply auto
-  apply (metis gcd_int.commute gcd_red_int)
-  done
+lemma mod_in_res_units [simp]:
+  assumes "1 < m" and "coprime a m"
+  shows "a mod m \<in> Units R"
+proof (cases "a mod m = 0")
+  case True with assms show ?thesis
+    by (auto simp add: res_units_eq gcd_red_int [symmetric])
+next
+  case False
+  from assms have "0 < m" by simp
+  with pos_mod_sign [of m a] have "0 \<le> a mod m" .
+  with False have "0 < a mod m" by simp
+  with assms show ?thesis
+    by (auto simp add: res_units_eq gcd_red_int [symmetric] ac_simps)
+qed
 
 lemma res_eq_to_cong: "(a mod m) = (b mod m) \<longleftrightarrow> [a = b] (mod m)"
   unfolding cong_int_def by auto
@@ -354,10 +359,7 @@
   shows "[a^(p - 1) = 1] (mod p)"
 proof -
   from assms have "[a ^ phi p = 1] (mod p)"
-    apply (intro euler_theorem)
-    apply (metis of_nat_0_le_iff)
-    apply (metis gcd_int.commute prime_imp_coprime_int)
-    done
+    by (auto intro!: euler_theorem dest!: prime_imp_coprime_int simp add: ac_simps)
   also have "phi p = nat p - 1"
     by (rule phi_prime) (rule assms)
   finally show ?thesis
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Rat.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -1001,7 +1001,7 @@
     in if a = 0 then (0, 1) else (sgn a * b, \<bar>a\<bar>))"
 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_int.commute)
+    by (cases "0::int" a rule: linorder_cases) (simp_all add: quotient_of_Fract gcd.commute)
 qed
 
 lemma rat_divide_code [code abstract]:
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Rings.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -636,6 +636,13 @@
 class algebraic_semidom = semidom_divide
 begin
 
+text \<open>
+  Class @{class algebraic_semidom} enriches a integral domain
+  by notions from algebra, like units in a ring.
+  It is a separate class to avoid spoiling fields with notions
+  which are degenerated there.
+\<close>
+
 lemma dvd_div_mult_self [simp]:
   "a dvd b \<Longrightarrow> b div a * a = b"
   by (cases "a = 0") (auto elim: dvdE simp add: ac_simps)
@@ -834,84 +841,11 @@
     by (rule dvd_div_mult2_eq)
 qed
 
-
-text \<open>Associated elements in a ring --- an equivalence relation induced
-  by the quasi-order divisibility.\<close>
-
-definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
-
-lemma associatedI:
-  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
-  by (simp add: associated_def)
-
-lemma associatedD1:
-  "associated a b \<Longrightarrow> a dvd b"
-  by (simp add: associated_def)
-
-lemma associatedD2:
-  "associated a b \<Longrightarrow> b dvd a"
-  by (simp add: associated_def)
-
-lemma associated_refl [simp]:
-  "associated a a"
-  by (auto intro: associatedI)
-
-lemma associated_sym:
-  "associated b a \<longleftrightarrow> associated a b"
-  by (auto intro: associatedI dest: associatedD1 associatedD2)
-
-lemma associated_trans:
-  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
-  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
-
-lemma associated_0 [simp]:
-  "associated 0 b \<longleftrightarrow> b = 0"
-  "associated a 0 \<longleftrightarrow> a = 0"
-  by (auto dest: associatedD1 associatedD2)
-
-lemma associated_unit:
-  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
-  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
-
-lemma is_unit_associatedI:
-  assumes "is_unit c" and "a = c * b"
-  shows "associated a b"
-proof (rule associatedI)
-  from `a = c * b` show "b dvd a" by auto
-  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
-  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
-  ultimately have "b = a * d" by (simp add: ac_simps)
-  then show "a dvd b" ..
-qed
-
-lemma associated_is_unitE:
-  assumes "associated a b"
-  obtains c where "is_unit c" and "a = c * b"
-proof (cases "b = 0")
-  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
-  with that show thesis .
-next
-  case False
-  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
-  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
-  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
-  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
-  then have "is_unit c" by auto
-  with `a = c * b` that show thesis by blast
-qed
-
 lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff
   dvd_div_unit_iff unit_div_mult_swap unit_div_commute
   unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel
   unit_eq_div1 unit_eq_div2
 
-end
-
-context algebraic_semidom
-begin
-
 lemma is_unit_divide_mult_cancel_left:
   assumes "a \<noteq> 0" and "is_unit b"
   shows "a div (a * b) = 1 div b"
@@ -941,6 +875,16 @@
   assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
 begin
 
+text \<open>
+  Class @{class normalization_semidom} cultivates the idea that
+  each integral domain can be split into equivalence classes
+  whose representants are associated, i.e. divide each other.
+  @{const normalize} specifies a canonical representant for each equivalence
+  class.  The rationale behind this is that it is easier to reason about equality
+  than equivalences, hence we prefer to think about equality of normalized
+  values rather than associated elements.
+\<close>
+
 lemma unit_factor_dvd [simp]:
   "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   by (rule unit_imp_dvd) simp
@@ -1140,54 +1084,74 @@
   then show ?thesis by simp
 qed
 
-lemma associated_normalize_left [simp]:
-  "associated (normalize a) b \<longleftrightarrow> associated a b"
-  by (auto simp add: associated_def)
+text \<open>
+  We avoid an explicit definition of associated elements but prefer
+  explicit normalisation instead.  In theory we could define an abbreviation
+  like @{prop "associated a b \<longleftrightarrow> normalize a = normalize b"} but this is
+  counterproductive without suggestive infix syntax, which we do not want
+  to sacrifice for this purpose here.
+\<close>
 
-lemma associated_normalize_right [simp]:
-  "associated a (normalize b) \<longleftrightarrow> associated a b"
-  by (auto simp add: associated_def)
-
-lemma associated_iff_normalize:
-  "associated a b \<longleftrightarrow> normalize a = normalize b" (is "?P \<longleftrightarrow> ?Q")
+lemma associatedI:
+  assumes "a dvd b" and "b dvd a"
+  shows "normalize a = normalize b"
 proof (cases "a = 0 \<or> b = 0")
-  case True then show ?thesis by auto
+  case True with assms show ?thesis by auto
 next
   case False
-  show ?thesis
-  proof
-    assume ?P then show ?Q
-      by (rule associated_is_unitE) (simp add: normalize_mult is_unit_normalize)
+  from \<open>a dvd b\<close> obtain c where b: "b = a * c" ..
+  moreover from \<open>b dvd a\<close> obtain d where a: "a = b * d" ..
+  ultimately have "b * 1 = b * (c * d)" by (simp add: ac_simps)
+  with False have "1 = c * d"
+    unfolding mult_cancel_left by simp
+  then have "is_unit c" and "is_unit d" by auto
+  with a b show ?thesis by (simp add: normalize_mult is_unit_normalize)
+qed
+
+lemma associatedD1:
+  "normalize a = normalize b \<Longrightarrow> a dvd b"
+  using dvd_normalize_iff [of _ b, symmetric] normalize_dvd_iff [of a _, symmetric]
+  by simp
+
+lemma associatedD2:
+  "normalize a = normalize b \<Longrightarrow> b dvd a"
+  using dvd_normalize_iff [of _ a, symmetric] normalize_dvd_iff [of b _, symmetric]
+  by simp
+
+lemma associated_unit:
+  "normalize a = normalize b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
+
+lemma associated_iff_dvd:
+  "normalize a = normalize b \<longleftrightarrow> a dvd b \<and> b dvd a" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q then show ?P by (auto intro!: associatedI)
+next
+  assume ?P
+  then have "unit_factor a * normalize a = unit_factor a * normalize b"
+    by simp
+  then have *: "normalize b * unit_factor a = a"
+    by (simp add: ac_simps)
+  show ?Q
+  proof (cases "a = 0 \<or> b = 0")
+    case True with \<open>?P\<close> show ?thesis by auto
   next
-    from False have *: "is_unit (unit_factor a div unit_factor b)"
-      by auto
-    assume ?Q then have "unit_factor a * normalize a = unit_factor a * normalize b"
-      by simp
-    then have "a = unit_factor a * (b div unit_factor b)"
-      by simp
-    with False have "a = (unit_factor a div unit_factor b) * b"
-      by (simp add: unit_div_commute unit_div_mult_swap [symmetric])
-    with * show ?P 
-      by (rule is_unit_associatedI)
+    case False 
+    then have "b dvd normalize b * unit_factor a" and "normalize b * unit_factor a dvd b"
+      by (simp_all add: mult_unit_dvd_iff dvd_mult_unit_iff)
+    with * show ?thesis by simp
   qed
 qed
 
 lemma associated_eqI:
-  assumes "associated a b"
-  assumes "a \<noteq> 0 \<Longrightarrow> unit_factor a = 1" and "b \<noteq> 0 \<Longrightarrow> unit_factor b = 1"
+  assumes "a dvd b" and "b dvd a"
+  assumes "normalize a = a" and "normalize b = b"
   shows "a = b"
-proof (cases "a = 0")
-  case True with assms show ?thesis by simp
-next
-  case False with assms have "b \<noteq> 0" by auto
-  with False assms have "unit_factor a = unit_factor b"
-    by simp
-  moreover from assms have "normalize a = normalize b"
-    by (simp add: associated_iff_normalize)
-  ultimately have "unit_factor a * normalize a = unit_factor b * normalize b"
-    by simp
-  then show ?thesis
-    by simp
+proof -
+  from assms have "normalize a = normalize b"
+    unfolding associated_iff_dvd by simp
+  with \<open>normalize a = a\<close> have "a = normalize b" by simp
+  with \<open>normalize b = b\<close> show "a = b" by simp
 qed
 
 end
diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/Transcendental.thy
--- a/src/HOL/Transcendental.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/Transcendental.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -3602,11 +3602,15 @@
     done
 qed
 
-lemma sin_zero_iff_int2: "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
+lemma sin_zero_iff_int2:
+  "sin x = 0 \<longleftrightarrow> (\<exists>n::int. x = real n * pi)"
   apply (simp only: sin_zero_iff_int)
   apply (safe elim!: evenE)
   apply (simp_all add: field_simps)
-  using dvd_triv_left by fastforce
+  apply (subst real_numeral(1) [symmetric])
+  apply (simp only: real_of_int_mult [symmetric] real_of_int_inject)
+  apply auto
+  done
 
 lemma cos_monotone_0_pi:
   assumes "0 \<le> y" and "y < x" and "x \<le> pi"