merged

--- a/CONTRIBUTORS	Thu Jul 09 15:20:54 2015 +0200
+++ b/CONTRIBUTORS	Thu Jul 09 16:49:08 2015 +0200
@@ -15,7 +15,8 @@
 
 * Summer 2015: Manuel Eberl and Florian Haftmann, TUM
   Type class hierarchy with common algebraic notions of integral
-  (semi)domains like units and associated elements.
+  (semi)domains like units, associated elements and normalization
+  wrt. units.
 
 
 Contributions to Isabelle2015

--- a/NEWS	Thu Jul 09 15:20:54 2015 +0200
+++ b/NEWS	Thu Jul 09 16:49:08 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

--- a/src/HOL/Divides.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Divides.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -118,8 +118,8 @@
 lemma mod_mult_self2_is_0 [simp]: "a * b mod b = 0"
   using mod_mult_self1 [of 0 a b] by simp
 
-lemma div_by_1 [simp]: "a div 1 = a"
-  using div_mult_self2_is_id [of 1 a] zero_neq_one by simp
+lemma div_by_1: "a div 1 = a"
+  by (fact divide_1)
 
 lemma mod_by_1 [simp]: "a mod 1 = 0"
 proof -
@@ -378,20 +378,6 @@
 lemma mult_mod_right: "c * (a mod b) = (c * a) mod (c * b)"
   by (fact mod_mult_mult1 [symmetric])
 
-lemma dvd_times_left_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
-  assumes "c \<noteq> 0"
-  shows "c * a dvd c * b \<longleftrightarrow> a dvd b"
-proof -
-  have "(c * b) mod (c * a) = 0 \<longleftrightarrow> b mod a = 0" (is "?P \<longleftrightarrow> ?Q")
-    using assms by (simp add: mod_mult_mult1)
-  then show ?thesis by (simp add: mod_eq_0_iff_dvd)
-qed
-
-lemma dvd_times_right_cancel_iff [simp]: -- \<open>FIXME generalize\<close>
-  assumes "c \<noteq> 0"
-  shows "a * c dvd b * c \<longleftrightarrow> a dvd b"
-  using assms dvd_times_left_cancel_iff [of c a b] by (simp add: ac_simps)
-
 lemma dvd_mod: "k dvd m \<Longrightarrow> k dvd n \<Longrightarrow> k dvd (m mod n)"
   unfolding dvd_def by (auto simp add: mod_mult_mult1)
 
@@ -1034,6 +1020,25 @@
 
 end
 
+instantiation nat :: normalization_semidom
+begin
+
+definition normalize_nat
+  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
+
+definition unit_factor_nat
+  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
+
+lemma unit_factor_simps [simp]:
+  "unit_factor 0 = (0::nat)"
+  "unit_factor (Suc n) = 1"
+  by (simp_all add: unit_factor_nat_def)
+
+instance
+  by standard (simp_all add: unit_factor_nat_def)
+  
+end
+
 lemma divmod_nat_if [code]: "divmod_nat m n = (if n = 0 \<or> m < n then (0, m) else
   let (q, r) = divmod_nat (m - n) n in (Suc q, r))"
   by (simp add: prod_eq_iff case_prod_beta not_less le_div_geq le_mod_geq)
@@ -1890,6 +1895,27 @@
   "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
   by auto
 
+instantiation int :: normalization_semidom
+begin
+
+definition normalize_int
+  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
+
+definition unit_factor_int
+  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
+
+instance
+proof
+  fix k :: int
+  assume "k \<noteq> 0"
+  then have "\<bar>sgn k\<bar> = 1"
+    by (cases "0::int" k rule: linorder_cases) simp_all
+  then show "is_unit (unit_factor k)"
+    by simp
+qed (simp_all add: sgn_times mult_sgn_abs)
+  
+end
+  
 text{*Basic laws about division and remainder*}
 
 lemma zmod_zdiv_equality: "(a::int) = b * (a div b) + (a mod b)"

--- a/src/HOL/Equiv_Relations.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Equiv_Relations.thy	Thu Jul 09 16:49:08 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

--- a/src/HOL/Fields.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Fields.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -145,9 +145,6 @@
 lemma add_divide_distrib: "(a+b) / c = a/c + b/c"
 by (simp add: divide_inverse algebra_simps)
 
-lemma divide_1 [simp]: "a / 1 = a"
-  by (simp add: divide_inverse)
-
 lemma times_divide_eq_right [simp]: "a * (b / c) = (a * b) / c"
   by (simp add: divide_inverse mult.assoc)
 

--- a/src/HOL/GCD.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/GCD.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -31,8 +31,6 @@
 imports Main
 begin
 
-declare One_nat_def [simp del]
-
 subsection {* GCD and LCM definitions *}
 
 class gcd = zero + one + dvd +
@@ -40,17 +38,521 @@
     and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
 begin
 
-abbreviation
-  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
-where
-  "coprime x y == (gcd x y = 1)"
+abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
+  where "coprime x y \<equiv> gcd x y = 1"
 
 end
 
-class semiring_gcd = comm_semiring_1 + gcd +
+class Gcd = gcd +
+  fixes Gcd :: "'a set \<Rightarrow> 'a"
+    and Lcm :: "'a set \<Rightarrow> 'a"
+
+class semiring_gcd = normalization_semidom + gcd +
   assumes gcd_dvd1 [iff]: "gcd a b dvd a"
     and gcd_dvd2 [iff]: "gcd a b dvd b"
     and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
