separate class for notions specific for integral (semi)domains, in contrast to fields where these are trivial

--- a/CONTRIBUTORS	Fri Jun 19 07:53:33 2015 +0200
+++ b/CONTRIBUTORS	Fri Jun 19 07:53:35 2015 +0200
@@ -10,6 +10,10 @@
   Generic partial division in rings as inverse operation
   of multiplication.
 
+* Summer 2015: Manuel Eberl and Florian Haftmann, TUM
+  Type class hierarchy with common algebraic notions of
+  integral (semi)domains like units and associated elements.
+
 
 Contributions to Isabelle2015
 -----------------------------

--- a/NEWS	Fri Jun 19 07:53:33 2015 +0200
+++ b/NEWS	Fri Jun 19 07:53:35 2015 +0200
@@ -95,6 +95,12 @@
 * 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
+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.
+
 * Former constants Fields.divide (_ / _) and Divides.div (_ div _)
 are logically unified to Rings.divide in syntactic type class
 Rings.divide, with infix syntax (_ div _).  Infix syntax (_ / _)

--- a/src/HOL/Divides.thy	Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Divides.thy	Fri Jun 19 07:53:35 2015 +0200
@@ -22,7 +22,7 @@
     and div_mult_mult1 [simp]: "c \<noteq> 0 \<Longrightarrow> (c * a) div (c * b) = a div b"
 begin
 
-subclass semidom_divide
+subclass algebraic_semidom
 proof
   fix b a
   assume "b \<noteq> 0"
@@ -212,18 +212,6 @@
   finally show ?thesis .
 qed
 
-lemma dvd_div_mult_self [simp]:
-  "a dvd b \<Longrightarrow> (b div a) * a = b"
-  using mod_div_equality [of b a, symmetric] by simp
-
-lemma dvd_mult_div_cancel [simp]:
-  "a dvd b \<Longrightarrow> a * (b div a) = b"
-  using dvd_div_mult_self by (simp add: ac_simps)
-
-lemma dvd_div_mult:
-  "a dvd b \<Longrightarrow> (b div a) * c = (b * c) div a"
-  by (cases "a = 0") (auto elim!: dvdE simp add: mult.assoc)
-
 lemma div_dvd_div [simp]:
   assumes "a dvd b" and "a dvd c"
   shows "b div a dvd c div a \<longleftrightarrow> b dvd c"
@@ -359,15 +347,6 @@
   apply (simp add: no_zero_divisors)
   done
 
-lemma div_mult_swap:
-  assumes "c dvd b"
-  shows "a * (b div c) = (a * b) div c"
-proof -
-  from assms have "b div c * (a div 1) = b * a div (c * 1)"
-    by (simp only: div_mult_div_if_dvd one_dvd)
-  then show ?thesis by (simp add: mult.commute)
-qed
-   
 lemma div_mult_mult2 [simp]:
   "c \<noteq> 0 \<Longrightarrow> (a * c) div (b * c) = a div b"
   by (drule div_mult_mult1) (simp add: mult.commute)
@@ -1911,6 +1890,10 @@
 
 end
 
+lemma is_unit_int:
+  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
+  by auto
+
 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	Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Equiv_Relations.thy	Fri Jun 19 07:53:35 2015 +0200
@@ -523,6 +523,20 @@
   "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/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Jun 19 07:53:35 2015 +0200
@@ -5,276 +5,6 @@
 theory Euclidean_Algorithm
 imports Complex_Main
 begin
