author haftmann Mon Jan 09 19:13:49 2017 +0100 (2017-01-09) changeset 64850 fc9265882329 parent 64849 766db3539859 child 64853 9178214b3588
gcd/lcm on finite sets
```     1.1 --- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jan 09 18:53:20 2017 +0100
1.2 +++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jan 09 19:13:49 2017 +0100
1.3 @@ -34,6 +34,8 @@
1.4    Cardinality.finite'
1.5    Cardinality.subset'
1.6    Cardinality.eq_set
1.7 +  Gcd_fin
1.8 +  Lcm_fin
1.9    "Gcd :: nat set \<Rightarrow> nat"
1.10    "Lcm :: nat set \<Rightarrow> nat"
1.11    "Gcd :: int set \<Rightarrow> int"
```
```     2.1 --- a/src/HOL/GCD.thy	Mon Jan 09 18:53:20 2017 +0100
2.2 +++ b/src/HOL/GCD.thy	Mon Jan 09 19:13:49 2017 +0100
2.3 @@ -34,6 +34,108 @@
2.4    imports Main
2.5  begin
2.6
2.7 +subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
2.8 +
2.9 +locale bounded_quasi_semilattice = abel_semigroup +
2.10 +  fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
2.11 +    and normalize :: "'a \<Rightarrow> 'a"
2.12 +  assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
2.13 +    and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
2.14 +    and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
2.15 +    and normalize_top [simp]: "normalize \<top> = \<top>"
2.16 +    and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
2.17 +    and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
2.18 +    and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
2.19 +begin
2.20 +
2.21 +lemma left_idem [simp]:
2.22 +  "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
2.23 +  using assoc [of a a b, symmetric] by simp
2.24 +
2.25 +lemma right_idem [simp]:
2.26 +  "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
2.27 +  using left_idem [of b a] by (simp add: ac_simps)
2.28 +
2.29 +lemma comp_fun_idem: "comp_fun_idem f"
2.30 +  by standard (simp_all add: fun_eq_iff ac_simps)
2.31 +
2.32 +interpretation comp_fun_idem f
2.33 +  by (fact comp_fun_idem)
2.34 +
2.35 +lemma top_right_normalize [simp]:
2.36 +  "a \<^bold>* \<top> = normalize a"
2.37 +  using top_left_normalize [of a] by (simp add: ac_simps)
2.38 +
2.39 +lemma bottom_right_bottom [simp]:
2.40 +  "a \<^bold>* \<bottom> = \<bottom>"
2.41 +  using bottom_left_bottom [of a] by (simp add: ac_simps)
2.42 +
2.43 +lemma normalize_right_idem [simp]:
2.44 +  "a \<^bold>* normalize b = a \<^bold>* b"
2.45 +  using normalize_left_idem [of b a] by (simp add: ac_simps)
2.46 +
2.47 +end
2.48 +
2.49 +locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
2.50 +begin
2.51 +
2.52 +interpretation comp_fun_idem f
2.53 +  by (fact comp_fun_idem)
2.54 +
2.55 +definition F :: "'a set \<Rightarrow> 'a"
2.56 +where
2.57 +  eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
2.58 +
2.59 +lemma set_eq_fold [code]:
2.60 +  "F (set xs) = fold f xs \<top>"
2.61 +  by (simp add: eq_fold fold_set_fold)
2.62 +
2.63 +lemma infinite [simp]:
2.64 +  "infinite A \<Longrightarrow> F A = \<bottom>"
2.65 +  by (simp add: eq_fold)
2.66 +
2.67 +lemma empty [simp]:
2.68 +  "F {} = \<top>"
2.69 +  by (simp add: eq_fold)
2.70 +
2.71 +lemma insert [simp]:
2.72 +  "F (insert a A) = a \<^bold>* F A"
2.73 +  by (cases "finite A") (simp_all add: eq_fold)
2.74 +
2.75 +lemma normalize [simp]:
2.76 +  "normalize (F A) = F A"
2.77 +  by (induct A rule: infinite_finite_induct) simp_all
2.78 +
2.79 +lemma in_idem:
2.80 +  assumes "a \<in> A"
2.81 +  shows "a \<^bold>* F A = F A"
2.82 +  using assms by (induct A rule: infinite_finite_induct)
2.83 +    (auto simp add: left_commute [of a])
2.84 +
2.85 +lemma union:
2.86 +  "F (A \<union> B) = F A \<^bold>* F B"
2.87 +  by (induct A rule: infinite_finite_induct)
2.89 +
2.90 +lemma remove:
2.91 +  assumes "a \<in> A"
2.92 +  shows "F A = a \<^bold>* F (A - {a})"
2.93 +proof -
2.94 +  from assms obtain B where "A = insert a B" and "a \<notin> B"
2.95 +    by (blast dest: mk_disjoint_insert)
2.96 +  with assms show ?thesis by simp
2.97 +qed
2.98 +
2.99 +lemma insert_remove:
2.100 +  "F (insert a A) = a \<^bold>* F (A - {a})"
2.101 +  by (cases "a \<in> A") (simp_all add: insert_absorb remove)
2.102 +
2.103 +lemma subset:
2.104 +  assumes "B \<subseteq> A"
2.105 +  shows "F B \<^bold>* F A = F A"
2.106 +  using assms by (simp add: union [symmetric] Un_absorb1)
2.107 +
2.108 +end
2.109
2.110  subsection \<open>Abstract GCD and LCM\<close>
2.111
2.112 @@ -165,25 +267,36 @@
2.113      by (rule associated_eqI) simp_all
2.114  qed
2.115
2.116 -lemma gcd_self [simp]: "gcd a a = normalize a"
2.117 -proof -
2.118 -  have "a dvd gcd a a"
2.119 -    by (rule gcd_greatest) simp_all
2.120 -  then show ?thesis
2.121 +sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
2.122 +proof
2.123 +  show "gcd a a = normalize a" for a
2.124 +  proof -
2.125 +    have "a dvd gcd a a"
2.126 +      by (rule gcd_greatest) simp_all
2.127 +    then show ?thesis
2.128 +      by (auto intro: associated_eqI)
2.129 +  qed
2.130 +  show "gcd (normalize a) b = gcd a b" for a b
2.131 +    using gcd_dvd1 [of "normalize a" b]
2.132      by (auto intro: associated_eqI)
2.133 -qed
2.134 -
2.135 -lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
2.136 -  by (auto intro: associated_eqI)
2.137 -
2.138 -lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
2.139 -  unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
2.140 -
2.141 -lemma coprime_1_left [simp]: "coprime 1 a"
2.142 -  by (rule associated_eqI) simp_all
2.143 -
2.144 -lemma coprime_1_right [simp]: "coprime a 1"
2.145 -  using coprime_1_left [of a] by (simp add: ac_simps)
2.146 +  show "coprime 1 a" for a
2.147 +    by (rule associated_eqI) simp_all
2.148 +qed simp_all
2.149 +
2.150 +lemma gcd_self: "gcd a a = normalize a"
2.151 +  by (fact gcd.idem_normalize)
2.152 +
2.153 +lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
2.154 +  by (fact gcd.left_idem)
2.155 +
2.156 +lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
2.157 +  by (fact gcd.right_idem)
2.158 +
2.159 +lemma coprime_1_left: "coprime 1 a"
2.160 +  by (fact gcd.bottom_left_bottom)
2.161 +
2.162 +lemma coprime_1_right: "coprime a 1"
2.163 +  by (fact gcd.bottom_right_bottom)
2.164
2.165  lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
2.166  proof (cases "c = 0")
2.167 @@ -325,19 +438,30 @@
2.168      by (rule associated_eqI) simp_all
2.169  qed
2.170
2.171 -lemma lcm_self [simp]: "lcm a a = normalize a"
2.172 -proof -
2.173 -  have "lcm a a dvd a"
2.174 -    by (rule lcm_least) simp_all
2.175 -  then show ?thesis
2.176 +sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
2.177 +proof
2.178 +  show "lcm a a = normalize a" for a
2.179 +  proof -
2.180 +    have "lcm a a dvd a"
2.181 +      by (rule lcm_least) simp_all
2.182 +    then show ?thesis
2.183 +      by (auto intro: associated_eqI)
2.184 +  qed
2.185 +  show "lcm (normalize a) b = lcm a b" for a b
2.186 +    using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
2.187      by (auto intro: associated_eqI)
2.188 -qed
2.189 -
2.190 -lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
2.191 -  by (auto intro: associated_eqI)
2.192 -
2.193 -lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
2.194 -  unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
2.195 +  show "lcm 1 a = normalize a" for a
2.196 +    by (rule associated_eqI) simp_all
2.197 +qed simp_all
2.198 +
2.199 +lemma lcm_self: "lcm a a = normalize a"
2.200 +  by (fact lcm.idem_normalize)
2.201 +
2.202 +lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
2.203 +  by (fact lcm.left_idem)
2.204 +
2.205 +lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
2.206 +  by (fact lcm.right_idem)
2.207
2.208  lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
2.209    by (simp add: lcm_gcd normalize_mult)
2.210 @@ -359,11 +483,11 @@
2.211      using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
2.212  qed
2.213
2.214 -lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
2.215 -  by (simp add: lcm_gcd)
2.216 -
2.217 -lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
2.218 -  by (simp add: lcm_gcd)
2.219 +lemma lcm_1_left: "lcm 1 a = normalize a"
2.220 +  by (fact lcm.top_left_normalize)
2.221 +
2.222 +lemma lcm_1_right: "lcm a 1 = normalize a"
2.223 +  by (fact lcm.top_right_normalize)
2.224
2.225  lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
2.226    by (cases "c = 0")
2.227 @@ -450,23 +574,11 @@
2.228  lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
2.229    by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
2.230
2.231 -lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
2.232 -proof (cases "a = 0")
2.233 -  case True
2.234 -  then show ?thesis
2.235 -    by simp
2.236 -next
2.237 -  case False
2.238 -  then have "is_unit (unit_factor a)"
2.239 -    by simp
2.240 -  moreover have "normalize a = a div unit_factor a"
2.241 -    by simp
2.242 -  ultimately show ?thesis
2.243 -    by (simp only: lcm_div_unit1)
2.244 -qed
2.245 -
2.246 -lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
2.247 -  using normalize_lcm_left [of b a] by (simp add: ac_simps)
2.248 +lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
2.249 +  by (fact lcm.normalize_left_idem)
2.250 +
2.251 +lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
2.252 +  by (fact lcm.normalize_right_idem)
2.253
2.254  lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
2.255    apply (rule gcdI)
2.256 @@ -489,23 +601,11 @@
2.257  lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
2.258    by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
2.259
2.260 -lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
2.261 -proof (cases "a = 0")
2.262 -  case True
2.263 -  then show ?thesis
2.264 -    by simp
2.265 -next
2.266 -  case False
2.267 -  then have "is_unit (unit_factor a)"
2.268 -    by simp
2.269 -  moreover have "normalize a = a div unit_factor a"
2.270 -    by simp
2.271 -  ultimately show ?thesis
2.272 -    by (simp only: gcd_div_unit1)
2.273 -qed
2.274 -
2.275 -lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
2.276 -  using normalize_gcd_left [of b a] by (simp add: ac_simps)
2.277 +lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
2.278 +  by (fact gcd.normalize_left_idem)
2.279 +
2.280 +lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
2.281 +  by (fact gcd.normalize_right_idem)
2.282
2.283  lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
2.284    by standard (simp_all add: fun_eq_iff ac_simps)
2.285 @@ -942,6 +1042,21 @@
2.286  lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
2.287    using lcm_proj1_iff [of n m] by (simp add: ac_simps)
2.288
2.289 +lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
2.290 +  by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
2.291 +
2.292 +lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
2.293 +proof-
2.294 +  have "normalize k * lcm a b = lcm (k * a) (k * b)"
2.295 +    by (simp add: lcm_mult_distrib')
2.296 +  then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
2.297 +    by simp
2.298 +  then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
2.299 +    by (simp only: ac_simps)
2.300 +  then show ?thesis
2.301 +    by simp
2.302 +qed
2.303 +
2.304  lemma dvd_productE:
2.305    assumes "p dvd (a * b)"
2.306    obtains x y where "p = x * y" "x dvd a" "y dvd b"
2.307 @@ -1229,26 +1344,6 @@
2.308      by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
2.309  qed
2.310
2.311 -lemma Gcd_finite:
2.312 -  assumes "finite A"
2.313 -  shows "Gcd A = Finite_Set.fold gcd 0 A"
2.314 -  by (induct rule: finite.induct[OF \<open>finite A\<close>])
2.315 -    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
2.316 -
2.317 -lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
2.318 -  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
2.319 -      foldl_conv_fold gcd.commute)
2.320 -
2.321 -lemma Lcm_finite:
2.322 -  assumes "finite A"
2.323 -  shows "Lcm A = Finite_Set.fold lcm 1 A"
2.324 -  by (induct rule: finite.induct[OF \<open>finite A\<close>])
2.325 -    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
2.326 -
2.327 -lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
2.328 -  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
2.329 -      foldl_conv_fold lcm.commute)
2.330 -
2.331  lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
2.332  proof -
2.333    have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
2.334 @@ -1432,6 +1527,145 @@
2.335
2.336  end
2.337
2.338 +
2.339 +subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
2.340 +
2.341 +context semiring_gcd
2.342 +begin
2.343 +
2.344 +sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
2.345 +defines
2.346 +  Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
2.347 +
2.348 +abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
2.349 +  where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
2.350 +
2.351 +sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
2.352 +defines
2.353 +  Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
2.354 +
2.355 +abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
2.356 +  where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
2.357 +
2.358 +lemma Gcd_fin_dvd:
2.359 +  "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
2.360 +  by (induct A rule: infinite_finite_induct)
2.361 +    (auto intro: dvd_trans)
2.362 +
2.363 +lemma dvd_Lcm_fin:
2.364 +  "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
2.365 +  by (induct A rule: infinite_finite_induct)
2.366 +    (auto intro: dvd_trans)
2.367 +
2.368 +lemma Gcd_fin_greatest:
2.369 +  "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
2.370 +  using that by (induct A) simp_all
2.371 +
2.372 +lemma Lcm_fin_least:
2.373 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
2.374 +  using that by (induct A) simp_all
2.375 +
2.376 +lemma gcd_list_greatest:
2.377 +  "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
2.378 +  by (rule Gcd_fin_greatest) (simp_all add: that)
2.379 +
2.380 +lemma lcm_list_least:
2.381 +  "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
2.382 +  by (rule Lcm_fin_least) (simp_all add: that)
2.383 +
2.384 +lemma dvd_Gcd_fin_iff:
2.385 +  "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
2.386 +  using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
2.387 +
2.388 +lemma dvd_gcd_list_iff:
2.389 +  "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
2.390 +  by (simp add: dvd_Gcd_fin_iff)
2.391 +
2.392 +lemma Lcm_fin_dvd_iff:
2.393 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
2.394 +  using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
2.395 +
2.396 +lemma lcm_list_dvd_iff:
2.397 +  "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
2.398 +  by (simp add: Lcm_fin_dvd_iff)
2.399 +
2.400 +lemma Gcd_fin_mult:
2.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"
2.402 +using that proof induct
2.403 +  case empty
2.404 +  then show ?case
2.405 +    by simp
2.406 +next
2.407 +  case (insert a A)
2.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))"
2.409 +    by simp
2.410 +  also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
2.411 +    by (simp add: normalize_mult)
2.412 +  finally show ?case
2.413 +    using insert by (simp add: gcd_mult_distrib')
2.414 +qed
2.415 +
2.416 +lemma Lcm_fin_mult:
2.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> {}"
2.418 +proof (cases "b = 0")
2.419 +  case True
2.420 +  moreover from that have "times 0 ` A = {0}"
2.421 +    by auto
2.422 +  ultimately show ?thesis
2.423 +    by simp
2.424 +next
2.425 +  case False
2.426 +  then have "inj (times b)"
2.427 +    by (rule inj_times)
2.428 +  show ?thesis proof (cases "finite A")
2.429 +    case False
2.430 +    moreover from \<open>inj (times b)\<close>
2.431 +    have "inj_on (times b) A"
2.432 +      by (rule inj_on_subset) simp
2.433 +    ultimately have "infinite (times b ` A)"
2.434 +      by (simp add: finite_image_iff)
2.435 +    with False show ?thesis
2.436 +      by simp
2.437 +  next
2.438 +    case True
2.439 +    then show ?thesis using that proof (induct A rule: finite_ne_induct)
2.440 +      case (singleton a)
2.441 +      then show ?case
2.442 +        by (simp add: normalize_mult)
2.443 +    next
2.444 +      case (insert a A)
2.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))"
2.446 +        by simp
2.447 +      also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
2.448 +        by (simp add: normalize_mult)
2.449 +      finally show ?case
2.450 +        using insert by (simp add: lcm_mult_distrib')
2.451 +    qed
2.452 +  qed
2.453 +qed
2.454 +
2.455 +end
2.456 +
2.457 +context semiring_Gcd
2.458 +begin
2.459 +
2.460 +lemma Gcd_fin_eq_Gcd [simp]:
2.461 +  "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
2.462 +  using that by induct simp_all
2.463 +
2.464 +lemma Gcd_set_eq_fold [code_unfold]:
2.465 +  "Gcd (set xs) = fold gcd xs 0"
2.466 +  by (simp add: Gcd_fin.set_eq_fold [symmetric])
2.467 +
2.468 +lemma Lcm_fin_eq_Lcm [simp]:
2.469 +  "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
2.470 +  using that by induct simp_all
2.471 +
2.472 +lemma Lcm_set_eq_fold [code_unfold]:
2.473 +  "Lcm (set xs) = fold lcm xs 1"
2.474 +  by (simp add: Lcm_fin.set_eq_fold [symmetric])
2.475 +
2.476 +end
2.477
2.478  subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
2.479
2.480 @@ -2514,11 +2748,10 @@
2.481
2.482  text \<open>Some code equations\<close>
2.483
2.484 -lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
2.485 -lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
2.486 -lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
2.487 -lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
2.488 -
2.489 +lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
2.490 +lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
2.491 +lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
2.492 +lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
2.493
2.494  text \<open>Fact aliases.\<close>
2.495
```
```     3.1 --- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 18:53:20 2017 +0100
3.2 +++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 19:13:49 2017 +0100
3.3 @@ -981,12 +981,9 @@
3.4    shows "lcm p q = normalize (p * q) div gcd p q"
3.5    by (fact lcm_gcd)
3.6
3.7 -declare Gcd_set
3.8 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
3.9 -
3.10 -declare Lcm_set
3.11 -  [where ?'a = "'a :: factorial_ring_gcd poly", code]
3.12 -
3.13 +lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
3.14 +lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
3.15 +
3.16  text \<open>Example:
3.17    @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
3.18  \<close>
```
```     4.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 18:53:20 2017 +0100
4.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 19:13:49 2017 +0100
4.3 @@ -254,12 +254,12 @@
4.4  qed
4.5
4.6  lemma Gcd_eucl_set [code]:
4.7 -  "Gcd (set xs) = foldl gcd 0 xs"
4.8 -  by (fact local.Gcd_set)
4.9 +  "Gcd (set xs) = fold gcd xs 0"
4.10 +  by (fact Gcd_set_eq_fold)
4.11
4.12  lemma Lcm_eucl_set [code]:
4.13 -  "Lcm (set xs) = foldl lcm 1 xs"
4.14 -  by (fact local.Lcm_set)
4.15 +  "Lcm (set xs) = fold lcm xs 1"
4.16 +  by (fact Lcm_set_eq_fold)
4.17
4.18  end
4.19
```