+    and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
+    and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
+begin    
+
+lemma gcd_greatest_iff [simp]:
+  "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
+  by (blast intro!: gcd_greatest intro: dvd_trans)
+
+lemma gcd_dvdI1:
+  "a dvd c \<Longrightarrow> gcd a b dvd c"
+  by (rule dvd_trans) (rule gcd_dvd1)
+
+lemma gcd_dvdI2:
+  "b dvd c \<Longrightarrow> gcd a b dvd c"
+  by (rule dvd_trans) (rule gcd_dvd2)
+
+lemma gcd_0_left [simp]:
+  "gcd 0 a = normalize a"
+  by (rule associated_eqI) simp_all
+
+lemma gcd_0_right [simp]:
+  "gcd a 0 = normalize a"
+  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")
+proof
+  assume ?P then have "0 dvd gcd a b" by simp
+  then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+
+  then show ?Q by simp
+next
+  assume ?Q then show ?P by simp
+qed
+
+lemma unit_factor_gcd:
+  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
+proof (cases "gcd a b = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
+    by (rule unit_factor_mult_normalize)
+  then have "unit_factor (gcd a b) * gcd a b = gcd a b"
+    by simp
+  then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
+    by simp
+  with False show ?thesis by simp
+qed
+
+lemma is_unit_gcd [simp]:
+  "is_unit (gcd a b) \<longleftrightarrow> coprime a b"
+  by (cases "a = 0 \<and> b = 0") (auto simp add: unit_factor_gcd dest: is_unit_unit_factor)
+
+sublocale gcd!: abel_semigroup gcd
+proof
+  fix a b c
+  show "gcd a b = gcd b a"
+    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"
+    by (rule dvd_trans) simp
+  ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
+    by (auto intro!: gcd_greatest)
+  from gcd_dvd2 have "gcd a (gcd b c) dvd b"
+    by (rule dvd_trans) simp
+  moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
+    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 show "gcd (gcd a b) c = gcd a (gcd b c)"
+    by (rule associated_eqI) simp_all
+qed
+
+lemma gcd_self [simp]:
+  "gcd a a = normalize a"
+proof -
+  have "a dvd gcd a a"
+    by (rule gcd_greatest) simp_all
+  then show ?thesis
+    by (auto intro: associated_eqI)
+qed
+    
+lemma coprime_1_left [simp]:
+  "coprime 1 a"
+  by (rule associated_eqI) simp_all
+
+lemma coprime_1_right [simp]:
+  "coprime a 1"
+  using coprime_1_left [of a] by (simp add: ac_simps)
+
+lemma gcd_mult_left:
+  "gcd (c * a) (c * b) = normalize c * gcd a b"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  then have "c * gcd a b dvd gcd (c * a) (c * b)"
+    by (auto intro: gcd_greatest)
+  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 (auto intro: associated_eqI)
+  then show ?thesis by (simp add: normalize_mult)
+qed
+
+lemma gcd_mult_right:
+  "gcd (a * c) (b * c) = gcd b a * normalize c"
+  using gcd_mult_left [of c a b] by (simp add: ac_simps)
+
+lemma mult_gcd_left:
+  "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
+  by (simp add: gcd_mult_left mult.assoc [symmetric])
+
+lemma mult_gcd_right:
+  "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
+  using mult_gcd_left [of c a b] by (simp add: ac_simps)
+
+lemma dvd_lcm1 [iff]:
+  "a dvd lcm a b"
+proof -
+  have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
+    by (simp add: lcm_gcd normalize_mult div_mult_swap)
+  then show ?thesis
+    by (simp add: lcm_gcd)
+qed
+  
+lemma dvd_lcm2 [iff]:
+  "b dvd lcm a b"
+proof -
+  have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
+    by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
+  then show ?thesis
+    by (simp add: lcm_gcd)
+qed
+
+lemma dvd_lcmI1:
+  "a dvd b \<Longrightarrow> a dvd lcm b c"
+  by (rule dvd_trans) (assumption, blast) 
+
+lemma dvd_lcmI2:
+  "a dvd c \<Longrightarrow> a dvd lcm b c"
+  by (rule dvd_trans) (assumption, blast)
+
+lemma lcm_least:
+  assumes "a dvd c" and "b dvd c"
+  shows "lcm a b dvd c"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False then have U: "is_unit (unit_factor c)" by simp
+  show ?thesis
+  proof (cases "gcd a b = 0")
+    case True with assms show ?thesis by simp
+  next
+    case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
+    with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
+      by (simp_all add: mult_dvd_mono)
+    then have "normalize (a * b) dvd gcd (a * c) (b * c)"
+      by (auto intro: gcd_greatest simp add: ac_simps)
+    then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
+      using U by (simp add: dvd_mult_unit_iff)
+    then have "normalize (a * b) dvd gcd a b * c"
+      by (simp add: mult_gcd_right [of a b c])
+    then have "normalize (a * b) div gcd a b dvd c"
+      using False by (simp add: div_dvd_iff_mult ac_simps)
+    then show ?thesis by (simp add: lcm_gcd)
+  qed
+qed
+
+lemma lcm_least_iff [simp]:
+  "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
+  by (blast intro!: lcm_least intro: dvd_trans)
+
+lemma normalize_lcm [simp]:
+  "normalize (lcm a b) = lcm a b"
+  by (simp add: lcm_gcd dvd_normalize_div)
+
+lemma lcm_0_left [simp]:
+  "lcm 0 a = 0"
+  by (simp add: lcm_gcd)
+  
+lemma lcm_0_right [simp]:
+  "lcm a 0 = 0"
+  by (simp add: lcm_gcd)
+
+lemma lcm_eq_0_iff:
+  "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then have "0 dvd lcm a b" by simp
+  then have "0 dvd normalize (a * b) div gcd a b"
+    by (simp add: lcm_gcd)
+  then have "0 * gcd a b dvd normalize (a * b)"
+    using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
+  then have "normalize (a * b) = 0"
+    by simp
+  then show ?Q by simp
+next
+  assume ?Q then show ?P by auto
+qed
+
+lemma unit_factor_lcm :
+  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
+  by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
+
+sublocale lcm!: abel_semigroup lcm
+proof
+  fix a b c
+  show "lcm a b = lcm b a"
+    by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
+  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
+qed
+
+lemma lcm_self [simp]:
+  "lcm a a = normalize a"
+proof -
+  have "lcm a a dvd a"
+    by (rule lcm_least) simp_all
+  then show ?thesis
+    by (auto intro: associated_eqI)
+qed
+
+lemma gcd_mult_lcm [simp]:
+  "gcd a b * lcm a b = normalize a * normalize b"
+  by (simp add: lcm_gcd normalize_mult)
+
+lemma lcm_mult_gcd [simp]:
+  "lcm a b * gcd a b = normalize a * normalize b"
+  using gcd_mult_lcm [of a b] by (simp add: ac_simps) 
+
+lemma gcd_lcm:
+  assumes "a \<noteq> 0" and "b \<noteq> 0"
+  shows "gcd a b = normalize (a * b) div lcm a b"
+proof -
+  from assms have "lcm a b \<noteq> 0"
+    by (simp add: lcm_eq_0_iff)
+  have "gcd a b * lcm a b = normalize a * normalize b" by simp
+  then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
+    by (simp_all add: normalize_mult)
+  with \<open>lcm a b \<noteq> 0\<close> show ?thesis
+    using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
+qed
+
+lemma lcm_1_left [simp]:
+  "lcm 1 a = normalize a"
+  by (simp add: lcm_gcd)
+
+lemma lcm_1_right [simp]:
+  "lcm a 1 = normalize a"
+  by (simp add: lcm_gcd)
+  
+lemma lcm_mult_left:
+  "lcm (c * a) (c * b) = normalize c * lcm a b"
+  by (cases "c = 0")
+    (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
+      simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
+
+lemma lcm_mult_right:
+  "lcm (a * c) (b * c) = lcm b a * normalize c"
+  using lcm_mult_left [of c a b] by (simp add: ac_simps)
+
+lemma mult_lcm_left:
+  "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
+  by (simp add: lcm_mult_left mult.assoc [symmetric])
+
+lemma mult_lcm_right:
+  "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
+  using mult_lcm_left [of c a b] by (simp add: ac_simps)
+  
+end
+
+class semiring_Gcd = semiring_gcd + Gcd +
+  assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
+    and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
+    and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
+begin
+
+lemma Gcd_empty [simp]:
+  "Gcd {} = 0"
+  by (rule dvd_0_left, rule Gcd_greatest) simp
+
+lemma Gcd_0_iff [simp]:
+  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  show ?Q
+  proof
+    fix a
+    assume "a \<in> A"
+    then have "Gcd A dvd a" by (rule Gcd_dvd)
+    with \<open>?P\<close> have "a = 0" by simp
+    then show "a \<in> {0}" by simp
+  qed
+next
+  assume ?Q
+  have "0 dvd Gcd A"
+  proof (rule Gcd_greatest)
+    fix a
+    assume "a \<in> A"
+    with \<open>?Q\<close> have "a = 0" by auto
+    then show "0 dvd a" by simp
+  qed
+  then show ?P by simp
+qed
+
+lemma unit_factor_Gcd:
+  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
+proof (cases "Gcd A = 0")
+  case True then show ?thesis by auto
+next
+  case False
+  from unit_factor_mult_normalize
+  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
+  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
+  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
+  with False have "unit_factor (Gcd A) = 1" by simp
+  with False show ?thesis by auto
+qed
+
+lemma Gcd_UNIV [simp]:
+  "Gcd UNIV = 1"
+  by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd)
+
+lemma Gcd_eq_1_I:
+  assumes "is_unit a" and "a \<in> A"
+  shows "Gcd A = 1"
+proof -
+  from assms have "is_unit (Gcd A)"
+    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
+  then have "normalize (Gcd A) = 1"
+    by (rule is_unit_normalize)
+  then show ?thesis
+    by simp
+qed
+
+lemma Gcd_insert [simp]:
+  "Gcd (insert a A) = gcd a (Gcd A)"
+proof -
+  have "Gcd (insert a A) dvd gcd a (Gcd A)"
+    by (auto intro: Gcd_dvd Gcd_greatest)
+  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
+  proof (rule Gcd_greatest)
+    fix b
+    assume "b \<in> insert a A"
+    then show "gcd a (Gcd A) dvd b"
+    proof
+      assume "b = a" then show ?thesis by simp
+    next
+      assume "b \<in> A"
+      then have "Gcd A dvd b" by (rule Gcd_dvd)
+      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
+      ultimately show ?thesis by (blast intro: dvd_trans)
+    qed
+  qed
+  ultimately show ?thesis
+    by (auto intro: associated_eqI)
+qed
+
+lemma dvd_Gcd: -- \<open>FIXME remove\<close>
+  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
+  by (blast intro: Gcd_greatest)
+
+lemma Gcd_set [code_unfold]:
+  "Gcd (set as) = foldr gcd as 0"
+  by (induct as) simp_all
+
+end  
+
+class semiring_Lcm = semiring_Gcd +
+  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
+begin
+
+lemma dvd_Lcm:
+  assumes "a \<in> A"
+  shows "a dvd Lcm A"
+  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
+
+lemma Gcd_image_normalize [simp]:
+  "Gcd (normalize ` A) = Gcd A"
+proof -
+  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
+  proof -
+    from that obtain B where "A = insert a B" by blast
+    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
+      by (rule gcd_dvd1)
+    ultimately show "Gcd (normalize ` A) dvd a"
+      by simp
+  qed
+  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 (auto intro: associated_eqI)
+qed
+
+lemma Lcm_least:
+  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
+  shows "Lcm A dvd a"
+  using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd)
+
+lemma normalize_Lcm [simp]:
+  "normalize (Lcm A) = Lcm A"
+  by (simp add: Lcm_Gcd)
+
+lemma unit_factor_Lcm:
+  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
+proof (cases "Lcm A = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
+    by blast
+  with False show ?thesis
+    by simp
+qed
+  
+lemma Lcm_empty [simp]:
+  "Lcm {} = 1"
+  by (simp add: Lcm_Gcd)
+
+lemma Lcm_1_iff [simp]:
+  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  show ?Q
+  proof
+    fix a
+    assume "a \<in> A"
+    then have "a dvd Lcm A"
+      by (rule dvd_Lcm)
+    with \<open>?P\<close> show "is_unit a"
+      by simp
+  qed
+next
+  assume ?Q
+  then have "is_unit (Lcm A)"
+    by (blast intro: Lcm_least)
+  then have "normalize (Lcm A) = 1"
+    by (rule is_unit_normalize)
+  then show ?P
+    by simp
+qed
+
+lemma Lcm_UNIV [simp]:
+  "Lcm UNIV = 0"
+proof -
+  have "0 dvd Lcm UNIV"
+    by (rule dvd_Lcm) simp
+  then show ?thesis
+    by simp
+qed
+
+lemma Lcm_eq_0_I:
+  assumes "0 \<in> A"
+  shows "Lcm A = 0"
+proof -
+  from assms have "0 dvd Lcm A"
+    by (rule dvd_Lcm)
+  then show ?thesis
+    by simp
+qed
+
+lemma Gcd_Lcm:
+  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
+  by (rule associated_eqI) (auto intro: associatedI Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least
+    simp add: unit_factor_Gcd unit_factor_Lcm)
+
+lemma Lcm_insert [simp]:
+  "Lcm (insert a A) = lcm a (Lcm A)"
+proof (rule sym)
+  have "lcm a (Lcm A) dvd Lcm (insert a A)"
+    by (auto intro: dvd_Lcm Lcm_least)
+  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
+  proof (rule Lcm_least)
+    fix b
+    assume "b \<in> insert a A"
+    then show "b dvd lcm a (Lcm A)"
+    proof
+      assume "b = a" then show ?thesis by simp
+    next
+      assume "b \<in> A"
+      then have "b dvd Lcm A" by (rule dvd_Lcm)
+      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
+      ultimately show ?thesis by (blast intro: dvd_trans)
+    qed
+  qed
+  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]:
+  "Lcm (set as) = foldr lcm as 1"
+  by (induct as) simp_all
+  
+end
 
 class ring_gcd = comm_ring_1 + semiring_gcd
 
@@ -229,7 +731,7 @@
   by simp
 
 lemma gcd_Suc_0 [simp]: "gcd (m::nat) (Suc 0) = Suc 0"
-  by (simp add: One_nat_def)
+  by simp
 
 lemma gcd_1_int [simp]: "gcd (m::int) 1 = 1"
   by (simp add: gcd_int_def)
@@ -265,10 +767,11 @@
   assume "k dvd m" and "k dvd n"
   then show "k dvd gcd m n"
     by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
-qed
+qed (simp_all add: lcm_nat_def)
 
 instance int :: ring_gcd
-  by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
+  by standard
+    (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def lcm_int_def zdiv_int nat_abs_mult_distrib [symmetric] lcm_gcd gcd_greatest)
 
 lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   by (metis gcd_dvd1 dvd_trans)
@@ -294,18 +797,21 @@
 lemma gcd_le2_int [simp]: "b > 0 \<Longrightarrow> gcd (a::int) b \<le> b"
   by (rule zdvd_imp_le, auto)
 
-lemma gcd_greatest_iff_nat [iff]: "(k dvd gcd (m::nat) n) =
-    (k dvd m & k dvd n)"
-  by (blast intro!: gcd_greatest intro: dvd_trans)
+lemma gcd_greatest_iff_nat:
+  "(k dvd gcd (m::nat) n) = (k dvd m & k dvd n)"
+  by (fact gcd_greatest_iff)
+
+lemma gcd_greatest_iff_int:
+  "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
+  by (fact gcd_greatest_iff)
 
-lemma gcd_greatest_iff_int: "((k::int) dvd gcd m n) = (k dvd m & k dvd n)"
-  by (blast intro!: gcd_greatest intro: dvd_trans)
+lemma gcd_zero_nat: 
+  "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
+  by (fact gcd_eq_0_iff)
 
