gcd/lcm on finite sets
authorhaftmann
Mon Jan 09 19:13:49 2017 +0100 (2017-01-09)
changeset 64850fc9265882329
parent 64849 766db3539859
child 64853 9178214b3588
gcd/lcm on finite sets
src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
src/HOL/GCD.thy
src/HOL/Library/Polynomial_Factorial.thy
src/HOL/Number_Theory/Euclidean_Algorithm.thy
     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.88 +    (simp_all add: ac_simps)
    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