author haftmann Wed Jul 08 14:01:39 2015 +0200 (2015-07-08) changeset 60686 ea5bc46c11e6 parent 60685 cb21b7022b00 child 60687 33dbbcb6a8a3
more algebraic properties for gcd/lcm
 src/HOL/GCD.thy file | annotate | diff | revisions src/HOL/Library/Polynomial.thy file | annotate | diff | revisions src/HOL/Number_Theory/Euclidean_Algorithm.thy file | annotate | diff | revisions
```     1.1 --- a/src/HOL/GCD.thy	Wed Jul 08 14:01:34 2015 +0200
1.2 +++ b/src/HOL/GCD.thy	Wed Jul 08 14:01:39 2015 +0200
1.3 @@ -31,6 +31,59 @@
1.4  imports Main
1.5  begin
1.6
1.7 +context semidom_divide
1.8 +begin
1.9 +
1.10 +lemma divide_1 [simp]:
1.11 +  "a div 1 = a"
1.12 +  using nonzero_mult_divide_cancel_left [of 1 a] by simp
1.13 +
1.14 +lemma dvd_mult_cancel_left [simp]:
1.15 +  assumes "a \<noteq> 0"
1.16 +  shows "a * b dvd a * c \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.17 +proof
1.18 +  assume ?P then obtain d where "a * c = a * b * d" ..
1.19 +  with assms have "c = b * d" by (simp add: ac_simps)
1.20 +  then show ?Q ..
1.21 +next
1.22 +  assume ?Q then obtain d where "c = b * d" ..
1.23 +  then have "a * c = a * b * d" by (simp add: ac_simps)
1.24 +  then show ?P ..
1.25 +qed
1.26 +
1.27 +lemma dvd_mult_cancel_right [simp]:
1.28 +  assumes "a \<noteq> 0"
1.29 +  shows "b * a dvd c * a \<longleftrightarrow> b dvd c" (is "?P \<longleftrightarrow> ?Q")
1.30 +using dvd_mult_cancel_left [of a b c] assms by (simp add: ac_simps)
1.31 +
1.32 +lemma div_dvd_iff_mult:
1.33 +  assumes "b \<noteq> 0" and "b dvd a"
1.34 +  shows "a div b dvd c \<longleftrightarrow> a dvd c * b"
1.35 +proof -
1.36 +  from \<open>b dvd a\<close> obtain d where "a = b * d" ..
1.37 +  with \<open>b \<noteq> 0\<close> show ?thesis by (simp add: ac_simps)
1.38 +qed
1.39 +
1.40 +lemma dvd_div_iff_mult:
1.41 +  assumes "c \<noteq> 0" and "c dvd b"
1.42 +  shows "a dvd b div c \<longleftrightarrow> a * c dvd b"
1.43 +proof -
1.44 +  from \<open>c dvd b\<close> obtain d where "b = c * d" ..
1.45 +  with \<open>c \<noteq> 0\<close> show ?thesis by (simp add: mult.commute [of a])
1.46 +qed
1.47 +
1.48 +end
1.49 +
1.50 +context algebraic_semidom
1.51 +begin
1.52 +
1.53 +lemma associated_1 [simp]:
1.54 +  "associated 1 a \<longleftrightarrow> is_unit a"
1.55 +  "associated a 1 \<longleftrightarrow> is_unit a"
1.56 +  by (auto simp add: associated_def)
1.57 +
1.58 +end
1.59 +
1.60  declare One_nat_def [simp del]
1.61
1.62  subsection {* GCD and LCM definitions *}
1.63 @@ -40,17 +93,527 @@
1.64      and lcm :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
1.65  begin
1.66
1.67 -abbreviation
1.68 -  coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.69 -where
1.70 -  "coprime x y == (gcd x y = 1)"
1.71 +abbreviation coprime :: "'a \<Rightarrow> 'a \<Rightarrow> bool"
1.72 +  where "coprime x y \<equiv> gcd x y = 1"
1.73
1.74  end
1.75
1.76 -class semiring_gcd = comm_semiring_1 + gcd +
1.77 +class Gcd = gcd +
1.78 +  fixes Gcd :: "'a set \<Rightarrow> 'a"
1.79 +    and Lcm :: "'a set \<Rightarrow> 'a"
1.80 +
1.81 +class semiring_gcd = normalization_semidom + gcd +
1.82    assumes gcd_dvd1 [iff]: "gcd a b dvd a"
1.83      and gcd_dvd2 [iff]: "gcd a b dvd b"
1.84      and gcd_greatest: "c dvd a \<Longrightarrow> c dvd b \<Longrightarrow> c dvd gcd a b"
1.85 +    and normalize_gcd [simp]: "normalize (gcd a b) = gcd a b"
1.86 +    and lcm_gcd: "lcm a b = normalize (a * b) div gcd a b"
1.87 +begin
1.88 +
1.89 +lemma gcd_greatest_iff [iff]:
1.90 +  "a dvd gcd b c \<longleftrightarrow> a dvd b \<and> a dvd c"
1.91 +  by (blast intro!: gcd_greatest intro: dvd_trans)
1.92 +
1.93 +lemma gcd_0_left [simp]:
1.94 +  "gcd 0 a = normalize a"
1.95 +proof (rule associated_eqI)
1.96 +  show "associated (gcd 0 a) (normalize a)"
1.97 +    by (auto intro!: associatedI gcd_greatest)
1.98 +  show "unit_factor (gcd 0 a) = 1" if "gcd 0 a \<noteq> 0"
1.99 +  proof -
1.100 +    from that have "unit_factor (normalize (gcd 0 a)) = 1"
1.101 +      by (rule unit_factor_normalize)
1.102 +    then show ?thesis by simp
1.103 +  qed
1.104 +qed simp
1.105 +
1.106 +lemma gcd_0_right [simp]:
1.107 +  "gcd a 0 = normalize a"
1.108 +proof (rule associated_eqI)
1.109 +  show "associated (gcd a 0) (normalize a)"
1.110 +    by (auto intro!: associatedI gcd_greatest)
1.111 +  show "unit_factor (gcd a 0) = 1" if "gcd a 0 \<noteq> 0"
1.112 +  proof -
1.113 +    from that have "unit_factor (normalize (gcd a 0)) = 1"
1.114 +      by (rule unit_factor_normalize)
1.115 +    then show ?thesis by simp
1.116 +  qed
1.117 +qed simp
1.118 +
1.119 +lemma gcd_eq_0_iff [simp]:
1.120 +  "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0" (is "?P \<longleftrightarrow> ?Q")
1.121 +proof
1.122 +  assume ?P then have "0 dvd gcd a b" by simp
1.123 +  then have "0 dvd a" and "0 dvd b" by (blast intro: dvd_trans)+
1.124 +  then show ?Q by simp
1.125 +next
1.126 +  assume ?Q then show ?P by simp
1.127 +qed
1.128 +
1.129 +lemma unit_factor_gcd:
1.130 +  "unit_factor (gcd a b) = (if a = 0 \<and> b = 0 then 0 else 1)"
1.131 +proof (cases "gcd a b = 0")
1.132 +  case True then show ?thesis by simp
1.133 +next
1.134 +  case False
1.135 +  have "unit_factor (gcd a b) * normalize (gcd a b) = gcd a b"
1.136 +    by (rule unit_factor_mult_normalize)
1.137 +  then have "unit_factor (gcd a b) * gcd a b = gcd a b"
1.138 +    by simp
1.139 +  then have "unit_factor (gcd a b) * gcd a b div gcd a b = gcd a b div gcd a b"
1.140 +    by simp
1.141 +  with False show ?thesis by simp
1.142 +qed
1.143 +
1.144 +sublocale gcd!: abel_semigroup gcd
1.145 +proof
1.146 +  fix a b c
1.147 +  show "gcd a b = gcd b a"
1.148 +    by (rule associated_eqI) (auto intro: associatedI gcd_greatest simp add: unit_factor_gcd)
1.149 +  from gcd_dvd1 have "gcd (gcd a b) c dvd a"
1.150 +    by (rule dvd_trans) simp
1.151 +  moreover from gcd_dvd1 have "gcd (gcd a b) c dvd b"
1.152 +    by (rule dvd_trans) simp
1.153 +  ultimately have P1: "gcd (gcd a b) c dvd gcd a (gcd b c)"
1.154 +    by (auto intro!: gcd_greatest)
1.155 +  from gcd_dvd2 have "gcd a (gcd b c) dvd b"
1.156 +    by (rule dvd_trans) simp
1.157 +  moreover from gcd_dvd2 have "gcd a (gcd b c) dvd c"
1.158 +    by (rule dvd_trans) simp
1.159 +  ultimately have P2: "gcd a (gcd b c) dvd gcd (gcd a b) c"
1.160 +    by (auto intro!: gcd_greatest)
1.161 +  from P1 P2 have "associated (gcd (gcd a b) c) (gcd a (gcd b c))"
1.162 +    by (rule associatedI)
1.163 +  then show "gcd (gcd a b) c = gcd a (gcd b c)"
1.164 +    by (rule associated_eqI) (simp_all add: unit_factor_gcd)
1.165 +qed
1.166 +
1.167 +lemma gcd_self [simp]:
1.168 +  "gcd a a = normalize a"
1.169 +proof -
1.170 +  have "a dvd gcd a a"
1.171 +    by (rule gcd_greatest) simp_all
1.172 +  then have "associated (gcd a a) (normalize a)"
1.173 +    by (auto intro: associatedI)
1.174 +  then show ?thesis
1.175 +    by (auto intro: associated_eqI simp add: unit_factor_gcd)
1.176 +qed
1.177 +
1.178 +lemma coprime_1_left [simp]:
1.179 +  "coprime 1 a"
1.180 +  by (rule associated_eqI) (simp_all add: unit_factor_gcd)
1.181 +
1.182 +lemma coprime_1_right [simp]:
1.183 +  "coprime a 1"
1.184 +  using coprime_1_left [of a] by (simp add: ac_simps)
1.185 +
1.186 +lemma gcd_mult_left:
1.187 +  "gcd (c * a) (c * b) = normalize c * gcd a b"
1.188 +proof (cases "c = 0")
1.189 +  case True then show ?thesis by simp
1.190 +next
1.191 +  case False
1.192 +  then have "c * gcd a b dvd gcd (c * a) (c * b)"
1.193 +    by (auto intro: gcd_greatest)
1.194 +  moreover from calculation False have "gcd (c * a) (c * b) dvd c * gcd a b"
1.195 +    by (metis div_dvd_iff_mult dvd_mult_left gcd_dvd1 gcd_dvd2 gcd_greatest mult_commute)
1.196 +  ultimately have "normalize (gcd (c * a) (c * b)) = normalize (c * gcd a b)"
1.197 +    by - (rule associated_eqI, auto intro: associated_eqI associatedI simp add: unit_factor_gcd)
1.198 +  then show ?thesis by (simp add: normalize_mult)
1.199 +qed
1.200 +
1.201 +lemma gcd_mult_right:
1.202 +  "gcd (a * c) (b * c) = gcd b a * normalize c"
1.203 +  using gcd_mult_left [of c a b] by (simp add: ac_simps)
1.204 +
1.205 +lemma mult_gcd_left:
1.206 +  "c * gcd a b = unit_factor c * gcd (c * a) (c * b)"
1.207 +  by (simp add: gcd_mult_left mult.assoc [symmetric])
1.208 +
1.209 +lemma mult_gcd_right:
1.210 +  "gcd a b * c = gcd (a * c) (b * c) * unit_factor c"
1.211 +  using mult_gcd_left [of c a b] by (simp add: ac_simps)
1.212 +
1.213 +lemma lcm_dvd1 [iff]:
1.214 +  "a dvd lcm a b"
1.215 +proof -
1.216 +  have "normalize (a * b) div gcd a b = normalize a * (normalize b div gcd a b)"
1.217 +    by (simp add: lcm_gcd normalize_mult div_mult_swap)
1.218 +  then show ?thesis
1.219 +    by (simp add: lcm_gcd)
1.220 +qed
1.221 +
1.222 +lemma lcm_dvd2 [iff]:
1.223 +  "b dvd lcm a b"
1.224 +proof -
1.225 +  have "normalize (a * b) div gcd a b = normalize b * (normalize a div gcd a b)"
1.226 +    by (simp add: lcm_gcd normalize_mult div_mult_swap ac_simps)
1.227 +  then show ?thesis
1.228 +    by (simp add: lcm_gcd)
1.229 +qed
1.230 +
1.231 +lemma lcm_least:
1.232 +  assumes "a dvd c" and "b dvd c"
1.233 +  shows "lcm a b dvd c"
1.234 +proof (cases "c = 0")
1.235 +  case True then show ?thesis by simp
1.236 +next
1.237 +  case False then have U: "is_unit (unit_factor c)" by simp
1.238 +  show ?thesis
1.239 +  proof (cases "gcd a b = 0")
1.240 +    case True with assms show ?thesis by simp
1.241 +  next
1.242 +    case False then have "a \<noteq> 0 \<or> b \<noteq> 0" by simp
1.243 +    with \<open>c \<noteq> 0\<close> assms have "a * b dvd a * c" "a * b dvd c * b"
1.244 +      by (simp_all add: mult_dvd_mono)
1.245 +    then have "normalize (a * b) dvd gcd (a * c) (b * c)"
1.246 +      by (auto intro: gcd_greatest simp add: ac_simps)
1.247 +    then have "normalize (a * b) dvd gcd (a * c) (b * c) * unit_factor c"
1.248 +      using U by (simp add: dvd_mult_unit_iff)
1.249 +    then have "normalize (a * b) dvd gcd a b * c"
1.250 +      by (simp add: mult_gcd_right [of a b c])
1.251 +    then have "normalize (a * b) div gcd a b dvd c"
1.252 +      using False by (simp add: div_dvd_iff_mult ac_simps)
1.253 +    then show ?thesis by (simp add: lcm_gcd)
1.254 +  qed
1.255 +qed
1.256 +
1.257 +lemma lcm_least_iff [iff]:
1.258 +  "lcm a b dvd c \<longleftrightarrow> a dvd c \<and> b dvd c"
1.259 +  by (blast intro!: lcm_least intro: dvd_trans)
1.260 +
1.261 +lemma normalize_lcm [simp]:
1.262 +  "normalize (lcm a b) = lcm a b"
1.263 +  by (simp add: lcm_gcd dvd_normalize_div)
1.264 +
1.265 +lemma lcm_0_left [simp]:
1.266 +  "lcm 0 a = 0"
1.267 +  by (simp add: lcm_gcd)
1.268 +
1.269 +lemma lcm_0_right [simp]:
1.270 +  "lcm a 0 = 0"
1.271 +  by (simp add: lcm_gcd)
1.272 +
1.273 +lemma lcm_eq_0_iff:
1.274 +  "lcm a b = 0 \<longleftrightarrow> a = 0 \<or> b = 0" (is "?P \<longleftrightarrow> ?Q")
1.275 +proof
1.276 +  assume ?P then have "0 dvd lcm a b" by simp
1.277 +  then have "0 dvd normalize (a * b) div gcd a b"
1.278 +    by (simp add: lcm_gcd)
1.279 +  then have "0 * gcd a b dvd normalize (a * b)"
1.280 +    using dvd_div_iff_mult [of "gcd a b" _ 0] by (cases "gcd a b = 0") simp_all
1.281 +  then have "normalize (a * b) = 0"
1.282 +    by simp
1.283 +  then show ?Q by simp
1.284 +next
1.285 +  assume ?Q then show ?P by auto
1.286 +qed
1.287 +
1.288 +lemma unit_factor_lcm :
1.289 +  "unit_factor (lcm a b) = (if a = 0 \<or> b = 0 then 0 else 1)"
1.290 +  by (simp add: unit_factor_gcd dvd_unit_factor_div lcm_gcd)
1.291 +
1.292 +sublocale lcm!: abel_semigroup lcm
1.293 +proof
1.294 +  fix a b c
1.295 +  show "lcm a b = lcm b a"
1.296 +    by (simp add: lcm_gcd ac_simps normalize_mult dvd_normalize_div)
1.297 +  have "associated (lcm (lcm a b) c) (lcm a (lcm b c))"
1.298 +    by (auto intro!: associatedI lcm_least
1.299 +      dvd_trans [of b "lcm b c" "lcm a (lcm b c)"]
1.300 +      dvd_trans [of c "lcm b c" "lcm a (lcm b c)"]
1.301 +      dvd_trans [of a "lcm a b" "lcm (lcm a b) c"]
1.302 +      dvd_trans [of b "lcm a b" "lcm (lcm a b) c"])
1.303 +  then show "lcm (lcm a b) c = lcm a (lcm b c)"
1.304 +    by (rule associated_eqI) (simp_all add: unit_factor_lcm lcm_eq_0_iff)
1.305 +qed
1.306 +
1.307 +lemma lcm_self [simp]:
1.308 +  "lcm a a = normalize a"
1.309 +proof -
1.310 +  have "lcm a a dvd a"
1.311 +    by (rule lcm_least) simp_all
1.312 +  then have "associated (lcm a a) (normalize a)"
1.313 +    by (auto intro: associatedI)
1.314 +  then show ?thesis
1.315 +    by (rule associated_eqI) (auto simp add: unit_factor_lcm)
1.316 +qed
1.317 +
1.318 +lemma gcd_mult_lcm [simp]:
1.319 +  "gcd a b * lcm a b = normalize a * normalize b"
1.320 +  by (simp add: lcm_gcd normalize_mult)
1.321 +
1.322 +lemma lcm_mult_gcd [simp]:
1.323 +  "lcm a b * gcd a b = normalize a * normalize b"
1.324 +  using gcd_mult_lcm [of a b] by (simp add: ac_simps)
1.325 +
1.326 +lemma gcd_lcm:
1.327 +  assumes "a \<noteq> 0" and "b \<noteq> 0"
1.328 +  shows "gcd a b = normalize (a * b) div lcm a b"
1.329 +proof -
1.330 +  from assms have "lcm a b \<noteq> 0"
1.331 +    by (simp add: lcm_eq_0_iff)
1.332 +  have "gcd a b * lcm a b = normalize a * normalize b" by simp
1.333 +  then have "gcd a b * lcm a b div lcm a b = normalize (a * b) div lcm a b"
1.334 +    by (simp_all add: normalize_mult)
1.335 +  with \<open>lcm a b \<noteq> 0\<close> show ?thesis
1.336 +    using nonzero_mult_divide_cancel_right [of "lcm a b" "gcd a b"] by simp
1.337 +qed
1.338 +
1.339 +lemma lcm_1_left [simp]:
1.340 +  "lcm 1 a = normalize a"
1.341 +  by (simp add: lcm_gcd)
1.342 +
1.343 +lemma lcm_1_right [simp]:
1.344 +  "lcm a 1 = normalize a"
1.345 +  by (simp add: lcm_gcd)
1.346 +
1.347 +lemma lcm_mult_left:
1.348 +  "lcm (c * a) (c * b) = normalize c * lcm a b"
1.349 +  by (cases "c = 0")
1.350 +    (simp_all add: gcd_mult_right lcm_gcd div_mult_swap normalize_mult ac_simps,
1.351 +      simp add: dvd_div_mult2_eq mult.left_commute [of "normalize c", symmetric])
1.352 +
1.353 +lemma lcm_mult_right:
1.354 +  "lcm (a * c) (b * c) = lcm b a * normalize c"
1.355 +  using lcm_mult_left [of c a b] by (simp add: ac_simps)
1.356 +
1.357 +lemma mult_lcm_left:
1.358 +  "c * lcm a b = unit_factor c * lcm (c * a) (c * b)"
1.359 +  by (simp add: lcm_mult_left mult.assoc [symmetric])
1.360 +
1.361 +lemma mult_lcm_right:
1.362 +  "lcm a b * c = lcm (a * c) (b * c) * unit_factor c"
1.363 +  using mult_lcm_left [of c a b] by (simp add: ac_simps)
1.364 +
1.365 +end
1.366 +
1.367 +class semiring_Gcd = semiring_gcd + Gcd +
1.368 +  assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1.369 +    and Gcd_greatest: "(\<And>b. b \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> a dvd Gcd A"
1.370 +    and normalize_Gcd [simp]: "normalize (Gcd A) = Gcd A"
1.371 +begin
1.372 +
1.373 +lemma Gcd_empty [simp]:
1.374 +  "Gcd {} = 0"
1.375 +  by (rule dvd_0_left, rule Gcd_greatest) simp
1.376 +
1.377 +lemma Gcd_0_iff [simp]:
1.378 +  "Gcd A = 0 \<longleftrightarrow> (\<forall>a\<in>A. a = 0)" (is "?P \<longleftrightarrow> ?Q")
1.379 +proof
1.380 +  assume ?P
1.381 +  show ?Q
1.382 +  proof
1.383 +    fix a
1.384 +    assume "a \<in> A"
1.385 +    then have "Gcd A dvd a" by (rule Gcd_dvd)
1.386 +    with \<open>?P\<close> show "a = 0" by simp
1.387 +  qed
1.388 +next
1.389 +  assume ?Q
1.390 +  have "0 dvd Gcd A"
1.391 +  proof (rule Gcd_greatest)
1.392 +    fix a
1.393 +    assume "a \<in> A"
1.394 +    with \<open>?Q\<close> have "a = 0" by simp
1.395 +    then show "0 dvd a" by simp
1.396 +  qed
1.397 +  then show ?P by simp
1.398 +qed
1.399 +
1.400 +lemma unit_factor_Gcd:
1.401 +  "unit_factor (Gcd A) = (if \<forall>a\<in>A. a = 0 then 0 else 1)"
1.402 +proof (cases "Gcd A = 0")
1.403 +  case True then show ?thesis by simp
1.404 +next
1.405 +  case False
1.406 +  from unit_factor_mult_normalize
1.407 +  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A" .
1.408 +  then have "unit_factor (Gcd A) * Gcd A = Gcd A" by simp
1.409 +  then have "unit_factor (Gcd A) * Gcd A div Gcd A = Gcd A div Gcd A" by simp
1.410 +  with False have "unit_factor (Gcd A) = 1" by simp
1.411 +  with False show ?thesis by simp
1.412 +qed
1.413 +
1.414 +lemma Gcd_UNIV [simp]:
1.415 +  "Gcd UNIV = 1"
1.416 +  by (rule associated_eqI) (auto intro: Gcd_dvd simp add: unit_factor_Gcd)
1.417 +
1.418 +lemma Gcd_eq_1_I:
1.419 +  assumes "is_unit a" and "a \<in> A"
1.420 +  shows "Gcd A = 1"
1.421 +proof -
1.422 +  from assms have "is_unit (Gcd A)"
1.423 +    by (blast intro: Gcd_dvd dvd_unit_imp_unit)
1.424 +  then have "normalize (Gcd A) = 1"
1.425 +    by (rule is_unit_normalize)
1.426 +  then show ?thesis
1.427 +    by simp
1.428 +qed
1.429 +
1.430 +lemma Gcd_insert [simp]:
1.431 +  "Gcd (insert a A) = gcd a (Gcd A)"
1.432 +proof -
1.433 +  have "Gcd (insert a A) dvd gcd a (Gcd A)"
1.434 +    by (auto intro: Gcd_dvd Gcd_greatest)
1.435 +  moreover have "gcd a (Gcd A) dvd Gcd (insert a A)"
1.436 +  proof (rule Gcd_greatest)
1.437 +    fix b
1.438 +    assume "b \<in> insert a A"
1.439 +    then show "gcd a (Gcd A) dvd b"
1.440 +    proof
1.441 +      assume "b = a" then show ?thesis by simp
1.442 +    next
1.443 +      assume "b \<in> A"
1.444 +      then have "Gcd A dvd b" by (rule Gcd_dvd)
1.445 +      moreover have "gcd a (Gcd A) dvd Gcd A" by simp
1.446 +      ultimately show ?thesis by (blast intro: dvd_trans)
1.447 +    qed
1.448 +  qed
1.449 +  ultimately have "associated (Gcd (insert a A)) (gcd a (Gcd A))"
1.450 +    by (rule associatedI)
1.451 +  then show ?thesis
1.452 +    by (rule associated_eqI) (simp_all add: unit_factor_gcd unit_factor_Gcd)
1.453 +qed
1.454 +
1.455 +lemma dvd_Gcd: -- \<open>FIXME remove\<close>
1.456 +  "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
1.457 +  by (blast intro: Gcd_greatest)
1.458 +
1.459 +lemma Gcd_set [code_unfold]:
1.460 +  "Gcd (set as) = foldr gcd as 0"
1.461 +  by (induct as) simp_all
1.462 +
1.463 +end
1.464 +
1.465 +class semiring_Lcm = semiring_Gcd +
1.466 +  assumes Lcm_Gcd: "Lcm A = Gcd {b. \<forall>a\<in>A. a dvd b}"
1.467 +begin
1.468 +
1.469 +lemma dvd_Lcm:
1.470 +  assumes "a \<in> A"
1.471 +  shows "a dvd Lcm A"
1.472 +  using assms by (auto intro: Gcd_greatest simp add: Lcm_Gcd)
1.473 +
1.474 +lemma Gcd_image_normalize [simp]:
1.475 +  "Gcd (normalize ` A) = Gcd A"
1.476 +proof -
1.477 +  have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
1.478 +  proof -
1.479 +    from that obtain B where "A = insert a B" by blast
1.480 +    moreover have " gcd (normalize a) (Gcd (normalize ` B)) dvd normalize a"
1.481 +      by (rule gcd_dvd1)
1.482 +    ultimately show "Gcd (normalize ` A) dvd a"
1.483 +      by simp
1.484 +  qed
1.485 +  then have "associated (Gcd (normalize ` A)) (Gcd A)"
1.486 +    by (auto intro!: associatedI Gcd_greatest intro: Gcd_dvd)
1.487 +  then show ?thesis
1.488 +    by (rule associated_eqI) (simp_all add: unit_factor_Gcd)
1.489 +qed
1.490 +
1.491 +lemma Lcm_least:
1.492 +  assumes "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
1.493 +  shows "Lcm A dvd a"
1.494 +  using assms by (auto intro: Gcd_dvd simp add: Lcm_Gcd)
1.495 +
1.496 +lemma normalize_Lcm [simp]:
1.497 +  "normalize (Lcm A) = Lcm A"
1.498 +  by (simp add: Lcm_Gcd)
1.499 +
1.500 +lemma unit_factor_Lcm:
1.501 +  "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
1.502 +proof (cases "Lcm A = 0")
1.503 +  case True then show ?thesis by simp
1.504 +next
1.505 +  case False
1.506 +  with unit_factor_normalize have "unit_factor (normalize (Lcm A)) = 1"
1.507 +    by blast
1.508 +  with False show ?thesis
1.509 +    by simp
1.510 +qed
1.511 +
1.512 +lemma Lcm_empty [simp]:
1.513 +  "Lcm {} = 1"
1.514 +  by (simp add: Lcm_Gcd)
1.515 +
1.516 +lemma Lcm_1_iff [simp]:
1.517 +  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)" (is "?P \<longleftrightarrow> ?Q")
1.518 +proof
1.519 +  assume ?P
1.520 +  show ?Q
1.521 +  proof
1.522 +    fix a
1.523 +    assume "a \<in> A"
1.524 +    then have "a dvd Lcm A"
1.525 +      by (rule dvd_Lcm)
1.526 +    with \<open>?P\<close> show "is_unit a"
1.527 +      by simp
1.528 +  qed
1.529 +next
1.530 +  assume ?Q
1.531 +  then have "is_unit (Lcm A)"
1.532 +    by (blast intro: Lcm_least)
1.533 +  then have "normalize (Lcm A) = 1"
1.534 +    by (rule is_unit_normalize)
1.535 +  then show ?P
1.536 +    by simp
1.537 +qed
1.538 +
1.539 +lemma Lcm_UNIV [simp]:
1.540 +  "Lcm UNIV = 0"
1.541 +proof -
1.542 +  have "0 dvd Lcm UNIV"
1.543 +    by (rule dvd_Lcm) simp
1.544 +  then show ?thesis
1.545 +    by simp
1.546 +qed
1.547 +
1.548 +lemma Lcm_eq_0_I:
1.549 +  assumes "0 \<in> A"
1.550 +  shows "Lcm A = 0"
1.551 +proof -
1.552 +  from assms have "0 dvd Lcm A"
1.553 +    by (rule dvd_Lcm)
1.554 +  then show ?thesis
1.555 +    by simp
1.556 +qed
1.557 +
1.558 +lemma Gcd_Lcm:
1.559 +  "Gcd A = Lcm {b. \<forall>a\<in>A. b dvd a}"
1.560 +  by (rule associated_eqI) (auto intro: associatedI Gcd_dvd dvd_Lcm Gcd_greatest Lcm_least
1.561 +    simp add: unit_factor_Gcd unit_factor_Lcm)
1.562 +
1.563 +lemma Lcm_insert [simp]:
1.564 +  "Lcm (insert a A) = lcm a (Lcm A)"
1.565 +proof (rule sym)
1.566 +  have "lcm a (Lcm A) dvd Lcm (insert a A)"
1.567 +    by (auto intro: dvd_Lcm Lcm_least)
1.568 +  moreover have "Lcm (insert a A) dvd lcm a (Lcm A)"
1.569 +  proof (rule Lcm_least)
1.570 +    fix b
1.571 +    assume "b \<in> insert a A"
1.572 +    then show "b dvd lcm a (Lcm A)"
1.573 +    proof
1.574 +      assume "b = a" then show ?thesis by simp
1.575 +    next
1.576 +      assume "b \<in> A"
1.577 +      then have "b dvd Lcm A" by (rule dvd_Lcm)
1.578 +      moreover have "Lcm A dvd lcm a (Lcm A)" by simp
1.579 +      ultimately show ?thesis by (blast intro: dvd_trans)
1.580 +    qed
1.581 +  qed
1.582 +  ultimately have "associated (lcm a (Lcm A)) (Lcm (insert a A))"
1.583 +    by (rule associatedI)
1.584 +  then show "lcm a (Lcm A) = Lcm (insert a A)"
1.585 +    by (rule associated_eqI) (simp_all add: unit_factor_lcm unit_factor_Lcm lcm_eq_0_iff)
1.586 +qed
1.587 +
1.588 +lemma Lcm_set [code_unfold]:
1.589 +  "Lcm (set as) = foldr lcm as 1"
1.590 +  by (induct as) simp_all
1.591 +
1.592 +end
1.593
1.594  class ring_gcd = comm_ring_1 + semiring_gcd
1.595
1.596 @@ -265,10 +828,11 @@
1.597    assume "k dvd m" and "k dvd n"
1.598    then show "k dvd gcd m n"
1.599      by (induct m n rule: gcd_nat_induct) (simp_all add: gcd_non_0_nat dvd_mod gcd_0_nat)
1.600 -qed
1.602
1.603  instance int :: ring_gcd
1.604 -  by intro_classes (simp_all add: dvd_int_unfold_dvd_nat gcd_int_def gcd_greatest)
1.605 +  by standard
1.606 +    (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)
1.607
1.608  lemma dvd_gcd_D1_nat: "k dvd gcd m n \<Longrightarrow> (k::nat) dvd m"
1.609    by (metis gcd_dvd1 dvd_trans)
1.610 @@ -332,21 +896,19 @@
1.611
1.612  interpretation gcd_nat: abel_semigroup "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.613    + gcd_nat: semilattice_neutr_order "gcd :: nat \<Rightarrow> nat \<Rightarrow> nat" 0 "op dvd" "(\<lambda>m n. m dvd n \<and> \<not> n dvd m)"
1.614 -apply default
1.615 -apply (auto intro: dvd_antisym dvd_trans)
1.616 +apply standard
1.617 +apply (auto intro: dvd_antisym dvd_trans)
1.618  apply (metis dvd.dual_order.refl gcd_unique_nat)+
1.619  done
1.620
1.621 -interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int"
1.622 -proof
1.623 -qed (simp_all add: gcd_int_def gcd_nat.assoc gcd_nat.commute gcd_nat.left_commute)
1.624 +interpretation gcd_int: abel_semigroup "gcd :: int \<Rightarrow> int \<Rightarrow> int" ..
1.625
1.626 -lemmas gcd_assoc_nat = gcd_nat.assoc
1.627 -lemmas gcd_commute_nat = gcd_nat.commute
1.628 -lemmas gcd_left_commute_nat = gcd_nat.left_commute
1.629 -lemmas gcd_assoc_int = gcd_int.assoc
1.630 -lemmas gcd_commute_int = gcd_int.commute
1.631 -lemmas gcd_left_commute_int = gcd_int.left_commute
1.632 +lemmas gcd_assoc_nat = gcd.assoc [where ?'a = nat]
1.633 +lemmas gcd_commute_nat = gcd.commute [where ?'a = nat]
1.634 +lemmas gcd_left_commute_nat = gcd.left_commute [where ?'a = nat]
1.635 +lemmas gcd_assoc_int = gcd.assoc [where ?'a = int]
1.636 +lemmas gcd_commute_int = gcd.commute [where ?'a = int]
1.637 +lemmas gcd_left_commute_int = gcd.left_commute [where ?'a = int]
1.638
1.639  lemmas gcd_ac_nat = gcd_assoc_nat gcd_commute_nat gcd_left_commute_nat
1.640
1.641 @@ -762,10 +1324,10 @@
1.642    by (induct n) (simp_all add: coprime_mult_int)
1.643
1.644  lemma coprime_exp2_nat [intro]: "coprime (a::nat) b \<Longrightarrow> coprime (a^n) (b^m)"
1.645 -  by (simp add: coprime_exp_nat gcd_nat.commute)
1.646 +  by (simp add: coprime_exp_nat ac_simps)
1.647
1.648  lemma coprime_exp2_int [intro]: "coprime (a::int) b \<Longrightarrow> coprime (a^n) (b^m)"
1.649 -  by (simp add: coprime_exp_int gcd_int.commute)
1.650 +  by (simp add: coprime_exp_int ac_simps)
1.651
1.652  lemma gcd_exp_nat: "gcd ((a::nat)^n) (b^n) = (gcd a b)^n"
1.653  proof (cases)
1.654 @@ -927,13 +1489,13 @@
1.655  qed
1.656
1.657  lemma coprime_plus_one_nat [simp]: "coprime ((n::nat) + 1) n"
1.658 -  by (simp add: gcd_nat.commute)
1.659 +  by (simp add: gcd.commute)
1.660
1.661  lemma coprime_Suc_nat [simp]: "coprime (Suc n) n"
1.662    using coprime_plus_one_nat by (simp add: One_nat_def)
1.663
1.664  lemma coprime_plus_one_int [simp]: "coprime ((n::int) + 1) n"
1.665 -  by (simp add: gcd_int.commute)
1.666 +  by (simp add: gcd.commute)
1.667
1.668  lemma coprime_minus_one_nat: "(n::nat) \<noteq> 0 \<Longrightarrow> coprime (n - 1) n"
1.669    using coprime_plus_one_nat [of "n - 1"]
1.670 @@ -958,12 +1520,12 @@
1.671  done
1.672
1.673  lemma coprime_common_divisor_nat:
1.674 -    "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
1.675 +  "coprime (a::nat) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> x = 1"
1.676    by (metis gcd_greatest_iff_nat nat_dvd_1_iff_1)
1.677
1.678  lemma coprime_common_divisor_int:
1.679 -    "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
1.680 -  using gcd_greatest by fastforce
1.681 +  "coprime (a::int) b \<Longrightarrow> x dvd a \<Longrightarrow> x dvd b \<Longrightarrow> abs x = 1"
1.682 +  using gcd_greatest_iff [of x a b] by auto
1.683
1.684  lemma coprime_divisors_nat:
1.685      "(d::int) dvd a \<Longrightarrow> e dvd b \<Longrightarrow> coprime a b \<Longrightarrow> coprime d e"
1.686 @@ -1266,42 +1828,11 @@
1.687  lemma lcm_least_nat:
1.688    assumes "(m::nat) dvd k" and "n dvd k"
1.689    shows "lcm m n dvd k"
1.690 -proof (cases k)
1.691 -  case 0 then show ?thesis by auto
1.692 -next
1.693 -  case (Suc _) then have pos_k: "k > 0" by auto
1.694 -  from assms dvd_pos_nat [OF this] have pos_mn: "m > 0" "n > 0" by auto
1.695 -  with gcd_zero_nat [of m n] have pos_gcd: "gcd m n > 0" by simp
1.696 -  from assms obtain p where k_m: "k = m * p" using dvd_def by blast
1.697 -  from assms obtain q where k_n: "k = n * q" using dvd_def by blast
1.698 -  from pos_k k_m have pos_p: "p > 0" by auto
1.699 -  from pos_k k_n have pos_q: "q > 0" by auto
1.700 -  have "k * k * gcd q p = k * gcd (k * q) (k * p)"
1.701 -    by (simp add: ac_simps gcd_mult_distrib_nat)
1.702 -  also have "\<dots> = k * gcd (m * p * q) (n * q * p)"
1.703 -    by (simp add: k_m [symmetric] k_n [symmetric])
1.704 -  also have "\<dots> = k * p * q * gcd m n"
1.705 -    by (simp add: ac_simps gcd_mult_distrib_nat)
1.706 -  finally have "(m * p) * (n * q) * gcd q p = k * p * q * gcd m n"
1.707 -    by (simp only: k_m [symmetric] k_n [symmetric])
1.708 -  then have "p * q * m * n * gcd q p = p * q * k * gcd m n"
1.709 -    by (simp add: ac_simps)
1.710 -  with pos_p pos_q have "m * n * gcd q p = k * gcd m n"
1.711 -    by simp
1.712 -  with prod_gcd_lcm_nat [of m n]
1.713 -  have "lcm m n * gcd q p * gcd m n = k * gcd m n"
1.714 -    by (simp add: ac_simps)
1.715 -  with pos_gcd have "lcm m n * gcd q p = k" by auto
1.716 -  then show ?thesis using dvd_def by auto
1.717 -qed
1.718 +  using assms by (rule lcm_least)
1.719
1.720  lemma lcm_least_int:
1.721    "(m::int) dvd k \<Longrightarrow> n dvd k \<Longrightarrow> lcm m n dvd k"
1.722 -apply (subst lcm_abs_int)
1.723 -apply (rule dvd_trans)
1.724 -apply (rule lcm_least_nat [transferred, of _ "abs k" _])
1.725 -apply auto
1.726 -done
1.727 +  by (rule lcm_least)
1.728
1.729  lemma lcm_dvd1_nat: "(m::nat) dvd lcm m n"
1.730  proof (cases m)
1.731 @@ -1333,10 +1864,10 @@
1.732  done
1.733
1.734  lemma lcm_dvd2_nat: "(n::nat) dvd lcm m n"
1.735 -  using lcm_dvd1_nat [of n m] by (simp only: lcm_nat_def mult.commute gcd_nat.commute)
1.736 +  by (rule lcm_dvd2)
1.737
1.738  lemma lcm_dvd2_int: "(n::int) dvd lcm m n"
1.739 -  using lcm_dvd1_int [of n m] by (simp only: lcm_int_def lcm_nat_def mult.commute gcd_nat.commute)
1.740 +  by (rule lcm_dvd2)
1.741
1.742  lemma dvd_lcm_I1_nat[simp]: "(k::nat) dvd m \<Longrightarrow> k dvd lcm m n"
1.743  by(metis lcm_dvd1_nat dvd_trans)
1.744 @@ -1360,33 +1891,16 @@
1.745
1.746  interpretation lcm_nat: abel_semigroup "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat"
1.747    + lcm_nat: semilattice_neutr "lcm :: nat \<Rightarrow> nat \<Rightarrow> nat" 1
1.748 -proof
1.749 -  fix n m p :: nat
1.750 -  show "lcm (lcm n m) p = lcm n (lcm m p)"
1.751 -    by (rule lcm_unique_nat [THEN iffD1]) (metis dvd.order_trans lcm_unique_nat)
1.752 -  show "lcm m n = lcm n m"
1.753 -    by (simp add: lcm_nat_def gcd_commute_nat field_simps)
1.754 -  show "lcm m m = m"
1.755 -    by (metis dvd.order_refl lcm_unique_nat)
1.756 -  show "lcm m 1 = m"
1.757 -    by (metis dvd.dual_order.refl lcm_unique_nat one_dvd)
1.758 -qed
1.759 +  by standard simp_all
1.760 +
1.761 +interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int" ..
1.762
1.763 -interpretation lcm_int: abel_semigroup "lcm :: int \<Rightarrow> int \<Rightarrow> int"
1.764 -proof
1.765 -  fix n m p :: int
1.766 -  show "lcm (lcm n m) p = lcm n (lcm m p)"
1.767 -    by (rule lcm_unique_int [THEN iffD1]) (metis dvd_trans lcm_unique_int)
1.768 -  show "lcm m n = lcm n m"
1.769 -    by (simp add: lcm_int_def lcm_nat.commute)
1.770 -qed
1.771 -
1.772 -lemmas lcm_assoc_nat = lcm_nat.assoc
1.773 -lemmas lcm_commute_nat = lcm_nat.commute
1.774 -lemmas lcm_left_commute_nat = lcm_nat.left_commute
1.775 -lemmas lcm_assoc_int = lcm_int.assoc
1.776 -lemmas lcm_commute_int = lcm_int.commute
1.777 -lemmas lcm_left_commute_int = lcm_int.left_commute
1.778 +lemmas lcm_assoc_nat = lcm.assoc [where ?'a = nat]
1.779 +lemmas lcm_commute_nat = lcm.commute [where ?'a = nat]
1.780 +lemmas lcm_left_commute_nat = lcm.left_commute [where ?'a = nat]
1.781 +lemmas lcm_assoc_int = lcm.assoc [where ?'a = int]
1.782 +lemmas lcm_commute_int = lcm.commute [where ?'a = int]
1.783 +lemmas lcm_left_commute_int = lcm.left_commute [where ?'a = int]
1.784
1.785  lemmas lcm_ac_nat = lcm_assoc_nat lcm_commute_nat lcm_left_commute_nat
1.786  lemmas lcm_ac_int = lcm_assoc_int lcm_commute_int lcm_left_commute_int
1.787 @@ -1452,16 +1966,10 @@
1.788  subsection {* The complete divisibility lattice *}
1.789
1.790  interpretation gcd_semilattice_nat: semilattice_inf gcd "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.791 -proof (default, goals)
1.792 -  case 3
1.793 -  thus ?case by(metis gcd_unique_nat)
1.794 -qed auto
1.795 +  by standard simp_all
1.796
1.797  interpretation lcm_semilattice_nat: semilattice_sup lcm "op dvd" "(\<lambda>m n::nat. m dvd n \<and> \<not> n dvd m)"
1.798 -proof (default, goals)
1.799 -  case 3
1.800 -  thus ?case by(metis lcm_unique_nat)
1.801 -qed auto
1.802 +  by standard simp_all
1.803
1.804  interpretation gcd_lcm_lattice_nat: lattice gcd "op dvd" "(\<lambda>m n::nat. m dvd n & ~ n dvd m)" lcm ..
1.805
1.806 @@ -1469,10 +1977,6 @@
1.807  Gcd is defined via Lcm to facilitate the proof that we have a complete lattice.
1.808  *}
1.809
1.810 -class Gcd = gcd +
1.811 -  fixes Gcd :: "'a set \<Rightarrow> 'a"
1.812 -  fixes Lcm :: "'a set \<Rightarrow> 'a"
1.813 -
1.814  instantiation nat :: Gcd
1.815  begin
1.816
1.817 @@ -1500,22 +2004,6 @@
1.818
1.819  end
1.820
1.821 -class semiring_Gcd = semiring_gcd + Gcd +
1.822 -  assumes Gcd_dvd: "a \<in> A \<Longrightarrow> Gcd A dvd a"
1.823 -    and dvd_Gcd: "\<forall>b\<in>A. a dvd b \<Longrightarrow> a dvd Gcd A"
1.824 -    and Gcd_insert [simp]: "Gcd (insert a A) = gcd a (Gcd A)"
1.825 -begin
1.826 -
1.827 -lemma Gcd_empty [simp]:
1.828 -  "Gcd {} = 0"
1.829 -  by (rule dvd_0_left, rule dvd_Gcd) simp
1.830 -
1.831 -lemma Gcd_set [code_unfold]:
1.832 -  "Gcd (set as) = foldr gcd as 0"
1.833 -  by (induct as) simp_all
1.834 -
1.835 -end
1.836 -
1.837  lemma dvd_Lcm_nat [simp]:
1.838    fixes M :: "nat set"
1.839    assumes "m \<in> M"
1.840 @@ -1544,25 +2032,7 @@
1.841    and "Sup.SUPREMUM Lcm A f = Lcm (f ` A)"
1.842  proof -
1.843    show "class.complete_lattice Gcd Lcm gcd Rings.dvd (\<lambda>m n. m dvd n \<and> \<not> n dvd m) lcm 1 (0::nat)"
1.844 -  proof (default, goals)
1.845 -    case 1
1.846 -    thus ?case by (simp add: Gcd_nat_def)
1.847 -  next
1.848 -    case 2
1.849 -    thus ?case by (simp add: Gcd_nat_def)
1.850 -  next
1.851 -    case 5
1.852 -    show ?case by (simp add: Gcd_nat_def Lcm_nat_infinite)
1.853 -  next
1.854 -    case 6
1.855 -    show ?case by (simp add: Lcm_nat_empty)
1.856 -  next
1.857 -    case 3
1.858 -    thus ?case by simp
1.859 -  next
1.860 -    case 4
1.861 -    thus ?case by simp
1.862 -  qed
1.863 +    by default (auto simp add: Gcd_nat_def Lcm_nat_empty Lcm_nat_infinite)
1.864    then interpret gcd_lcm_complete_lattice_nat:
1.865      complete_lattice Gcd Lcm gcd Rings.dvd "\<lambda>m n. m dvd n \<and> \<not> n dvd m" lcm 1 "0::nat" .
1.866    from gcd_lcm_complete_lattice_nat.INF_def show "Inf.INFIMUM Gcd A f = Gcd (f ` A)" .
1.867 @@ -1590,13 +2060,37 @@
1.868    show "Gcd N dvd n" if "n \<in> N" for N and n :: nat
1.869      using that by (fact gcd_lcm_complete_lattice_nat.Inf_lower)
1.870  next
1.871 -  show "n dvd Gcd N" if "\<forall>m\<in>N. n dvd m" for N and n :: nat
1.872 +  show "n dvd Gcd N" if "\<And>m. m \<in> N \<Longrightarrow> n dvd m" for N and n :: nat
1.873      using that by (simp only: gcd_lcm_complete_lattice_nat.Inf_greatest)
1.874  next
1.875 -  show "Gcd (insert n N) = gcd n (Gcd N)" for N and n :: nat
1.876 +  show "normalize (Gcd N) = Gcd N" for N :: "nat set"
1.877      by simp
1.878  qed
1.879
1.880 +instance nat :: semiring_Lcm
1.881 +proof
1.882 +  have uf: "unit_factor (Lcm N) = 1" if "0 < Lcm N" for N :: "nat set"
1.883 +  proof (cases "finite N")
1.884 +    case False with that show ?thesis by (simp add: Lcm_nat_infinite)
1.885 +  next
1.886 +    case True then show ?thesis
1.887 +    using that proof (induct N)
1.888 +      case empty then show ?case by simp
1.889 +    next
1.890 +      case (insert n N)
1.891 +      have "lcm n (Lcm N) \<noteq> 0 \<longleftrightarrow> n \<noteq> 0 \<and> Lcm N \<noteq> 0"
1.892 +        using lcm_eq_0_iff [of n "Lcm N"] by simp
1.893 +      then have "lcm n (Lcm N) > 0 \<longleftrightarrow> n > 0 \<and> Lcm N > 0"
1.894 +        unfolding neq0_conv .
1.895 +      with insert show ?case
1.896 +        by (simp add: Lcm_nat_insert unit_factor_lcm)
1.897 +    qed
1.898 +  qed
1.899 +  show "Lcm N = Gcd {m. \<forall>n\<in>N. n dvd m}" for N :: "nat set"
1.900 +    by (rule associated_eqI) (auto intro!: associatedI Gcd_dvd Gcd_greatest
1.901 +      simp add: unit_factor_Gcd uf)
1.902 +qed
1.903 +
1.904  text{* Alternative characterizations of Gcd: *}
1.905
1.906  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.907 @@ -1682,8 +2176,36 @@
1.908    "Gcd M = int (Gcd (nat ` abs ` M))"
1.909
1.910  instance ..
1.911 +
1.912  end
1.913
1.914 +instance int :: semiring_Gcd
1.915 +  by standard (auto intro!: Gcd_dvd Gcd_greatest simp add: Gcd_int_def Lcm_int_def int_dvd_iff dvd_int_iff
1.916 +    dvd_int_unfold_dvd_nat [symmetric])
1.917 +
1.918 +instance int :: semiring_Lcm
1.919 +proof
1.920 +  fix K :: "int set"
1.921 +  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})"
1.922 +  proof (rule set_eqI)
1.923 +    fix n
1.924 +    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")
1.925 +    proof
1.926 +      assume ?P
1.927 +      then have "(\<forall>k\<in>K. k dvd int n) \<and> n = nat \<bar>int n\<bar>"
1.928 +        by (auto simp add: dvd_int_unfold_dvd_nat)
1.929 +      then show ?Q by blast
1.930 +    next
1.931 +      assume ?Q then show ?P
1.932 +        by (auto simp add: dvd_int_unfold_dvd_nat)
1.933 +    qed
1.934 +    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}"
1.935 +      by auto
1.936 +  qed
1.937 +  then show "Lcm K = Gcd {l. \<forall>k\<in>K. k dvd l}"
1.938 +    by (simp add: Gcd_int_def Lcm_int_def Lcm_Gcd)
1.939 +qed
1.940 +
1.941  lemma Lcm_empty_int [simp]: "Lcm {} = (1::int)"
1.943
1.944 @@ -1692,7 +2214,7 @@
1.945    by (simp add: Lcm_int_def lcm_int_def)
1.946
1.947  lemma dvd_int_iff: "x dvd y \<longleftrightarrow> nat (abs x) dvd nat (abs y)"
1.948 -  by (simp add: zdvd_int)
1.949 +  by (fact dvd_int_unfold_dvd_nat)
1.950
1.951  lemma dvd_Lcm_int [simp]:
1.952    fixes M :: "int set" assumes "m \<in> M" shows "m dvd Lcm M"
1.953 @@ -1703,9 +2225,6 @@
1.954    assumes "\<forall>m\<in>M. m dvd n" shows "Lcm M dvd n"
1.955    using assms by (simp add: Lcm_int_def dvd_int_iff)
1.956
1.957 -instance int :: semiring_Gcd
1.958 -  by intro_classes (simp_all add: Gcd_int_def gcd_int_def dvd_int_iff Gcd_dvd dvd_Gcd)
1.959 -
1.960  lemma Lcm_set_int [code, code_unfold]:
1.961    "Lcm (set xs) = fold lcm xs (1::int)"
1.962    by (induct xs rule: rev_induct) (simp_all add: lcm_commute_int)
```
```     2.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:34 2015 +0200
2.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:39 2015 +0200
2.3 @@ -1832,7 +1832,7 @@
2.4  lemma dvd_poly_gcd_iff [iff]:
2.5    fixes k x y :: "_ poly"
2.6    shows "k dvd gcd x y \<longleftrightarrow> k dvd x \<and> k dvd y"
2.7 -  by (blast intro!: poly_gcd_greatest intro: dvd_trans)
2.8 +  by (auto intro!: poly_gcd_greatest intro: dvd_trans [of _ "gcd x y"])
2.9
2.10  lemma poly_gcd_monic:
2.11    fixes x y :: "_ poly"
```
```     3.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:34 2015 +0200
3.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Wed Jul 08 14:01:39 2015 +0200
3.3 @@ -1363,8 +1363,17 @@
3.5
3.6  subclass semiring_gcd
3.7 -  by unfold_locales (simp_all add: gcd_greatest_iff)
3.8 -
3.9 +  apply standard
3.10 +  using gcd_right_idem
3.11 +  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
3.12 +  done
3.13 +
3.14 +subclass semiring_Gcd
3.15 +  by standard (simp_all add: Gcd_greatest)
3.16 +
3.17 +subclass semiring_Lcm
3.18 +  by standard (simp add: Lcm_Gcd)
3.19 +
3.20  end
3.21
3.22  text \<open>
3.23 @@ -1382,7 +1391,7 @@
3.24  lemma euclid_ext_gcd [simp]:
3.25    "(case euclid_ext a b of (_, _ , t) \<Rightarrow> t) = gcd a b"
3.26    by (induct a b rule: gcd_eucl_induct)
3.27 -    (simp_all add: euclid_ext_0 gcd_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
3.28 +    (simp_all add: euclid_ext_0 euclid_ext_non_0 ac_simps split: prod.split prod.split_asm)
3.29
3.30  lemma euclid_ext_gcd' [simp]:
3.31    "euclid_ext a b = (r, s, t) \<Longrightarrow> t = gcd a b"
3.32 @@ -1453,9 +1462,6 @@
3.33  definition [simp]:
3.34    "euclidean_size_nat = (id :: nat \<Rightarrow> nat)"
3.35
3.36 -definition [simp]:
3.37 -  "unit_factor_nat (n::nat) = (if n = 0 then 0 else 1 :: nat)"
3.38 -
3.39  instance proof
3.40  qed simp_all
3.41
3.42 @@ -1467,11 +1473,8 @@
3.43  definition [simp]:
3.44    "euclidean_size_int = (nat \<circ> abs :: int \<Rightarrow> nat)"
3.45
3.46 -definition [simp]:
3.47 -  "unit_factor_int = (sgn :: int \<Rightarrow> int)"
3.48 -
3.49  instance
3.50 -by standard (auto simp add: abs_mult nat_mult_distrib sgn_times split: abs_split)
3.51 +by standard (auto simp add: abs_mult nat_mult_distrib split: abs_split)
3.52
3.53  end
3.54
```