-lemma gcd_zero_nat [simp]: "(gcd (m::nat) n = 0) = (m = 0 & n = 0)"
-  by (simp only: dvd_0_left_iff [symmetric] gcd_greatest_iff_nat)
-
-lemma gcd_zero_int [simp]: "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
-  by (auto simp add: gcd_int_def)
+lemma gcd_zero_int [simp]:
+  "(gcd (m::int) n = 0) = (m = 0 & n = 0)"
+  by (fact gcd_eq_0_iff)
 
 lemma gcd_pos_nat [simp]: "(gcd (m::nat) n > 0) = (m ~= 0 | n ~= 0)"
   by (insert gcd_zero_nat [of m n], arith)
@@ -332,21 +838,19 @@
 
 interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
   + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
-apply default
-apply (auto intro: dvd_antisym dvd_trans)[4]
+apply standard
+apply (auto intro: dvd_antisym dvd_trans)[2]
 apply (metis dvd.dual_order.refl gcd_unique_nat)+
 done
 
-interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
-proof
-qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
+interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" ..
 
-lemmas gcd_assoc_nat = gcd_nat.assoc
-lemmas gcd_commute_nat = gcd_nat.commute
-lemmas gcd_left_commute_nat = gcd_nat.left_commute
-lemmas gcd_assoc_int = gcd_int.assoc
-lemmas gcd_commute_int = gcd_int.commute
-lemmas gcd_left_commute_int = gcd_int.left_commute
+lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
+lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
+lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
+lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
+lemmas gcd_commute_int = gcd.commute [where ?'a = int]
+lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
 
 lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
 
@@ -383,23 +887,29 @@
   apply auto
 done
 
-lemma coprime_dvd_mult_nat: "coprime (k::nat) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
-  apply (insert gcd_mult_distrib_nat [of m k n])
-  apply simp
-  apply (erule_tac t = m in ssubst)
-  apply simp
-  done
+context semiring_gcd
+begin
 
-lemma coprime_dvd_mult_int:
-  "coprime (k::int) n \<Longrightarrow> k dvd m * n \<Longrightarrow> k dvd m"
-apply (subst abs_dvd_iff [symmetric])
-apply (subst dvd_abs_iff [symmetric])
-apply (subst (asm) gcd_abs_int)
-apply (rule coprime_dvd_mult_nat [transferred])
-    prefer 4 apply assumption
-   apply auto
-apply (subst abs_mult [symmetric], auto)
-done
+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
+
+end
+
+lemmas coprime_dvd_mult_nat = coprime_dvd_mult [where ?'a = nat]
+lemmas coprime_dvd_mult_int = coprime_dvd_mult [where ?'a = int]
 
 lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
     (k dvd m * n) = (k dvd m)"
@@ -409,21 +919,22 @@
     (k dvd m * n) = (k dvd m)"
   by (auto intro: coprime_dvd_mult_int)
 
-lemma gcd_mult_cancel_nat: "coprime k n \<Longrightarrow> gcd ((k::nat) * m) n = gcd m n"
-  apply (rule dvd_antisym)
+context semiring_gcd
+begin
+
+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 n = k in coprime_dvd_mult_nat)
-  apply (simp add: gcd_assoc_nat)
-  apply (simp add: gcd_commute_nat)
-  apply (simp_all add: mult.commute)
-done
+  apply (rule_tac b = c in coprime_dvd_mult)
+  apply (simp add: gcd.assoc)
+  apply (simp_all add: ac_simps)
+  done
 
-lemma gcd_mult_cancel_int:
-  "coprime (k::int) n \<Longrightarrow> gcd (k * m) n = gcd m n"
-apply (subst (1 2) gcd_abs_int)
-apply (subst abs_mult)
-apply (rule gcd_mult_cancel_nat [transferred], auto)
-done
+end  
+
+lemmas gcd_mult_cancel_nat = gcd_mult_cancel [where ?'a = nat] 
+lemmas gcd_mult_cancel_int = gcd_mult_cancel [where ?'a = int] 
 
 lemma coprime_crossproduct_nat:
   fixes a b c d :: nat
@@ -516,8 +1027,7 @@
 (* to do: differences, and all variations of addition rules
     as simplification rules for nat and int *)
 
-(* FIXME remove iff *)
-lemma gcd_dvd_prod_nat [iff]: "gcd (m::nat) n dvd k * n"
+lemma gcd_dvd_prod_nat: "gcd (m::nat) n dvd k * n"
   using mult_dvd_mono [of 1] by auto
 
 (* to do: add the three variations of these, and for ints? *)
@@ -577,8 +1087,11 @@
 
 subsection {* Coprimality *}
 
-lemma div_gcd_coprime_nat:
-  assumes nz: "(a::nat) \<noteq> 0 \<or> b \<noteq> 0"
+context semiring_gcd
+begin
+
+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"
@@ -596,29 +1109,22 @@
     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
-  then have gp: "?g > 0" by arith
-  from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
-  with dvd_mult_cancel1 [OF gp] show "?g' = 1" by simp
+  moreover from gcd_greatest [OF dvdgg'] have "?g * ?g' dvd ?g" .
+  thm dvd_mult_cancel_left
+  ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
 qed
 
-lemma div_gcd_coprime_int:
-  assumes nz: "(a::int) \<noteq> 0 \<or> b \<noteq> 0"
-  shows "coprime (a div gcd a b) (b div gcd a b)"
-apply (subst (1 2 3) gcd_abs_int)
-apply (subst (1 2) abs_div)
-  apply simp
- apply simp
-apply(subst (1 2) abs_gcd_int)
-apply (rule div_gcd_coprime_nat [transferred])
-using nz apply (auto simp add: gcd_abs_int [symmetric])
-done
+end
+
+lemmas div_gcd_coprime_nat = div_gcd_coprime [where ?'a = nat]
+lemmas div_gcd_coprime_int = div_gcd_coprime [where ?'a = int]
 
 lemma coprime_nat: "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   using gcd_unique_nat[of 1 a b, simplified] by auto
 
 lemma coprime_Suc_0_nat:
     "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
-  using coprime_nat by (simp add: One_nat_def)
+  using coprime_nat by simp
 
 lemma coprime_int: "coprime (a::int) b \<longleftrightarrow>
     (\<forall>d. d >= 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
@@ -667,22 +1173,23 @@
   using z apply force
   done
 
-lemma coprime_mult_nat: assumes da: "coprime (d::nat) a" and db: "coprime d b"
-    shows "coprime d (a * b)"
-  apply (subst gcd_commute_nat)
-  using da apply (subst gcd_mult_cancel_nat)
-  apply (subst gcd_commute_nat, assumption)
-  apply (subst gcd_commute_nat, rule db)
-done
+context semiring_gcd
+begin
 
-lemma coprime_mult_int: assumes da: "coprime (d::int) a" and db: "coprime d b"
-    shows "coprime d (a * b)"
-  apply (subst gcd_commute_int)
-  using da apply (subst gcd_mult_cancel_int)
-  apply (subst gcd_commute_int, assumption)
-  apply (subst gcd_commute_int, rule db)
-done
+lemma coprime_mult:
+  assumes da: "coprime d a" and db: "coprime d b"
+  shows "coprime d (a * b)"
+  apply (subst gcd.commute)
+  using da apply (subst gcd_mult_cancel)
+  apply (subst gcd.commute, assumption)
+  apply (subst gcd.commute, rule db)
+  done
 
+end
+
+lemmas coprime_mult_nat = coprime_mult [where ?'a = nat]
+lemmas coprime_mult_int = coprime_mult [where ?'a = int]
+  
 lemma coprime_lmult_nat:
   assumes dab: "coprime (d::nat) (a * b)" shows "coprime d a"
 proof -
@@ -761,20 +1268,41 @@
 lemma coprime_exp_int: "coprime (d::int) a \<Longrightarrow> coprime d (a^n)"
   by (induct n) (simp_all add: coprime_mult_int)
 
+context semiring_gcd
+begin
+
+lemma coprime_exp_left:
+  assumes "coprime a b"
+  shows "coprime (a ^ n) b"
+  using assms 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
+
+end
+
 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
-  by (simp add: coprime_exp_nat gcd_nat.commute)
+  by (fact coprime_exp2)
 
 lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
-  by (simp add: coprime_exp_int gcd_int.commute)
+  by (fact coprime_exp2)
 
-lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
-proof (cases)
-  assume "a = 0 & b = 0"
-  thus ?thesis by simp
-  next assume "~(a = 0 & b = 0)"
-  hence "coprime ((a div gcd a b)^n) ((b div gcd a b)^n)"
-    by (auto simp:div_gcd_coprime_nat)
-  hence "gcd ((a div gcd a b)^n * (gcd a b)^n)
+lemma gcd_exp_nat:
+  "gcd ((a :: nat) ^ n) (b ^ n) = gcd a b ^ n"
+proof (cases "a = 0 \<and> b = 0")
+  case True then show ?thesis by (cases "n > 0") (simp_all add: zero_power)
+next
+  case False
+  then have "coprime (a div gcd a b) (b div gcd a b)"
+    by (auto simp: div_gcd_coprime)
+  then have "coprime ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
+    by (simp add: coprime_exp2)
+  then have "gcd ((a div gcd a b)^n * (gcd a b)^n)
       ((b div gcd a b)^n * (gcd a b)^n) = (gcd a b)^n"
     by (metis gcd_mult_distrib_nat mult.commute mult.right_neutral)
   also have "(a div gcd a b)^n * (gcd a b)^n = a^n"
@@ -829,7 +1357,7 @@
     with dc have th0: "a' dvd b*c"
       using dvd_trans[of a' a "b*c"] by simp
     from dc ab'(1,2) have "a'*?g dvd (b'*?g) *c" by auto
-    hence "?g*a' dvd ?g * (b' * c)" by (simp add: mult.assoc)
+    hence "?g*a' dvd ?g * (b' * c)" by (simp add: ac_simps)
     with z have th_1: "a' dvd b' * c" by auto
     from coprime_dvd_mult_int[OF ab'(3)] th_1
     have thc: "a' dvd c" by (subst (asm) mult.commute, blast)
@@ -927,13 +1455,13 @@
 qed
 
 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
-  by (simp add: gcd_nat.commute)
+  by (simp add: gcd.commute del: One_nat_def)
 
 lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
-  using coprime_plus_one_nat by (simp add: One_nat_def)
+  using coprime_plus_one_nat by simp
 
 lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
-  by (simp add: gcd_int.commute)
+  by (simp add: gcd.commute)
 
 lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
   using coprime_plus_one_nat [of "n - 1"]
@@ -958,12 +1486,12 @@
 done
 
 lemma coprime_common_divisor_nat: 
-    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
+  "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
   by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
 
 lemma coprime_common_divisor_int:
-    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
-  using gcd_greatest by fastforce
+  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
+  using gcd_greatest_iff [of x a b] by auto
 
 lemma coprime_divisors_nat:
     "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
@@ -1266,77 +1794,23 @@
 lemma lcm_least_nat:
   assumes "(m::nat) dvd k" and "n dvd k"
   shows "lcm m n dvd k"
-proof (cases k)
-  case 0 then show ?thesis by auto
-next
-  case (Suc _) then have pos_k: "k > 0" by auto
-  from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
-  with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
-  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
-  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
-  from pos_k k_m have pos_p: "p > 0" by auto
-  from pos_k k_n have pos_q: "q > 0" by auto
-  have "k * k * gcd q p = k * gcd (k * q) (k * p)"
-    by (simp add: ac_simps gcd_mult_distrib_nat)
-  also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
-    by (simp add: k_m [symmetric] k_n [symmetric])
-  also have "\<dots> = k * p * q * gcd m n"
-    by (simp add: ac_simps gcd_mult_distrib_nat)
-  finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
-    by (simp only: k_m [symmetric] k_n [symmetric])
-  then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
-    by (simp add: ac_simps)
-  with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
-    by simp
-  with prod_gcd_lcm_nat [of m n]
-  have "lcm m n * gcd q p * gcd m n = k * gcd m n"
-    by (simp add: ac_simps)
-  with pos_gcd have "lcm m n * gcd q p = k" by auto
-  then show ?thesis using dvd_def by auto
-qed
+  using assms by (rule lcm_least)
 
 lemma lcm_least_int:
   "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
-apply (subst lcm_abs_int)
-apply (rule dvd_trans)
-apply (rule lcm_least_nat [transferred, of _ "abs k" _])
-apply auto
-done
+  by (rule lcm_least)
 
 lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
-proof (cases m)
-  case 0 then show ?thesis by simp
-next
-  case (Suc _)
-  then have mpos: "m > 0" by simp
-  show ?thesis
-  proof (cases n)
-    case 0 then show ?thesis by simp
-  next
-    case (Suc _)
-    then have npos: "n > 0" by simp
-    have "gcd m n dvd n" by simp
-    then obtain k where "n = gcd m n * k" using dvd_def by auto
-    then have "m * n div gcd m n = m * (gcd m n * k) div gcd m n"
-      by (simp add: ac_simps)
-    also have "\<dots> = m * k" using mpos npos gcd_zero_nat by simp
-    finally show ?thesis by (simp add: lcm_nat_def)
-  qed
-qed
+  by (fact dvd_lcm1)
 
 lemma lcm_dvd1_int: "(m::int) dvd lcm m n"
-  apply (subst lcm_abs_int)
-  apply (rule dvd_trans)
-  prefer 2
-  apply (rule lcm_dvd1_nat [transferred])
-  apply auto
-done
+  by (fact dvd_lcm1)
 
 lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
-  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
+  by (fact dvd_lcm2)
 
 lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
-  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
+  by (fact dvd_lcm2)
 
 lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
 by(metis lcm_dvd1_nat dvd_trans)
@@ -1360,33 +1834,16 @@
 
 interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
   + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
-proof
-  fix n m p :: nat
-  show "lcm (lcm n m) p = lcm n (lcm m p)"
-    by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
-  show "lcm m n = lcm n m"
-    by (simp add: lcm_nat_def gcd_commute_nat field_simps)
-  show "lcm m m = m"
-    by (metis dvd.order_refl lcm_unique_nat)
-  show "lcm m 1 = m"
-    by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
-qed
+  by standard (simp_all del: One_nat_def)
+
+interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
 
-interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
-proof
-  fix n m p :: int
-  show "lcm (lcm n m) p = lcm n (lcm m p)"
-    by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
-  show "lcm m n = lcm n m"
-    by (simp add: lcm_int_def lcm_nat.commute)
-qed
-
-lemmas lcm_assoc_nat = lcm_nat.assoc
-lemmas lcm_commute_nat = lcm_nat.commute
-lemmas lcm_left_commute_nat = lcm_nat.left_commute
-lemmas lcm_assoc_int = lcm_int.assoc
-lemmas lcm_commute_int = lcm_int.commute
-lemmas lcm_left_commute_int = lcm_int.left_commute
+lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
+lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
+lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
+lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
+lemmas lcm_commute_int = lcm.commute [where ?'a = int]
+lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
 
 lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
 lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
@@ -1452,16 +1909,10 @@
 subsection {* The complete divisibility lattice *}
 
 interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
-proof (default, goals)
-  case 3
-  thus ?case by(metis gcd_unique_nat)
-qed auto
+  by standard simp_all
 
 interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
-proof (default, goals)
-  case 3
-  thus ?case by(metis lcm_unique_nat)
-qed auto
+  by standard simp_all
 
 interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
 
@@ -1469,10 +1920,6 @@
 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
 *}
 
-class Gcd = gcd +
-  fixes Gcd :: "'a set \<Rightarrow> 'a"
-  fixes Lcm :: "'a set \<Rightarrow> 'a"
-
 instantiation nat :: Gcd
 begin
 
@@ -1487,11 +1934,11 @@
 
 lemma Lcm_nat_empty:
   "Lcm {} = (1::nat)"
-  by (simp add: Lcm_nat_def)
+  by (simp add: Lcm_nat_def del: One_nat_def)
 
 lemma Lcm_nat_insert:
   "Lcm (insert n M) = lcm (n::nat) (Lcm M)"
-  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite)
+  by (cases "finite M") (simp_all add: Lcm_nat_def Lcm_nat_infinite del: One_nat_def)
 
 definition
   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
@@ -1500,22 +1947,6 @@
 
 end
 
-class semiring_Gcd = semiring_gcd + Gcd +
-  assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
-    and dvd_Gcd: "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
-    and Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
-begin
-
-lemma Gcd_empty [simp]:
-  "Gcd {} = 0"
-  by (rule dvd_0_left, rule dvd_Gcd) simp
-
-lemma Gcd_set [code_unfold]:
-  "Gcd (set as) = foldr gcd as 0"
-  by (induct as) simp_all
-  
-end
-
 lemma dvd_Lcm_nat [simp]:
   fixes M :: "nat set"
   assumes "m \<in> M"
@@ -1544,25 +1975,7 @@
   and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
 proof -
   show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
-  proof (default, goals)
-    case 1
-    thus ?case by (simp add: Gcd_nat_def)
-  next
-    case 2
-    thus ?case by (simp add: Gcd_nat_def)
-  next
-    case 5
-    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
-  next
-    case 6
-    show ?case by (simp add: Lcm_nat_empty)
-  next
-    case 3
-    thus ?case by simp
-  next
-    case 4
-    thus ?case by simp
-  qed
+    by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
   then interpret gcd_lcm_complete_lattice_nat:
     complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
   from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
@@ -1590,13 +2003,37 @@
   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
     using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
 next
-  show "n dvd Gcd N" if "\<forall>m\<in>N. n dvd m" for N and n :: nat
+  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
     using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
 next
-  show "Gcd (insert n N) = gcd n (Gcd N)" for N and n :: nat
+  show "normalize (Gcd N) = Gcd N" for N :: "nat set"
     by simp
 qed
 
+instance nat :: semiring_Lcm
+proof
+  have uf: "unit_factor (Lcm N) = 1" if "0 < Lcm N" for N :: "nat set"
+  proof (cases "finite N")
+    case False with that show ?thesis by (simp add: Lcm_nat_infinite)
+  next
+    case True then show ?thesis
+    using that proof (induct N)
+      case empty then show ?case by simp
+    next
+      case (insert n N)
+      have "lcm n (Lcm N) \<noteq> 0 \<longleftrightarrow> n \<noteq> 0 \<and> Lcm N \<noteq> 0"
+        using lcm_eq_0_iff [of n "Lcm N"] by simp
+      then have "lcm n (Lcm N) > 0 \<longleftrightarrow> n > 0 \<and> Lcm N > 0"
+        unfolding neq0_conv .
+      with insert show ?case
+        by (simp add: Lcm_nat_insert unit_factor_lcm)
+    qed
+  qed
+  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
+    by (rule associated_eqI) (auto intro!: associatedI Gcd_dvd Gcd_greatest
+      simp add: unit_factor_Gcd uf)
+qed
+
 text{* Alternative characterizations of Gcd: *}
 
 lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
@@ -1654,7 +2091,7 @@
 lemma mult_inj_if_coprime_nat:
   "inj_on f A \<Longrightarrow> inj_on g B \<Longrightarrow> ALL a:A. ALL b:B. coprime (f a) (g b)
    \<Longrightarrow> inj_on (%(a,b). f a * g b::nat) (A \<times> B)"
-apply(auto simp add:inj_on_def)
+apply (auto simp add: inj_on_def simp del: One_nat_def)
 apply (metis coprime_dvd_mult_iff_nat dvd.neq_le_trans dvd_triv_left)
 apply (metis gcd_semilattice_nat.inf_commute coprime_dvd_mult_iff_nat
              dvd.neq_le_trans dvd_triv_right mult.commute)
@@ -1682,8 +2119,36 @@
   "Gcd M = int (Gcd (nat ` abs ` M))"
 
 instance ..
+
 end
 
+instance int :: semiring_Gcd
+  by standard (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def Lcm_int_def int_dvd_iff dvd_int_iff
+    dvd_int_unfold_dvd_nat [symmetric])
+
+instance int :: semiring_Lcm
+proof
+  fix K :: "int set"
+  have "{n. \<forall>k\<in>K. nat \<bar>k\<bar> dvd n} = ((\<lambda>k. nat \<bar>k\<bar>) ` {l. \<forall>k\<in>K. k dvd l})"
+  proof (rule set_eqI)
+    fix n
+    have "(\<forall>k\<in>K. nat \<bar>k\<bar> dvd n) \<longleftrightarrow> (\<exists>l. (\<forall>k\<in>K. k dvd l) \<and> n = nat \<bar>l\<bar>)" (is "?P \<longleftrightarrow> ?Q")
+    proof
+      assume ?P
+      then have "(\<forall>k\<in>K. k dvd int n) \<and> n = nat \<bar>int n\<bar>"
+        by (auto simp add: dvd_int_unfold_dvd_nat)
+      then show ?Q by blast
+    next
+      assume ?Q then show ?P
+        by (auto simp add: dvd_int_unfold_dvd_nat)
+    qed
+    then show "n \<in> {n. \<forall>k\<in>K. nat \<bar>k\<bar> dvd n} \<longleftrightarrow> n \<in> (\<lambda>k. nat \<bar>k\<bar>) ` {l. \<forall>k\<in>K. k dvd l}"
+      by auto
+  qed
+  then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
+    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd)
+qed
+
 lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
   by (simp add: Lcm_int_def)
 
@@ -1692,7 +2157,7 @@
   by (simp add: Lcm_int_def lcm_int_def)
 
 lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
-  by (simp add: zdvd_int)
+  by (fact dvd_int_unfold_dvd_nat)
 
 lemma dvd_Lcm_int [simp]:
   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
@@ -1703,9 +2168,6 @@
   assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   using assms by (simp add: Lcm_int_def dvd_int_iff)
 
-instance int :: semiring_Gcd
-  by intro_classes (simp_all add: Gcd_int_def gcd_int_def dvd_int_iff Gcd_dvd dvd_Gcd)
-  
 lemma Lcm_set_int [code, code_unfold]:
   "Lcm (set xs) = fold lcm xs (1::int)"
   by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)

--- a/src/HOL/Library/Poly_Deriv.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Library/Poly_Deriv.thy	Thu Jul 09 16:49:08 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)))"

--- a/src/HOL/Library/Polynomial.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Library/Polynomial.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -7,7 +7,7 @@
 section \<open>Polynomials as type over a ring structure\<close>
 
 theory Polynomial
-imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
+imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
 begin
 
 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
@@ -1495,6 +1495,63 @@
   shows "monom (coeff p (degree p)) 0 = p"
   using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
 
+lemma is_unit_polyE:
+  assumes "is_unit p"
+  obtains a where "p = monom a 0" and "a \<noteq> 0"
+proof -
+  obtain a q where "p = pCons a q" by (cases p)
+  with assms have "p = [:a:]" and "a \<noteq> 0"
+    by (simp_all add: is_unit_pCons_iff)
+  with that show thesis by (simp add: monom_0)
+qed
+
+instantiation poly :: (field) normalization_semidom
+begin
+
+definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
+  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
+
+definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
+  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
+
+instance
+proof
+  fix p :: "'a poly"
+  show "unit_factor p * normalize p = p"
+    by (simp add: normalize_poly_def unit_factor_poly_def)
+      (simp only: mult_smult_left [symmetric] smult_monom, simp)
+next
+  show "normalize 0 = (0::'a poly)"
+    by (simp add: normalize_poly_def)
+next
+  show "unit_factor 0 = (0::'a poly)"
+    by (simp add: unit_factor_poly_def)
+next
+  fix p :: "'a poly"
+  assume "is_unit p"
+  then obtain a where "p = monom a 0" and "a \<noteq> 0"
+    by (rule is_unit_polyE)
+  then show "normalize p = 1"
+    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
+next
+  fix p q :: "'a poly"
+  assume "q \<noteq> 0"
+  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
+    by (auto intro: is_unit_monom_0)
+  then show "is_unit (unit_factor q)"
+    by (simp add: unit_factor_poly_def)
+next
+  fix p q :: "'a poly"
+  have "monom (coeff (p * q) (degree (p * q))) 0 =
+    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
+    by (simp add: monom_0 coeff_degree_mult)
+  then show "unit_factor (p * q) =
+    unit_factor p * unit_factor q"
+    by (simp add: unit_factor_poly_def)
+qed
+
+end
+
 lemma degree_mod_less:
   "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
   using pdivmod_rel [of x y]
@@ -1775,7 +1832,7 @@
 lemma dvd_poly_gcd_iff [iff]:
   fixes k x y :: "_ poly"
   shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
-  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
+  by (auto intro!: poly_gcd_greatest intro: dvd_trans [of _ "gcd x y"])
 
 lemma poly_gcd_monic:
   fixes x y :: "_ poly"

--- a/src/HOL/Number_Theory/Cong.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Cong.thy	Thu Jul 09 16:49:08 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:

--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -3,66 +3,9 @@
 section \<open>Abstract euclidean algorithm\<close>
 
 theory Euclidean_Algorithm
-imports Complex_Main "~~/src/HOL/Library/Polynomial" "~~/src/HOL/Number_Theory/Normalization_Semidom"
-begin
-
-lemma is_unit_polyE:
-  assumes "is_unit p"
-  obtains a where "p = monom a 0" and "a \<noteq> 0"
-proof -
-  obtain a q where "p = pCons a q" by (cases p)
-  with assms have "p = [:a:]" and "a \<noteq> 0"
-    by (simp_all add: is_unit_pCons_iff)
-  with that show thesis by (simp add: monom_0)
-qed
-
-instantiation poly :: (field) normalization_semidom
+imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/Polynomial"
 begin
 
-definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
-
-definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
-
-instance
-proof
-  fix p :: "'a poly"
-  show "unit_factor p * normalize p = p"
-    by (simp add: normalize_poly_def unit_factor_poly_def)
-      (simp only: mult_smult_left [symmetric] smult_monom, simp)
-next
-  show "normalize 0 = (0::'a poly)"
-    by (simp add: normalize_poly_def)
-next
-  show "unit_factor 0 = (0::'a poly)"
-    by (simp add: unit_factor_poly_def)
-next
-  fix p :: "'a poly"
-  assume "is_unit p"
-  then obtain a where "p = monom a 0" and "a \<noteq> 0"
-    by (rule is_unit_polyE)
-  then show "normalize p = 1"
-    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
-next
-  fix p q :: "'a poly"
-  assume "q \<noteq> 0"
-  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
-    by (auto intro: is_unit_monom_0)
-  then show "is_unit (unit_factor q)"
-    by (simp add: unit_factor_poly_def)
-next
-  fix p q :: "'a poly"
-  have "monom (coeff (p * q) (degree (p * q))) 0 =
-    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
-    by (simp add: monom_0 coeff_degree_mult)
-  then show "unit_factor (p * q) =
-    unit_factor p * unit_factor q"
-    by (simp add: unit_factor_poly_def)
-qed
-
-end
-
 text \<open>
   A Euclidean semiring is a semiring upon which the Euclidean algorithm can be
   implemented. It must provide:
@@ -285,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
@@ -308,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)
@@ -323,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
@@ -435,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"
@@ -518,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)
@@ -541,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]:
@@ -673,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"
@@ -806,88 +762,13 @@
     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)
-
 lemma lcm_gcd_prod:
   "lcm a b * gcd a b = normalize (a * b)"
   by (simp add: lcm_gcd)
 
-lemma lcm_dvd1 [iff]:
-  "a dvd lcm a b"
-proof (cases "a*b = 0")
-  assume "a * b \<noteq> 0"
-  hence "gcd a b \<noteq> 0" by simp
-  let ?c = "1 div unit_factor (a * b)"
-  from \<open>a * b \<noteq> 0\<close> have [simp]: "is_unit (unit_factor (a * b))" by simp
-  from lcm_gcd_prod[of a b] have "lcm a b * gcd a b = a * ?c * b"
-    by (simp add: div_mult_swap unit_div_commute)
-  hence "lcm a b * gcd a b div gcd a b = a * ?c * b div gcd a b" by simp
-  with \<open>gcd a b \<noteq> 0\<close> have "lcm a b = a * ?c * b div gcd a b"
-    by (subst (asm) div_mult_self2_is_id, simp_all)
-  also have "... = a * (?c * b div gcd a b)"
-    by (metis div_mult_swap gcd_dvd2 mult_assoc)
-  finally show ?thesis by (rule dvdI)
-qed (auto simp add: lcm_gcd)
-
-lemma lcm_least:
-  "\<lbrakk>a dvd k; b dvd k\<rbrakk> \<Longrightarrow> lcm a b dvd k"
-proof (cases "k = 0")
-  let ?nf = unit_factor
-  assume "k \<noteq> 0"
-  hence "is_unit (?nf k)" by simp
-  hence "?nf k \<noteq> 0" by (metis not_is_unit_0)
-  assume A: "a dvd k" "b dvd k"
-  hence "gcd a b \<noteq> 0" using \<open>k \<noteq> 0\<close> by auto
-  from A obtain r s where ar: "k = a * r" and bs: "k = b * s" 
-    unfolding dvd_def by blast
-  with \<open>k \<noteq> 0\<close> have "r * s \<noteq> 0"
-    by auto (drule sym [of 0], simp)
-  hence "is_unit (?nf (r * s))" by simp
-  let ?c = "?nf k div ?nf (r*s)"
-  from \<open>is_unit (?nf k)\<close> and \<open>is_unit (?nf (r * s))\<close> have "is_unit ?c" by (rule unit_div)
-  hence "?c \<noteq> 0" using not_is_unit_0 by fast 
-  from ar bs have "k * k * gcd s r = ?nf k * k * gcd (k * s) (k * r)"
-    by (subst mult_assoc, subst gcd_mult_distrib[of k s r], simp only: ac_simps)
-  also have "... = ?nf k * k * gcd ((r*s) * a) ((r*s) * b)"
-    by (subst (3) \<open>k = a * r\<close>, subst (3) \<open>k = b * s\<close>, simp add: algebra_simps)
-  also have "... = ?c * r*s * k * gcd a b" using \<open>r * s \<noteq> 0\<close>
-    by (subst gcd_mult_distrib'[symmetric], simp add: algebra_simps unit_simps)
-  finally have "(a*r) * (b*s) * gcd s r = ?c * k * r * s * gcd a b"
-    by (subst ar[symmetric], subst bs[symmetric], simp add: mult_ac)
-  hence "a * b * gcd s r * (r * s) = ?c * k * gcd a b * (r * s)"
-    by (simp add: algebra_simps)
-  hence "?c * k * gcd a b = a * b * gcd s r" using \<open>r * s \<noteq> 0\<close>
-    by (metis div_mult_self2_is_id)
-  also have "... = lcm a b * gcd a b * gcd s r * ?nf (a*b)"
-    by (subst lcm_gcd_prod[of a b], metis gcd_mult_distrib gcd_mult_distrib') 
-  also have "... = lcm a b * gcd s r * ?nf (a*b) * gcd a b"
-    by (simp add: algebra_simps)
-  finally have "k * ?c = lcm a b * gcd s r * ?nf (a*b)" using \<open>gcd a b \<noteq> 0\<close>
-    by (metis mult.commute div_mult_self2_is_id)
-  hence "k = lcm a b * (gcd s r * ?nf (a*b)) div ?c" using \<open>?c \<noteq> 0\<close>
-    by (metis div_mult_self2_is_id mult_assoc) 
-  also have "... = lcm a b * (gcd s r * ?nf (a*b) div ?c)" using \<open>is_unit ?c\<close>
-    by (simp add: unit_simps)
-  finally show ?thesis by (rule dvdI)
-qed simp
-
 lemma lcm_zero:
   "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0"
-proof -
-  let ?nf = unit_factor
-  {
-    assume "a \<noteq> 0" "b \<noteq> 0"
-    hence "a * b div ?nf (a * b) \<noteq> 0" by (simp add: no_zero_divisors)
-    moreover from \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "gcd a b \<noteq> 0" by simp
-    ultimately have "lcm a b \<noteq> 0" using lcm_gcd_prod[of a b] by (intro notI, simp)
-  } moreover {
-    assume "a = 0 \<or> b = 0"
-    hence "lcm a b = 0" by (elim disjE, simp_all add: lcm_gcd)
-  }
-  ultimately show ?thesis by blast
-qed
+  by (fact lcm_eq_0_iff)
 
 lemmas lcm_0_iff = lcm_zero
 
@@ -901,57 +782,27 @@
     by (metis nonzero_mult_divide_cancel_left)
 qed
 
-lemma unit_factor_lcm [simp]:
-  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
-  by (simp add: dvd_unit_factor_div lcm_gcd)
-
-lemma lcm_dvd2 [iff]: "b dvd lcm a b"
-  using lcm_dvd1 [of b a] by (simp add: lcm_gcd ac_simps)
+declare unit_factor_lcm [simp]
 
 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 associated_def intro: lcm_least)
+  by (rule associated_eqI) (auto simp: assms intro: lcm_least)
 
-sublocale lcm!: abel_semigroup lcm
-proof
-  fix a b c
-  show "lcm (lcm a b) c = lcm a (lcm b c)"
-  proof (rule lcmI)
-    have "a dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
-    then show "a dvd lcm (lcm a b) c" by (rule dvd_trans)
-    
-    have "b dvd lcm a b" and "lcm a b dvd lcm (lcm a b) c" by simp_all
-    hence "b dvd lcm (lcm a b) c" by (rule dvd_trans)
-    moreover have "c dvd lcm (lcm a b) c" by simp
-    ultimately show "lcm b c dvd lcm (lcm a b) c" by (rule lcm_least)
-
-    fix l assume "a dvd l" and "lcm b c dvd l"
-    have "b dvd lcm b c" by simp
-    from this and \<open>lcm b c dvd l\<close> have "b dvd l" by (rule dvd_trans)
-    have "c dvd lcm b c" by simp
-    from this and \<open>lcm b c dvd l\<close> have "c dvd l" by (rule dvd_trans)
-    from \<open>a dvd l\<close> and \<open>b dvd l\<close> have "lcm a b dvd l" by (rule lcm_least)
-    from this and \<open>c dvd l\<close> show "lcm (lcm a b) c dvd l" by (rule lcm_least)
-  qed (simp add: lcm_zero)
-next
-  fix a b
-  show "lcm a b = lcm b a"
-    by (simp add: lcm_gcd ac_simps)
-qed
+sublocale lcm!: abel_semigroup lcm ..
 
 lemma dvd_lcm_D1:
   "lcm m n dvd k \<Longrightarrow> m dvd k"
-  by (rule dvd_trans, rule lcm_dvd1, assumption)
+  by (rule dvd_trans, rule dvd_lcm1, assumption)
 
 lemma dvd_lcm_D2:
   "lcm m n dvd k \<Longrightarrow> n dvd k"
-  by (rule dvd_trans, rule lcm_dvd2, assumption)
+  by (rule dvd_trans, rule dvd_lcm2, assumption)
 
 lemma gcd_dvd_lcm [simp]:
   "gcd a b dvd lcm a b"
-  by (metis dvd_trans gcd_dvd2 lcm_dvd2)
+  using gcd_dvd2 by (rule dvd_lcmI2)
 
 lemma lcm_1_iff:
   "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
@@ -969,35 +820,15 @@
   finally show "lcm a b = 1" .
 qed
 
-lemma lcm_0_left [simp]:
-  "lcm 0 a = 0"
-  by (rule sym, rule lcmI, simp_all)
-
-lemma lcm_0 [simp]:
+lemma lcm_0:
   "lcm a 0 = 0"
-  by (rule sym, rule lcmI, simp_all)
+  by (fact lcm_0_right)
 
 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)
-
-lemma dvd_lcm_I1 [simp]:
-  "k dvd m \<Longrightarrow> k dvd lcm m n"
-  by (metis lcm_dvd1 dvd_trans)
-
-lemma dvd_lcm_I2 [simp]:
-  "k dvd n \<Longrightarrow> k dvd lcm m n"
-  by (metis lcm_dvd2 dvd_trans)
-
-lemma lcm_1_left [simp]:
-  "lcm 1 a = normalize a"
-  by (cases "a = 0") (simp, rule sym, rule lcmI, simp_all)
-
-lemma lcm_1_right [simp]:
-  "lcm a 1 = normalize a"
-  using lcm_1_left [of a] by (simp add: ac_simps)
+  by rule (auto intro: lcmI simp: lcm_least lcm_zero)
 
 lemma lcm_coprime:
   "gcd a b = 1 \<Longrightarrow> lcm a b = normalize (a * b)"
@@ -1035,8 +866,8 @@
   assumes "a \<noteq> 0" and "b \<noteq> 0"
   shows "euclidean_size a \<le> euclidean_size (lcm a b)"
 proof -
-  have "a dvd lcm a b" by (rule lcm_dvd1)
-  then obtain c where A: "lcm a b = a * c" unfolding dvd_def by blast
+  have "a dvd lcm a b" by (rule dvd_lcm1)
+  then obtain c where A: "lcm a b = a * c" ..
   with \<open>a \<noteq> 0\<close> and \<open>b \<noteq> 0\<close> have "c \<noteq> 0" by (auto simp: lcm_zero)
   then show ?thesis by (subst A, intro size_mult_mono)
 qed
@@ -1066,12 +897,7 @@
 
 lemma lcm_mult_unit1:
   "is_unit a \<Longrightarrow> lcm (b * a) c = lcm b c"
-  apply (rule lcmI)
-  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)
-  done
+  by (rule associated_eqI) (simp_all add: mult_unit_dvd_iff dvd_lcmI1)
 
 lemma lcm_mult_unit2:
   "is_unit a \<Longrightarrow> lcm b (c * a) = lcm b c"
@@ -1105,22 +931,11 @@
 
 lemma lcm_left_idem:
   "lcm a (lcm a b) = lcm a b"
-  apply (rule lcmI)
-  apply simp
-  apply (subst lcm.assoc [symmetric], rule lcm_dvd2)
-  apply (rule lcm_least, assumption)
-  apply (erule (1) lcm_least)
-  apply (auto simp: lcm_zero)
-  done
+  by (rule associated_eqI) simp_all
 
 lemma lcm_right_idem:
   "lcm (lcm a b) b = lcm a b"
-  apply (rule lcmI)
-  apply (subst lcm.assoc, rule lcm_dvd1)
-  apply (rule lcm_dvd2)
-  apply (rule lcm_least, erule (1) lcm_least, assumption)
-  apply (auto simp: lcm_zero)
-  done
+  by (rule associated_eqI) simp_all
 
 lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
 proof
@@ -1173,9 +988,10 @@
         also note \<open>euclidean_size l = n\<close>
         finally show "euclidean_size (gcd l l') \<le> n" .
       qed
-      ultimately have "euclidean_size l = euclidean_size (gcd l l')" 
+      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
         by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
-      with \<open>l \<noteq> 0\<close> have "l dvd gcd l l'" by (blast intro: dvd_euclidean_size_eq_imp_dvd)
+      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
+        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
       hence "l dvd l'" by (blast dest: dvd_gcd_D2)
     }
 
@@ -1198,12 +1014,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"
@@ -1302,7 +1125,7 @@
   "Lcm (insert a A) = lcm a (Lcm A)"
 proof (rule lcmI)
   fix l assume "a dvd l" and "Lcm A dvd l"
-  hence "\<forall>a\<in>A. a dvd l" by (blast intro: dvd_trans dvd_Lcm)
+  then have "\<forall>a\<in>A. a dvd l" by (auto intro: dvd_trans [of _ "Lcm A" l])
   with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_least)
 qed (auto intro: Lcm_least dvd_Lcm)
  
