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.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) = "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) = 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
```