src/HOL/GCD.thy
changeset 64850 fc9265882329
parent 64591 240a39af9ec4
child 65552 f533820e7248
     1.1 --- a/src/HOL/GCD.thy	Mon Jan 09 18:53:20 2017 +0100
     1.2 +++ b/src/HOL/GCD.thy	Mon Jan 09 19:13:49 2017 +0100
     1.3 @@ -34,6 +34,108 @@
     1.4    imports Main
     1.5  begin
     1.6  
     1.7 +subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
     1.8 +  
     1.9 +locale bounded_quasi_semilattice = abel_semigroup + 
    1.10 +  fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
    1.11 +    and normalize :: "'a \<Rightarrow> 'a"
    1.12 +  assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
    1.13 +    and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
    1.14 +    and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
    1.15 +    and normalize_top [simp]: "normalize \<top> = \<top>"
    1.16 +    and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
    1.17 +    and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
    1.18 +    and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
    1.19 +begin
    1.20 +
    1.21 +lemma left_idem [simp]:
    1.22 +  "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
    1.23 +  using assoc [of a a b, symmetric] by simp
    1.24 +
    1.25 +lemma right_idem [simp]:
    1.26 +  "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
    1.27 +  using left_idem [of b a] by (simp add: ac_simps)
    1.28 +
    1.29 +lemma comp_fun_idem: "comp_fun_idem f"
    1.30 +  by standard (simp_all add: fun_eq_iff ac_simps)
    1.31 +
    1.32 +interpretation comp_fun_idem f
    1.33 +  by (fact comp_fun_idem)
    1.34 +
    1.35 +lemma top_right_normalize [simp]:
    1.36 +  "a \<^bold>* \<top> = normalize a"
    1.37 +  using top_left_normalize [of a] by (simp add: ac_simps)
    1.38 +  
    1.39 +lemma bottom_right_bottom [simp]:
    1.40 +  "a \<^bold>* \<bottom> = \<bottom>"
    1.41 +  using bottom_left_bottom [of a] by (simp add: ac_simps)
    1.42 +
    1.43 +lemma normalize_right_idem [simp]:
    1.44 +  "a \<^bold>* normalize b = a \<^bold>* b"
    1.45 +  using normalize_left_idem [of b a] by (simp add: ac_simps)
    1.46 +
    1.47 +end    
    1.48 +
    1.49 +locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
    1.50 +begin
    1.51 +
    1.52 +interpretation comp_fun_idem f
    1.53 +  by (fact comp_fun_idem)
    1.54 +
    1.55 +definition F :: "'a set \<Rightarrow> 'a"
    1.56 +where
    1.57 +  eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
    1.58 +
    1.59 +lemma set_eq_fold [code]:
    1.60 +  "F (set xs) = fold f xs \<top>"
    1.61 +  by (simp add: eq_fold fold_set_fold)
    1.62 +
    1.63 +lemma infinite [simp]:
    1.64 +  "infinite A \<Longrightarrow> F A = \<bottom>"
    1.65 +  by (simp add: eq_fold)
    1.66 +
    1.67 +lemma empty [simp]:
    1.68 +  "F {} = \<top>"
    1.69 +  by (simp add: eq_fold)
    1.70 +
    1.71 +lemma insert [simp]:
    1.72 +  "F (insert a A) = a \<^bold>* F A"
    1.73 +  by (cases "finite A") (simp_all add: eq_fold)
    1.74 +
    1.75 +lemma normalize [simp]:
    1.76 +  "normalize (F A) = F A"
    1.77 +  by (induct A rule: infinite_finite_induct) simp_all
    1.78 +
    1.79 +lemma in_idem:
    1.80 +  assumes "a \<in> A"
    1.81 +  shows "a \<^bold>* F A = F A"
    1.82 +  using assms by (induct A rule: infinite_finite_induct)
    1.83 +    (auto simp add: left_commute [of a])
    1.84 +
    1.85 +lemma union:
    1.86 +  "F (A \<union> B) = F A \<^bold>* F B"
    1.87 +  by (induct A rule: infinite_finite_induct)
    1.88 +    (simp_all add: ac_simps)
    1.89 +
    1.90 +lemma remove:
    1.91 +  assumes "a \<in> A"
    1.92 +  shows "F A = a \<^bold>* F (A - {a})"
    1.93 +proof -
    1.94 +  from assms obtain B where "A = insert a B" and "a \<notin> B"
    1.95 +    by (blast dest: mk_disjoint_insert)
    1.96 +  with assms show ?thesis by simp
    1.97 +qed
    1.98 +
    1.99 +lemma insert_remove:
   1.100 +  "F (insert a A) = a \<^bold>* F (A - {a})"
   1.101 +  by (cases "a \<in> A") (simp_all add: insert_absorb remove)
   1.102 +
   1.103 +lemma subset:
   1.104 +  assumes "B \<subseteq> A"
   1.105 +  shows "F B \<^bold>* F A = F A"
   1.106 +  using assms by (simp add: union [symmetric] Un_absorb1)
   1.107 +  
   1.108 +end
   1.109  
   1.110  subsection \<open>Abstract GCD and LCM\<close>
   1.111  
   1.112 @@ -165,25 +267,36 @@
   1.113      by (rule associated_eqI) simp_all
   1.114  qed
   1.115  
   1.116 -lemma gcd_self [simp]: "gcd a a = normalize a"
   1.117 -proof -
   1.118 -  have "a dvd gcd a a"
   1.119 -    by (rule gcd_greatest) simp_all
   1.120 -  then show ?thesis
   1.121 +sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
   1.122 +proof
   1.123 +  show "gcd a a = normalize a" for a
   1.124 +  proof -
   1.125 +    have "a dvd gcd a a"
   1.126 +      by (rule gcd_greatest) simp_all
   1.127 +    then show ?thesis
   1.128 +      by (auto intro: associated_eqI)
   1.129 +  qed
   1.130 +  show "gcd (normalize a) b = gcd a b" for a b
   1.131 +    using gcd_dvd1 [of "normalize a" b]
   1.132      by (auto intro: associated_eqI)
   1.133 -qed
   1.134 -
   1.135 -lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
   1.136 -  by (auto intro: associated_eqI)
   1.137 -
   1.138 -lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
   1.139 -  unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
   1.140 -
   1.141 -lemma coprime_1_left [simp]: "coprime 1 a"
   1.142 -  by (rule associated_eqI) simp_all
   1.143 -
   1.144 -lemma coprime_1_right [simp]: "coprime a 1"
   1.145 -  using coprime_1_left [of a] by (simp add: ac_simps)
   1.146 +  show "coprime 1 a" for a
   1.147 +    by (rule associated_eqI) simp_all
   1.148 +qed simp_all
   1.149 +  
   1.150 +lemma gcd_self: "gcd a a = normalize a"
   1.151 +  by (fact gcd.idem_normalize)
   1.152 +
   1.153 +lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
   1.154 +  by (fact gcd.left_idem)
   1.155 +
   1.156 +lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   1.157 +  by (fact gcd.right_idem)
   1.158 +
   1.159 +lemma coprime_1_left: "coprime 1 a"
   1.160 +  by (fact gcd.bottom_left_bottom)
   1.161 +
   1.162 +lemma coprime_1_right: "coprime a 1"
   1.163 +  by (fact gcd.bottom_right_bottom)
   1.164  
   1.165  lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
   1.166  proof (cases "c = 0")
   1.167 @@ -325,19 +438,30 @@
   1.168      by (rule associated_eqI) simp_all
   1.169  qed
   1.170  
   1.171 -lemma lcm_self [simp]: "lcm a a = normalize a"
   1.172 -proof -
   1.173 -  have "lcm a a dvd a"
   1.174 -    by (rule lcm_least) simp_all
   1.175 -  then show ?thesis
   1.176 +sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
   1.177 +proof
   1.178 +  show "lcm a a = normalize a" for a
   1.179 +  proof -
   1.180 +    have "lcm a a dvd a"
   1.181 +      by (rule lcm_least) simp_all
   1.182 +    then show ?thesis
   1.183 +      by (auto intro: associated_eqI)
   1.184 +  qed
   1.185 +  show "lcm (normalize a) b = lcm a b" for a b
   1.186 +    using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
   1.187      by (auto intro: associated_eqI)
   1.188 -qed
   1.189 -
   1.190 -lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
   1.191 -  by (auto intro: associated_eqI)
   1.192 -
   1.193 -lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
   1.194 -  unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
   1.195 +  show "lcm 1 a = normalize a" for a
   1.196 +    by (rule associated_eqI) simp_all
   1.197 +qed simp_all
   1.198 +
   1.199 +lemma lcm_self: "lcm a a = normalize a"
   1.200 +  by (fact lcm.idem_normalize)
   1.201 +
   1.202 +lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
   1.203 +  by (fact lcm.left_idem)
   1.204 +
   1.205 +lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
   1.206 +  by (fact lcm.right_idem)
   1.207  
   1.208  lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
   1.209    by (simp add: lcm_gcd normalize_mult)
   1.210 @@ -359,11 +483,11 @@
   1.211      using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
   1.212  qed
   1.213  
   1.214 -lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
   1.215 -  by (simp add: lcm_gcd)
   1.216 -
   1.217 -lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
   1.218 -  by (simp add: lcm_gcd)
   1.219 +lemma lcm_1_left: "lcm 1 a = normalize a"
   1.220 +  by (fact lcm.top_left_normalize)
   1.221 +
   1.222 +lemma lcm_1_right: "lcm a 1 = normalize a"
   1.223 +  by (fact lcm.top_right_normalize)
   1.224  
   1.225  lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
   1.226    by (cases "c = 0")
   1.227 @@ -450,23 +574,11 @@
   1.228  lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   1.229    by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
   1.230  
   1.231 -lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
   1.232 -proof (cases "a = 0")
   1.233 -  case True
   1.234 -  then show ?thesis
   1.235 -    by simp
   1.236 -next
   1.237 -  case False
   1.238 -  then have "is_unit (unit_factor a)"
   1.239 -    by simp
   1.240 -  moreover have "normalize a = a div unit_factor a"
   1.241 -    by simp
   1.242 -  ultimately show ?thesis
   1.243 -    by (simp only: lcm_div_unit1)
   1.244 -qed
   1.245 -
   1.246 -lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
   1.247 -  using normalize_lcm_left [of b a] by (simp add: ac_simps)
   1.248 +lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
   1.249 +  by (fact lcm.normalize_left_idem)
   1.250 +
   1.251 +lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
   1.252 +  by (fact lcm.normalize_right_idem)
   1.253  
   1.254  lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   1.255    apply (rule gcdI)
   1.256 @@ -489,23 +601,11 @@
   1.257  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   1.258    by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
   1.259  
   1.260 -lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
   1.261 -proof (cases "a = 0")
   1.262 -  case True
   1.263 -  then show ?thesis
   1.264 -    by simp
   1.265 -next
   1.266 -  case False
   1.267 -  then have "is_unit (unit_factor a)"
   1.268 -    by simp
   1.269 -  moreover have "normalize a = a div unit_factor a"
   1.270 -    by simp
   1.271 -  ultimately show ?thesis
   1.272 -    by (simp only: gcd_div_unit1)
   1.273 -qed
   1.274 -
   1.275 -lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
   1.276 -  using normalize_gcd_left [of b a] by (simp add: ac_simps)
   1.277 +lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
   1.278 +  by (fact gcd.normalize_left_idem)
   1.279 +
   1.280 +lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
   1.281 +  by (fact gcd.normalize_right_idem)
   1.282  
   1.283  lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   1.284    by standard (simp_all add: fun_eq_iff ac_simps)
   1.285 @@ -942,6 +1042,21 @@
   1.286  lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   1.287    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
   1.288  
   1.289 +lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
   1.290 +  by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
   1.291 +
   1.292 +lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
   1.293 +proof-
   1.294 +  have "normalize k * lcm a b = lcm (k * a) (k * b)"
   1.295 +    by (simp add: lcm_mult_distrib')
   1.296 +  then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
   1.297 +    by simp
   1.298 +  then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
   1.299 +    by (simp only: ac_simps)
   1.300 +  then show ?thesis
   1.301 +    by simp
   1.302 +qed
   1.303 +
   1.304  lemma dvd_productE:
   1.305    assumes "p dvd (a * b)"
   1.306    obtains x y where "p = x * y" "x dvd a" "y dvd b"
   1.307 @@ -1229,26 +1344,6 @@
   1.308      by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
   1.309  qed
   1.310  
   1.311 -lemma Gcd_finite:
   1.312 -  assumes "finite A"
   1.313 -  shows "Gcd A = Finite_Set.fold gcd 0 A"
   1.314 -  by (induct rule: finite.induct[OF \<open>finite A\<close>])
   1.315 -    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
   1.316 -
   1.317 -lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
   1.318 -  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
   1.319 -      foldl_conv_fold gcd.commute)
   1.320 -
   1.321 -lemma Lcm_finite:
   1.322 -  assumes "finite A"
   1.323 -  shows "Lcm A = Finite_Set.fold lcm 1 A"
   1.324 -  by (induct rule: finite.induct[OF \<open>finite A\<close>])
   1.325 -    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
   1.326 -
   1.327 -lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
   1.328 -  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
   1.329 -      foldl_conv_fold lcm.commute)
   1.330 -
   1.331  lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
   1.332  proof -
   1.333    have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
   1.334 @@ -1432,6 +1527,145 @@
   1.335  
   1.336  end
   1.337  
   1.338 +  
   1.339 +subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
   1.340 +
   1.341 +context semiring_gcd
   1.342 +begin
   1.343 +
   1.344 +sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
   1.345 +defines
   1.346 +  Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
   1.347 +
   1.348 +abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
   1.349 +  where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
   1.350 +
   1.351 +sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
   1.352 +defines
   1.353 +  Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
   1.354 +
   1.355 +abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
   1.356 +  where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
   1.357 +    
   1.358 +lemma Gcd_fin_dvd:
   1.359 +  "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
   1.360 +  by (induct A rule: infinite_finite_induct) 
   1.361 +    (auto intro: dvd_trans)
   1.362 +
   1.363 +lemma dvd_Lcm_fin:
   1.364 +  "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
   1.365 +  by (induct A rule: infinite_finite_induct) 
   1.366 +    (auto intro: dvd_trans)
   1.367 +
   1.368 +lemma Gcd_fin_greatest:
   1.369 +  "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
   1.370 +  using that by (induct A) simp_all
   1.371 +
   1.372 +lemma Lcm_fin_least:
   1.373 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
   1.374 +  using that by (induct A) simp_all
   1.375 +
   1.376 +lemma gcd_list_greatest:
   1.377 +  "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
   1.378 +  by (rule Gcd_fin_greatest) (simp_all add: that)
   1.379 +
   1.380 +lemma lcm_list_least:
   1.381 +  "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
   1.382 +  by (rule Lcm_fin_least) (simp_all add: that)
   1.383 +
   1.384 +lemma dvd_Gcd_fin_iff:
   1.385 +  "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
   1.386 +  using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
   1.387 +
   1.388 +lemma dvd_gcd_list_iff:
   1.389 +  "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
   1.390 +  by (simp add: dvd_Gcd_fin_iff)
   1.391 +  
   1.392 +lemma Lcm_fin_dvd_iff:
   1.393 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
   1.394 +  using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
   1.395 +
   1.396 +lemma lcm_list_dvd_iff:
   1.397 +  "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
   1.398 +  by (simp add: Lcm_fin_dvd_iff)
   1.399 +
   1.400 +lemma Gcd_fin_mult:
   1.401 +  "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
   1.402 +using that proof induct
   1.403 +  case empty
   1.404 +  then show ?case
   1.405 +    by simp
   1.406 +next
   1.407 +  case (insert a A)
   1.408 +  have "gcd (b * a) (b * Gcd\<^sub>f\<^sub>i\<^sub>n A) = gcd (b * a) (normalize (b * Gcd\<^sub>f\<^sub>i\<^sub>n A))"
   1.409 +    by simp
   1.410 +  also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
   1.411 +    by (simp add: normalize_mult)
   1.412 +  finally show ?case
   1.413 +    using insert by (simp add: gcd_mult_distrib')
   1.414 +qed
   1.415 +
   1.416 +lemma Lcm_fin_mult:
   1.417 +  "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
   1.418 +proof (cases "b = 0")
   1.419 +  case True
   1.420 +  moreover from that have "times 0 ` A = {0}"
   1.421 +    by auto
   1.422 +  ultimately show ?thesis
   1.423 +    by simp
   1.424 +next
   1.425 +  case False
   1.426 +  then have "inj (times b)"
   1.427 +    by (rule inj_times)
   1.428 +  show ?thesis proof (cases "finite A")
   1.429 +    case False
   1.430 +    moreover from \<open>inj (times b)\<close>
   1.431 +    have "inj_on (times b) A"
   1.432 +      by (rule inj_on_subset) simp
   1.433 +    ultimately have "infinite (times b ` A)"
   1.434 +      by (simp add: finite_image_iff)
   1.435 +    with False show ?thesis
   1.436 +      by simp
   1.437 +  next
   1.438 +    case True
   1.439 +    then show ?thesis using that proof (induct A rule: finite_ne_induct)
   1.440 +      case (singleton a)
   1.441 +      then show ?case
   1.442 +        by (simp add: normalize_mult)
   1.443 +    next
   1.444 +      case (insert a A)
   1.445 +      have "lcm (b * a) (b * Lcm\<^sub>f\<^sub>i\<^sub>n A) = lcm (b * a) (normalize (b * Lcm\<^sub>f\<^sub>i\<^sub>n A))"
   1.446 +        by simp
   1.447 +      also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
   1.448 +        by (simp add: normalize_mult)
   1.449 +      finally show ?case
   1.450 +        using insert by (simp add: lcm_mult_distrib')
   1.451 +    qed
   1.452 +  qed
   1.453 +qed
   1.454 +
   1.455 +end
   1.456 +
   1.457 +context semiring_Gcd
   1.458 +begin
   1.459 +
   1.460 +lemma Gcd_fin_eq_Gcd [simp]:
   1.461 +  "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
   1.462 +  using that by induct simp_all
   1.463 +
   1.464 +lemma Gcd_set_eq_fold [code_unfold]:
   1.465 +  "Gcd (set xs) = fold gcd xs 0"
   1.466 +  by (simp add: Gcd_fin.set_eq_fold [symmetric])
   1.467 +
   1.468 +lemma Lcm_fin_eq_Lcm [simp]:
   1.469 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
   1.470 +  using that by induct simp_all
   1.471 +
   1.472 +lemma Lcm_set_eq_fold [code_unfold]:
   1.473 +  "Lcm (set xs) = fold lcm xs 1"
   1.474 +  by (simp add: Lcm_fin.set_eq_fold [symmetric])
   1.475 +
   1.476 +end
   1.477  
   1.478  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
   1.479  
   1.480 @@ -2514,11 +2748,10 @@
   1.481  
   1.482  text \<open>Some code equations\<close>
   1.483  
   1.484 -lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
   1.485 -lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
   1.486 -lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
   1.487 -lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
   1.488 -
   1.489 +lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
   1.490 +lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
   1.491 +lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
   1.492 +lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
   1.493  
   1.494  text \<open>Fact aliases.\<close>
   1.495