@@ -1367,40 +1190,34 @@
 
 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}"
   by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
 
-lemma Gcd_0_iff:
-  "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}"
-  apply (rule iffI)
-  apply (rule subsetI, drule Gcd_dvd, simp)
-  apply (auto intro: GcdI[symmetric])
-  done
-
-lemma Gcd_empty [simp]:
-  "Gcd {} = 0"
-  by (simp add: Gcd_0_iff)
+subclass semiring_Lcm
+  by standard (simp add: Lcm_Gcd)
 
 lemma Gcd_1:
   "1 \<in> A \<Longrightarrow> Gcd A = 1"
-  by (intro GcdI[symmetric]) (auto intro: Gcd_dvd dvd_Gcd)
-
-lemma Gcd_insert [simp]:
-  "Gcd (insert a A) = gcd a (Gcd A)"
-proof (rule gcdI)
-  fix l assume "l dvd a" and "l dvd Gcd A"
-  hence "\<forall>a\<in>A. l dvd a" by (blast intro: dvd_trans Gcd_dvd)
-  with \<open>l dvd a\<close> show "l dvd Gcd (insert a A)" by (force intro: Gcd_dvd Gcd_greatest)
-qed (auto intro: Gcd_greatest)
+  by (auto intro!: Gcd_eq_1_I)
 
 lemma Gcd_finite:
   assumes "finite A"