-
-context semidom_divide
-begin
-
-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)
-
-lemma dvd_mult_div_cancel [simp]:
-  "a dvd b \<Longrightarrow> a * (b div a) = b"
-  using dvd_div_mult_self [of a b] by (simp add: ac_simps)
-  
-lemma div_mult_swap:
-  assumes "c dvd b"
-  shows "a * (b div c) = (a * b) div c"
-proof (cases "c = 0")
-  case True then show ?thesis by simp
-next
-  case False from assms obtain d where "b = c * d" ..
-  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
-    by simp
-  ultimately show ?thesis by (simp add: ac_simps)
-qed
-
-lemma dvd_div_mult:
-  assumes "c dvd b"
-  shows "b div c * a = (b * a) div c"
-  using assms div_mult_swap [of c b a] by (simp add: ac_simps)
-
-  
-text \<open>Units: invertible elements in a ring\<close>
-
-abbreviation is_unit :: "'a \<Rightarrow> bool"
-where
-  "is_unit a \<equiv> a dvd 1"
-
-lemma not_is_unit_0 [simp]:
-  "\<not> is_unit 0"
-  by simp
-
-lemma unit_imp_dvd [dest]: 
-  "is_unit b \<Longrightarrow> b dvd a"
-  by (rule dvd_trans [of _ 1]) simp_all
-
-lemma unit_dvdE:
-  assumes "is_unit a"
-  obtains c where "a \<noteq> 0" and "b = a * c"
-proof -
-  from assms have "a dvd b" by auto
-  then obtain c where "b = a * c" ..
-  moreover from assms have "a \<noteq> 0" by auto
-  ultimately show thesis using that by blast
-qed
-
-lemma dvd_unit_imp_unit:
-  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
-  by (rule dvd_trans)
-
-lemma unit_div_1_unit [simp, intro]:
-  assumes "is_unit a"
-  shows "is_unit (1 div a)"
-proof -
-  from assms have "1 = 1 div a * a" by simp
-  then show "is_unit (1 div a)" by (rule dvdI)
-qed
-
-lemma is_unitE [elim?]:
-  assumes "is_unit a"
-  obtains b where "a \<noteq> 0" and "b \<noteq> 0"
-    and "is_unit b" and "1 div a = b" and "1 div b = a"
-    and "a * b = 1" and "c div a = c * b"
-proof (rule that)
-  def b \<equiv> "1 div a"
-  then show "1 div a = b" by simp
-  from b_def `is_unit a` show "is_unit b" by simp
-  from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
-  from b_def `is_unit a` show "a * b = 1" by simp
-  then have "1 = a * b" ..
-  with b_def `b \<noteq> 0` show "1 div b = a" by simp
-  from `is_unit a` have "a dvd c" ..
-  then obtain d where "c = a * d" ..
-  with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
-    by (simp add: mult.assoc mult.left_commute [of a])
-qed
-
-lemma unit_prod [intro]:
-  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
-  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
-  
-lemma unit_div [intro]:
-  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
-  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
-
-lemma mult_unit_dvd_iff:
-  assumes "is_unit b"
-  shows "a * b dvd c \<longleftrightarrow> a dvd c"
-proof
-  assume "a * b dvd c"
-  with assms show "a dvd c"
-    by (simp add: dvd_mult_left)
-next
-  assume "a dvd c"
-  then obtain k where "c = a * k" ..
-  with assms have "c = (a * b) * (1 div b * k)"
-    by (simp add: mult_ac)
-  then show "a * b dvd c" by (rule dvdI)
-qed
-
-lemma dvd_mult_unit_iff:
-  assumes "is_unit b"
-  shows "a dvd c * b \<longleftrightarrow> a dvd c"
-proof
-  assume "a dvd c * b"
-  with assms have "c * b dvd c * (b * (1 div b))"
-    by (subst mult_assoc [symmetric]) simp
-  also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
-  finally have "c * b dvd c" by simp
-  with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
-next
-  assume "a dvd c"
-  then show "a dvd c * b" by simp
-qed
-
-lemma div_unit_dvd_iff:
-  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
-  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
-
-lemma dvd_div_unit_iff:
-  "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
-  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
-
-lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
-  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
-
-lemma unit_mult_div_div [simp]:
-  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
-  by (erule is_unitE [of _ b]) simp
-
-lemma unit_div_mult_self [simp]:
-  "is_unit a \<Longrightarrow> b div a * a = b"
-  by (rule dvd_div_mult_self) auto
-
-lemma unit_div_1_div_1 [simp]:
-  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
-  by (erule is_unitE) simp
-
-lemma unit_div_mult_swap:
-  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
-  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
-
-lemma unit_div_commute:
-  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
-  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
-
-lemma unit_eq_div1:
-  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
-  by (auto elim: is_unitE)
-
-lemma unit_eq_div2:
-  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
-  using unit_eq_div1 [of b c a] by auto
-
-lemma unit_mult_left_cancel:
-  assumes "is_unit a"
-  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
-  using assms mult_cancel_left [of a b c] by auto 
-
-lemma unit_mult_right_cancel:
-  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
-  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
-
-lemma unit_div_cancel:
-  assumes "is_unit a"
-  shows "b div a = c div a \<longleftrightarrow> b = c"
-proof -
-  from assms have "is_unit (1 div a)" by simp
-  then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
-    by (rule unit_mult_right_cancel)
-  with assms show ?thesis by simp
-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 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
-
-lemma associated_0 [simp]:
-  "associated 0 b \<longleftrightarrow> b = 0"
-  "associated a 0 \<longleftrightarrow> a = 0"
-  by (auto dest: associatedD1 associatedD2)
-
-lemma associated_unit:
-  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
-  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
-
-lemma is_unit_associatedI:
-  assumes "is_unit c" and "a = c * b"
-  shows "associated a b"
-proof (rule associatedI)
-  from `a = c * b` show "b dvd a" by auto
-  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
-  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
-  ultimately have "b = a * d" by (simp add: ac_simps)
-  then show "a dvd b" ..
-qed
-
-lemma associated_is_unitE:
-  assumes "associated a b"
-  obtains c where "is_unit c" and "a = c * b"
-proof (cases "b = 0")
-  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
-  with that show thesis .
-next
-  case False
-  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
-  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
-  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
-  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
-  then have "is_unit c" by auto
-  with `a = c * b` that show thesis by blast
-qed
-  
-lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
-  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
-  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
-  unit_eq_div1 unit_eq_div2
-
-end
-
-lemma is_unit_int:
-  "is_unit (k::int) \<longleftrightarrow> k = 1 \<or> k = - 1"
-  by auto
-
   
 text {*
   A Euclidean semiring is a semiring upon which the Euclidean algorithm can be

--- a/src/HOL/Rings.thy	Fri Jun 19 07:53:33 2015 +0200
+++ b/src/HOL/Rings.thy	Fri Jun 19 07:53:35 2015 +0200
@@ -630,6 +630,260 @@
 
 class idom_divide = idom + semidom_divide
 
+class algebraic_semidom = semidom_divide
+begin
+
+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)
+
+lemma dvd_mult_div_cancel [simp]:
+  "a dvd b \<Longrightarrow> a * (b div a) = b"
+  using dvd_div_mult_self [of a b] by (simp add: ac_simps)
+  
+lemma div_mult_swap:
+  assumes "c dvd b"
+  shows "a * (b div c) = (a * b) div c"
+proof (cases "c = 0")
+  case True then show ?thesis by simp
+next
+  case False from assms obtain d where "b = c * d" ..
+  moreover from False have "a * divide (d * c) c = ((a * d) * c) div c"
+    by simp
+  ultimately show ?thesis by (simp add: ac_simps)
+qed
+
+lemma dvd_div_mult:
+  assumes "c dvd b"
+  shows "b div c * a = (b * a) div c"
+  using assms div_mult_swap [of c b a] by (simp add: ac_simps)
+
+  
+text \<open>Units: invertible elements in a ring\<close>
+
+abbreviation is_unit :: "'a \<Rightarrow> bool"
+where
+  "is_unit a \<equiv> a dvd 1"
+
+lemma not_is_unit_0 [simp]:
+  "\<not> is_unit 0"
+  by simp
+
+lemma unit_imp_dvd [dest]: 
+  "is_unit b \<Longrightarrow> b dvd a"
+  by (rule dvd_trans [of _ 1]) simp_all
+
+lemma unit_dvdE:
+  assumes "is_unit a"
+  obtains c where "a \<noteq> 0" and "b = a * c"
+proof -
+  from assms have "a dvd b" by auto
+  then obtain c where "b = a * c" ..
+  moreover from assms have "a \<noteq> 0" by auto
+  ultimately show thesis using that by blast
+qed
+
+lemma dvd_unit_imp_unit:
+  "a dvd b \<Longrightarrow> is_unit b \<Longrightarrow> is_unit a"
+  by (rule dvd_trans)
+
+lemma unit_div_1_unit [simp, intro]:
+  assumes "is_unit a"
+  shows "is_unit (1 div a)"
+proof -
+  from assms have "1 = 1 div a * a" by simp
+  then show "is_unit (1 div a)" by (rule dvdI)
+qed
+
+lemma is_unitE [elim?]:
+  assumes "is_unit a"
+  obtains b where "a \<noteq> 0" and "b \<noteq> 0"
+    and "is_unit b" and "1 div a = b" and "1 div b = a"
+    and "a * b = 1" and "c div a = c * b"
+proof (rule that)
+  def b \<equiv> "1 div a"
+  then show "1 div a = b" by simp
+  from b_def `is_unit a` show "is_unit b" by simp
+  from `is_unit a` and `is_unit b` show "a \<noteq> 0" and "b \<noteq> 0" by auto
+  from b_def `is_unit a` show "a * b = 1" by simp
+  then have "1 = a * b" ..
+  with b_def `b \<noteq> 0` show "1 div b = a" by simp
+  from `is_unit a` have "a dvd c" ..
+  then obtain d where "c = a * d" ..
+  with `a \<noteq> 0` `a * b = 1` show "c div a = c * b"
+    by (simp add: mult.assoc mult.left_commute [of a])
+qed
+
+lemma unit_prod [intro]:
+  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a * b)"
+  by (subst mult_1_left [of 1, symmetric]) (rule mult_dvd_mono) 
+  
+lemma unit_div [intro]:
+  "is_unit a \<Longrightarrow> is_unit b \<Longrightarrow> is_unit (a div b)"
+  by (erule is_unitE [of b a]) (simp add: ac_simps unit_prod)
+
+lemma mult_unit_dvd_iff:
+  assumes "is_unit b"
+  shows "a * b dvd c \<longleftrightarrow> a dvd c"
+proof
+  assume "a * b dvd c"
+  with assms show "a dvd c"
+    by (simp add: dvd_mult_left)
+next
+  assume "a dvd c"
+  then obtain k where "c = a * k" ..
+  with assms have "c = (a * b) * (1 div b * k)"
+    by (simp add: mult_ac)
+  then show "a * b dvd c" by (rule dvdI)
+qed
+
+lemma dvd_mult_unit_iff:
+  assumes "is_unit b"
+  shows "a dvd c * b \<longleftrightarrow> a dvd c"
+proof
+  assume "a dvd c * b"
+  with assms have "c * b dvd c * (b * (1 div b))"
+    by (subst mult_assoc [symmetric]) simp
+  also from `is_unit b` have "b * (1 div b) = 1" by (rule is_unitE) simp
+  finally have "c * b dvd c" by simp
+  with `a dvd c * b` show "a dvd c" by (rule dvd_trans)
+next
+  assume "a dvd c"
+  then show "a dvd c * b" by simp
+qed
+
+lemma div_unit_dvd_iff:
+  "is_unit b \<Longrightarrow> a div b dvd c \<longleftrightarrow> a dvd c"
+  by (erule is_unitE [of _ a]) (auto simp add: mult_unit_dvd_iff)
+
+lemma dvd_div_unit_iff:
+  "is_unit b \<Longrightarrow> a dvd c div b \<longleftrightarrow> a dvd c"
+  by (erule is_unitE [of _ c]) (simp add: dvd_mult_unit_iff)
+
+lemmas unit_dvd_iff = mult_unit_dvd_iff div_unit_dvd_iff
+  dvd_mult_unit_iff dvd_div_unit_iff -- \<open>FIXME consider fact collection\<close>
+
+lemma unit_mult_div_div [simp]:
+  "is_unit a \<Longrightarrow> b * (1 div a) = b div a"
+  by (erule is_unitE [of _ b]) simp
+
+lemma unit_div_mult_self [simp]:
+  "is_unit a \<Longrightarrow> b div a * a = b"
+  by (rule dvd_div_mult_self) auto
+
+lemma unit_div_1_div_1 [simp]:
+  "is_unit a \<Longrightarrow> 1 div (1 div a) = a"
+  by (erule is_unitE) simp
+
+lemma unit_div_mult_swap:
+  "is_unit c \<Longrightarrow> a * (b div c) = (a * b) div c"
+  by (erule unit_dvdE [of _ b]) (simp add: mult.left_commute [of _ c])
+
+lemma unit_div_commute:
+  "is_unit b \<Longrightarrow> (a div b) * c = (a * c) div b"
+  using unit_div_mult_swap [of b c a] by (simp add: ac_simps)
+
+lemma unit_eq_div1:
+  "is_unit b \<Longrightarrow> a div b = c \<longleftrightarrow> a = c * b"
+  by (auto elim: is_unitE)
+
+lemma unit_eq_div2:
+  "is_unit b \<Longrightarrow> a = c div b \<longleftrightarrow> a * b = c"
+  using unit_eq_div1 [of b c a] by auto
+
+lemma unit_mult_left_cancel:
+  assumes "is_unit a"
+  shows "a * b = a * c \<longleftrightarrow> b = c" (is "?P \<longleftrightarrow> ?Q")
+  using assms mult_cancel_left [of a b c] by auto 
+
+lemma unit_mult_right_cancel:
+  "is_unit a \<Longrightarrow> b * a = c * a \<longleftrightarrow> b = c"
+  using unit_mult_left_cancel [of a b c] by (auto simp add: ac_simps)
+
+lemma unit_div_cancel:
+  assumes "is_unit a"
+  shows "b div a = c div a \<longleftrightarrow> b = c"
+proof -
+  from assms have "is_unit (1 div a)" by simp
+  then have "b * (1 div a) = c * (1 div a) \<longleftrightarrow> b = c"
+    by (rule unit_mult_right_cancel)
+  with assms show ?thesis by simp
+qed
+  
+
+text \<open>Associated elements in a ring – an equivalence relation induced by the quasi-order divisibility \<close>
+
+definition associated :: "'a \<Rightarrow> 'a \<Rightarrow> bool" 
+where
+  "associated a b \<longleftrightarrow> a dvd b \<and> b dvd a"
+
+lemma associatedI:
+  "a dvd b \<Longrightarrow> b dvd a \<Longrightarrow> associated a b"
+  by (simp add: associated_def)
+
+lemma associatedD1:
+  "associated a b \<Longrightarrow> a dvd b"
+  by (simp add: associated_def)
+
+lemma associatedD2:
+  "associated a b \<Longrightarrow> b dvd a"
+  by (simp add: associated_def)
+
+lemma associated_refl [simp]:
+  "associated a a"
+  by (auto intro: associatedI)
+
+lemma associated_sym:
+  "associated b a \<longleftrightarrow> associated a b"
+  by (auto intro: associatedI dest: associatedD1 associatedD2)
+
+lemma associated_trans:
+  "associated a b \<Longrightarrow> associated b c \<Longrightarrow> associated a c"
+  by (auto intro: associatedI dvd_trans dest: associatedD1 associatedD2)
+
+lemma associated_0 [simp]:
+  "associated 0 b \<longleftrightarrow> b = 0"
+  "associated a 0 \<longleftrightarrow> a = 0"
+  by (auto dest: associatedD1 associatedD2)
+
+lemma associated_unit:
+  "associated a b \<Longrightarrow> is_unit a \<Longrightarrow> is_unit b"
+  using dvd_unit_imp_unit by (auto dest!: associatedD1 associatedD2)
+
+lemma is_unit_associatedI:
+  assumes "is_unit c" and "a = c * b"
+  shows "associated a b"
+proof (rule associatedI)
+  from `a = c * b` show "b dvd a" by auto
+  from `is_unit c` obtain d where "c * d = 1" by (rule is_unitE)
+  moreover from `a = c * b` have "d * a = d * (c * b)" by simp
+  ultimately have "b = a * d" by (simp add: ac_simps)
+  then show "a dvd b" ..
+qed
+
+lemma associated_is_unitE:
+  assumes "associated a b"
+  obtains c where "is_unit c" and "a = c * b"
+proof (cases "b = 0")
+  case True with assms have "is_unit 1" and "a = 1 * b" by simp_all
+  with that show thesis .
+next
+  case False
+  from assms have "a dvd b" and "b dvd a" by (auto dest: associatedD1 associatedD2)
+  then obtain c d where "b = a * d" and "a = b * c" by (blast elim: dvdE)
+  then have "a = c * b" and "(c * d) * b = 1 * b" by (simp_all add: ac_simps)
+  with False have "c * d = 1" using mult_cancel_right [of "c * d" b 1] by simp
+  then have "is_unit c" by auto
+  with `a = c * b` that show thesis by blast
+qed
+  
+lemmas unit_simps = mult_unit_dvd_iff div_unit_dvd_iff dvd_mult_unit_iff 
+  dvd_div_unit_iff unit_div_mult_swap unit_div_commute
+  unit_mult_left_cancel unit_mult_right_cancel unit_div_cancel 
+  unit_eq_div1 unit_eq_div2
+
+end
+
 class ordered_semiring = semiring + comm_monoid_add + ordered_ab_semigroup_add +
   assumes mult_left_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> c * a \<le> c * b"
   assumes mult_right_mono: "a \<le> b \<Longrightarrow> 0 \<le> c \<Longrightarrow> a * c \<le> b * c"