diff -r 19f627407264 -r ccab07d1196c src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
+++ b/src/HOL/GCD.thy	Sat Dec 02 16:50:53 2017 +0000
@@ -1756,6 +1756,59 @@
 
 end
 
+lemma gcd_int_int_eq [simp]:
+  "gcd (int m) (int n) = int (gcd m n)"
+  by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_left_eq [simp]:
+  "gcd (nat \<bar>k\<bar>) n = nat (gcd k (int n))"
+  by (simp add: gcd_int_def)
+
+lemma gcd_nat_abs_right_eq [simp]:
+  "gcd n (nat \<bar>k\<bar>) = nat (gcd (int n) k)"
+  by (simp add: gcd_int_def)
+
+lemma abs_gcd_int [simp]:
+  "\<bar>gcd x y\<bar> = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def)
+
+lemma gcd_abs1_int [simp]:
+  "gcd \<bar>x\<bar> y = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def) simp
+
+lemma gcd_abs2_int [simp]:
+  "gcd x \<bar>y\<bar> = gcd x y"
+  for x y :: int
+  by (simp only: gcd_int_def) simp
+
+lemma lcm_int_int_eq [simp]:
+  "lcm (int m) (int n) = int (lcm m n)"
+  by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_left_eq [simp]:
+  "lcm (nat \<bar>k\<bar>) n = nat (lcm k (int n))"
+  by (simp add: lcm_int_def)
+
+lemma lcm_nat_abs_right_eq [simp]:
+  "lcm n (nat \<bar>k\<bar>) = nat (lcm (int n) k)"
+  by (simp add: lcm_int_def)
+
+lemma lcm_abs1_int [simp]:
+  "lcm \<bar>x\<bar> y = lcm x y"
+  for x y :: int
+  by (simp only: lcm_int_def) simp
+
+lemma lcm_abs2_int [simp]:
+  "lcm x \<bar>y\<bar> = lcm x y"
+  for x y :: int
+  by (simp only: lcm_int_def) simp
+
+lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
+  for i j :: int
+  by (simp only: lcm_int_def)
+
 lemma gcd_nat_induct:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
@@ -1767,35 +1820,13 @@
    apply simp_all
   done
 
-lemma gcd_eq_int_iff: "gcd k l = int n \<longleftrightarrow> gcd (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
-  by (simp add: gcd_int_def)
-
-lemma lcm_eq_int_iff: "lcm k l = int n \<longleftrightarrow> lcm (nat \<bar>k\<bar>) (nat \<bar>l\<bar>) = n"
-  by (simp add: lcm_int_def)
-
 lemma gcd_neg1_int [simp]: "gcd (- x) y = gcd x y"
   for x y :: int
-  by (simp add: gcd_int_def)
+  by (simp only: gcd_int_def) simp
 
 lemma gcd_neg2_int [simp]: "gcd x (- y) = gcd x y"
   for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma abs_gcd_int [simp]: "\<bar>gcd x y\<bar> = gcd x y"
-  for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma gcd_abs_int: "gcd x y = gcd \<bar>x\<bar> \<bar>y\<bar>"
-  for x y :: int
-  by (simp add: gcd_int_def)
-
-lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> y = gcd x y"
-  for x y :: int
-  by (metis abs_idempotent gcd_abs_int)
-
-lemma gcd_abs2_int [simp]: "gcd x \<bar>y\<bar> = gcd x y"
-  for x y :: int
-  by (metis abs_idempotent gcd_abs_int)
+  by (simp only: gcd_int_def) simp
 
 lemma gcd_cases_int:
   fixes x y :: int
@@ -1812,27 +1843,11 @@
 
 lemma lcm_neg1_int: "lcm (- x) y = lcm x y"
   for x y :: int
-  by (simp add: lcm_int_def)
+  by (simp only: lcm_int_def) simp
 
 lemma lcm_neg2_int: "lcm x (- y) = lcm x y"
   for x y :: int
-  by (simp add: lcm_int_def)
-
-lemma lcm_abs_int: "lcm x y = lcm \<bar>x\<bar> \<bar>y\<bar>"
-  for x y :: int
-  by (simp add: lcm_int_def)
-
-lemma abs_lcm_int [simp]: "\<bar>lcm i j\<bar> = lcm i j"
-  for i j :: int
-  by (simp add:lcm_int_def)
-
-lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> y = lcm x y"
-  for x y :: int
-  by (metis abs_idempotent lcm_int_def)
-
-lemma lcm_abs2_int [simp]: "lcm x \<bar>y\<bar> = lcm x y"
-  for x y :: int
-  by (metis abs_idempotent lcm_int_def)
+  by (simp only: lcm_int_def) simp
 
 lemma lcm_cases_int:
   fixes x y :: int