@@ -1413,14 +1230,11 @@
   using comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd] Gcd_finite by (simp add: ac_simps)
 
 lemma Gcd_singleton [simp]: "Gcd {a} = normalize a"
-  by (simp add: gcd_0)
+  by simp
 
 lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
-  by (simp add: gcd_0)
+  by simp
 
-subclass semiring_gcd
-  by unfold_locales (simp_all add: gcd_greatest_iff)
-  
 end
 
 text \<open>
@@ -1438,7 +1252,7 @@
 lemma euclid_ext_gcd [simp]:
   "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
   by (induct a b rule: gcd_eucl_induct)
-    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
+    (simp_all add: euclid_ext_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
 
 lemma euclid_ext_gcd' [simp]:
   "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
@@ -1509,9 +1323,6 @@
 definition [simp]:
   "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
 
-definition [simp]:
-  "unit_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
-
 instance proof
 qed simp_all
 
@@ -1523,11 +1334,8 @@
 definition [simp]:
   "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
 
-definition [simp]:
-  "unit_factor_int = (sgn :: int \<Rightarrow> int)"
-
 instance
-by standard (auto simp add: abs_mult nat_mult_distrib sgn_times split: abs_split)
+by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
 
 end
 
@@ -1568,4 +1376,19 @@
 
 end
 
+(*instance nat :: euclidean_semiring_gcd
+proof (standard, auto intro!: ext)
+  fix m n :: nat
+  show *: "gcd m n = gcd_eucl m n"
+  proof (induct m n rule: gcd_eucl_induct)
+    case zero then show ?case by (simp add: gcd_eucl_0)
+  next
+    case (mod m n)
+    with gcd_eucl_non_0 [of n m, symmetric]
+    show ?case by (simp add: gcd_non_0_nat)
+  qed
+  show "lcm m n = lcm_eucl m n"
+    by (simp add: lcm_eucl_def lcm_gcd * [symmetric] lcm_nat_def)
+qed*)
+
 end

--- a/src/HOL/Number_Theory/Fib.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Fib.thy	Thu Jul 09 16:49:08 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)"

