src/HOL/GCD.thy
changeset 62353 7f927120b5a2
parent 62350 66a381d3f88f
child 62429 25271ff79171
     1.1 --- a/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
     1.2 +++ b/src/HOL/GCD.thy	Wed Feb 17 21:51:58 2016 +0100
     1.3 @@ -585,10 +585,6 @@
     1.4        (auto simp add: lcm_eq_0_iff)
     1.5  qed
     1.6  
     1.7 -lemma dvd_Gcd: \<comment> \<open>FIXME remove\<close>
     1.8 -  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
     1.9 -  by (blast intro: Gcd_greatest)
    1.10 -
    1.11  lemma Gcd_set [code_unfold]:
    1.12    "Gcd (set as) = foldr gcd as 0"
    1.13    by (induct as) simp_all
    1.14 @@ -715,16 +711,16 @@
    1.15  lemma gcd_neg2_int [simp]: "gcd (x::int) (-y) = gcd x y"
    1.16    by (simp add: gcd_int_def)
    1.17  
    1.18 -lemma abs_gcd_int[simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    1.19 +lemma abs_gcd_int [simp]: "\<bar>gcd (x::int) y\<bar> = gcd x y"
    1.20  by(simp add: gcd_int_def)
    1.21  
    1.22  lemma gcd_abs_int: "gcd (x::int) y = gcd \<bar>x\<bar> \<bar>y\<bar>"
    1.23  by (simp add: gcd_int_def)
    1.24  
    1.25 -lemma gcd_abs1_int[simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    1.26 +lemma gcd_abs1_int [simp]: "gcd \<bar>x\<bar> (y::int) = gcd x y"
    1.27  by (metis abs_idempotent gcd_abs_int)
    1.28  
    1.29 -lemma gcd_abs2_int[simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    1.30 +lemma gcd_abs2_int [simp]: "gcd x \<bar>y::int\<bar> = gcd x y"
    1.31  by (metis abs_idempotent gcd_abs_int)
    1.32  
    1.33  lemma gcd_cases_int:
    1.34 @@ -751,10 +747,10 @@
    1.35  lemma abs_lcm_int [simp]: "\<bar>lcm i j::int\<bar> = lcm i j"
    1.36    by (simp add:lcm_int_def)
    1.37  
    1.38 -lemma lcm_abs1_int[simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    1.39 +lemma lcm_abs1_int [simp]: "lcm \<bar>x\<bar> (y::int) = lcm x y"
    1.40    by (metis abs_idempotent lcm_int_def)
    1.41  
    1.42 -lemma lcm_abs2_int[simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    1.43 +lemma lcm_abs2_int [simp]: "lcm x \<bar>y::int\<bar> = lcm x y"
    1.44    by (metis abs_idempotent lcm_int_def)
    1.45  
    1.46  lemma lcm_cases_int:
    1.47 @@ -1047,38 +1043,44 @@
    1.48  
    1.49  (* to do: add the three variations of these, and for ints? *)
    1.50  
    1.51 -lemma finite_divisors_nat[simp]:
    1.52 -  assumes "(m::nat) ~= 0" shows "finite{d. d dvd m}"
    1.53 +lemma finite_divisors_nat [simp]: -- \<open>FIXME move\<close>
    1.54 +  fixes m :: nat
    1.55 +  assumes "m > 0" 
    1.56 +  shows "finite {d. d dvd m}"
    1.57  proof-
    1.58 -  have "finite{d. d <= m}"
    1.59 -    by (blast intro: bounded_nat_set_is_finite)
    1.60 -  from finite_subset[OF _ this] show ?thesis using assms
    1.61 -    by (metis Collect_mono dvd_imp_le neq0_conv)
    1.62 +  from assms have "{d. d dvd m} \<subseteq> {d. d \<le> m}"
    1.63 +    by (auto dest: dvd_imp_le)
    1.64 +  then show ?thesis
    1.65 +    using finite_Collect_le_nat by (rule finite_subset)
    1.66  qed
    1.67  
    1.68 -lemma finite_divisors_int[simp]:
    1.69 -  assumes "(i::int) ~= 0" shows "finite{d. d dvd i}"
    1.70 -proof-
    1.71 -  have "{d. \<bar>d\<bar> <= \<bar>i\<bar>} = {- \<bar>i\<bar> .. \<bar>i\<bar>}" by(auto simp:abs_if)
    1.72 -  hence "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}" by simp
    1.73 -  from finite_subset[OF _ this] show ?thesis using assms
    1.74 +lemma finite_divisors_int [simp]:
    1.75 +  fixes i :: int
    1.76 +  assumes "i \<noteq> 0"
    1.77 +  shows "finite {d. d dvd i}"
    1.78 +proof -
    1.79 +  have "{d. \<bar>d\<bar> \<le> \<bar>i\<bar>} = {- \<bar>i\<bar>..\<bar>i\<bar>}"
    1.80 +    by (auto simp: abs_if)
    1.81 +  then have "finite {d. \<bar>d\<bar> <= \<bar>i\<bar>}"
    1.82 +    by simp
    1.83 +  from finite_subset [OF _ this] show ?thesis using assms
    1.84      by (simp add: dvd_imp_le_int subset_iff)
    1.85  qed
    1.86  
    1.87 -lemma Max_divisors_self_nat[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    1.88 +lemma Max_divisors_self_nat [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::nat. d dvd n} = n"
    1.89  apply(rule antisym)
    1.90   apply (fastforce intro: Max_le_iff[THEN iffD2] simp: dvd_imp_le)
    1.91  apply simp
    1.92  done
    1.93  
    1.94 -lemma Max_divisors_self_int[simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
    1.95 +lemma Max_divisors_self_int [simp]: "n\<noteq>0 \<Longrightarrow> Max{d::int. d dvd n} = \<bar>n\<bar>"
    1.96  apply(rule antisym)
    1.97   apply(rule Max_le_iff [THEN iffD2])
    1.98    apply (auto intro: abs_le_D1 dvd_imp_le_int)
    1.99  done
   1.100  
   1.101  lemma gcd_is_Max_divisors_nat:
   1.102 -  "m ~= 0 \<Longrightarrow> n ~= 0 \<Longrightarrow> gcd (m::nat) n = (Max {d. d dvd m & d dvd n})"
   1.103 +  "m > 0 \<Longrightarrow> n > 0 \<Longrightarrow> gcd (m::nat) n = Max {d. d dvd m \<and> d dvd n}"
   1.104  apply(rule Max_eqI[THEN sym])
   1.105    apply (metis finite_Collect_conjI finite_divisors_nat)
   1.106   apply simp
   1.107 @@ -1438,35 +1440,33 @@
   1.108    ultimately show ?thesis by blast
   1.109  qed
   1.110  
   1.111 -lemma pow_divides_eq_nat [simp]: "n ~= 0 \<Longrightarrow> ((a::nat)^n dvd b^n) = (a dvd b)"
   1.112 +lemma pow_divides_eq_nat [simp]:
   1.113 +  "n > 0 \<Longrightarrow> (a::nat) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   1.114    by (auto intro: pow_divides_pow_nat dvd_power_same)
   1.115  
   1.116 -lemma pow_divides_eq_int [simp]: "n ~= 0 \<Longrightarrow> ((a::int)^n dvd b^n) = (a dvd b)"
   1.117 +lemma pow_divides_eq_int [simp]:
   1.118 +  "n ~= 0 \<Longrightarrow> (a::int) ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   1.119    by (auto intro: pow_divides_pow_int dvd_power_same)
   1.120  
   1.121 -lemma divides_mult_nat:
   1.122 -  assumes mr: "(m::nat) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   1.123 -  shows "m * n dvd r"
   1.124 +context semiring_gcd
   1.125 +begin
   1.126 +
   1.127 +lemma divides_mult:
   1.128 +  assumes "a dvd c" and nr: "b dvd c" and "coprime a b"
   1.129 +  shows "a * b dvd c"
   1.130  proof-
   1.131 -  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.132 -    unfolding dvd_def by blast
   1.133 -  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.134 -  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   1.135 -  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.136 -  from n' k show ?thesis unfolding dvd_def by auto
   1.137 +  from \<open>b dvd c\<close> obtain b' where"c = b * b'" ..
   1.138 +  with \<open>a dvd c\<close> have "a dvd b' * b"
   1.139 +    by (simp add: ac_simps)
   1.140 +  with \<open>coprime a b\<close> have "a dvd b'"
   1.141 +    by (simp add: coprime_dvd_mult_iff)
   1.142 +  then obtain a' where "b' = a * a'" ..
   1.143 +  with \<open>c = b * b'\<close> have "c = (a * b) * a'"
   1.144 +    by (simp add: ac_simps)
   1.145 +  then show ?thesis ..
   1.146  qed
   1.147  
   1.148 -lemma divides_mult_int:
   1.149 -  assumes mr: "(m::int) dvd r" and nr: "n dvd r" and mn:"coprime m n"
   1.150 -  shows "m * n dvd r"
   1.151 -proof-
   1.152 -  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
   1.153 -    unfolding dvd_def by blast
   1.154 -  from mr n' have "m dvd n'*n" by (simp add: mult.commute)
   1.155 -  hence "m dvd n'" using coprime_dvd_mult_iff [OF mn] by simp
   1.156 -  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
   1.157 -  from n' k show ?thesis unfolding dvd_def by auto
   1.158 -qed
   1.159 +end
   1.160  
   1.161  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
   1.162    by (simp add: gcd.commute del: One_nat_def)
   1.163 @@ -1773,18 +1773,6 @@
   1.164    apply (simp, simp add: abs_mult)
   1.165  done
   1.166  
   1.167 -lemma lcm_0_nat [simp]: "lcm (m::nat) 0 = 0"
   1.168 -  unfolding lcm_nat_def by simp
   1.169 -
   1.170 -lemma lcm_0_int [simp]: "lcm (m::int) 0 = 0"
   1.171 -  unfolding lcm_int_def by simp
   1.172 -
   1.173 -lemma lcm_0_left_nat [simp]: "lcm (0::nat) n = 0"
   1.174 -  unfolding lcm_nat_def by simp
   1.175 -
   1.176 -lemma lcm_0_left_int [simp]: "lcm (0::int) n = 0"
   1.177 -  unfolding lcm_int_def by simp
   1.178 -
   1.179  lemma lcm_pos_nat:
   1.180    "(m::nat) > 0 \<Longrightarrow> n>0 \<Longrightarrow> lcm m n > 0"
   1.181  by (metis gr0I mult_is_0 prod_gcd_lcm_nat)
   1.182 @@ -1796,7 +1784,7 @@
   1.183    apply auto
   1.184    done
   1.185  
   1.186 -lemma dvd_pos_nat:
   1.187 +lemma dvd_pos_nat: -- \<open>FIXME move\<close>
   1.188    fixes n m :: nat
   1.189    assumes "n > 0" and "m dvd n"
   1.190    shows "m > 0"
   1.191 @@ -1828,16 +1816,16 @@
   1.192  lemma lcm_proj1_if_dvd_int [simp]: "(x::int) dvd y \<Longrightarrow> lcm y x = \<bar>y\<bar>"
   1.193  by (subst lcm.commute, erule lcm_proj2_if_dvd_int)
   1.194  
   1.195 -lemma lcm_proj1_iff_nat[simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   1.196 +lemma lcm_proj1_iff_nat [simp]: "lcm m n = (m::nat) \<longleftrightarrow> n dvd m"
   1.197  by (metis lcm_proj1_if_dvd_nat lcm_unique_nat)
   1.198  
   1.199 -lemma lcm_proj2_iff_nat[simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   1.200 +lemma lcm_proj2_iff_nat [simp]: "lcm m n = (n::nat) \<longleftrightarrow> m dvd n"
   1.201  by (metis lcm_proj2_if_dvd_nat lcm_unique_nat)
   1.202  
   1.203 -lemma lcm_proj1_iff_int[simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   1.204 +lemma lcm_proj1_iff_int [simp]: "lcm m n = \<bar>m::int\<bar> \<longleftrightarrow> n dvd m"
   1.205  by (metis dvd_abs_iff lcm_proj1_if_dvd_int lcm_unique_int)
   1.206  
   1.207 -lemma lcm_proj2_iff_int[simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   1.208 +lemma lcm_proj2_iff_int [simp]: "lcm m n = \<bar>n::int\<bar> \<longleftrightarrow> m dvd n"
   1.209  by (metis dvd_abs_iff lcm_proj2_if_dvd_int lcm_unique_int)
   1.210  
   1.211  lemma (in semiring_gcd) comp_fun_idem_gcd:
   1.212 @@ -1848,10 +1836,12 @@
   1.213    "comp_fun_idem lcm"
   1.214    by standard (simp_all add: fun_eq_iff ac_simps)
   1.215  
   1.216 -lemma lcm_1_iff_nat [simp]: "lcm (m::nat) n = 1 \<longleftrightarrow> m=1 \<and> n=1"
   1.217 -  by (simp only: lcm_eq_1_iff) simp
   1.218 +lemma lcm_1_iff_nat [simp]:
   1.219 +  "lcm (m::nat) n = Suc 0 \<longleftrightarrow> m = Suc 0 \<and> n = Suc 0"
   1.220 +  using lcm_eq_1_iff [of m n] by simp
   1.221    
   1.222 -lemma lcm_1_iff_int [simp]: "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   1.223 +lemma lcm_1_iff_int [simp]:
   1.224 +  "lcm (m::int) n = 1 \<longleftrightarrow> (m=1 \<or> m = -1) \<and> (n=1 \<or> n = -1)"
   1.225    by auto
   1.226  
   1.227  
   1.228 @@ -1897,14 +1887,15 @@
   1.229    fixes M :: "nat set"
   1.230    assumes "\<forall>m\<in>M. m dvd n"
   1.231    shows "Lcm M dvd n"
   1.232 -proof (cases "n = 0")
   1.233 -  case True then show ?thesis by simp
   1.234 +proof (cases "n > 0")
   1.235 +  case False then show ?thesis by simp
   1.236  next
   1.237 -  case False
   1.238 +  case True
   1.239    then have "finite {d. d dvd n}" by (rule finite_divisors_nat)
   1.240    moreover have "M \<subseteq> {d. d dvd n}" using assms by fast
   1.241    ultimately have "finite M" by (rule rev_finite_subset)
   1.242 -  then show ?thesis using assms by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   1.243 +  then show ?thesis using assms
   1.244 +    by (induct M) (simp_all add: Lcm_nat_empty Lcm_nat_insert)
   1.245  qed
   1.246  
   1.247  definition
   1.248 @@ -1933,17 +1924,25 @@
   1.249  
   1.250  text\<open>Alternative characterizations of Gcd:\<close>
   1.251  
   1.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})"
   1.253 -apply(rule antisym)
   1.254 - apply(rule Max_ge)
   1.255 -  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   1.256 - apply (simp add: Gcd_dvd)
   1.257 -apply (rule Max_le_iff[THEN iffD2])
   1.258 -  apply (metis all_not_in_conv finite_divisors_nat finite_INT)
   1.259 - apply fastforce
   1.260 -apply clarsimp
   1.261 -apply (metis Gcd_dvd Max_in dvd_0_left dvd_Gcd dvd_imp_le linorder_antisym_conv3 not_less0)
   1.262 -done
   1.263 +lemma Gcd_eq_Max:
   1.264 +  fixes M :: "nat set"
   1.265 +  assumes "finite (M::nat set)" and "M \<noteq> {}" and "0 \<notin> M"
   1.266 +  shows "Gcd M = Max (\<Inter>m\<in>M. {d. d dvd m})"
   1.267 +proof (rule antisym)
   1.268 +  from assms obtain m where "m \<in> M" and "m > 0"
   1.269 +    by auto
   1.270 +  from \<open>m > 0\<close> have "finite {d. d dvd m}"
   1.271 +    by (blast intro: finite_divisors_nat)
   1.272 +  with \<open>m \<in> M\<close> have fin: "finite (\<Inter>m\<in>M. {d. d dvd m})"
   1.273 +    by blast
   1.274 +  from fin show "Gcd M \<le> Max (\<Inter>m\<in>M. {d. d dvd m})"
   1.275 +    by (auto intro: Max_ge Gcd_dvd)
   1.276 +  from fin show "Max (\<Inter>m\<in>M. {d. d dvd m}) \<le> Gcd M"
   1.277 +    apply (rule Max.boundedI)
   1.278 +    apply auto
   1.279 +    apply (meson Gcd_dvd Gcd_greatest \<open>0 < m\<close> \<open>m \<in> M\<close> dvd_imp_le dvd_pos_nat)
   1.280 +    done
   1.281 +qed
   1.282  
   1.283  lemma Gcd_remove0_nat: "finite M \<Longrightarrow> Gcd M = Gcd (M - {0::nat})"
   1.284  apply(induct pred:finite)
   1.285 @@ -2088,7 +2087,7 @@
   1.286  
   1.287  text \<open>Fact aliasses\<close>
   1.288  
   1.289 -lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n= 0"
   1.290 +lemma lcm_0_iff_nat [simp]: "lcm (m::nat) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   1.291    by (fact lcm_eq_0_iff)
   1.292  
   1.293  lemma lcm_0_iff_int [simp]: "lcm (m::int) n = 0 \<longleftrightarrow> m = 0 \<or> n = 0"
   1.294 @@ -2103,17 +2102,9 @@
   1.295  lemma dvd_lcm_I1_int [simp]: "(i::int) dvd m \<Longrightarrow> i dvd lcm m n"
   1.296    by (fact dvd_lcmI1)
   1.297  
   1.298 -lemma dvd_lcm_I2_int[simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   1.299 +lemma dvd_lcm_I2_int [simp]: "(i::int) dvd n \<Longrightarrow> i dvd lcm m n"
   1.300    by (fact dvd_lcmI2)
   1.301  
   1.302 -lemma coprime_dvd_mult_iff_nat: "coprime (k::nat) n \<Longrightarrow>
   1.303 -    (k dvd m * n) = (k dvd m)"
   1.304 -  by (fact coprime_dvd_mult_iff)
   1.305 -
   1.306 -lemma coprime_dvd_mult_iff_int: "coprime (k::int) n \<Longrightarrow>
   1.307 -    (k dvd m * n) = (k dvd m)"
   1.308 -  by (fact coprime_dvd_mult_iff)
   1.309 -
   1.310  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
   1.311    by (fact coprime_exp2)
   1.312  
   1.313 @@ -2122,29 +2113,13 @@
   1.314  
   1.315  lemmas Gcd_dvd_nat [simp] = Gcd_dvd [where ?'a = nat]
   1.316  lemmas Gcd_dvd_int [simp] = Gcd_dvd [where ?'a = int]
   1.317 -lemmas dvd_Gcd_nat [simp] = dvd_Gcd [where ?'a = nat]
   1.318 -lemmas dvd_Gcd_int [simp] = dvd_Gcd [where ?'a = int]
   1.319 +lemmas Gcd_greatest_nat [simp] = Gcd_greatest [where ?'a = nat]
   1.320 +lemmas Gcd_greatest_int [simp] = Gcd_greatest [where ?'a = int]
   1.321  
   1.322  lemma dvd_Lcm_int [simp]:
   1.323    fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
   1.324    using assms by (fact dvd_Lcm)
   1.325  
   1.326 -lemma Lcm_empty_nat:
   1.327 -  "Lcm {} = (1::nat)"
   1.328 -  by (fact Lcm_empty)
   1.329 -
   1.330 -lemma Lcm_empty_int:
   1.331 -  "Lcm {} = (1::int)"
   1.332 -  by (fact Lcm_empty)
   1.333 -
   1.334 -lemma Lcm_insert_nat:
   1.335 -  "Lcm (insert (n::nat) N) = lcm n (Lcm N)"
   1.336 -  by (fact Lcm_insert)
   1.337 -
   1.338 -lemma Lcm_insert_int:
   1.339 -  "Lcm (insert (n::int) N) = lcm n (Lcm N)"
   1.340 -  by (fact Lcm_insert)
   1.341 -
   1.342  lemma gcd_neg_numeral_1_int [simp]:
   1.343    "gcd (- numeral n :: int) x = gcd (numeral n) x"
   1.344    by (fact gcd_neg1_int)
   1.345 @@ -2159,43 +2134,8 @@
   1.346  lemma gcd_proj2_if_dvd_nat [simp]: "(y::nat) dvd x \<Longrightarrow> gcd x y = y"
   1.347    by (fact gcd_nat.absorb2)
   1.348  
   1.349 -lemma comp_fun_idem_gcd_nat: "comp_fun_idem (gcd :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.350 -  by (fact comp_fun_idem_gcd)
   1.351 -
   1.352 -lemma comp_fun_idem_gcd_int: "comp_fun_idem (gcd :: int\<Rightarrow>int\<Rightarrow>int)"
   1.353 -  by (fact comp_fun_idem_gcd)
   1.354 -
   1.355 -lemma comp_fun_idem_lcm_nat: "comp_fun_idem (lcm :: nat\<Rightarrow>nat\<Rightarrow>nat)"
   1.356 -  by (fact comp_fun_idem_lcm)
   1.357 -
   1.358 -lemma comp_fun_idem_lcm_int: "comp_fun_idem (lcm :: int\<Rightarrow>int\<Rightarrow>int)"
   1.359 -  by (fact comp_fun_idem_lcm)
   1.360 -
   1.361 -lemma Lcm_eq_0 [simp]:
   1.362 -  "finite (M::nat set) \<Longrightarrow> 0 \<in> M \<Longrightarrow> Lcm M = 0"
   1.363 -  by (rule Lcm_eq_0_I)
   1.364 -
   1.365 -lemma Lcm0_iff [simp]:
   1.366 -  fixes M :: "nat set"
   1.367 -  assumes "finite M" and "M \<noteq> {}"
   1.368 -  shows "Lcm M = 0 \<longleftrightarrow> 0 \<in> M"
   1.369 -  using assms by (simp add: Lcm_0_iff)
   1.370 -
   1.371 -lemma Lcm_dvd_int [simp]:
   1.372 -  fixes M :: "int set"
   1.373 -  assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
   1.374 -  using assms by (auto intro: Lcm_least)
   1.375 -
   1.376 -lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
   1.377 -  by (fact dvd_gcdD1)
   1.378 -
   1.379 -lemma dvd_gcd_D2_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd n"
   1.380 -  by (fact dvd_gcdD2)
   1.381 -
   1.382 -lemma dvd_gcd_D1_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd m"
   1.383 -  by (fact dvd_gcdD1)
   1.384 -
   1.385 -lemma dvd_gcd_D2_int: "i dvd gcd m n \<Longrightarrow> (i::int) dvd n"
   1.386 -  by (fact dvd_gcdD2)
   1.387 +lemmas Lcm_eq_0_I_nat [simp] = Lcm_eq_0_I [where ?'a = nat]
   1.388 +lemmas Lcm_0_iff_nat [simp] = Lcm_0_iff [where ?'a = nat]
   1.389 +lemmas Lcm_least_int [simp] = Lcm_least [where ?'a = int]
   1.390  
   1.391  end