# HG changeset patch
# User haftmann
# Date 1455742318 -3600
# Node ID 7f927120b5a2f11fe728125e87e5a8cec4180216
# Parent  35a9e1cbb5b345cca9921973b58abd26151dfb6a
dropped various legacy fact bindings and tuned proofs

diff -r 35a9e1cbb5b3 -r 7f927120b5a2 NEWS
--- a/NEWS	Wed Feb 17 21:51:58 2016 +0100
+++ b/NEWS	Wed Feb 17 21:51:58 2016 +0100
@@ -107,8 +107,32 @@
   inj_int ~> inj_of_nat
   int_1 ~> of_nat_1
   int_0 ~> of_nat_0
+  Lcm_empty_nat ~> Lcm_empty
+  Lcm_empty_int ~> Lcm_empty
+  Lcm_insert_nat ~> Lcm_insert
+  Lcm_insert_int ~> Lcm_insert
+  comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
+  comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
+  comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
+  comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
+  Lcm_eq_0 ~> Lcm_eq_0_I
+  Lcm0_iff ~> Lcm_0_iff
+  Lcm_dvd_int ~> Lcm_least
+  divides_mult_nat ~> divides_mult
+  divides_mult_int ~> divides_mult
+  lcm_0_nat ~> lcm_0_right
+  lcm_0_int ~> lcm_0_right
+  lcm_0_left_nat ~> lcm_0_left
+  lcm_0_left_int ~> lcm_0_left
+  dvd_gcd_D1_nat ~> dvd_gcdD1
+  dvd_gcd_D1_int ~> dvd_gcdD1
+  dvd_gcd_D2_nat ~> dvd_gcdD2
+  dvd_gcd_D2_int ~> dvd_gcdD2
+  coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
+  coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
   realpow_minus_mult ~> power_minus_mult
   realpow_Suc_le_self ~> power_Suc_le_self
+  dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
 INCOMPATIBILITY.
 
 
diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
@@ -585,10 +585,6 @@
       (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
@@ -715,16 +711,16 @@
 lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
   by (simp add: gcd_int_def)
 
-lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
+lemma abs_gcd_int [simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
 by(simp add: gcd_int_def)
 
 lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
 by (simp add: gcd_int_def)
 
-lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
+lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
 by (metis abs_idempotent gcd_abs_int)
 
-lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
+lemma gcd_abs2_int [simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
 by (metis abs_idempotent gcd_abs_int)
 
 lemma gcd_cases_int:
@@ -751,10 +747,10 @@
 lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
   by (simp add:lcm_int_def)
 
-lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
+lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
   by (metis abs_idempotent lcm_int_def)
 
-lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
+lemma lcm_abs2_int [simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
   by (metis abs_idempotent lcm_int_def)
 
 lemma lcm_cases_int:
@@ -1047,38 +1043,44 @@
 
 (* to do: add the three variations of these, and for ints? *)
 
-lemma finite_divisors_nat[simp]:
-  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
+lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
+  fixes m :: nat
+  assumes "m > 0" 
+  shows "finite {d. d dvd m}"
 proof-
-  have "finite{d. d <= m}"
-    by (blast intro: bounded_nat_set_is_finite)
-  from finite_subset[OF _ this] show ?thesis using assms
-    by (metis Collect_mono dvd_imp_le neq0_conv)
+  from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
+    by (auto dest: dvd_imp_le)
+  then show ?thesis
+    using finite_Collect_le_nat by (rule finite_subset)
 qed
 
-lemma finite_divisors_int[simp]:
-  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
-proof-
-  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
-  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
-  from finite_subset[OF _ this] show ?thesis using assms
+lemma finite_divisors_int [simp]:
+  fixes i :: int
+  assumes "i \<noteq> 0"
+  shows "finite {d. d dvd i}"
+proof -
+  have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
+    by (auto simp: abs_if)
+  then have "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}"
+    by simp
+  from finite_subset [OF _ this] show ?thesis using assms
     by (simp add: dvd_imp_le_int subset_iff)
 qed
 
-lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
+lemma Max_divisors_self_nat [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
 apply(rule antisym)
  apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
 apply simp
 done
 
-lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
+lemma Max_divisors_self_int [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
 apply(rule antisym)
  apply(rule Max_le_iff [THEN iffD2])
   apply (auto intro: abs_le_D1 dvd_imp_le_int)
 done
 
 lemma gcd_is_Max_divisors_nat:
-  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
+  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd (m::nat) n = Max {d. d dvd m \<and> d dvd n}"
 apply(rule Max_eqI[THEN sym])
   apply (metis finite_Collect_conjI finite_divisors_nat)
  apply simp
@@ -1438,35 +1440,33 @@
   ultimately show ?thesis by blast
 qed
 
-lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
+lemma pow_divides_eq_nat [simp]:
+  "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   by (auto intro: pow_divides_pow_nat dvd_power_same)
 
-lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
+lemma pow_divides_eq_int [simp]:
+  "n ~= 0 \<Longrightarrow> (a::int) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   by (auto intro: pow_divides_pow_int dvd_power_same)
 
-lemma divides_mult_nat:
-  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
-  shows "m * n dvd r"
+context semiring_gcd
+begin
+
+lemma divides_mult:
+  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
+  shows "a * b dvd c"
 proof-
-  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
-    unfolding dvd_def by blast
-  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
-  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
-  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
-  from n' k show ?thesis unfolding dvd_def by auto
+  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
+  with \<open>a dvd c\<close> have "a dvd b' * b"
+    by (simp add: ac_simps)
+  with \<open>coprime a b\<close> have "a dvd b'"
+    by (simp add: coprime_dvd_mult_iff)
+  then obtain a' where "b' = a * a'" ..
+  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
+    by (simp add: ac_simps)
+  then show ?thesis ..
 qed
 
-lemma divides_mult_int:
-  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
-  shows "m * n dvd r"
-proof-
-  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
-    unfolding dvd_def by blast
-  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
-  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
-  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
-  from n' k show ?thesis unfolding dvd_def by auto
-qed
+end
 
 lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   by (simp add: gcd.commute del: One_nat_def)
@@ -1773,18 +1773,6 @@
   apply (simp, simp add: abs_mult)
 done
 
-lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
-  unfolding lcm_nat_def by simp
-
-lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
-  unfolding lcm_int_def by simp
-
-lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
-  unfolding lcm_nat_def by simp
-
-lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
-  unfolding lcm_int_def by simp
-
 lemma lcm_pos_nat:
   "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
 by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
@@ -1796,7 +1784,7 @@
   apply auto
   done
 
-lemma dvd_pos_nat:
+lemma dvd_pos_nat: -- \<open>FIXME move\<close>
   fixes n m :: nat
   assumes "n > 0" and "m dvd n"
   shows "m > 0"
@@ -1828,16 +1816,16 @@
 lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
 by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
 
-lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
+lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
 by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
 
-lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
+lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
 by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
 
-lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
+lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
 by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
 
-lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
+lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
 by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
 
 lemma (in semiring_gcd) comp_fun_idem_gcd:
@@ -1848,10 +1836,12 @@
   "comp_fun_idem lcm"
   by standard (simp_all add: fun_eq_iff ac_simps)
 
-lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
-  by (simp only: lcm_eq_1_iff) simp
+lemma lcm_1_iff_nat [simp]:
+  "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
+  using lcm_eq_1_iff [of m n] by simp
   
-lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
+lemma lcm_1_iff_int [simp]:
+  "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   by auto
 
 
@@ -1897,14 +1887,15 @@
   fixes M :: "nat set"
   assumes "\<forall>m\<in>M. m dvd n"
   shows "Lcm M dvd n"
-proof (cases "n = 0")
-  case True then show ?thesis by simp
+proof (cases "n > 0")
+  case False then show ?thesis by simp
 next
-  case False
+  case True
   then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
   moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
   ultimately have "finite M" by (rule rev_finite_subset)
-  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
+  then show ?thesis using assms
+    by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
 qed
 
 definition
@@ -1933,17 +1924,25 @@
 
 text\<open>Alternative characterizations of Gcd:\<close>
 
-lemma Gcd_eq_Max: "finite(M::nat set) \<Longrightarrow> M \<noteq> {} \<Longrightarrow> 0 \<notin> M \<Longrightarrow> Gcd M = Max(\<Inter>m\<in>M. {d. d dvd m})"
-apply(rule antisym)
- apply(rule Max_ge)
-  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
- apply (simp add: Gcd_dvd)
-apply (rule Max_le_iff[THEN iffD2])
-  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
- apply fastforce
-apply clarsimp
-apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
-done
+lemma Gcd_eq_Max:
+  fixes M :: "nat set"
+  assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
+  shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
+proof (rule antisym)
+  from assms obtain m where "m \<in> M" and "m > 0"
+    by auto
+  from \<open>m > 0\<close> have "finite {d. d dvd m}"
+    by (blast intro: finite_divisors_nat)
+  with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
+    by blast
+  from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
+    by (auto intro: Max_ge Gcd_dvd)
+  from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
+    apply (rule Max.boundedI)
+    apply auto
+    apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
+    done
+qed
 
 lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
 apply(induct pred:finite)
@@ -2088,7 +2087,7 @@
 
 text \<open>Fact aliasses\<close>
 
-lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
+lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   by (fact lcm_eq_0_iff)
 
 lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
@@ -2103,17 +2102,9 @@
 lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   by (fact dvd_lcmI1)
 
-lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
+lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   by (fact dvd_lcmI2)
 
-lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
-    (k dvd m * n) = (k dvd m)"
-  by (fact coprime_dvd_mult_iff)
-
-lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
-    (k dvd m * n) = (k dvd m)"
-  by (fact coprime_dvd_mult_iff)
-
 lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   by (fact coprime_exp2)
 
@@ -2122,29 +2113,13 @@
 
 lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
 lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
-lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
-lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
+lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
+lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
 
 lemma dvd_Lcm_int [simp]:
   fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   using assms by (fact dvd_Lcm)
 
-lemma Lcm_empty_nat:
-  "Lcm {} = (1::nat)"
-  by (fact Lcm_empty)
-
-lemma Lcm_empty_int:
-  "Lcm {} = (1::int)"
-  by (fact Lcm_empty)
-
-lemma Lcm_insert_nat:
-  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
-  by (fact Lcm_insert)
-
-lemma Lcm_insert_int:
-  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
-  by (fact Lcm_insert)
-
 lemma gcd_neg_numeral_1_int [simp]:
   "gcd (- numeral n :: int) x = gcd (numeral n) x"
   by (fact gcd_neg1_int)
@@ -2159,43 +2134,8 @@
 lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   by (fact gcd_nat.absorb2)
 
-lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
-  by (fact comp_fun_idem_gcd)
-
-lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
-  by (fact comp_fun_idem_gcd)
-
-lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
-  by (fact comp_fun_idem_lcm)
-
-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)
+lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
+lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
+lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
 
 end
diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/Number_Theory/Cong.thy
--- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:58 2016 +0100
@@ -267,7 +267,7 @@
 
 lemma cong_mult_rcancel_int:
     "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
-  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute)
+  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
 
 lemma cong_mult_rcancel_nat:
     "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
@@ -285,7 +285,7 @@
 lemma coprime_cong_mult_int:
   "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
     \<Longrightarrow> [a = b] (mod m * n)"
-by (metis divides_mult_int cong_altdef_int)
+by (metis divides_mult cong_altdef_int)
 
 lemma coprime_cong_mult_nat:
   assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
diff -r 35a9e1cbb5b3 -r 7f927120b5a2 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:58 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:58 2016 +0100
@@ -1064,11 +1064,11 @@
   "Lcm {} = 1"
   by (simp add: Lcm_1_iff)
 
-lemma Lcm_eq_0 [simp]:
+lemma Lcm_eq_0_I [simp]:
   "0 \<in> A \<Longrightarrow> Lcm A = 0"
   by (drule dvd_Lcm) simp
 
-lemma Lcm0_iff':
+lemma Lcm_0_iff':
   "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
 proof
   assume "Lcm A = 0"
@@ -1092,7 +1092,7 @@
   qed
 qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
 
-lemma Lcm0_iff [simp]:
+lemma Lcm_0_iff [simp]:
   "finite A \<Longrightarrow> Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
 proof -
   assume "finite A"
@@ -1108,7 +1108,7 @@
       done
     moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
     ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
-    with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
+    with Lcm_0_iff' have "Lcm A \<noteq> 0" by simp
   }
   ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
 qed
@@ -1210,7 +1210,7 @@
 
 lemma Lcm_Gcd:
   "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
-  by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
+  by (rule LcmI[symmetric]) (auto intro: Gcd_greatest Gcd_greatest)
 
 lemma Gcd_1:
   "1 \<in> A \<Longrightarrow> Gcd A = 1"