--- a/src/HOL/Number_Theory/Gauss.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Gauss.thy	Thu Jul 09 16:49:08 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)

--- a/src/HOL/Number_Theory/Normalization_Semidom.thy	Thu Jul 09 15:20:54 2015 +0200
+++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
@@ -1,336 +0,0 @@
-theory Normalization_Semidom
-imports Main
-begin
-
-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"
-proof -
-  from assms have "a div (a * b) = a div a div b"
-    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
-  with assms show ?thesis by simp
-qed
-
-lemma is_unit_divide_mult_cancel_right:
-  assumes "a \<noteq> 0" and "is_unit b"
-  shows "a div (b * a) = 1 div b"
-  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
-
-end
-
-class normalization_semidom = algebraic_semidom +
-  fixes normalize :: "'a \<Rightarrow> 'a"
-    and unit_factor :: "'a \<Rightarrow> 'a"
-  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
-  assumes normalize_0 [simp]: "normalize 0 = 0"
-    and unit_factor_0 [simp]: "unit_factor 0 = 0"
-  assumes is_unit_normalize:
-    "is_unit a  \<Longrightarrow> normalize a = 1"
-  assumes unit_factor_is_unit [iff]: 
-    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
-  assumes unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
-begin
-
-lemma unit_factor_dvd [simp]:
-  "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
-  by (rule unit_imp_dvd) simp
-
-lemma unit_factor_self [simp]:
-  "unit_factor a dvd a"
-  by (cases "a = 0") simp_all 
-  
-lemma normalize_mult_unit_factor [simp]:
-  "normalize a * unit_factor a = a"
-  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
-
-lemma normalize_eq_0_iff [simp]:
-  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  moreover have "unit_factor a * normalize a = a" by simp
-  ultimately show ?Q by simp 
-next
-  assume ?Q then show ?P by simp
-qed
-
-lemma unit_factor_eq_0_iff [simp]:
-  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?P
-  moreover have "unit_factor a * normalize a = a" by simp
-  ultimately show ?Q by simp 
-next
-  assume ?Q then show ?P by simp
-qed
-
-lemma is_unit_unit_factor:
-  assumes "is_unit a" shows "unit_factor a = a"
-proof - 
-  from assms have "normalize a = 1" by (rule is_unit_normalize)
-  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
-  ultimately show ?thesis by simp
-qed
-
-lemma unit_factor_1 [simp]:
-  "unit_factor 1 = 1"
-  by (rule is_unit_unit_factor) simp
-
-lemma normalize_1 [simp]:
-  "normalize 1 = 1"
-  by (rule is_unit_normalize) simp
-
-lemma normalize_1_iff:
-  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
-proof
-  assume ?Q then show ?P by (rule is_unit_normalize)
-next
-  assume ?P
-  then have "a \<noteq> 0" by auto
-  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
-    by simp
-  then have "unit_factor a = a"
-    by simp
-  moreover have "is_unit (unit_factor a)"
-    using \<open>a \<noteq> 0\<close> by simp
-  ultimately show ?Q by simp
-qed
-  
-lemma div_normalize [simp]:
-  "a div normalize a = unit_factor a"
-proof (cases "a = 0")
-  case True then show ?thesis by simp
-next
-  case False then have "normalize a \<noteq> 0" by simp 
-  with nonzero_mult_divide_cancel_right
-  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
-  then show ?thesis by simp
-qed
-
-lemma div_unit_factor [simp]:
-  "a div unit_factor a = normalize a"
-proof (cases "a = 0")
-  case True then show ?thesis by simp
-next
-  case False then have "unit_factor a \<noteq> 0" by simp 
-  with nonzero_mult_divide_cancel_left
-  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
-  then show ?thesis by simp
-qed
-
-lemma normalize_div [simp]:
-  "normalize a div a = 1 div unit_factor a"
-proof (cases "a = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
-    by simp
-  also have "\<dots> = 1 div unit_factor a"
-    using False by (subst is_unit_divide_mult_cancel_right) simp_all
-  finally show ?thesis .
-qed
-
-lemma mult_one_div_unit_factor [simp]:
-  "a * (1 div unit_factor b) = a div unit_factor b"
-  by (cases "b = 0") simp_all
-
-lemma normalize_mult:
-  "normalize (a * b) = normalize a * normalize b"
-proof (cases "a = 0 \<or> b = 0")
-  case True then show ?thesis by auto
-next
-  case False
-  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
-  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
-  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
-  also have "\<dots> = a * b div unit_factor b div unit_factor a"
-    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
-  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
-    using False by (subst unit_div_mult_swap) simp_all
-  also have "\<dots> = normalize a * normalize b"
-    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
-  finally show ?thesis .
-qed
- 
-lemma unit_factor_idem [simp]:
-  "unit_factor (unit_factor a) = unit_factor a"
-  by (cases "a = 0") (auto intro: is_unit_unit_factor)
-
-lemma normalize_unit_factor [simp]:
-  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
-  by (rule is_unit_normalize) simp
-  
-lemma normalize_idem [simp]:
-  "normalize (normalize a) = normalize a"
-proof (cases "a = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  have "normalize a = normalize (unit_factor a * normalize a)" by simp
-  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
-    by (simp only: normalize_mult)
-  finally show ?thesis using False by simp_all
-qed
-
-lemma unit_factor_normalize [simp]:
-  assumes "a \<noteq> 0"
-  shows "unit_factor (normalize a) = 1"
-proof -
-  from assms have "normalize a \<noteq> 0" by simp
-  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
-    by (simp only: unit_factor_mult_normalize)
-  then have "unit_factor (normalize a) * normalize a = normalize a"
-    by simp
-  with \<open>normalize a \<noteq> 0\<close>
-  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
-    by simp
-  with \<open>normalize a \<noteq> 0\<close>
-  show ?thesis by simp
-qed
-
-lemma dvd_unit_factor_div:
-  assumes "b dvd a"
-  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
-proof -
-  from assms have "a = a div b * b"
-    by simp
-  then have "unit_factor a = unit_factor (a div b * b)"
-    by simp
-  then show ?thesis
-    by (cases "b = 0") (simp_all add: unit_factor_mult)
-qed
-
-lemma dvd_normalize_div:
-  assumes "b dvd a"
-  shows "normalize (a div b) = normalize a div normalize b"
-proof -
-  from assms have "a = a div b * b"
-    by simp
-  then have "normalize a = normalize (a div b * b)"
-    by simp
-  then show ?thesis
-    by (cases "b = 0") (simp_all add: normalize_mult)
-qed
-
-lemma normalize_dvd_iff [simp]:
-  "normalize a dvd b \<longleftrightarrow> a dvd b"
-proof -
-  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
-    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
-      by (cases "a = 0") simp_all
-  then show ?thesis by simp
-qed
-
-lemma dvd_normalize_iff [simp]:
-  "a dvd normalize b \<longleftrightarrow> a dvd b"
-proof -
-  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
-    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
-      by (cases "b = 0") simp_all
-  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)
-
-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")
-proof (cases "a = 0 \<or> b = 0")
-  case True then 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)
-  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)
-  qed
-qed
-
-lemma normalize_power:
-  "normalize (a ^ n) = normalize a ^ n"
-  by (induct n) (simp_all add: normalize_mult)
-
-lemma unit_factor_power:
-  "unit_factor (a ^ n) = unit_factor a ^ n"
-  by (induct n) (simp_all add: unit_factor_mult)
-
-lemma associated_eqI:
-  assumes "associated a b"
-  assumes "unit_factor a \<in> {0, 1}" and "unit_factor b \<in> {0, 1}"
-  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
-qed
-
-end
-
-instantiation nat :: normalization_semidom
-begin
-
-definition normalize_nat
-  where [simp]: "normalize = (id :: nat \<Rightarrow> nat)"
-
-definition unit_factor_nat
-  where "unit_factor n = (if n = 0 then 0 else 1 :: nat)"
-
-lemma unit_factor_simps [simp]:
-  "unit_factor 0 = (0::nat)"
-  "unit_factor (Suc n) = 1"
-  by (simp_all add: unit_factor_nat_def)
-
-instance
-  by default (simp_all add: unit_factor_nat_def)
-  
-end
-
-instantiation int :: normalization_semidom
-begin
-
-definition normalize_int
-  where [simp]: "normalize = (abs :: int \<Rightarrow> int)"
-
-definition unit_factor_int
-  where [simp]: "unit_factor = (sgn :: int \<Rightarrow> int)"
-
-instance
-proof
-  fix k :: int
-  assume "k \<noteq> 0"
-  then have "\<bar>sgn k\<bar> = 1"
-    by (cases "0::int" k rule: linorder_cases) simp_all
-  then show "is_unit (unit_factor k)"
-    by simp
-qed (simp_all add: sgn_times mult_sgn_abs)
-  
-end
-
-end

