dropped various legacy fact bindings and tuned proofs
authorhaftmann
Wed Feb 17 21:51:58 2016 +0100 (2016-02-17)
changeset 623537f927120b5a2
parent 62352 35a9e1cbb5b3
child 62357 ab76bd43c14a
dropped various legacy fact bindings and tuned proofs
NEWS
src/HOL/GCD.thy
src/HOL/Number_Theory/Cong.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     1.1 --- a/NEWS	Wed Feb 17 21:51:58 2016 +0100
     1.2 +++ b/NEWS	Wed Feb 17 21:51:58 2016 +0100
     1.3 @@ -107,8 +107,32 @@
     1.4    inj_int ~> inj_of_nat
     1.5    int_1 ~> of_nat_1
     1.6    int_0 ~> of_nat_0
     1.7 +  Lcm_empty_nat ~> Lcm_empty
     1.8 +  Lcm_empty_int ~> Lcm_empty
     1.9 +  Lcm_insert_nat ~> Lcm_insert
    1.10 +  Lcm_insert_int ~> Lcm_insert
    1.11 +  comp_fun_idem_gcd_nat ~> comp_fun_idem_gcd
    1.12 +  comp_fun_idem_gcd_int ~> comp_fun_idem_gcd
    1.13 +  comp_fun_idem_lcm_nat ~> comp_fun_idem_lcm
    1.14 +  comp_fun_idem_lcm_int ~> comp_fun_idem_lcm
    1.15 +  Lcm_eq_0 ~> Lcm_eq_0_I
    1.16 +  Lcm0_iff ~> Lcm_0_iff
    1.17 +  Lcm_dvd_int ~> Lcm_least
    1.18 +  divides_mult_nat ~> divides_mult
    1.19 +  divides_mult_int ~> divides_mult
    1.20 +  lcm_0_nat ~> lcm_0_right
    1.21 +  lcm_0_int ~> lcm_0_right
    1.22 +  lcm_0_left_nat ~> lcm_0_left
    1.23 +  lcm_0_left_int ~> lcm_0_left
    1.24 +  dvd_gcd_D1_nat ~> dvd_gcdD1
    1.25 +  dvd_gcd_D1_int ~> dvd_gcdD1
    1.26 +  dvd_gcd_D2_nat ~> dvd_gcdD2
    1.27 +  dvd_gcd_D2_int ~> dvd_gcdD2
    1.28 +  coprime_dvd_mult_iff_nat ~> coprime_dvd_mult_iff
    1.29 +  coprime_dvd_mult_iff_int ~> coprime_dvd_mult_iff
    1.30    realpow_minus_mult ~> power_minus_mult
    1.31    realpow_Suc_le_self ~> power_Suc_le_self
    1.32 +  dvd_Gcd, dvd_Gcd_nat, dvd_Gcd_int removed in favour of Gcd_greatest
    1.33  INCOMPATIBILITY.
    1.34  
    1.35  
     2.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
     2.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
     2.3 @@ -585,10 +585,6 @@
     2.4        (auto simp add: lcm_eq_0_iff)
     2.5  qed
     2.6  
     2.7 -lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
     2.8 -  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
     2.9 -  by (blast intro: Gcd_greatest)
    2.10 -
    2.11  lemma Gcd_set [code_unfold]:
    2.12    "Gcd (set as) = foldr gcd as 0"
    2.13    by (induct as) simp_all
    2.14 @@ -715,16 +711,16 @@
    2.15  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
    2.16    by (simp add: gcd_int_def)
    2.17  
    2.18 -lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    2.19 +lemma abs_gcd_int [simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    2.20  by(simp add: gcd_int_def)
    2.21  
    2.22  lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
    2.23  by (simp add: gcd_int_def)
    2.24  
    2.25 -lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    2.26 +lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    2.27  by (metis abs_idempotent gcd_abs_int)
    2.28  
    2.29 -lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    2.30 +lemma gcd_abs2_int [simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    2.31  by (metis abs_idempotent gcd_abs_int)
    2.32  
    2.33  lemma gcd_cases_int:
    2.34 @@ -751,10 +747,10 @@
    2.35  lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
    2.36    by (simp add:lcm_int_def)
    2.37  
    2.38 -lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    2.39 +lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    2.40    by (metis abs_idempotent lcm_int_def)
    2.41  
    2.42 -lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    2.43 +lemma lcm_abs2_int [simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    2.44    by (metis abs_idempotent lcm_int_def)
    2.45  
    2.46  lemma lcm_cases_int:
    2.47 @@ -1047,38 +1043,44 @@
    2.48  
    2.49  (* to do: add the three variations of these, and for ints? *)
    2.50  
    2.51 -lemma finite_divisors_nat[simp]:
    2.52 -  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
    2.53 +lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
    2.54 +  fixes m :: nat
    2.55 +  assumes "m > 0" 
    2.56 +  shows "finite {d. d dvd m}"
    2.57  proof-
    2.58 -  have "finite{d. d <= m}"
    2.59 -    by (blast intro: bounded_nat_set_is_finite)
    2.60 -  from finite_subset[OF _ this] show ?thesis using assms
    2.61 -    by (metis Collect_mono dvd_imp_le neq0_conv)
    2.62 +  from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
    2.63 +    by (auto dest: dvd_imp_le)
    2.64 +  then show ?thesis
    2.65 +    using finite_Collect_le_nat by (rule finite_subset)
    2.66  qed
    2.67  
    2.68 -lemma finite_divisors_int[simp]:
    2.69 -  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
    2.70 -proof-
    2.71 -  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
    2.72 -  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
    2.73 -  from finite_subset[OF _ this] show ?thesis using assms
    2.74 +lemma finite_divisors_int [simp]:
    2.75 +  fixes i :: int
    2.76 +  assumes "i \<noteq> 0"
    2.77 +  shows "finite {d. d dvd i}"
    2.78 +proof -
    2.79 +  have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
    2.80 +    by (auto simp: abs_if)
    2.81 +  then have "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}"
    2.82 +    by simp
    2.83 +  from finite_subset [OF _ this] show ?thesis using assms
    2.84      by (simp add: dvd_imp_le_int subset_iff)
    2.85  qed
    2.86  
    2.87 -lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    2.88 +lemma Max_divisors_self_nat [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    2.89  apply(rule antisym)
    2.90   apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
    2.91  apply simp
    2.92  done
    2.93  
    2.94 -lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
    2.95 +lemma Max_divisors_self_int [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
    2.96  apply(rule antisym)
    2.97   apply(rule Max_le_iff [THEN iffD2])
    2.98    apply (auto intro: abs_le_D1 dvd_imp_le_int)
    2.99  done
   2.100  
   2.101  lemma gcd_is_Max_divisors_nat:
   2.102 -  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   2.103 +  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd (m::nat) n = Max {d. d dvd m \<and> d dvd n}"
   2.104  apply(rule Max_eqI[THEN sym])
   2.105    apply (metis finite_Collect_conjI finite_divisors_nat)
   2.106   apply simp
   2.107 @@ -1438,35 +1440,33 @@
   2.108    ultimately show ?thesis by blast
   2.109  qed
   2.110  
   2.111 -lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   2.112 +lemma pow_divides_eq_nat [simp]:
   2.113 +  "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   2.114    by (auto intro: pow_divides_pow_nat dvd_power_same)
   2.115  
   2.116 -lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   2.117 +lemma pow_divides_eq_int [simp]:
   2.118 +  "n ~= 0 \<Longrightarrow> (a::int) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   2.119    by (auto intro: pow_divides_pow_int dvd_power_same)
   2.120  
   2.121 -lemma divides_mult_nat:
   2.122 -  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   2.123 -  shows "m * n dvd r"
   2.124 +context semiring_gcd
   2.125 +begin
   2.126 +
   2.127 +lemma divides_mult:
   2.128 +  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   2.129 +  shows "a * b dvd c"
   2.130  proof-
   2.131 -  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   2.132 -    unfolding dvd_def by blast
   2.133 -  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   2.134 -  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   2.135 -  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   2.136 -  from n' k show ?thesis unfolding dvd_def by auto
   2.137 +  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   2.138 +  with \<open>a dvd c\<close> have "a dvd b' * b"
   2.139 +    by (simp add: ac_simps)
   2.140 +  with \<open>coprime a b\<close> have "a dvd b'"
   2.141 +    by (simp add: coprime_dvd_mult_iff)
   2.142 +  then obtain a' where "b' = a * a'" ..
   2.143 +  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   2.144 +    by (simp add: ac_simps)
   2.145 +  then show ?thesis ..
   2.146  qed
   2.147  
   2.148 -lemma divides_mult_int:
   2.149 -  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   2.150 -  shows "m * n dvd r"
   2.151 -proof-
   2.152 -  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   2.153 -    unfolding dvd_def by blast
   2.154 -  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   2.155 -  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   2.156 -  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   2.157 -  from n' k show ?thesis unfolding dvd_def by auto
   2.158 -qed
   2.159 +end
   2.160  
   2.161  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   2.162    by (simp add: gcd.commute del: One_nat_def)
   2.163 @@ -1773,18 +1773,6 @@
   2.164    apply (simp, simp add: abs_mult)
   2.165  done
   2.166  
   2.167 -lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
   2.168 -  unfolding lcm_nat_def by simp
   2.169 -
   2.170 -lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
   2.171 -  unfolding lcm_int_def by simp
   2.172 -
   2.173 -lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
   2.174 -  unfolding lcm_nat_def by simp
   2.175 -
   2.176 -lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
   2.177 -  unfolding lcm_int_def by simp
   2.178 -
   2.179  lemma lcm_pos_nat:
   2.180    "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
   2.181  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
   2.182 @@ -1796,7 +1784,7 @@
   2.183    apply auto
   2.184    done
   2.185  
   2.186 -lemma dvd_pos_nat:
   2.187 +lemma dvd_pos_nat: -- \<open>FIXME move\<close>
   2.188    fixes n m :: nat
   2.189    assumes "n > 0" and "m dvd n"
   2.190    shows "m > 0"
   2.191 @@ -1828,16 +1816,16 @@
   2.192  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   2.193  by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
   2.194  
   2.195 -lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   2.196 +lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   2.197  by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
   2.198  
   2.199 -lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   2.200 +lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   2.201  by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
   2.202  
   2.203 -lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   2.204 +lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   2.205  by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
   2.206  
   2.207 -lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   2.208 +lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   2.209  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   2.210  
   2.211  lemma (in semiring_gcd) comp_fun_idem_gcd:
   2.212 @@ -1848,10 +1836,12 @@
   2.213    "comp_fun_idem lcm"
   2.214    by standard (simp_all add: fun_eq_iff ac_simps)
   2.215  
   2.216 -lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
   2.217 -  by (simp only: lcm_eq_1_iff) simp
   2.218 +lemma lcm_1_iff_nat [simp]:
   2.219 +  "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   2.220 +  using lcm_eq_1_iff [of m n] by simp
   2.221    
   2.222 -lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   2.223 +lemma lcm_1_iff_int [simp]:
   2.224 +  "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   2.225    by auto
   2.226  
   2.227  
   2.228 @@ -1897,14 +1887,15 @@
   2.229    fixes M :: "nat set"
   2.230    assumes "\<forall>m\<in>M. m dvd n"
   2.231    shows "Lcm M dvd n"
   2.232 -proof (cases "n = 0")
   2.233 -  case True then show ?thesis by simp
   2.234 +proof (cases "n > 0")
   2.235 +  case False then show ?thesis by simp
   2.236  next
   2.237 -  case False
   2.238 +  case True
   2.239    then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
   2.240    moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
   2.241    ultimately have "finite M" by (rule rev_finite_subset)
   2.242 -  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   2.243 +  then show ?thesis using assms
   2.244 +    by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   2.245  qed
   2.246  
   2.247  definition
   2.248 @@ -1933,17 +1924,25 @@
   2.249  
   2.250  text\<open>Alternative characterizations of Gcd:\<close>
   2.251  
   2.252 -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})"
   2.253 -apply(rule antisym)
   2.254 - apply(rule Max_ge)
   2.255 -  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   2.256 - apply (simp add: Gcd_dvd)
   2.257 -apply (rule Max_le_iff[THEN iffD2])
   2.258 -  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   2.259 - apply fastforce
   2.260 -apply clarsimp
   2.261 -apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
   2.262 -done
   2.263 +lemma Gcd_eq_Max:
   2.264 +  fixes M :: "nat set"
   2.265 +  assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
   2.266 +  shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
   2.267 +proof (rule antisym)
   2.268 +  from assms obtain m where "m \<in> M" and "m > 0"
   2.269 +    by auto
   2.270 +  from \<open>m > 0\<close> have "finite {d. d dvd m}"
   2.271 +    by (blast intro: finite_divisors_nat)
   2.272 +  with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
   2.273 +    by blast
   2.274 +  from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
   2.275 +    by (auto intro: Max_ge Gcd_dvd)
   2.276 +  from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
   2.277 +    apply (rule Max.boundedI)
   2.278 +    apply auto
   2.279 +    apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
   2.280 +    done
   2.281 +qed
   2.282  
   2.283  lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
   2.284  apply(induct pred:finite)
   2.285 @@ -2088,7 +2087,7 @@
   2.286  
   2.287  text \<open>Fact aliasses\<close>
   2.288  
   2.289 -lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
   2.290 +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   2.291    by (fact lcm_eq_0_iff)
   2.292  
   2.293  lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   2.294 @@ -2103,17 +2102,9 @@
   2.295  lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   2.296    by (fact dvd_lcmI1)
   2.297  
   2.298 -lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   2.299 +lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   2.300    by (fact dvd_lcmI2)
   2.301  
   2.302 -lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   2.303 -    (k dvd m * n) = (k dvd m)"
   2.304 -  by (fact coprime_dvd_mult_iff)
   2.305 -
   2.306 -lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   2.307 -    (k dvd m * n) = (k dvd m)"
   2.308 -  by (fact coprime_dvd_mult_iff)
   2.309 -
   2.310  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   2.311    by (fact coprime_exp2)
   2.312  
   2.313 @@ -2122,29 +2113,13 @@
   2.314  
   2.315  lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   2.316  lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   2.317 -lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   2.318 -lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   2.319 +lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
   2.320 +lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
   2.321  
   2.322  lemma dvd_Lcm_int [simp]:
   2.323    fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   2.324    using assms by (fact dvd_Lcm)
   2.325  
   2.326 -lemma Lcm_empty_nat:
   2.327 -  "Lcm {} = (1::nat)"
   2.328 -  by (fact Lcm_empty)
   2.329 -
   2.330 -lemma Lcm_empty_int:
   2.331 -  "Lcm {} = (1::int)"
   2.332 -  by (fact Lcm_empty)
   2.333 -
   2.334 -lemma Lcm_insert_nat:
   2.335 -  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   2.336 -  by (fact Lcm_insert)
   2.337 -
   2.338 -lemma Lcm_insert_int:
   2.339 -  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   2.340 -  by (fact Lcm_insert)
   2.341 -
   2.342  lemma gcd_neg_numeral_1_int [simp]:
   2.343    "gcd (- numeral n :: int) x = gcd (numeral n) x"
   2.344    by (fact gcd_neg1_int)
   2.345 @@ -2159,43 +2134,8 @@
   2.346  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   2.347    by (fact gcd_nat.absorb2)
   2.348  
   2.349 -lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.350 -  by (fact comp_fun_idem_gcd)
   2.351 -
   2.352 -lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   2.353 -  by (fact comp_fun_idem_gcd)
   2.354 -
   2.355 -lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   2.356 -  by (fact comp_fun_idem_lcm)
   2.357 -
   2.358 -lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   2.359 -  by (fact comp_fun_idem_lcm)
   2.360 -
   2.361 -lemma Lcm_eq_0 [simp]:
   2.362 -  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   2.363 -  by (rule Lcm_eq_0_I)
   2.364 -
   2.365 -lemma Lcm0_iff [simp]:
   2.366 -  fixes M :: "nat set"
   2.367 -  assumes "finite M" and "M \<noteq> {}"
   2.368 -  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   2.369 -  using assms by (simp add: Lcm_0_iff)
   2.370 -
   2.371 -lemma Lcm_dvd_int [simp]:
   2.372 -  fixes M :: "int set"
   2.373 -  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   2.374 -  using assms by (auto intro: Lcm_least)
   2.375 -
   2.376 -lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   2.377 -  by (fact dvd_gcdD1)
   2.378 -
   2.379 -lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   2.380 -  by (fact dvd_gcdD2)
   2.381 -
   2.382 -lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   2.383 -  by (fact dvd_gcdD1)
   2.384 -
   2.385 -lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   2.386 -  by (fact dvd_gcdD2)
   2.387 +lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
   2.388 +lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
   2.389 +lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
   2.390  
   2.391  end
     3.1 --- a/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:58 2016 +0100
     3.2 +++ b/src/HOL/Number_Theory/Cong.thy	Wed Feb 17 21:51:58 2016 +0100
     3.3 @@ -267,7 +267,7 @@
     3.4  
     3.5  lemma cong_mult_rcancel_int:
     3.6      "coprime k (m::int) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
     3.7 -  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff_int gcd.commute)
     3.8 +  by (metis cong_altdef_int left_diff_distrib coprime_dvd_mult_iff gcd.commute)
     3.9  
    3.10  lemma cong_mult_rcancel_nat:
    3.11      "coprime k (m::nat) \<Longrightarrow> [a * k = b * k] (mod m) = [a = b] (mod m)"
    3.12 @@ -285,7 +285,7 @@
    3.13  lemma coprime_cong_mult_int:
    3.14    "[(a::int) = b] (mod m) \<Longrightarrow> [a = b] (mod n) \<Longrightarrow> coprime m n
    3.15      \<Longrightarrow> [a = b] (mod m * n)"
    3.16 -by (metis divides_mult_int cong_altdef_int)
    3.17 +by (metis divides_mult cong_altdef_int)
    3.18  
    3.19  lemma coprime_cong_mult_nat:
    3.20    assumes "[(a::nat) = b] (mod m)" and "[a = b] (mod n)" and "coprime m n"
     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:58 2016 +0100
     4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Feb 17 21:51:58 2016 +0100
     4.3 @@ -1064,11 +1064,11 @@
     4.4    "Lcm {} = 1"
     4.5    by (simp add: Lcm_1_iff)
     4.6  
     4.7 -lemma Lcm_eq_0 [simp]:
     4.8 +lemma Lcm_eq_0_I [simp]:
     4.9    "0 \<in> A \<Longrightarrow> Lcm A = 0"
    4.10    by (drule dvd_Lcm) simp
    4.11  
    4.12 -lemma Lcm0_iff':
    4.13 +lemma Lcm_0_iff':
    4.14    "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
    4.15  proof
    4.16    assume "Lcm A = 0"
    4.17 @@ -1092,7 +1092,7 @@
    4.18    qed
    4.19  qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
    4.20  
    4.21 -lemma Lcm0_iff [simp]:
    4.22 +lemma Lcm_0_iff [simp]:
    4.23    "finite A \<Longrightarrow> Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
    4.24  proof -
    4.25    assume "finite A"
    4.26 @@ -1108,7 +1108,7 @@
    4.27        done
    4.28      moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
    4.29      ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
    4.30 -    with Lcm0_iff' have "Lcm A \<noteq> 0" by simp
    4.31 +    with Lcm_0_iff' have "Lcm A \<noteq> 0" by simp
    4.32    }
    4.33    ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
    4.34  qed
    4.35 @@ -1210,7 +1210,7 @@
    4.36  
    4.37  lemma Lcm_Gcd:
    4.38    "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
    4.39 -  by (rule LcmI[symmetric]) (auto intro: dvd_Gcd Gcd_greatest)
    4.40 +  by (rule LcmI[symmetric]) (auto intro: Gcd_greatest Gcd_greatest)
    4.41  
    4.42  lemma Gcd_1:
    4.43    "1 \<in> A \<Longrightarrow> Gcd A = 1"