@@ -1845,7 +1860,7 @@
 
 lemma lcm_ge_0_int [simp]: "lcm x y \<ge> 0"
   for x y :: int
-  by (simp add: lcm_int_def)
+  by (simp only: lcm_int_def)
 
 lemma gcd_0_nat: "gcd x 0 = x"
   for x :: nat
@@ -1861,7 +1876,7 @@
 
 lemma gcd_0_left_int [simp]: "gcd 0 x = \<bar>x\<bar>"
   for x :: int
-  by (auto simp:gcd_int_def)
+  by (auto simp: gcd_int_def)
 
 lemma gcd_red_nat: "gcd x y = gcd y (x mod y)"
   for x y :: nat
@@ -1923,9 +1938,20 @@
 qed (simp_all add: lcm_nat_def)
 
 instance int :: ring_gcd
-  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)
+proof
+  fix k l r :: int
+  show "gcd k l dvd k" "gcd k l dvd l"
+    using gcd_dvd1 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+      gcd_dvd2 [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by simp_all
+  show "lcm k l = normalize (k * l) div gcd k l"
+    using lcm_gcd [of "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by (simp add: nat_eq_iff of_nat_div abs_mult)
+  assume "r dvd k" "r dvd l"
+  then show "r dvd gcd k l"
+    using gcd_greatest [of "nat \<bar>r\<bar>" "nat \<bar>k\<bar>" "nat \<bar>l\<bar>"]
+    by simp
+qed simp
 
 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd a b \<le> a"
   for a b :: nat
@@ -1975,7 +2001,7 @@
 
 lemma gcd_proj1_if_dvd_int [simp]: "x dvd y \<Longrightarrow> gcd x y = \<bar>x\<bar>"
   for x y :: int
-  by (metis abs_dvd_iff gcd_0_left_int gcd_abs_int gcd_unique_int)
+  by (metis abs_dvd_iff gcd_0_left_int gcd_unique_int)
 
 lemma gcd_proj2_if_dvd_int [simp]: "y dvd x \<Longrightarrow> gcd x y = \<bar>y\<bar>"
   for x y :: int
@@ -1995,7 +2021,7 @@
 
 lemma gcd_mult_distrib_int: "\<bar>k\<bar> * gcd m n = gcd (k * m) (k * n)"
   for k m n :: int
-  by (simp add: gcd_int_def abs_mult nat_mult_distrib gcd_mult_distrib_nat [symmetric])
+  using gcd_mult_distrib' [of k m n] by simp
 
 text \<open>\medskip Addition laws.\<close>
 
@@ -2097,7 +2123,7 @@
 
 lemma gcd_code_int [code]: "gcd k l = \<bar>if l = 0 then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
   for k l :: int
-  by (simp add: gcd_int_def nat_mod_distrib gcd_non_0_nat)
+  using gcd_red_int [of "\<bar>k\<bar>" "\<bar>l\<bar>"] by simp
 
 lemma coprime_Suc_left_nat [simp]:
   "coprime (Suc n) n"
@@ -2421,8 +2447,8 @@
 
 lemma lcm_altdef_int [code]: "lcm a b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   for a b :: int
-  by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
-
+  by (simp add: abs_mult lcm_gcd)
+  
 lemma prod_gcd_lcm_nat: "m * n = gcd m n * lcm m n"
   for m n :: nat
   unfolding lcm_nat_def
@@ -2439,11 +2465,11 @@
 
 lemma lcm_pos_nat: "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> lcm m n > 0"
   for m n :: nat
-  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
+  using lcm_eq_0_iff [of m n] by auto
 
 lemma lcm_pos_int: "m \<noteq> 0 \<Longrightarrow> n \<noteq> 0 \<Longrightarrow> lcm m n > 0"
   for m n :: int
-  by (simp add: lcm_int_def lcm_pos_nat)
+  by (simp add: less_le lcm_eq_0_iff)
 
 lemma dvd_pos_nat: "n > 0 \<Longrightarrow> m dvd n \<Longrightarrow> m > 0"  (* FIXME move *)
   for m n :: nat
@@ -2653,33 +2679,83 @@
 
 subsubsection \<open>Setwise GCD and LCM for integers\<close>
 
-instantiation int :: semiring_Gcd
+instantiation int :: Gcd
 begin
 
-definition "Lcm M = int (LCM m\<in>M. (nat \<circ> abs) m)"
-
-definition "Gcd M = int (GCD m\<in>M. (nat \<circ> abs) m)"
-
-instance
-  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])
+definition Gcd_int :: "int set \<Rightarrow> int"
+  where "Gcd K = int (GCD k\<in>K. (nat \<circ> abs) k)"
+
+definition Lcm_int :: "int set \<Rightarrow> int"
+  where "Lcm K = int (LCM k\<in>K. (nat \<circ> abs) k)"
+
+instance ..
 
 end
 
-lemma abs_Gcd [simp]: "\<bar>Gcd K\<bar> = Gcd K"
+lemma Gcd_int_eq [simp]:
+  "(GCD n\<in>N. int n) = int (Gcd N)"
+  by (simp add: Gcd_int_def image_image)
+
+lemma Gcd_nat_abs_eq [simp]:
+  "(GCD k\<in>K. nat \<bar>k\<bar>) = nat (Gcd K)"
+  by (simp add: Gcd_int_def)
+
+lemma abs_Gcd_eq [simp]:
+  "\<bar>Gcd K\<bar> = Gcd K" for K :: "int set"
+  by (simp only: Gcd_int_def)
+
+lemma Gcd_int_greater_eq_0 [simp]:
+  "Gcd K \<ge> 0"
   for K :: "int set"
-  using normalize_Gcd [of K] by simp
-
-lemma abs_Lcm [simp]: "\<bar>Lcm K\<bar> = Lcm K"
+  using abs_ge_zero [of "Gcd K"] by simp
+
+lemma Gcd_abs_eq [simp]:
+  "(GCD k\<in>K. \<bar>k\<bar>) = Gcd K"
   for K :: "int set"
-  using normalize_Lcm [of K] by simp
-
-lemma Gcm_eq_int_iff: "Gcd K = int n \<longleftrightarrow> Gcd ((nat \<circ> abs) ` K) = n"
-  by (simp add: Gcd_int_def comp_def image_image)
-
-lemma Lcm_eq_int_iff: "Lcm K = int n \<longleftrightarrow> Lcm ((nat \<circ> abs) ` K) = n"
-  by (simp add: Lcm_int_def comp_def image_image)
+  by (simp only: Gcd_int_def image_image) simp
+
+lemma Lcm_int_eq [simp]:
+  "(LCM n\<in>N. int n) = int (Lcm N)"
+  by (simp add: Lcm_int_def image_image)
+
+lemma Lcm_nat_abs_eq [simp]:
+  "(LCM k\<in>K. nat \<bar>k\<bar>) = nat (Lcm K)"
+  by (simp add: Lcm_int_def)
+
+lemma abs_Lcm_eq [simp]:
+  "\<bar>Lcm K\<bar> = Lcm K" for K :: "int set"
+  by (simp only: Lcm_int_def)
+
+lemma Lcm_int_greater_eq_0 [simp]:
+  "Lcm K \<ge> 0"
+  for K :: "int set"
+  using abs_ge_zero [of "Lcm K"] by simp
+
+lemma Lcm_abs_eq [simp]:
+  "(LCM k\<in>K. \<bar>k\<bar>) = Lcm K"
+  for K :: "int set"
+  by (simp only: Lcm_int_def image_image) simp
+
+instance int :: semiring_Gcd
+proof
+  fix K :: "int set" and k :: int
+  show "Gcd K dvd k" and "k dvd Lcm K" if "k \<in> K"
+    using that Gcd_dvd [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+      dvd_Lcm [of "nat \<bar>k\<bar>" "(nat \<circ> abs) ` K"]
+    by (simp_all add: comp_def)
+  show "k dvd Gcd K" if "\<And>l. l \<in> K \<Longrightarrow> k dvd l"
+  proof -
+    have "nat \<bar>k\<bar> dvd (GCD k\<in>K. nat \<bar>k\<bar>)"
+      by (rule Gcd_greatest) (use that in auto)
+    then show ?thesis by simp
+  qed
+  show "Lcm K dvd k" if "\<And>l. l \<in> K \<Longrightarrow> l dvd k"
+  proof -
+    have "(LCM k\<in>K. nat \<bar>k\<bar>) dvd nat \<bar>k\<bar>"
+      by (rule Lcm_least) (use that in auto)
+    then show ?thesis by simp
+  qed
+qed simp_all
 
 
 subsection \<open>GCD and LCM on @{typ integer}\<close>