--- a/src/HOL/Number_Theory/Pocklington.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Pocklington.thy	Thu Jul 09 16:49:08 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" 

--- a/src/HOL/Number_Theory/Primes.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Primes.thy	Thu Jul 09 16:49:08 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

--- a/src/HOL/Number_Theory/Residues.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Number_Theory/Residues.thy	Thu Jul 09 16:49:08 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

--- a/src/HOL/Power.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Power.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -306,6 +306,19 @@
 
 end
 
+context normalization_semidom
+begin
+
+lemma normalize_power:
+  "normalize (a ^ n) = normalize a ^ n"
+  by (induct n) (simp_all add: normalize_mult)
+
+lemma unit_factor_power:
+  "unit_factor (a ^ n) = unit_factor a ^ n"
+  by (induct n) (simp_all add: unit_factor_mult)
+
+end
+
 context division_ring
 begin
 

--- a/src/HOL/Rat.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Rat.thy	Thu Jul 09 16:49:08 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]:

--- a/src/HOL/Rings.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Rings.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -629,6 +629,44 @@
   then show ?thesis by simp
 qed 
 
+lemma divide_1 [simp]:
+  "a div 1 = a"
+  using nonzero_mult_divide_cancel_left [of 1 a] by simp
+
+lemma dvd_times_left_cancel_iff [simp]:
+  assumes "a \<noteq> 0"
+  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then obtain d where "a * c = a * b * d" ..
+  with assms have "c = b * d" by (simp add: ac_simps)
+  then show ?Q ..
+next
+  assume ?Q then obtain d where "c = b * d" .. 
+  then have "a * c = a * b * d" by (simp add: ac_simps)
+  then show ?P ..
+qed
+  
+lemma dvd_times_right_cancel_iff [simp]:
+  assumes "a \<noteq> 0"
+  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
+using dvd_times_left_cancel_iff [of a b c] assms by (simp add: ac_simps)
+  
+lemma div_dvd_iff_mult:
+  assumes "b \<noteq> 0" and "b dvd a"
+  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
+proof -
+  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
+  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
+qed
+
+lemma dvd_div_iff_mult:
+  assumes "c \<noteq> 0" and "c dvd b"
+  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
+proof -
+  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
+  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
+qed
+
 end
 
 class idom_divide = idom + semidom_divide
