diff -r 33dbbcb6a8a3 -r 01488b559910 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Jul 08 14:01:40 2015 +0200
+++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:41 2015 +0200
@@ -74,16 +74,6 @@
 
 end
 
-context algebraic_semidom
-begin
-
-lemma associated_1 [simp]:
-  "associated 1 a \<longleftrightarrow> is_unit a"
-  "associated a 1 \<longleftrightarrow> is_unit a"
-  by (auto simp add: associated_def)
-
-end
-
 declare One_nat_def [simp del]
 
 subsection {* GCD and LCM definitions *}
@@ -116,29 +106,11 @@
 
 lemma gcd_0_left [simp]:
   "gcd 0 a = normalize a"
-proof (rule associated_eqI)
-  show "associated (gcd 0 a) (normalize a)"
-    by (auto intro!: associatedI gcd_greatest)
-  show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0"
-  proof -
-    from that have "unit_factor (normalize (gcd 0 a)) = 1"
-      by (rule unit_factor_normalize)
-    then show ?thesis by simp
-  qed
-qed simp
+  by (rule associated_eqI) simp_all
 
 lemma gcd_0_right [simp]:
   "gcd a 0 = normalize a"
-proof (rule associated_eqI)
-  show "associated (gcd a 0) (normalize a)"
-    by (auto intro!: associatedI gcd_greatest)
-  show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0"
-  proof -
-    from that have "unit_factor (normalize (gcd a 0)) = 1"
-      by (rule unit_factor_normalize)
-    then show ?thesis by simp
-  qed
-qed simp
+  by (rule associated_eqI) simp_all
   
 lemma gcd_eq_0_iff [simp]:
   "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
@@ -169,7 +141,7 @@
 proof
   fix a b c
   show "gcd a b = gcd b a"
-    by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd)
+    by (rule associated_eqI) simp_all
   from gcd_dvd1 have "gcd (gcd a b) c dvd a"
     by (rule dvd_trans) simp
   moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
@@ -182,10 +154,8 @@
     by (rule dvd_trans) simp
   ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
     by (auto intro!: gcd_greatest)
-  from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))"
-    by (rule associatedI)
-  then show "gcd (gcd a b) c = gcd a (gcd b c)"
-    by (rule associated_eqI) (simp_all add: unit_factor_gcd)
+  from P1 P2 show "gcd (gcd a b) c = gcd a (gcd b c)"
+    by (rule associated_eqI) simp_all
 qed
 
 lemma gcd_self [simp]:
@@ -193,15 +163,13 @@
 proof -
   have "a dvd gcd a a"
     by (rule gcd_greatest) simp_all
-  then have "associated (gcd a a) (normalize a)"
-    by (auto intro: associatedI)
   then show ?thesis
-    by (auto intro: associated_eqI simp add: unit_factor_gcd)
+    by (auto intro: associated_eqI)
 qed
     
 lemma coprime_1_left [simp]:
   "coprime 1 a"
-  by (rule associated_eqI) (simp_all add: unit_factor_gcd)
+  by (rule associated_eqI) simp_all
 
 lemma coprime_1_right [simp]:
   "coprime a 1"
@@ -218,7 +186,7 @@
   moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
     by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
   ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
-    by - (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd)
+    by (auto intro: associated_eqI)
   then show ?thesis by (simp add: normalize_mult)
 qed
 
@@ -318,14 +286,15 @@
   fix a b c
   show "lcm a b = lcm b a"
     by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
-  have "associated (lcm (lcm a b) c) (lcm a (lcm b c))"
-    by (auto intro!: associatedI lcm_least
+  have "lcm (lcm a b) c dvd lcm a (lcm b c)"
+    and "lcm a (lcm b c) dvd lcm (lcm a b) c"
+    by (auto intro: lcm_least
       dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
       dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
       dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
       dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
   then show "lcm (lcm a b) c = lcm a (lcm b c)"
-    by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff)
+    by (rule associated_eqI) simp_all
 qed
 
 lemma lcm_self [simp]:
@@ -333,10 +302,8 @@
 proof -
   have "lcm a a dvd a"
     by (rule lcm_least) simp_all
-  then have "associated (lcm a a) (normalize a)"
-    by (auto intro: associatedI)
   then show ?thesis
-    by (rule associated_eqI) (auto simp add: unit_factor_lcm)
+    by (auto intro: associated_eqI)
 qed
 
 lemma gcd_mult_lcm [simp]:
@@ -471,10 +438,8 @@
       ultimately show ?thesis by (blast intro: dvd_trans)
     qed
   qed
-  ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
-    by (rule associatedI)
-  then show ?thesis
-    by (rule associated_eqI) (auto simp add: unit_factor_gcd unit_factor_Gcd)
+  ultimately show ?thesis
+    by (auto intro: associated_eqI)
 qed
 
 lemma dvd_Gcd: -- \<open>FIXME remove\<close>
@@ -507,10 +472,10 @@
     ultimately show "Gcd (normalize ` A) dvd a"
       by simp
   qed
-  then have "associated (Gcd (normalize ` A)) (Gcd A)"
-    by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
+  then have "Gcd (normalize ` A) dvd Gcd A" and "Gcd A dvd Gcd (normalize ` A)"
+    by (auto intro!: Gcd_greatest intro: Gcd_dvd)
   then show ?thesis
-    by (rule associated_eqI) (simp_all add: unit_factor_Gcd, auto dest!: bspec)
+    by (auto intro: associated_eqI)
 qed
 
 lemma Lcm_least:
@@ -604,10 +569,8 @@
       ultimately show ?thesis by (blast intro: dvd_trans)
     qed
   qed
-  ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))"
-    by (rule associatedI)
-  then show "lcm a (Lcm A) = Lcm (insert a A)"
-    by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff)
+  ultimately show "lcm a (Lcm A) = Lcm (insert a A)"
+    by (rule associated_eqI) (simp_all add: lcm_eq_0_iff)
 qed
   
 lemma Lcm_set [code_unfold]: