# HG changeset patch
# User haftmann
# Date 1455742316 -3600
# Node ID e66d7841d5a2dba24690e14ace468e1713ca0330
# Parent  759d684c0e60eecee239326908f47bc26685f677
further generalization and polishing

diff -r 759d684c0e60 -r e66d7841d5a2 NEWS
--- a/NEWS	Wed Feb 17 21:51:56 2016 +0100
+++ b/NEWS	Wed Feb 17 21:51:56 2016 +0100
@@ -35,6 +35,8 @@
 * Compound constants INFIMUM and SUPREMUM are mere abbreviations now.
 INCOMPATIBILITY.
 
+* Class semiring_Lcd merged into semiring_Gcd.  INCOMPATIBILITY.
+
 
 New in Isabelle2016 (February 2016)
 -----------------------------------
diff -r 759d684c0e60 -r e66d7841d5a2 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
+++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:56 2016 +0100
@@ -31,7 +31,7 @@
 imports Main
 begin
 
-subsection \<open>GCD and LCM definitions\<close>
+subsection \<open>Abstract GCD and LCM\<close>
 
 class gcd = zero + one + dvd +
   fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
@@ -67,6 +67,14 @@
   "b dvd c \<Longrightarrow> gcd a b dvd c"
   by (rule dvd_trans) (rule gcd_dvd2)
 
+lemma dvd_gcdD1:
+  "a dvd gcd b c \<Longrightarrow> a dvd b"
+  using gcd_dvd1 [of b c] by (blast intro: dvd_trans)
+
+lemma dvd_gcdD2:
+  "a dvd gcd b c \<Longrightarrow> a dvd c"
+  using gcd_dvd2 [of b c] by (blast intro: dvd_trans)
+
 lemma gcd_0_left [simp]:
   "gcd 0 a = normalize a"
   by (rule associated_eqI) simp_all
@@ -203,6 +211,14 @@
   "a dvd c \<Longrightarrow> a dvd lcm b c"
   by (rule dvd_trans) (assumption, blast)
 
+lemma lcm_dvdD1:
+  "lcm a b dvd c \<Longrightarrow> a dvd c"
+  using dvd_lcm1 [of a b] by (blast intro: dvd_trans)
+
+lemma lcm_dvdD2:
+  "lcm a b dvd c \<Longrightarrow> b dvd c"
+  using dvd_lcm2 [of a b] by (blast intro: dvd_trans)
+
 lemma lcm_least:
   assumes "a dvd c" and "b dvd c"
   shows "lcm a b dvd c"
@@ -350,16 +366,79 @@
   
 end
 
+class ring_gcd = comm_ring_1 + semiring_gcd
+
 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"
+  assumes dvd_Lcm: "a \<in> A \<Longrightarrow> a dvd Lcm A"
+    and Lcm_least: "(\<And>b. b \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> Lcm A dvd a"
+    and normalize_Lcm [simp]: "normalize (Lcm A) = Lcm A"
 begin
 
+lemma Lcm_Gcd:
+  "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
+  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
+
+lemma Gcd_Lcm:
+  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
+  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
+
 lemma Gcd_empty [simp]:
   "Gcd {} = 0"
   by (rule dvd_0_left, rule Gcd_greatest) simp
 
+lemma Lcm_empty [simp]:
+  "Lcm {} = 1"
+  by (auto intro: associated_eqI Lcm_least)
+
+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 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 Gcd_0_iff [simp]:
   "Gcd A = 0 \<longleftrightarrow> A \<subseteq> {0}" (is "?P \<longleftrightarrow> ?Q")
 proof
@@ -384,147 +463,6 @@
   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: \<comment> \<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
-
-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
-
-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 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 Gcd_Lcm:
-  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
-  by (rule associated_eqI) (auto intro: Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least)
- 
-lemma Lcm_empty [simp]:
-  "Lcm {} = 1"
-  by (simp add: Lcm_Gcd)
-
-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_1_iff [simp]:
   "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
 proof
@@ -548,6 +486,44 @@
     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 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 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 Lcm_eq_0_I:
   assumes "0 \<in> A"
   shows "Lcm A = 0"
@@ -558,6 +534,10 @@
     by simp
 qed
 
+lemma Gcd_UNIV [simp]:
+  "Gcd UNIV = 1"
+  using dvd_refl by (rule Gcd_eq_1_I) simp
+
 lemma Lcm_UNIV [simp]:
   "Lcm UNIV = 0"
   by (rule Lcm_eq_0_I) simp
@@ -573,25 +553,48 @@
       (auto simp add: lcm_eq_0_iff)
 qed
 
+lemma dvd_Gcd: \<comment> \<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
+
 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
+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
+
+end  
+
+
+subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
 
 instantiation nat :: gcd
 begin
 
-fun
-  gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
-where
-  "gcd_nat x y =
-   (if y = 0 then x else gcd y (x mod y))"
+fun gcd_nat  :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+where "gcd_nat x y =
+  (if y = 0 then x else gcd y (x mod y))"
 
-definition
-  lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
+definition lcm_nat :: "nat \<Rightarrow> nat \<Rightarrow> nat"
 where
   "lcm_nat x y = x * y div (gcd x y)"
 
@@ -602,22 +605,17 @@
 instantiation int :: gcd
 begin
 
-definition
-  gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
-where
-  "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
+definition gcd_int  :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "gcd_int x y = int (gcd (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
-definition
-  lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
-where
-  "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
+definition lcm_int :: "int \<Rightarrow> int \<Rightarrow> int"
+  where "lcm_int x y = int (lcm (nat \<bar>x\<bar>) (nat \<bar>y\<bar>))"
 
 instance ..
 
 end
 
-
-subsection \<open>Transfer setup\<close>
+text \<open>Transfer setup\<close>
 
 lemma transfer_nat_int_gcd:
   "(x::int) >= 0 \<Longrightarrow> y >= 0 \<Longrightarrow> gcd (nat x) (nat y) = nat (gcd x y)"
@@ -646,10 +644,6 @@
 declare transfer_morphism_int_nat[transfer add return:
     transfer_int_nat_gcd transfer_int_nat_gcd_closures]
 
-
-subsection \<open>GCD properties\<close>
-
-(* was gcd_induct *)
 lemma gcd_nat_induct:
   fixes m n :: nat
   assumes "\<And>m. P m 0"
@@ -722,11 +716,9 @@
 lemma lcm_ge_0_int [simp]: "lcm (x::int) y >= 0"
   by (simp add: lcm_int_def)
 
-(* was gcd_0, etc. *)
 lemma gcd_0_nat: "gcd (x::nat) 0 = x"
   by simp
 
-(* was igcd_0, etc. *)
 lemma gcd_0_int [simp]: "gcd (x::int) 0 = \<bar>x\<bar>"
   by (unfold gcd_int_def, auto)
 
@@ -741,7 +733,7 @@
 
 (* weaker, but useful for the simplifier *)
 
-lemma gcd_non_0_nat: "y ~= (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
+lemma gcd_non_0_nat: "y \<noteq> (0::nat) \<Longrightarrow> gcd (x::nat) y = gcd y (x mod y)"
   by simp
 
 lemma gcd_1_nat [simp]: "gcd (m::nat) 1 = 1"
@@ -790,18 +782,6 @@
   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)
-
-lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
-  by (metis gcd_dvd2 dvd_trans)
-
-lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
-  by (metis gcd_dvd1 dvd_trans)
-
-lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
-  by (metis gcd_dvd2 dvd_trans)
-
 lemma gcd_le1_nat [simp]: "a \<noteq> 0 \<Longrightarrow> gcd (a::nat) b \<le> a"
   by (rule dvd_imp_le, auto)
 
@@ -1096,17 +1076,32 @@
   ultimately show ?thesis using dvd_times_left_cancel_iff [of "gcd a b" _ 1] by simp
 qed
 
+lemma coprime:
+  "coprime a b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)" (is "?P \<longleftrightarrow> ?Q")
+proof
+  assume ?P then show ?Q by auto
+next
+  assume ?Q
+  then have "is_unit (gcd a b) \<longleftrightarrow> gcd a b dvd a \<and> gcd a b dvd b"
+    by blast
+  then have "is_unit (gcd a b)"
+    by simp
+  then show ?P
+    by simp
+qed
+
 end
 
-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_nat:
+  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
+  using coprime [of a b] by simp
 
 lemma coprime_Suc_0_nat:
-    "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
+  "coprime (a::nat) b \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> d = Suc 0)"
   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)"
+lemma coprime_int:
+  "coprime (a::int) b \<longleftrightarrow> (\<forall>d. d \<ge> 0 \<and> d dvd a \<and> d dvd b \<longleftrightarrow> d = 1)"
   using gcd_unique_int [of 1 a b]
   apply clarsimp
   apply (erule subst)
@@ -1136,7 +1131,6 @@
   assumes z: "gcd (a::int) b \<noteq> 0" and a: "a = a' * gcd a b" and
     b: "b = b' * gcd a b"
   shows    "coprime a' b'"
-
   apply (subgoal_tac "a' = a div gcd a b")
   apply (erule ssubst)
   apply (subgoal_tac "b' = b div gcd a b")
@@ -1709,7 +1703,7 @@
 qed
 
 
-subsection \<open>LCM properties\<close>
+subsection \<open>LCM properties  on @{typ nat} and @{typ int}\<close>
 
 lemma lcm_altdef_int [code]: "lcm (a::int) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
   by (simp add: lcm_int_def lcm_nat_def zdiv_int gcd_int_def)
@@ -1808,13 +1802,13 @@
   by auto
 
 
-subsection \<open>The complete divisibility lattice\<close>
+subsection \<open>The complete divisibility lattice on @{typ nat} and @{typ int}\<close>
 
 text\<open>Lifting gcd and lcm to sets (Gcd/Lcm).
 Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
 \<close>
 
-instantiation nat :: Gcd
+instantiation nat :: semiring_Gcd
 begin
 
 interpretation semilattice_neutr_set lcm "1::nat"
@@ -1863,35 +1857,22 @@
 definition
   "Gcd (M::nat set) = Lcm {d. \<forall>m\<in>M. d dvd m}"
 
-instance ..
-
-end
-
-instance nat :: semiring_Gcd
-proof
+instance proof
   show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
   using that by (induct N rule: infinite_finite_induct)
     (auto simp add: Gcd_nat_def)
   show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
   using that by (induct N rule: infinite_finite_induct)
     (auto simp add: Gcd_nat_def)
-qed simp
-
-instance nat :: semiring_Lcm
-proof
-  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
-    by (rule associated_eqI) (auto intro!: Gcd_dvd Gcd_greatest)
-qed
+  show "n dvd Lcm N" if "n \<in> N" for N and n ::nat
+  using that by (induct N rule: infinite_finite_induct)
+    auto
+  show "Lcm N dvd n" if "\<And>m. m \<in> N \<Longrightarrow> m dvd n" for N and n ::nat
+  using that by (induct N rule: infinite_finite_induct)
+    auto
+qed simp_all
 
-lemma Lcm_eq_0 [simp]:
-  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
-  by (rule Lcm_eq_0_I)
-
-lemma Lcm0_iff [simp]:
-  fixes M :: "nat set"
-  assumes "finite M" and "M \<noteq> {}"
-  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
-  using assms by (simp add: Lcm_0_iff)
+end
 
 text\<open>Alternative characterizations of Gcd:\<close>
 
@@ -1935,8 +1916,7 @@
 apply(rule antisym)
  apply(rule Max_ge, assumption)
  apply(erule (2) Lcm_in_lcm_closed_set_nat)
-apply clarsimp
-apply (metis Lcm0_iff dvd_Lcm_nat dvd_imp_le neq0_conv)
+apply (auto simp add: not_le Lcm_0_iff dvd_imp_le leD le_neq_trans)
 done
 
 lemma mult_inj_if_coprime_nat:
@@ -1956,7 +1936,7 @@
 
 subsubsection \<open>Setwise gcd and lcm for integers\<close>
 
-instantiation int :: Gcd
+instantiation int :: semiring_Gcd
 begin
 
 definition
@@ -1965,63 +1945,45 @@
 definition
   "Gcd M = int (Gcd (nat ` 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])
+
+end
+
+
+subsection \<open>GCD and LCM on @{typ integer}\<close>
+
+instantiation integer :: gcd
+begin
+
+context
+  includes integer.lifting
+begin
+
+lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is gcd .
+lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
+  is lcm .
+
+end
 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 image_image)
-qed
-
-lemma Lcm_dvd_int [simp]:
-  fixes M :: "int set"
-  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
-  using assms by (auto intro: Lcm_least)
-
-
-subsection \<open>gcd and lcm instances for @{typ integer}\<close>
-
-instantiation integer :: gcd begin
-context includes integer.lifting begin
-lift_definition gcd_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is gcd .
-lift_definition lcm_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer" is lcm .
-end
-instance ..
-end
 lifting_update integer.lifting
 lifting_forget integer.lifting
 
-context includes integer.lifting begin
+context
+  includes integer.lifting
+begin
 
 lemma gcd_code_integer [code]:
   "gcd k l = \<bar>if l = (0::integer) then k else gcd l (\<bar>k\<bar> mod \<bar>l\<bar>)\<bar>"
-by transfer(fact gcd_code_int)
+  by transfer (fact gcd_code_int)
 
 lemma lcm_code_integer [code]: "lcm (a::integer) b = \<bar>a\<bar> * \<bar>b\<bar> div gcd a b"
-by transfer(fact lcm_altdef_int)
+  by transfer (fact lcm_altdef_int)
 
 end
 
@@ -2184,6 +2146,33 @@
 lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   by (fact comp_fun_idem_lcm)
 
+lemma Lcm_eq_0 [simp]:
+  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
+  by (rule Lcm_eq_0_I)
+
+lemma Lcm0_iff [simp]:
+  fixes M :: "nat set"
+  assumes "finite M" and "M \<noteq> {}"
+  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
+  using assms by (simp add: Lcm_0_iff)
+
+lemma Lcm_dvd_int [simp]:
+  fixes M :: "int set"
+  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
+  using assms by (auto intro: Lcm_least)
+
+lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
+  by (fact dvd_gcdD1)
+
+lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
+  by (fact dvd_gcdD2)
+
+lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
+  by (fact dvd_gcdD1)
+
+lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
+  by (fact dvd_gcdD2)
+
 interpretation dvd:
   order "op dvd" "\<lambda>n m :: nat. n dvd m \<and> m \<noteq> n"
   by standard (auto intro: dvd_refl dvd_trans dvd_antisym)