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 \ is_unit a"
 "associated a 1 \ 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 \ 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 \ 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 \ a = 0 \ b = 0" (is "?P \ ?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:  \FIXME remove\
@@ 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]: