# HG changeset patch
# User nipkow
# Date 1483986856 -3600
# Node ID 9178214b3588d421f11c473c06d1837befd4cfb3
# Parent  fc9265882329f3b941e3a10b332b864d401cc00c# Parent  f3504bc69ea3dc42522638069089916c60a6ae4c
merged

diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Code_Numeral.thy
--- a/src/HOL/Code_Numeral.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Code_Numeral.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -225,7 +225,7 @@
   "of_nat (nat_of_integer k) = max 0 k"
   by transfer auto
 
-instantiation integer :: "{ring_div, normalization_semidom}"
+instantiation integer :: normalization_semidom
 begin
 
 lift_definition normalize_integer :: "integer \<Rightarrow> integer"
@@ -245,7 +245,16 @@
   .
 
 declare divide_integer.rep_eq [simp]
+  
+instance
+  by (standard; transfer)
+    (auto simp add: mult_sgn_abs sgn_mult abs_eq_iff')
 
+end
+
+instantiation integer :: ring_div
+begin
+  
 lift_definition modulo_integer :: "integer \<Rightarrow> integer \<Rightarrow> integer"
   is "modulo :: int \<Rightarrow> int \<Rightarrow> int"
   .
@@ -253,7 +262,7 @@
 declare modulo_integer.rep_eq [simp]
 
 instance
-  by standard (transfer, simp add: mult_sgn_abs sgn_mult)+
+  by (standard; transfer) simp_all
 
 end
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy
--- a/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Codegenerator_Test/Generate_Efficient_Datastructures.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -34,6 +34,8 @@
   Cardinality.finite'
   Cardinality.subset'
   Cardinality.eq_set
+  Gcd_fin
+  Lcm_fin
   "Gcd :: nat set \<Rightarrow> nat"
   "Lcm :: nat set \<Rightarrow> nat"
   "Gcd :: int set \<Rightarrow> int"
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Divides.thy
--- a/src/HOL/Divides.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Divides.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -1812,7 +1812,7 @@
   assume "l \<noteq> 0"
   then show "k * l div l = k"
     by (auto simp add: eucl_rel_int_iff ac_simps intro: div_int_unique [of _ _ _ 0])
-qed (simp_all add: sgn_mult mult_sgn_abs abs_sgn_eq)
+qed (auto simp add: sgn_mult mult_sgn_abs abs_eq_iff')
 
 end
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/GCD.thy
--- a/src/HOL/GCD.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/GCD.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -34,6 +34,108 @@
   imports Main
 begin
 
+subsection \<open>Abstract bounded quasi semilattices as common foundation\<close>
+  
+locale bounded_quasi_semilattice = abel_semigroup + 
+  fixes top :: 'a  ("\<top>") and bot :: 'a  ("\<bottom>")
+    and normalize :: "'a \<Rightarrow> 'a"
+  assumes idem_normalize [simp]: "a \<^bold>* a = normalize a"
+    and normalize_left_idem [simp]: "normalize a \<^bold>* b = a \<^bold>* b"
+    and normalize_idem [simp]: "normalize (a \<^bold>* b) = a \<^bold>* b"
+    and normalize_top [simp]: "normalize \<top> = \<top>"
+    and normalize_bottom [simp]: "normalize \<bottom> = \<bottom>"
+    and top_left_normalize [simp]: "\<top> \<^bold>* a = normalize a"
+    and bottom_left_bottom [simp]: "\<bottom> \<^bold>* a = \<bottom>"
+begin
+
+lemma left_idem [simp]:
+  "a \<^bold>* (a \<^bold>* b) = a \<^bold>* b"
+  using assoc [of a a b, symmetric] by simp
+
+lemma right_idem [simp]:
+  "(a \<^bold>* b) \<^bold>* b = a \<^bold>* b"
+  using left_idem [of b a] by (simp add: ac_simps)
+
+lemma comp_fun_idem: "comp_fun_idem f"
+  by standard (simp_all add: fun_eq_iff ac_simps)
+
+interpretation comp_fun_idem f
+  by (fact comp_fun_idem)
+
+lemma top_right_normalize [simp]:
+  "a \<^bold>* \<top> = normalize a"
+  using top_left_normalize [of a] by (simp add: ac_simps)
+  
+lemma bottom_right_bottom [simp]:
+  "a \<^bold>* \<bottom> = \<bottom>"
+  using bottom_left_bottom [of a] by (simp add: ac_simps)
+
+lemma normalize_right_idem [simp]:
+  "a \<^bold>* normalize b = a \<^bold>* b"
+  using normalize_left_idem [of b a] by (simp add: ac_simps)
+
+end    
+
+locale bounded_quasi_semilattice_set = bounded_quasi_semilattice
+begin
+
+interpretation comp_fun_idem f
+  by (fact comp_fun_idem)
+
+definition F :: "'a set \<Rightarrow> 'a"
+where
+  eq_fold: "F A = (if finite A then Finite_Set.fold f \<top> A else \<bottom>)"
+
+lemma set_eq_fold [code]:
+  "F (set xs) = fold f xs \<top>"
+  by (simp add: eq_fold fold_set_fold)
+
+lemma infinite [simp]:
+  "infinite A \<Longrightarrow> F A = \<bottom>"
+  by (simp add: eq_fold)
+
+lemma empty [simp]:
+  "F {} = \<top>"
+  by (simp add: eq_fold)
+
+lemma insert [simp]:
+  "F (insert a A) = a \<^bold>* F A"
+  by (cases "finite A") (simp_all add: eq_fold)
+
+lemma normalize [simp]:
+  "normalize (F A) = F A"
+  by (induct A rule: infinite_finite_induct) simp_all
+
+lemma in_idem:
+  assumes "a \<in> A"
+  shows "a \<^bold>* F A = F A"
+  using assms by (induct A rule: infinite_finite_induct)
+    (auto simp add: left_commute [of a])
+
+lemma union:
+  "F (A \<union> B) = F A \<^bold>* F B"
+  by (induct A rule: infinite_finite_induct)
+    (simp_all add: ac_simps)
+
+lemma remove:
+  assumes "a \<in> A"
+  shows "F A = a \<^bold>* F (A - {a})"
+proof -
+  from assms obtain B where "A = insert a B" and "a \<notin> B"
+    by (blast dest: mk_disjoint_insert)
+  with assms show ?thesis by simp
+qed
+
+lemma insert_remove:
+  "F (insert a A) = a \<^bold>* F (A - {a})"
+  by (cases "a \<in> A") (simp_all add: insert_absorb remove)
+
+lemma subset:
+  assumes "B \<subseteq> A"
+  shows "F B \<^bold>* F A = F A"
+  using assms by (simp add: union [symmetric] Un_absorb1)
+  
+end
 
 subsection \<open>Abstract GCD and LCM\<close>
 
@@ -165,25 +267,36 @@
     by (rule associated_eqI) simp_all
 qed
 
-lemma gcd_self [simp]: "gcd a a = normalize a"
-proof -
-  have "a dvd gcd a a"
-    by (rule gcd_greatest) simp_all
-  then show ?thesis
+sublocale gcd: bounded_quasi_semilattice gcd 0 1 normalize
+proof
+  show "gcd a a = normalize a" for a
+  proof -
+    have "a dvd gcd a a"
+      by (rule gcd_greatest) simp_all
+    then show ?thesis
+      by (auto intro: associated_eqI)
+  qed
+  show "gcd (normalize a) b = gcd a b" for a b
+    using gcd_dvd1 [of "normalize a" b]
     by (auto intro: associated_eqI)
-qed
-
-lemma gcd_left_idem [simp]: "gcd a (gcd a b) = gcd a b"
-  by (auto intro: associated_eqI)
-
-lemma gcd_right_idem [simp]: "gcd (gcd a b) b = gcd a b"
-  unfolding gcd.commute [of a] gcd.commute [of "gcd b a"] by simp
-
-lemma coprime_1_left [simp]: "coprime 1 a"
-  by (rule associated_eqI) simp_all
-
-lemma coprime_1_right [simp]: "coprime a 1"
-  using coprime_1_left [of a] by (simp add: ac_simps)
+  show "coprime 1 a" for a
+    by (rule associated_eqI) simp_all
+qed simp_all
+  
+lemma gcd_self: "gcd a a = normalize a"
+  by (fact gcd.idem_normalize)
+
+lemma gcd_left_idem: "gcd a (gcd a b) = gcd a b"
+  by (fact gcd.left_idem)
+
+lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
+  by (fact gcd.right_idem)
+
+lemma coprime_1_left: "coprime 1 a"
+  by (fact gcd.bottom_left_bottom)
+
+lemma coprime_1_right: "coprime a 1"
+  by (fact gcd.bottom_right_bottom)
 
 lemma gcd_mult_left: "gcd (c * a) (c * b) = normalize c * gcd a b"
 proof (cases "c = 0")
@@ -325,19 +438,30 @@
     by (rule associated_eqI) simp_all
 qed
 
-lemma lcm_self [simp]: "lcm a a = normalize a"
-proof -
-  have "lcm a a dvd a"
-    by (rule lcm_least) simp_all
-  then show ?thesis
+sublocale lcm: bounded_quasi_semilattice lcm 1 0 normalize
+proof
+  show "lcm a a = normalize a" for a
+  proof -
+    have "lcm a a dvd a"
+      by (rule lcm_least) simp_all
+    then show ?thesis
+      by (auto intro: associated_eqI)
+  qed
+  show "lcm (normalize a) b = lcm a b" for a b
+    using dvd_lcm1 [of "normalize a" b] unfolding normalize_dvd_iff
     by (auto intro: associated_eqI)
-qed
-
-lemma lcm_left_idem [simp]: "lcm a (lcm a b) = lcm a b"
-  by (auto intro: associated_eqI)
-
-lemma lcm_right_idem [simp]: "lcm (lcm a b) b = lcm a b"
-  unfolding lcm.commute [of a] lcm.commute [of "lcm b a"] by simp
+  show "lcm 1 a = normalize a" for a
+    by (rule associated_eqI) simp_all
+qed simp_all
+
+lemma lcm_self: "lcm a a = normalize a"
+  by (fact lcm.idem_normalize)
+
+lemma lcm_left_idem: "lcm a (lcm a b) = lcm a b"
+  by (fact lcm.left_idem)
+
+lemma lcm_right_idem: "lcm (lcm a b) b = lcm a b"
+  by (fact lcm.right_idem)
 
 lemma gcd_mult_lcm [simp]: "gcd a b * lcm a b = normalize a * normalize b"
   by (simp add: lcm_gcd normalize_mult)
@@ -359,11 +483,11 @@
     using nonzero_mult_div_cancel_right [of "lcm a b" "gcd a b"] by simp
 qed
 
-lemma lcm_1_left [simp]: "lcm 1 a = normalize a"
-  by (simp add: lcm_gcd)
-
-lemma lcm_1_right [simp]: "lcm a 1 = normalize a"
-  by (simp add: lcm_gcd)
+lemma lcm_1_left: "lcm 1 a = normalize a"
+  by (fact lcm.top_left_normalize)
+
+lemma lcm_1_right: "lcm a 1 = normalize a"
+  by (fact lcm.top_right_normalize)
 
 lemma lcm_mult_left: "lcm (c * a) (c * b) = normalize c * lcm a b"
   by (cases "c = 0")
@@ -450,23 +574,11 @@
 lemma lcm_div_unit2: "is_unit a \<Longrightarrow> lcm b (c div a) = lcm b c"
   by (erule is_unitE [of _ c]) (simp add: lcm_mult_unit2)
 
-lemma normalize_lcm_left [simp]: "lcm (normalize a) b = lcm a b"
-proof (cases "a = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have "is_unit (unit_factor a)"
-    by simp
-  moreover have "normalize a = a div unit_factor a"
-    by simp
-  ultimately show ?thesis
-    by (simp only: lcm_div_unit1)
-qed
-
-lemma normalize_lcm_right [simp]: "lcm a (normalize b) = lcm a b"
-  using normalize_lcm_left [of b a] by (simp add: ac_simps)
+lemma normalize_lcm_left: "lcm (normalize a) b = lcm a b"
+  by (fact lcm.normalize_left_idem)
+
+lemma normalize_lcm_right: "lcm a (normalize b) = lcm a b"
+  by (fact lcm.normalize_right_idem)
 
 lemma gcd_mult_unit1: "is_unit a \<Longrightarrow> gcd (b * a) c = gcd b c"
   apply (rule gcdI)
@@ -489,23 +601,11 @@
 lemma gcd_div_unit2: "is_unit a \<Longrightarrow> gcd b (c div a) = gcd b c"
   by (erule is_unitE [of _ c]) (simp add: gcd_mult_unit2)
 
-lemma normalize_gcd_left [simp]: "gcd (normalize a) b = gcd a b"
-proof (cases "a = 0")
-  case True
-  then show ?thesis
-    by simp
-next
-  case False
-  then have "is_unit (unit_factor a)"
-    by simp
-  moreover have "normalize a = a div unit_factor a"
-    by simp
-  ultimately show ?thesis
-    by (simp only: gcd_div_unit1)
-qed
-
-lemma normalize_gcd_right [simp]: "gcd a (normalize b) = gcd a b"
-  using normalize_gcd_left [of b a] by (simp add: ac_simps)
+lemma normalize_gcd_left: "gcd (normalize a) b = gcd a b"
+  by (fact gcd.normalize_left_idem)
+
+lemma normalize_gcd_right: "gcd a (normalize b) = gcd a b"
+  by (fact gcd.normalize_right_idem)
 
 lemma comp_fun_idem_gcd: "comp_fun_idem gcd"
   by standard (simp_all add: fun_eq_iff ac_simps)
@@ -942,6 +1042,21 @@
 lemma lcm_proj2_iff: "lcm m n = normalize n \<longleftrightarrow> m dvd n"
   using lcm_proj1_iff [of n m] by (simp add: ac_simps)
 
+lemma lcm_mult_distrib': "normalize c * lcm a b = lcm (c * a) (c * b)"
+  by (rule lcmI) (auto simp: normalize_mult lcm_least mult_dvd_mono lcm_mult_left [symmetric])
+
+lemma lcm_mult_distrib: "k * lcm a b = lcm (k * a) (k * b) * unit_factor k"
+proof-
+  have "normalize k * lcm a b = lcm (k * a) (k * b)"
+    by (simp add: lcm_mult_distrib')
+  then have "normalize k * lcm a b * unit_factor k = lcm (k * a) (k * b) * unit_factor k"
+    by simp
+  then have "normalize k * unit_factor k * lcm a b  = lcm (k * a) (k * b) * unit_factor k"
+    by (simp only: ac_simps)
+  then show ?thesis
+    by simp
+qed
+
 lemma dvd_productE:
   assumes "p dvd (a * b)"
   obtains x y where "p = x * y" "x dvd a" "y dvd b"
@@ -1229,26 +1344,6 @@
     by (induct A rule: finite_ne_induct) (auto simp add: lcm_eq_0_iff)
 qed
 
-lemma Gcd_finite:
-  assumes "finite A"
-  shows "Gcd A = Finite_Set.fold gcd 0 A"
-  by (induct rule: finite.induct[OF \<open>finite A\<close>])
-    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_gcd])
-
-lemma Gcd_set [code_unfold]: "Gcd (set as) = foldl gcd 0 as"
-  by (simp add: Gcd_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_gcd]
-      foldl_conv_fold gcd.commute)
-
-lemma Lcm_finite:
-  assumes "finite A"
-  shows "Lcm A = Finite_Set.fold lcm 1 A"
-  by (induct rule: finite.induct[OF \<open>finite A\<close>])
-    (simp_all add: comp_fun_idem.fold_insert_idem[OF comp_fun_idem_lcm])
-
-lemma Lcm_set [code_unfold]: "Lcm (set as) = foldl lcm 1 as"
-  by (simp add: Lcm_finite comp_fun_idem.fold_set_fold[OF comp_fun_idem_lcm]
-      foldl_conv_fold lcm.commute)
-
 lemma Gcd_image_normalize [simp]: "Gcd (normalize ` A) = Gcd A"
 proof -
   have "Gcd (normalize ` A) dvd a" if "a \<in> A" for a
@@ -1432,6 +1527,145 @@
 
 end
 
+  
+subsection \<open>An aside: GCD and LCM on finite sets for incomplete gcd rings\<close>
+
+context semiring_gcd
+begin
+
+sublocale Gcd_fin: bounded_quasi_semilattice_set gcd 0 1 normalize
+defines
+  Gcd_fin ("Gcd\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = "Gcd_fin.F :: 'a set \<Rightarrow> 'a" ..
+
+abbreviation gcd_list :: "'a list \<Rightarrow> 'a"
+  where "gcd_list xs \<equiv> Gcd\<^sub>f\<^sub>i\<^sub>n (set xs)"
+
+sublocale Lcm_fin: bounded_quasi_semilattice_set lcm 1 0 normalize
+defines
+  Lcm_fin ("Lcm\<^sub>f\<^sub>i\<^sub>n _" [900] 900) = Lcm_fin.F ..
+
+abbreviation lcm_list :: "'a list \<Rightarrow> 'a"
+  where "lcm_list xs \<equiv> Lcm\<^sub>f\<^sub>i\<^sub>n (set xs)"
+    
+lemma Gcd_fin_dvd:
+  "a \<in> A \<Longrightarrow> Gcd\<^sub>f\<^sub>i\<^sub>n A dvd a"
+  by (induct A rule: infinite_finite_induct) 
+    (auto intro: dvd_trans)
+
+lemma dvd_Lcm_fin:
+  "a \<in> A \<Longrightarrow> a dvd Lcm\<^sub>f\<^sub>i\<^sub>n A"
+  by (induct A rule: infinite_finite_induct) 
+    (auto intro: dvd_trans)
+
+lemma Gcd_fin_greatest:
+  "a dvd Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> a dvd b"
+  using that by (induct A) simp_all
+
+lemma Lcm_fin_least:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd a" if "finite A" and "\<And>b. b \<in> A \<Longrightarrow> b dvd a"
+  using that by (induct A) simp_all
+
+lemma gcd_list_greatest:
+  "a dvd gcd_list bs" if "\<And>b. b \<in> set bs \<Longrightarrow> a dvd b"
+  by (rule Gcd_fin_greatest) (simp_all add: that)
+
+lemma lcm_list_least:
+  "lcm_list bs dvd a" if "\<And>b. b \<in> set bs \<Longrightarrow> b dvd a"
+  by (rule Lcm_fin_least) (simp_all add: that)
+
+lemma dvd_Gcd_fin_iff:
+  "b dvd Gcd\<^sub>f\<^sub>i\<^sub>n A \<longleftrightarrow> (\<forall>a\<in>A. b dvd a)" if "finite A"
+  using that by (auto intro: Gcd_fin_greatest Gcd_fin_dvd dvd_trans [of b "Gcd\<^sub>f\<^sub>i\<^sub>n A"])
+
+lemma dvd_gcd_list_iff:
+  "b dvd gcd_list xs \<longleftrightarrow> (\<forall>a\<in>set xs. b dvd a)"
+  by (simp add: dvd_Gcd_fin_iff)
+  
+lemma Lcm_fin_dvd_iff:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n A dvd b  \<longleftrightarrow> (\<forall>a\<in>A. a dvd b)" if "finite A"
+  using that by (auto intro: Lcm_fin_least dvd_Lcm_fin dvd_trans [of _ "Lcm\<^sub>f\<^sub>i\<^sub>n A" b])
+
+lemma lcm_list_dvd_iff:
+  "lcm_list xs dvd b  \<longleftrightarrow> (\<forall>a\<in>set xs. a dvd b)"
+  by (simp add: Lcm_fin_dvd_iff)
+
+lemma Gcd_fin_mult:
+  "Gcd\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A" if "finite A"
+using that proof induct
+  case empty
+  then show ?case
+    by simp
+next
+  case (insert a A)
+  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))"
+    by simp
+  also have "\<dots> = gcd (b * a) (normalize b * Gcd\<^sub>f\<^sub>i\<^sub>n A)"
+    by (simp add: normalize_mult)
+  finally show ?case
+    using insert by (simp add: gcd_mult_distrib')
+qed
+
+lemma Lcm_fin_mult:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n (image (times b) A) = normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A" if "A \<noteq> {}"
+proof (cases "b = 0")
+  case True
+  moreover from that have "times 0 ` A = {0}"
+    by auto
+  ultimately show ?thesis
+    by simp
+next
+  case False
+  then have "inj (times b)"
+    by (rule inj_times)
+  show ?thesis proof (cases "finite A")
+    case False
+    moreover from \<open>inj (times b)\<close>
+    have "inj_on (times b) A"
+      by (rule inj_on_subset) simp
+    ultimately have "infinite (times b ` A)"
+      by (simp add: finite_image_iff)
+    with False show ?thesis
+      by simp
+  next
+    case True
+    then show ?thesis using that proof (induct A rule: finite_ne_induct)
+      case (singleton a)
+      then show ?case
+        by (simp add: normalize_mult)
+    next
+      case (insert a A)
+      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))"
+        by simp
+      also have "\<dots> = lcm (b * a) (normalize b * Lcm\<^sub>f\<^sub>i\<^sub>n A)"
+        by (simp add: normalize_mult)
+      finally show ?case
+        using insert by (simp add: lcm_mult_distrib')
+    qed
+  qed
+qed
+
+end
+
+context semiring_Gcd
+begin
+
+lemma Gcd_fin_eq_Gcd [simp]:
+  "Gcd\<^sub>f\<^sub>i\<^sub>n A = Gcd A" if "finite A" for A :: "'a set"
+  using that by induct simp_all
+
+lemma Gcd_set_eq_fold [code_unfold]:
+  "Gcd (set xs) = fold gcd xs 0"
+  by (simp add: Gcd_fin.set_eq_fold [symmetric])
+
+lemma Lcm_fin_eq_Lcm [simp]:
+  "Lcm\<^sub>f\<^sub>i\<^sub>n A = Lcm A" if "finite A" for A :: "'a set"
+  using that by induct simp_all
+
+lemma Lcm_set_eq_fold [code_unfold]:
+  "Lcm (set xs) = fold lcm xs 1"
+  by (simp add: Lcm_fin.set_eq_fold [symmetric])
+
+end
 
 subsection \<open>GCD and LCM on @{typ nat} and @{typ int}\<close>
 
@@ -2514,11 +2748,10 @@
 
 text \<open>Some code equations\<close>
 
-lemmas Lcm_set_nat [code, code_unfold] = Lcm_set[where ?'a = nat]
-lemmas Gcd_set_nat [code] = Gcd_set[where ?'a = nat]
-lemmas Lcm_set_int [code, code_unfold] = Lcm_set[where ?'a = int]
-lemmas Gcd_set_int [code] = Gcd_set[where ?'a = int]
-
+lemmas Gcd_nat_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = nat]
+lemmas Lcm_nat_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = nat]
+lemmas Gcd_int_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = int]
+lemmas Lcm_int_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = int]
 
 text \<open>Fact aliases.\<close>
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Int.thy
--- a/src/HOL/Int.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Int.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -357,7 +357,6 @@
   then show ?thesis ..
 qed
 
-
 end
 
 text \<open>Comparisons involving @{term of_int}.\<close>
@@ -848,6 +847,13 @@
     by simp
 qed (auto elim!: Nats_cases)
 
+lemma (in idom_divide) of_int_divide_in_Ints: 
+  "of_int a div of_int b \<in> \<int>" if "b dvd a"
+proof -
+  from that obtain c where "a = b * c" ..
+  then show ?thesis
+    by (cases "of_int b = 0") simp_all
+qed
 
 text \<open>The premise involving @{term Ints} prevents @{term "a = 1/2"}.\<close>
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Library/Polynomial.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -12,21 +12,6 @@
   "~~/src/HOL/Library/Infinite_Set"
 begin
 
-subsection \<open>Misc\<close>
-
-lemma quotient_of_denom_pos': "snd (quotient_of x) > 0"
-  using quotient_of_denom_pos [OF surjective_pairing] .
-  
-lemma of_int_divide_in_Ints: 
-  "b dvd a \<Longrightarrow> of_int a div of_int b \<in> (\<int> :: 'a :: idom_divide set)"
-proof (cases "of_int b = (0 :: 'a)")
-  case False
-  assume "b dvd a"
-  then obtain c where "a = b * c" ..
-  with \<open>of_int b \<noteq> (0::'a)\<close> show ?thesis by simp
-qed auto
-
-  
 subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
 
 definition cCons :: "'a::zero \<Rightarrow> 'a list \<Rightarrow> 'a list"  (infixr "##" 65)
@@ -3423,59 +3408,104 @@
       by force
 qed
 
-instantiation poly :: ("{normalization_semidom, idom_divide}") normalization_semidom
+instantiation poly :: ("{semidom_divide_unit_factor, idom_divide}") normalization_semidom
 begin
 
 definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "unit_factor_poly p = monom (unit_factor (lead_coeff p)) 0"
+  where "unit_factor_poly p = [:unit_factor (lead_coeff p):]"
 
 definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
-  where "normalize_poly p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+  where "normalize p = p div [:unit_factor (lead_coeff p):]"
 
 instance proof
   fix p :: "'a poly"
   show "unit_factor p * normalize p = p"
-    by (cases "p = 0")
-       (simp_all add: unit_factor_poly_def normalize_poly_def monom_0 
-          smult_conv_map_poly map_poly_map_poly o_def)
+  proof (cases "p = 0")
+    case True
+    then show ?thesis
+      by (simp add: unit_factor_poly_def normalize_poly_def)
+  next
+    case False
+    then have "lead_coeff p \<noteq> 0"
+      by simp
+    then have *: "unit_factor (lead_coeff p) \<noteq> 0"
+      using unit_factor_is_unit [of "lead_coeff p"] by auto
+    then have "unit_factor (lead_coeff p) dvd 1"
+      by (auto intro: unit_factor_is_unit)
+    then have **: "unit_factor (lead_coeff p) dvd c" for c
+      by (rule dvd_trans) simp
+    have ***: "unit_factor (lead_coeff p) * (c div unit_factor (lead_coeff p)) = c" for c
+    proof -
+      from ** obtain b where "c = unit_factor (lead_coeff p) * b" ..
+      then show ?thesis
+        using False * by simp
+    qed
+    have "p div [:unit_factor (lead_coeff p):] =
+      map_poly (\<lambda>c. c div unit_factor (lead_coeff p)) p"
+      by (simp add: const_poly_dvd_iff div_const_poly_conv_map_poly **)
+    then show ?thesis
+      by (simp add: normalize_poly_def unit_factor_poly_def
+        smult_conv_map_poly map_poly_map_poly o_def ***)
+  qed
 next
   fix p :: "'a poly"
   assume "is_unit p"
-  then obtain c where p: "p = [:c:]" "is_unit c"
+  then obtain c where p: "p = [:c:]" "c dvd 1"
     by (auto simp: is_unit_poly_iff)
-  thus "normalize p = 1"
-    by (simp add: normalize_poly_def map_poly_pCons is_unit_normalize one_poly_def)
+  then show "unit_factor p = p"
+    by (simp add: unit_factor_poly_def monom_0 is_unit_unit_factor)
 next
   fix p :: "'a poly" assume "p \<noteq> 0"
-  thus "is_unit (unit_factor p)"
-    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff)
+  then show "is_unit (unit_factor p)"
+    by (simp add: unit_factor_poly_def monom_0 is_unit_poly_iff unit_factor_is_unit)
 qed (simp_all add: normalize_poly_def unit_factor_poly_def monom_0 lead_coeff_mult unit_factor_mult)
 
 end
 
-lemma normalize_poly_eq_div:
-  "normalize p = p div [:unit_factor (lead_coeff p):]"
-proof (cases "p = 0")
-  case False
-  thus ?thesis
-    by (subst div_const_poly_conv_map_poly)
-       (auto simp: normalize_poly_def const_poly_dvd_iff)
-qed (auto simp: normalize_poly_def)
+lemma normalize_poly_eq_map_poly:
+  "normalize p = map_poly (\<lambda>x. x div unit_factor (lead_coeff p)) p"
+proof -
+  have "[:unit_factor (lead_coeff p):] dvd p"
+    by (metis unit_factor_poly_def unit_factor_self)
+  then show ?thesis
+    by (simp add: normalize_poly_def div_const_poly_conv_map_poly)
+qed
+
+lemma coeff_normalize [simp]:
+  "coeff (normalize p) n = coeff p n div unit_factor (lead_coeff p)"
+  by (simp add: normalize_poly_eq_map_poly coeff_map_poly)
+
+class field_unit_factor = field + unit_factor +
+  assumes unit_factor_field [simp]: "unit_factor = id"
+begin
+
+subclass semidom_divide_unit_factor
+proof
+  fix a
+  assume "a \<noteq> 0"
+  then have "1 = a * inverse a"
+    by simp
+  then have "a dvd 1" ..
+  then show "unit_factor a dvd 1"
+    by simp
+qed simp_all
+
+end
 
 lemma unit_factor_pCons:
-  "unit_factor (pCons a p) = (if p = 0 then monom (unit_factor a) 0 else unit_factor p)"
+  "unit_factor (pCons a p) = (if p = 0 then [:unit_factor a:] else unit_factor p)"
   by (simp add: unit_factor_poly_def)
 
 lemma normalize_monom [simp]:
   "normalize (monom a n) = monom (normalize a) n"
-  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_def degree_monom_eq)
+  by (cases "a = 0") (simp_all add: map_poly_monom normalize_poly_eq_map_poly degree_monom_eq)
 
 lemma unit_factor_monom [simp]:
-  "unit_factor (monom a n) = monom (unit_factor a) 0"
+  "unit_factor (monom a n) = [:unit_factor a:]"
   by (cases "a = 0") (simp_all add: unit_factor_poly_def degree_monom_eq)
 
 lemma normalize_const_poly: "normalize [:c:] = [:normalize c:]"
-  by (simp add: normalize_poly_def map_poly_pCons)
+  by (simp add: normalize_poly_eq_map_poly map_poly_pCons)
 
 lemma normalize_smult: "normalize (smult c p) = smult (normalize c) (normalize p)"
 proof -
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Library/Polynomial_Factorial.thy
--- a/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Library/Polynomial_Factorial.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -520,8 +520,8 @@
        (simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
 next
   fix p :: "'a poly" assume "is_unit p"
-  thus "normalize_field_poly p = 1"
-    by (elim is_unit_polyE) (auto simp: normalize_field_poly_def monom_0 one_poly_def field_simps)
+  then show "unit_factor_field_poly p = p"
+    by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
 next
   fix p :: "'a poly" assume "p \<noteq> 0"
   thus "is_unit (unit_factor_field_poly p)"
@@ -566,7 +566,7 @@
 proof -
   have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
-             normalize_field_poly unit_factor_field_poly" ..
+             unit_factor_field_poly normalize_field_poly" ..
   from field_poly.in_prime_factors_imp_prime [of p x] assms
     show ?thesis unfolding prime_elem_def dvd_field_poly
       comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
@@ -981,12 +981,9 @@
   shows "lcm p q = normalize (p * q) div gcd p q"
   by (fact lcm_gcd)
 
-declare Gcd_set
-  [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
-declare Lcm_set
-  [where ?'a = "'a :: factorial_ring_gcd poly", code]
-
+lemmas Gcd_poly_set_eq_fold [code] = Gcd_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+lemmas Lcm_poly_set_eq_fold [code] = Lcm_set_eq_fold [where ?'a = "'a :: factorial_ring_gcd poly"]
+  
 text \<open>Example:
   @{lemma "Lcm {[:1, 2, 3:], [:2, 3, 4:]} = [:[:2:], [:7:], [:16:], [:17:], [:12 :: int:]:]" by eval}
 \<close>
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Nat.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -170,6 +170,28 @@
 
 text \<open>Injectiveness and distinctness lemmas\<close>
 
+lemma (in semidom_divide) inj_times:
+  "inj (times a)" if "a \<noteq> 0"
+proof (rule injI)
+  fix b c
+  assume "a * b = a * c"
+  then have "a * b div a = a * c div a"
+    by (simp only:)
+  with that show "b = c"
+    by simp
+qed
+
+lemma (in cancel_ab_semigroup_add) inj_plus:
+  "inj (plus a)"
+proof (rule injI)
+  fix b c
+  assume "a + b = a + c"
+  then have "a + b - a = a + c - a"
+    by (simp only:)
+  then show "b = c"
+    by simp
+qed
+
 lemma inj_Suc[simp]: "inj_on Suc N"
   by (simp add: inj_on_def)
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -71,7 +71,7 @@
 
 lemma semiring_gcd:
   "class.semiring_gcd one zero times gcd lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof
   show "gcd a b dvd a"
     and "gcd a b dvd b" for a b
@@ -97,12 +97,12 @@
 qed
 
 interpretation semiring_gcd one zero times gcd lcm
-  divide plus minus normalize unit_factor
+  divide plus minus unit_factor normalize
   by (fact semiring_gcd)
   
 lemma semiring_Gcd:
   "class.semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor"
+    divide plus minus unit_factor normalize"
 proof -
   show ?thesis
   proof
@@ -180,13 +180,13 @@
 qed
 
 interpretation semiring_Gcd one zero times gcd lcm Gcd Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
   by (fact semiring_Gcd)
 
 subclass factorial_semiring
 proof -
   show "class.factorial_semiring divide plus minus zero times one
-     normalize unit_factor"
+     unit_factor normalize"
   proof (standard, rule factorial_semiring_altI_aux) -- \<open>FIXME rule\<close>
     fix x assume "x \<noteq> 0"
     thus "finite {p. p dvd x \<and> normalize p = p}"
@@ -254,12 +254,12 @@
 qed
 
 lemma Gcd_eucl_set [code]:
-  "Gcd (set xs) = foldl gcd 0 xs"
-  by (fact local.Gcd_set)
+  "Gcd (set xs) = fold gcd xs 0"
+  by (fact Gcd_set_eq_fold)
 
 lemma Lcm_eucl_set [code]:
-  "Lcm (set xs) = foldl lcm 1 xs"
-  by (fact local.Lcm_set)
+  "Lcm (set xs) = fold lcm xs 1"
+  by (fact Lcm_set_eq_fold)
  
 end
 
@@ -406,7 +406,7 @@
   interpret semiring_Gcd 1 0 times
     Euclidean_Algorithm.gcd Euclidean_Algorithm.lcm
     Euclidean_Algorithm.Gcd Euclidean_Algorithm.Lcm
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "Euclidean_Algorithm.gcd = (gcd :: 'a \<Rightarrow> _)"
@@ -558,7 +558,7 @@
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: nat \<Rightarrow> _) = gcd"
@@ -590,7 +590,7 @@
   interpret semiring_Gcd 1 0 times
     "Euclidean_Algorithm.gcd" "Euclidean_Algorithm.lcm"
     "Euclidean_Algorithm.Gcd" "Euclidean_Algorithm.Lcm"
-    divide plus minus normalize unit_factor
+    divide plus minus unit_factor normalize
     rewrites "dvd.dvd op * = Rings.dvd"
     by (fact semiring_Gcd) (simp add: dvd.dvd_def dvd_def fun_eq_iff)
   show [simp]: "(Euclidean_Algorithm.gcd :: int \<Rightarrow> _) = gcd"
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Rat.thy
--- a/src/HOL/Rat.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Rat.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -401,6 +401,9 @@
 lemma quotient_of_denom_pos: "quotient_of r = (p, q) \<Longrightarrow> q > 0"
   by (cases r) (simp add: quotient_of_Fract normalize_denom_pos)
 
+lemma quotient_of_denom_pos': "snd (quotient_of r) > 0"
+  using quotient_of_denom_pos [of r] by (simp add: prod_eq_iff)
+    
 lemma quotient_of_coprime: "quotient_of r = (p, q) \<Longrightarrow> coprime p q"
   by (cases r) (simp add: quotient_of_Fract normalize_coprime)
 
diff -r f3504bc69ea3 -r 9178214b3588 src/HOL/Rings.thy
--- a/src/HOL/Rings.thy	Mon Jan 09 19:34:02 2017 +0100
+++ b/src/HOL/Rings.thy	Mon Jan 09 19:34:16 2017 +0100
@@ -1156,15 +1156,20 @@
 
 end
 
-class normalization_semidom = algebraic_semidom +
+class unit_factor =
+  fixes unit_factor :: "'a \<Rightarrow> 'a"
+
+class semidom_divide_unit_factor = semidom_divide + unit_factor +
+  assumes unit_factor_0 [simp]: "unit_factor 0 = 0"
+    and is_unit_unit_factor: "a dvd 1 \<Longrightarrow> unit_factor a = a"
+    and unit_factor_is_unit: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd 1"
+    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
+  -- \<open>This fine-grained hierarchy will later on allow lean normalization of polynomials\<close>
+  
+class normalization_semidom = algebraic_semidom + semidom_divide_unit_factor +
   fixes normalize :: "'a \<Rightarrow> 'a"
-    and unit_factor :: "'a \<Rightarrow> 'a"
   assumes unit_factor_mult_normalize [simp]: "unit_factor a * normalize a = a"
     and normalize_0 [simp]: "normalize 0 = 0"
-    and unit_factor_0 [simp]: "unit_factor 0 = 0"
-    and is_unit_normalize: "is_unit a  \<Longrightarrow> normalize a = 1"
-    and unit_factor_is_unit [iff]: "a \<noteq> 0 \<Longrightarrow> is_unit (unit_factor a)"
-    and unit_factor_mult: "unit_factor (a * b) = unit_factor a * unit_factor b"
 begin
 
 text \<open>
@@ -1176,6 +1181,8 @@
   think about equality of normalized values rather than associated elements.
 \<close>
 
+declare unit_factor_is_unit [iff]
+  
 lemma unit_factor_dvd [simp]: "a \<noteq> 0 \<Longrightarrow> unit_factor a dvd b"
   by (rule unit_imp_dvd) simp
 
@@ -1207,13 +1214,45 @@
   then show ?lhs by simp
 qed
 
-lemma is_unit_unit_factor:
+lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  then have "unit_factor a \<noteq> 0"
+    by simp
+  with nonzero_mult_div_cancel_left
+  have "unit_factor a * normalize a div unit_factor a = normalize a"
+    by blast
+  then show ?thesis by simp
+qed
+
+lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
+proof (cases "a = 0")
+  case True
+  then show ?thesis by simp
+next
+  case False
+  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
+    by simp
+  also have "\<dots> = 1 div unit_factor a"
+    using False by (subst is_unit_div_mult_cancel_right) simp_all
+  finally show ?thesis .
+qed
+
+lemma is_unit_normalize:
   assumes "is_unit a"
-  shows "unit_factor a = a"
+  shows "normalize a = 1"
 proof -
-  from assms have "normalize a = 1" by (rule is_unit_normalize)
-  moreover from unit_factor_mult_normalize have "unit_factor a * normalize a = a" .
-  ultimately show ?thesis by simp
+  from assms have "unit_factor a = a"
+    by (rule is_unit_unit_factor)
+  moreover from assms have "a \<noteq> 0"
+    by auto
+  moreover have "normalize a = a div unit_factor a"
+    by simp
+  ultimately show ?thesis
+    by simp
 qed
 
 lemma unit_factor_1 [simp]: "unit_factor 1 = 1"
@@ -1251,32 +1290,6 @@
   then show ?thesis by simp
 qed
 
-lemma div_unit_factor [simp]: "a div unit_factor a = normalize a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  then have "unit_factor a \<noteq> 0" by simp
-  with nonzero_mult_div_cancel_left
-  have "unit_factor a * normalize a div unit_factor a = normalize a"
-    by blast
-  then show ?thesis by simp
-qed
-
-lemma normalize_div [simp]: "normalize a div a = 1 div unit_factor a"
-proof (cases "a = 0")
-  case True
-  then show ?thesis by simp
-next
-  case False
-  have "normalize a div a = normalize a div (unit_factor a * normalize a)"
-    by simp
-  also have "\<dots> = 1 div unit_factor a"
-    using False by (subst is_unit_div_mult_cancel_right) simp_all
-  finally show ?thesis .
-qed
-
 lemma mult_one_div_unit_factor [simp]: "a * (1 div unit_factor b) = a div unit_factor b"
   by (cases "b = 0") simp_all
 
@@ -1823,6 +1836,14 @@
 proposition abs_eq_iff: "\<bar>x\<bar> = \<bar>y\<bar> \<longleftrightarrow> x = y \<or> x = -y"
   by (auto simp add: abs_if split: if_split_asm)
 
+lemma abs_eq_iff':
+  "\<bar>a\<bar> = b \<longleftrightarrow> b \<ge> 0 \<and> (a = b \<or> a = - b)"
+  by (cases "a \<ge> 0") auto
+
+lemma eq_abs_iff':
+  "a = \<bar>b\<bar> \<longleftrightarrow> a \<ge> 0 \<and> (b = a \<or> b = - a)"
+  using abs_eq_iff' [of b a] by auto
+
 lemma sum_squares_ge_zero: "0 \<le> x * x + y * y"
   by (intro add_nonneg_nonneg zero_le_square)