@@ -636,6 +674,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,79 +879,319 @@
     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
 
+lemma is_unit_divide_mult_cancel_left:
+  assumes "a \<noteq> 0" and "is_unit b"
+  shows "a div (a * b) = 1 div b"
+proof -
+  from assms have "a div (a * b) = a div a div b"
+    by (simp add: mult_unit_dvd_iff dvd_div_mult2_eq)
+  with assms show ?thesis by simp
+qed
+
+lemma is_unit_divide_mult_cancel_right:
+  assumes "a \<noteq> 0" and "is_unit b"
+  shows "a div (b * a) = 1 div b"
+  using assms is_unit_divide_mult_cancel_left [of a b] by (simp add: ac_simps)
+
+end
+
+class normalization_semidom = algebraic_semidom +
+  fixes normalize :: "'a \<Rightarrow> 'a"
+    and unit_factor :: "'a \<Rightarrow> 'a"
+  assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
+  assumes normalize_0 [simp]: "normalize 0 = 0"
+    and unit_factor_0 [simp]: "unit_factor 0 = 0"
+  assumes is_unit_normalize:
+    "is_unit a  \<Longrightarrow> normalize a = 1"
+  assumes unit_factor_is_unit [iff]: 
+    "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
+  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
+
+lemma unit_factor_self [simp]:
+  "unit_factor a dvd a"
+  by (cases "a = 0") simp_all 
+  
+lemma normalize_mult_unit_factor [simp]:
+  "normalize a * unit_factor a = a"
+  using unit_factor_mult_normalize [of a] by (simp add: ac_simps)
+
+lemma normalize_eq_0_iff [simp]:
+  "normalize a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  moreover have "unit_factor a * normalize a = a" by simp
+  ultimately show ?Q by simp 
+next
+  assume ?Q then show ?P by simp
+qed
+
+lemma unit_factor_eq_0_iff [simp]:
+  "unit_factor a = 0 \<longleftrightarrow> a = 0" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P
+  moreover have "unit_factor a * normalize a = a" by simp
+  ultimately show ?Q by simp 
+next
+  assume ?Q then show ?P by simp
+qed
+
+lemma is_unit_unit_factor:
+  assumes "is_unit a" shows "unit_factor a = a"
+proof - 
+  from assms have "normalize a = 1" by (rule is_unit_normalize)
+  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
+  ultimately show ?thesis by simp
+qed
+
+lemma unit_factor_1 [simp]:
+  "unit_factor 1 = 1"
+  by (rule is_unit_unit_factor) simp
+
+lemma normalize_1 [simp]:
+  "normalize 1 = 1"
+  by (rule is_unit_normalize) simp
+
+lemma normalize_1_iff:
+  "normalize a = 1 \<longleftrightarrow> is_unit a" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?Q then show ?P by (rule is_unit_normalize)
+next
+  assume ?P
+  then have "a \<noteq> 0" by auto
+  from \<open>?P\<close> have "unit_factor a * normalize a = unit_factor a * 1"
+    by simp
+  then have "unit_factor a = a"
+    by simp
+  moreover have "is_unit (unit_factor a)"
+    using \<open>a \<noteq> 0\<close> by simp
+  ultimately show ?Q by simp
+qed
+  
+lemma div_normalize [simp]:
+  "a div normalize a = unit_factor a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False then have "normalize a \<noteq> 0" by simp 
+  with nonzero_mult_divide_cancel_right
+  have "unit_factor a * normalize a div normalize a = unit_factor a" by blast
+  then show ?thesis by simp
+qed
+
+lemma div_unit_factor [simp]:
+  "a div unit_factor a = normalize a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False then have "unit_factor a \<noteq> 0" by simp 
+  with nonzero_mult_divide_cancel_left
+  have "unit_factor a * normalize a div unit_factor a = normalize a" by blast
+  then show ?thesis by simp
+qed
+
+lemma normalize_div [simp]:
+  "normalize a div a = 1 div unit_factor a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
+    by simp
+  also have "\<dots> = 1 div unit_factor a"
+    using False by (subst is_unit_divide_mult_cancel_right) simp_all
+  finally show ?thesis .
+qed
+
+lemma mult_one_div_unit_factor [simp]:
+  "a * (1 div unit_factor b) = a div unit_factor b"
+  by (cases "b = 0") simp_all
+
+lemma normalize_mult:
+  "normalize (a * b) = normalize a * normalize b"
+proof (cases "a = 0 \<or> b = 0")
+  case True then show ?thesis by auto
+next
+  case False
+  from unit_factor_mult_normalize have "unit_factor (a * b) * normalize (a * b) = a * b" .
+  then have "normalize (a * b) = a * b div unit_factor (a * b)" by simp
+  also have "\<dots> = a * b div unit_factor (b * a)" by (simp add: ac_simps)
+  also have "\<dots> = a * b div unit_factor b div unit_factor a"
+    using False by (simp add: unit_factor_mult is_unit_div_mult2_eq [symmetric])
+  also have "\<dots> = a * (b div unit_factor b) div unit_factor a"
+    using False by (subst unit_div_mult_swap) simp_all
+  also have "\<dots> = normalize a * normalize b"
+    using False by (simp add: mult.commute [of a] mult.commute [of "normalize a"] unit_div_mult_swap [symmetric])
+  finally show ?thesis .
+qed
+ 
+lemma unit_factor_idem [simp]:
+  "unit_factor (unit_factor a) = unit_factor a"
+  by (cases "a = 0") (auto intro: is_unit_unit_factor)
+
+lemma normalize_unit_factor [simp]:
+  "a \<noteq> 0 \<Longrightarrow> normalize (unit_factor a) = 1"
+  by (rule is_unit_normalize) simp
+  
+lemma normalize_idem [simp]:
+  "normalize (normalize a) = normalize a"
+proof (cases "a = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "normalize a = normalize (unit_factor a * normalize a)" by simp
+  also have "\<dots> = normalize (unit_factor a) * normalize (normalize a)"
+    by (simp only: normalize_mult)
+  finally show ?thesis using False by simp_all
+qed
+
+lemma unit_factor_normalize [simp]:
+  assumes "a \<noteq> 0"
+  shows "unit_factor (normalize a) = 1"
+proof -
+  from assms have "normalize a \<noteq> 0" by simp
+  have "unit_factor (normalize a) * normalize (normalize a) = normalize a"
+    by (simp only: unit_factor_mult_normalize)
+  then have "unit_factor (normalize a) * normalize a = normalize a"
+    by simp
+  with \<open>normalize a \<noteq> 0\<close>
+  have "unit_factor (normalize a) * normalize a div normalize a = normalize a div normalize a"
+    by simp
+  with \<open>normalize a \<noteq> 0\<close>
+  show ?thesis by simp
+qed
+
+lemma dvd_unit_factor_div:
+  assumes "b dvd a"
+  shows "unit_factor (a div b) = unit_factor a div unit_factor b"
+proof -
+  from assms have "a = a div b * b"
+    by simp
+  then have "unit_factor a = unit_factor (a div b * b)"
+    by simp
+  then show ?thesis
+    by (cases "b = 0") (simp_all add: unit_factor_mult)
+qed
+
+lemma dvd_normalize_div:
+  assumes "b dvd a"
+  shows "normalize (a div b) = normalize a div normalize b"
+proof -
+  from assms have "a = a div b * b"
+    by simp
+  then have "normalize a = normalize (a div b * b)"
+    by simp
+  then show ?thesis
+    by (cases "b = 0") (simp_all add: normalize_mult)
+qed
+
+lemma normalize_dvd_iff [simp]:
+  "normalize a dvd b \<longleftrightarrow> a dvd b"
+proof -
+  have "normalize a dvd b \<longleftrightarrow> unit_factor a * normalize a dvd b"
+    using mult_unit_dvd_iff [of "unit_factor a" "normalize a" b]
+      by (cases "a = 0") simp_all
+  then show ?thesis by simp
+qed
+
+lemma dvd_normalize_iff [simp]:
+  "a dvd normalize b \<longleftrightarrow> a dvd b"
+proof -
+  have "a dvd normalize  b \<longleftrightarrow> a dvd normalize b * unit_factor b"
+    using dvd_mult_unit_iff [of "unit_factor b" a "normalize b"]
+      by (cases "b = 0") simp_all
+  then show ?thesis by simp
+qed
+
+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 associatedI:
+  assumes "a dvd b" and "b dvd a"
+  shows "normalize a = normalize b"
+proof (cases "a = 0 \<or> b = 0")
+  case True with assms show ?thesis by auto
+next
+  case False
+  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
+    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 "a dvd b" and "b dvd a"
+  assumes "normalize a = a" and "normalize b = b"
+  shows "a = b"
+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
 
 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +

--- a/src/HOL/Transcendental.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/Transcendental.thy	Thu Jul 09 16:49:08 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"

--- a/src/HOL/ex/Sqrt.thy	Thu Jul 09 15:20:54 2015 +0200
+++ b/src/HOL/ex/Sqrt.thy	Thu Jul 09 16:49:08 2015 +0200
@@ -18,7 +18,7 @@
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
-    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+    and "coprime m n" by (rule Rats_abs_nat_div_natE)
   have eq: "m\<^sup>2 = p * n\<^sup>2"
   proof -
     from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
@@ -38,9 +38,8 @@
     then have "p dvd n\<^sup>2" ..
     with \<open>prime p\<close> show "p dvd n" by (rule prime_dvd_power_nat)
   qed
-  then have "p dvd gcd m n" ..
-  with gcd have "p dvd 1" by simp
-  then have "p \<le> 1" by (simp add: dvd_imp_le)
+  then have "p dvd gcd m n" by simp
+  with \<open>coprime m n\<close> have "p = 1" by simp
   with p show False by simp
 qed
 
@@ -64,7 +63,7 @@
   assume "sqrt p \<in> \<rat>"
   then obtain m n :: nat where
       n: "n \<noteq> 0" and sqrt_rat: "\<bar>sqrt p\<bar> = m / n"
-    and gcd: "gcd m n = 1" by (rule Rats_abs_nat_div_natE)
+    and "coprime m n" by (rule Rats_abs_nat_div_natE)
   from n and sqrt_rat have "m = \<bar>sqrt p\<bar> * n" by simp
   then have "m\<^sup>2 = (sqrt p)\<^sup>2 * n\<^sup>2"
     by (auto simp add: power2_eq_square)
@@ -79,8 +78,7 @@
   then have "p dvd n\<^sup>2" ..
   with \<open>prime p\<close> have "p dvd n" by (rule prime_dvd_power_nat)
   with dvd_m have "p dvd gcd m n" by (rule gcd_greatest_nat)
-  with gcd have "p dvd 1" by simp
-  then have "p \<le> 1" by (simp add: dvd_imp_le)
+  with \<open>coprime m n\<close> have "p = 1" by simp
   with p show False by simp
 qed