more algebraic properties for gcd/lcm
authorhaftmann
Wed Jul 08 14:01:39 2015 +0200 (2015-07-08)
changeset 60686ea5bc46c11e6
parent 60685 cb21b7022b00
child 60687 33dbbcb6a8a3
more algebraic properties for gcd/lcm
src/HOL/GCD.thy
src/HOL/Library/Polynomial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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.601 +qed (simp_all add: lcm_nat_def)
   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)[4]
   1.616 +apply standard
   1.617 +apply (auto intro: dvd_antisym dvd_trans)[2]
   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.942    by (simp add: Lcm_int_def)
   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.4    by (simp add: gcd_0)
     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