# HG changeset patch
# User eberlm
# Date 1456495247 -3600
# Node ID bd650e3a210f62a1041e3be7fc1345db3643a5c8
# Parent  d0936b500bf5b8fa81f6eebf403be3cc1c2f326b# Parent  28d2c75dd180d58818fdf3eef36d47b052357f2b
Merged

diff -r 28d2c75dd180 -r bd650e3a210f src/HOL/Codegenerator_Test/Candidates.thy
--- a/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 26 11:53:45 2016 +0100
+++ b/src/HOL/Codegenerator_Test/Candidates.thy	Fri Feb 26 15:00:47 2016 +0100
@@ -8,7 +8,7 @@
   Complex_Main
   "~~/src/HOL/Library/Library"
   "~~/src/HOL/Library/Sublist_Order"
-  "~~/src/HOL/Library/Polynomial_GCD_euclidean"
+  "~~/src/HOL/Number_Theory/Euclidean_Algorithm"
   "~~/src/HOL/Data_Structures/Tree_Map"
   "~~/src/HOL/Data_Structures/Tree_Set"
   "~~/src/HOL/Number_Theory/Eratosthenes"
diff -r 28d2c75dd180 -r bd650e3a210f src/HOL/Library/Formal_Power_Series.thy
--- a/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 26 11:53:45 2016 +0100
+++ b/src/HOL/Library/Formal_Power_Series.thy	Fri Feb 26 15:00:47 2016 +0100
@@ -1361,7 +1361,7 @@
 begin
 
 definition fps_euclidean_size_def:
-  "euclidean_size f = (if f = 0 then 0 else Suc (subdegree f))"
+  "euclidean_size f = (if f = 0 then 0 else 2 ^ subdegree f)"
 
 instance proof
   fix f g :: "'a fps" assume [simp]: "g \<noteq> 0"
@@ -1372,7 +1372,7 @@
     apply (rule disjE[OF le_less_linear[of "subdegree g" "subdegree f"]])
     apply (simp_all add: fps_mod_eq_zero fps_euclidean_size_def subdegree_mod)
     done
-qed
+qed (simp_all add: fps_euclidean_size_def)
 
 end
 
@@ -1382,7 +1382,7 @@
 definition fps_lcm_def: "(lcm :: 'a fps \<Rightarrow> _) = lcm_eucl"
 definition fps_Gcd_def: "(Gcd :: 'a fps set \<Rightarrow> _) = Gcd_eucl"
 definition fps_Lcm_def: "(Lcm :: 'a fps set \<Rightarrow> _) = Lcm_eucl"
-instance by intro_classes (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
+instance by standard (simp_all add: fps_gcd_def fps_lcm_def fps_Gcd_def fps_Lcm_def)
 end
 
 lemma fps_gcd:
@@ -1473,11 +1473,12 @@
     from unbounded obtain f where f: "f \<in> A" "subdegree (Lcm A) < subdegree f"
       unfolding bdd_above_def by (auto simp: not_le)
     moreover from this and \<open>Lcm A \<noteq> 0\<close> have "subdegree f \<le> subdegree (Lcm A)"
-      by (intro dvd_imp_subdegree_le) simp_all
+      by (intro dvd_imp_subdegree_le dvd_Lcm) simp_all
     ultimately show False by simp
   qed
   with unbounded show ?thesis by simp
-qed (simp_all add: fps_Lcm)
+qed (simp_all add: fps_Lcm Lcm_eq_0_I)
+
 
 
 subsection \<open>Formal Derivatives, and the MacLaurin theorem around 0\<close>
@@ -4254,6 +4255,7 @@
 
 subsection \<open>Hypergeometric series\<close>
 
+(* TODO: Rename this *)
 definition "F as bs (c::'a::{field_char_0,field}) =
   Abs_fps (\<lambda>n. (foldl (\<lambda>r a. r* pochhammer a n) 1 as * c^n) /
     (foldl (\<lambda>r b. r * pochhammer b n) 1 bs * of_nat (fact n)))"
diff -r 28d2c75dd180 -r bd650e3a210f src/HOL/Library/Polynomial.thy
--- a/src/HOL/Library/Polynomial.thy	Fri Feb 26 11:53:45 2016 +0100
+++ b/src/HOL/Library/Polynomial.thy	Fri Feb 26 15:00:47 2016 +0100
@@ -258,6 +258,11 @@
 qed
 
 
+subsection \<open>Quickcheck generator for polynomials\<close>
+
+quickcheck_generator poly constructors: "0 :: _ poly", pCons
+
+
 subsection \<open>List-style syntax for polynomials\<close>
 
 syntax
diff -r 28d2c75dd180 -r bd650e3a210f src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 11:53:45 2016 +0100
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Fri Feb 26 15:00:47 2016 +0100
@@ -19,6 +19,7 @@
 \<close> 
 class euclidean_semiring = semiring_div + normalization_semidom + 
   fixes euclidean_size :: "'a \<Rightarrow> nat"
+  assumes size_0 [simp]: "euclidean_size 0 = 0"
   assumes mod_size_less: 
     "b \<noteq> 0 \<Longrightarrow> euclidean_size (a mod b) < euclidean_size b"
   assumes size_mult_mono:
@@ -110,6 +111,122 @@
   "b \<noteq> 0 \<Longrightarrow> gcd_eucl a b = gcd_eucl b (a mod b)"
   by (simp add: gcd_eucl.simps [of a b] gcd_eucl.simps [of b 0])
 
+lemma gcd_eucl_dvd1 [iff]: "gcd_eucl a b dvd a"
+  and gcd_eucl_dvd2 [iff]: "gcd_eucl a b dvd b"
+  by (induct a b rule: gcd_eucl_induct)
+     (simp_all add: gcd_eucl_0 gcd_eucl_non_0 dvd_mod_iff)
+
+lemma normalize_gcd_eucl [simp]:
+  "normalize (gcd_eucl a b) = gcd_eucl a b"
+  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_eucl_0 gcd_eucl_non_0)
+     
+lemma gcd_eucl_greatest:
+  fixes k a b :: 'a
+  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd_eucl a b"
+proof (induct a b rule: gcd_eucl_induct)
+  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_eucl_0)
+next
+  case (mod a b)
+  then show ?case
+    by (simp add: gcd_eucl_non_0 dvd_mod_iff)
+qed
+
+lemma eq_gcd_euclI:
+  fixes gcd :: "'a \<Rightarrow> 'a \<Rightarrow> 'a"
+  assumes "\<And>a b. gcd a b dvd a" "\<And>a b. gcd a b dvd b" "\<And>a b. normalize (gcd a b) = gcd a b"
+          "\<And>a b k. k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
+  shows   "gcd = gcd_eucl"
+  by (intro ext, rule associated_eqI) (simp_all add: gcd_eucl_greatest assms)
+
+lemma gcd_eucl_zero [simp]:
+  "gcd_eucl a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
+  by (metis dvd_0_left dvd_refl gcd_eucl_dvd1 gcd_eucl_dvd2 gcd_eucl_greatest)+
+
+  
+lemma dvd_Lcm_eucl [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm_eucl A"
+  and Lcm_eucl_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm_eucl A dvd b"
+  and unit_factor_Lcm_eucl [simp]: 
+          "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)"
+proof -
+  have "(\<forall>a\<in>A. a dvd Lcm_eucl A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm_eucl A dvd l') \<and>
+    unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" (is ?thesis)
+  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
+    case False
+    hence "Lcm_eucl A = 0" by (auto simp: Lcm_eucl_def)
+    with False show ?thesis by auto
+  next
+    case True
+    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
+    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
+      apply (subst n_def)
+      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
+      apply (rule exI[of _ l\<^sub>0])
+      apply (simp add: l\<^sub>0_props)
+      done
+    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
+      unfolding l_def by simp_all
+    {
+      fix l' assume "\<forall>a\<in>A. a dvd l'"
+      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd_eucl l l'" by (auto intro: gcd_eucl_greatest)
+      moreover from \<open>l \<noteq> 0\<close> have "gcd_eucl l l' \<noteq> 0" by simp
+      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> 
+                          euclidean_size b = euclidean_size (gcd_eucl l l')"
+        by (intro exI[of _ "gcd_eucl l l'"], auto)
+      hence "euclidean_size (gcd_eucl l l') \<ge> n" by (subst n_def) (rule Least_le)
+      moreover have "euclidean_size (gcd_eucl l l') \<le> n"
+      proof -
+        have "gcd_eucl l l' dvd l" by simp
+        then obtain a where "l = gcd_eucl l l' * a" unfolding dvd_def by blast
+        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
+        hence "euclidean_size (gcd_eucl l l') \<le> euclidean_size (gcd_eucl l l' * a)"
+          by (rule size_mult_mono)
+        also have "gcd_eucl l l' * a = l" using \<open>l = gcd_eucl l l' * a\<close> ..
+        also note \<open>euclidean_size l = n\<close>
+        finally show "euclidean_size (gcd_eucl l l') \<le> n" .
+      qed
+      ultimately have *: "euclidean_size l = euclidean_size (gcd_eucl l l')" 
+        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
+      from \<open>l \<noteq> 0\<close> have "l dvd gcd_eucl l l'"
+        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
+      hence "l dvd l'" by (rule dvd_trans[OF _ gcd_eucl_dvd2])
+    }
+
+    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and unit_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
+      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
+        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
+        unit_factor (normalize l) = 
+        (if normalize l = 0 then 0 else 1)"
+      by (auto simp: unit_simps)
+    also from True have "normalize l = Lcm_eucl A"
+      by (simp add: Lcm_eucl_def Let_def n_def l_def)
+    finally show ?thesis .
+  qed
+  note A = this
+
+  {fix a assume "a \<in> A" then show "a dvd Lcm_eucl A" using A by blast}
+  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm_eucl A dvd b" using A by blast}
+  from A show "unit_factor (Lcm_eucl A) = (if Lcm_eucl A = 0 then 0 else 1)" by blast
+qed
+  
+lemma normalize_Lcm_eucl [simp]:
+  "normalize (Lcm_eucl A) = Lcm_eucl A"
+proof (cases "Lcm_eucl A = 0")
+  case True then show ?thesis by simp
+next
+  case False
+  have "unit_factor (Lcm_eucl A) * normalize (Lcm_eucl A) = Lcm_eucl A"
+    by (fact unit_factor_mult_normalize)
+  with False show ?thesis by simp
+qed
+
+lemma eq_Lcm_euclI:
+  fixes lcm :: "'a set \<Rightarrow> 'a"
+  assumes "\<And>A a. a \<in> A \<Longrightarrow> a dvd lcm A" and "\<And>A c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> lcm A dvd c"
+          "\<And>A. normalize (lcm A) = lcm A" shows "lcm = Lcm_eucl"
+  by (intro ext, rule associated_eqI) (auto simp: assms intro: Lcm_eucl_least)  
+
 end
 
 class euclidean_ring = euclidean_semiring + idom
@@ -184,86 +301,28 @@
   assumes Gcd_Gcd_eucl: "Gcd = Gcd_eucl" and Lcm_Lcm_eucl: "Lcm = Lcm_eucl"
 begin
 
-lemma gcd_0_left:
-  "gcd 0 a = normalize a"
-  unfolding gcd_gcd_eucl by (fact gcd_eucl_0_left)
+subclass semiring_gcd
+  by standard (simp_all add: gcd_gcd_eucl gcd_eucl_greatest lcm_lcm_eucl lcm_eucl_def)
 
-lemma gcd_0:
-  "gcd a 0 = normalize a"
-  unfolding gcd_gcd_eucl by (fact gcd_eucl_0)
+subclass semiring_Gcd
+  by standard (auto simp: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def intro: Lcm_eucl_least)
+  
 
 lemma gcd_non_0:
   "b \<noteq> 0 \<Longrightarrow> gcd a b = gcd b (a mod b)"
   unfolding gcd_gcd_eucl by (fact gcd_eucl_non_0)
 
-lemma gcd_dvd1 [iff]: "gcd a b dvd a"
-  and gcd_dvd2 [iff]: "gcd a b dvd b"
-  by (induct a b rule: gcd_eucl_induct)
-    (simp_all add: gcd_0 gcd_non_0 dvd_mod_iff)
-    
-lemma dvd_gcd_D1: "k dvd gcd m n \<Longrightarrow> k dvd m"
-  by (rule dvd_trans, assumption, rule gcd_dvd1)
-
-lemma dvd_gcd_D2: "k dvd gcd m n \<Longrightarrow> k dvd n"
-  by (rule dvd_trans, assumption, rule gcd_dvd2)
-
-lemma gcd_greatest:
-  fixes k a b :: 'a
-  shows "k dvd a \<Longrightarrow> k dvd b \<Longrightarrow> k dvd gcd a b"
-proof (induct a b rule: gcd_eucl_induct)
-  case (zero a) from zero(1) show ?case by (rule dvd_trans) (simp add: gcd_0)
-next
-  case (mod a b)
-  then show ?case
-    by (simp add: gcd_non_0 dvd_mod_iff)
-qed
-
-lemma dvd_gcd_iff:
-  "k dvd gcd a b \<longleftrightarrow> k dvd a \<and> k dvd b"
-  by (blast intro!: gcd_greatest intro: dvd_trans)
+lemmas gcd_0 = gcd_0_right
+lemmas dvd_gcd_iff = gcd_greatest_iff
 
 lemmas gcd_greatest_iff = dvd_gcd_iff
 
-lemma gcd_zero [simp]:
-  "gcd a b = 0 \<longleftrightarrow> a = 0 \<and> b = 0"
-  by (metis dvd_0_left dvd_refl gcd_dvd1 gcd_dvd2 gcd_greatest)+
-
-lemma normalize_gcd [simp]:
-  "normalize (gcd a b) = gcd a b"
-  by (induct a b rule: gcd_eucl_induct) (simp_all add: gcd_0 gcd_non_0)
-
 lemma gcdI:
   assumes "c dvd a" and "c dvd b" and greatest: "\<And>d. d dvd a \<Longrightarrow> d dvd b \<Longrightarrow> d dvd c"
     and "normalize c = c"
   shows "c = gcd a b"
   by (rule associated_eqI) (auto simp: assms intro: gcd_greatest)
 
-sublocale gcd: abel_semigroup gcd
-proof
-  fix a b c 
-  show "gcd (gcd a b) c = gcd a (gcd b c)"
-  proof (rule gcdI)
-    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd a" by simp_all
-    then show "gcd (gcd a b) c dvd a" by (rule dvd_trans)
-    have "gcd (gcd a b) c dvd gcd a b" "gcd a b dvd b" by simp_all
-    hence "gcd (gcd a b) c dvd b" by (rule dvd_trans)
-    moreover have "gcd (gcd a b) c dvd c" by simp
-    ultimately show "gcd (gcd a b) c dvd gcd b c"
-      by (rule gcd_greatest)
-    show "normalize (gcd (gcd a b) c) = gcd (gcd a b) c"
-      by auto
-    fix l assume "l dvd a" and "l dvd gcd b c"
-    with dvd_trans [OF _ gcd_dvd1] and dvd_trans [OF _ gcd_dvd2]
-      have "l dvd b" and "l dvd c" by blast+
-    with \<open>l dvd a\<close> show "l dvd gcd (gcd a b) c"
-      by (intro gcd_greatest)
-  qed
-next
-  fix a b
-  show "gcd a b = gcd b a"
-    by (rule gcdI) (simp_all add: gcd_greatest)
-qed
-
 lemma gcd_unique: "d dvd a \<and> d dvd b \<and> 
     normalize d = d \<and>
     (\<forall>e. e dvd a \<and> e dvd b \<longrightarrow> e dvd d) \<longleftrightarrow> d = gcd a b"
@@ -272,15 +331,9 @@
 lemma gcd_dvd_prod: "gcd a b dvd k * b"
   using mult_dvd_mono [of 1] by auto
 
-lemma gcd_1_left [simp]: "gcd 1 a = 1"
-  by (rule sym, rule gcdI, simp_all)
-
-lemma gcd_1 [simp]: "gcd a 1 = 1"
-  by (rule sym, rule gcdI, simp_all)
-
 lemma gcd_proj2_if_dvd: 
   "b dvd a \<Longrightarrow> gcd a b = normalize b"
-  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0 gcd_0)
+  by (cases "b = 0", simp_all add: dvd_eq_mod_eq_0 gcd_non_0)
 
 lemma gcd_proj1_if_dvd: 
   "a dvd b \<Longrightarrow> gcd a b = normalize a"
@@ -315,17 +368,17 @@
 lemma gcd_mult_distrib': 
   "normalize c * gcd a b = gcd (c * a) (c * b)"
 proof (cases "c = 0")
-  case True then show ?thesis by (simp_all add: gcd_0)
+  case True then show ?thesis by simp_all
 next
   case False then have [simp]: "is_unit (unit_factor c)" by simp
   show ?thesis
   proof (induct a b rule: gcd_eucl_induct)
     case (zero a) show ?case
     proof (cases "a = 0")
-      case True then show ?thesis by (simp add: gcd_0)
+      case True then show ?thesis by simp
     next
       case False
-      then show ?thesis by (simp add: gcd_0 normalize_mult)
+      then show ?thesis by (simp add: normalize_mult)
     qed
     case (mod a b)
     then show ?case by (simp add: mult_mod_right gcd.commute)
@@ -363,10 +416,11 @@
   shows "euclidean_size (gcd a b) < euclidean_size a"
 proof (rule ccontr)
   assume "\<not>euclidean_size (gcd a b) < euclidean_size a"
-  with \<open>a \<noteq> 0\<close> have "euclidean_size (gcd a b) = euclidean_size a"
+  with \<open>a \<noteq> 0\<close> have A: "euclidean_size (gcd a b) = euclidean_size a"
     by (intro le_antisym, simp_all)
-  with assms have "a dvd gcd a b" by (auto intro: dvd_euclidean_size_eq_imp_dvd)
-  hence "a dvd b" using dvd_gcd_D2 by blast
+  have "a dvd gcd a b"
+    by (rule dvd_euclidean_size_eq_imp_dvd) (simp_all add: assms A)
+  hence "a dvd b" using dvd_gcdD2 by blast
   with \<open>\<not>a dvd b\<close> show False by contradiction
 qed
 
@@ -379,7 +433,6 @@
   apply (rule gcdI)
   apply simp_all
   apply (rule dvd_trans, rule gcd_dvd1, simp add: unit_simps)
-  apply (rule gcd_greatest, simp add: unit_simps, assumption)
   done
 
 lemma gcd_mult_unit2: "is_unit a \<Longrightarrow> gcd b (c * a) = gcd b c"
@@ -410,7 +463,7 @@
   using normalize_gcd_left [of b a] by (simp add: ac_simps)
 
 lemma gcd_idem: "gcd a a = normalize a"
-  by (cases "a = 0") (simp add: gcd_0_left, rule sym, rule gcdI, simp_all)
+  by (cases "a = 0") (simp, rule sym, rule gcdI, simp_all)
 
 lemma gcd_right_idem: "gcd (gcd a b) b = gcd a b"
   apply (rule gcdI)
@@ -437,20 +490,6 @@
     by (simp add: fun_eq_iff gcd_left_idem)
 qed
 
-lemma coprime_dvd_mult:
-  assumes "gcd c b = 1" and "c dvd a * b"
-  shows "c dvd a"
-proof -
-  let ?nf = "unit_factor"
-  from assms gcd_mult_distrib [of a c b] 
-    have A: "a = gcd (a * c) (a * b) * ?nf a" by simp
-  from \<open>c dvd a * b\<close> show ?thesis by (subst A, simp_all add: gcd_greatest)
-qed
-
-lemma coprime_dvd_mult_iff:
-  "gcd c b = 1 \<Longrightarrow> (c dvd a * b) = (c dvd a)"
-  by (rule, rule coprime_dvd_mult, simp_all)
-
 lemma gcd_dvd_antisym:
   "gcd a b dvd gcd c d \<Longrightarrow> gcd c d dvd gcd a b \<Longrightarrow> gcd a b = gcd c d"
 proof (rule gcdI)
@@ -466,20 +505,6 @@
   from this and B show "l dvd gcd a b" by (rule dvd_trans)
 qed
 
-lemma gcd_mult_cancel:
-  assumes "gcd k n = 1"
-  shows "gcd (k * m) n = gcd m n"
-proof (rule gcd_dvd_antisym)
-  have "gcd (gcd (k * m) n) k = gcd (gcd k n) (k * m)" by (simp add: ac_simps)
-  also note \<open>gcd k n = 1\<close>
-  finally have "gcd (gcd (k * m) n) k = 1" by simp
-  hence "gcd (k * m) n dvd m" by (rule coprime_dvd_mult, simp add: ac_simps)
-  moreover have "gcd (k * m) n dvd n" by simp
-  ultimately show "gcd (k * m) n dvd gcd m n" by (rule gcd_greatest)
-  have "gcd m n dvd (k * m)" and "gcd m n dvd n" by simp_all
-  then show "gcd m n dvd gcd (k * m) n" by (rule gcd_greatest)
-qed
-
 lemma coprime_crossproduct:
   assumes [simp]: "gcd a d = 1" "gcd b c = 1"
   shows "normalize (a * c) = normalize (b * d) \<longleftrightarrow> normalize a  = normalize b \<and> normalize c = normalize d"
@@ -525,7 +550,7 @@
   by (rule sym, rule gcdI, simp_all)
 
 lemma coprime: "gcd a b = 1 \<longleftrightarrow> (\<forall>d. d dvd a \<and> d dvd b \<longleftrightarrow> is_unit d)"
-  by (auto intro: coprimeI gcd_greatest dvd_gcd_D1 dvd_gcd_D2)
+  by (auto intro: coprimeI gcd_greatest dvd_gcdD1 dvd_gcdD2)
 
 lemma div_gcd_coprime:
   assumes nz: "a \<noteq> 0 \<or> b \<noteq> 0"
@@ -549,15 +574,6 @@
   then show "l dvd 1" ..
 qed
 
-lemma coprime_mult: 
-  assumes da: "gcd d a = 1" and db: "gcd d b = 1"
-  shows "gcd d (a * b) = 1"
-  apply (subst gcd.commute)
-  using da apply (subst gcd_mult_cancel)
-  apply (subst gcd.commute, assumption)
-  apply (subst gcd.commute, rule db)
-  done
-
 lemma coprime_lmult:
   assumes dab: "gcd d (a * b) = 1" 
   shows "gcd d a = 1"
@@ -610,25 +626,6 @@
   "gcd d a = 1 \<Longrightarrow> gcd d (a^n) = 1"
   by (induct n, simp_all add: coprime_mult)
 
-lemma coprime_exp2 [intro]:
-  "gcd a b = 1 \<Longrightarrow> gcd (a^n) (b^m) = 1"
-  apply (rule coprime_exp)
-  apply (subst gcd.commute)
-  apply (rule coprime_exp)
-  apply (subst gcd.commute)
-  apply assumption
-  done
-
-lemma lcm_gcd:
-  "lcm a b = normalize (a * b) div gcd a b"
-  by (simp add: lcm_lcm_eucl gcd_gcd_eucl lcm_eucl_def)
-
-subclass semiring_gcd
-  apply standard
-  using gcd_right_idem
-  apply (simp_all add: lcm_gcd gcd_greatest_iff gcd_proj1_if_dvd)
-  done
-
 lemma gcd_exp:
   "gcd (a ^ n) (b ^ n) = gcd a b ^ n"
 proof (cases "a = 0 \<and> b = 0")
@@ -637,7 +634,7 @@
 next
   case False
   then have "1 = gcd ((a div gcd a b) ^ n) ((b div gcd a b) ^ n)"
-    using div_gcd_coprime by (subst sym) (auto simp: div_gcd_coprime)
+    using coprime_exp2[OF div_gcd_coprime[of a b], of n n, symmetric] by simp
   then have "gcd a b ^ n = gcd a b ^ n * ..." by simp
   also note gcd_mult_distrib
   also have "unit_factor (gcd a b ^ n) = 1"
@@ -712,18 +709,7 @@
   "n \<noteq> 0 \<Longrightarrow> a ^ n dvd b ^ n \<longleftrightarrow> a dvd b"
   by (auto intro: pow_divs_pow dvd_power_same)
 
-lemma divs_mult:
-  assumes mr: "m dvd r" and nr: "n dvd r" and mn: "gcd m n = 1"
-  shows "m * n dvd r"
-proof -
-  from mr nr obtain m' n' where m': "r = m*m'" and n': "r = n*n'"
-    unfolding dvd_def by blast
-  from mr n' have "m dvd n'*n" by (simp add: ac_simps)
-  hence "m dvd n'" using coprime_dvd_mult_iff[OF mn] by simp
-  then obtain k where k: "n' = m*k" unfolding dvd_def by blast
-  with n' have "r = m * n * k" by (simp add: mult_ac)
-  then show ?thesis unfolding dvd_def by blast
-qed
+lemmas divs_mult = divides_mult
 
 lemma coprime_plus_one [simp]: "gcd (n + 1) n = 1"
   by (subst add_commute, simp)
@@ -734,6 +720,10 @@
   apply (induct set: finite)
   apply (auto simp add: gcd_mult_cancel)
   done
+  
+lemma listprod_coprime:
+  "(\<And>x. x \<in> set xs \<Longrightarrow> coprime x y) \<Longrightarrow> coprime (listprod xs) y" 
+  by (induction xs) (simp_all add: gcd_mult_cancel)
 
 lemma coprime_divisors: 
   assumes "d dvd a" "e dvd b" "gcd a b = 1"
@@ -790,39 +780,11 @@
   shows "c = lcm a b"
   by (rule associated_eqI) (auto simp: assms intro: lcm_least)
 
-sublocale lcm: abel_semigroup lcm ..
-
-lemma dvd_lcm_D1:
-  "lcm m n dvd k \<Longrightarrow> m dvd k"
-  by (rule dvd_trans, rule dvd_lcm1, assumption)
-
-lemma dvd_lcm_D2:
-  "lcm m n dvd k \<Longrightarrow> n dvd k"
-  by (rule dvd_trans, rule dvd_lcm2, assumption)
-
 lemma gcd_dvd_lcm [simp]:
   "gcd a b dvd lcm a b"
   using gcd_dvd2 by (rule dvd_lcmI2)
 
-lemma lcm_1_iff:
-  "lcm a b = 1 \<longleftrightarrow> is_unit a \<and> is_unit b"
-proof
-  assume "lcm a b = 1"
-  then show "is_unit a \<and> is_unit b" by auto
-next
-  assume "is_unit a \<and> is_unit b"
-  hence "a dvd 1" and "b dvd 1" by simp_all
-  hence "is_unit (lcm a b)" by (rule lcm_least)
-  hence "lcm a b = unit_factor (lcm a b)"
-    by (blast intro: sym is_unit_unit_factor)
-  also have "\<dots> = 1" using \<open>is_unit a \<and> is_unit b\<close>
-    by auto
-  finally show "lcm a b = 1" .
-qed
-
-lemma lcm_0:
-  "lcm a 0 = 0"
-  by (fact lcm_0_right)
+lemmas lcm_0 = lcm_0_right
 
 lemma lcm_unique:
   "a dvd d \<and> b dvd d \<and> 
@@ -886,7 +848,7 @@
     by (intro le_antisym, simp, intro euclidean_size_lcm_le1)
   with assms have "lcm a b dvd a" 
     by (rule_tac dvd_euclidean_size_eq_imp_dvd) (auto simp: lcm_zero)
-  hence "b dvd a" by (rule dvd_lcm_D2)
+  hence "b dvd a" by (rule lcm_dvdD2)
   with \<open>\<not>b dvd a\<close> show False by contradiction
 qed
 
@@ -929,104 +891,10 @@
   "lcm a (normalize b) = lcm a b"
   using normalize_lcm_left [of b a] by (simp add: ac_simps)
 
-lemma lcm_left_idem:
-  "lcm a (lcm a b) = lcm a b"
-  by (rule associated_eqI) simp_all
-
-lemma lcm_right_idem:
-  "lcm (lcm a b) b = lcm a b"
-  by (rule associated_eqI) simp_all
-
-lemma comp_fun_idem_lcm: "comp_fun_idem lcm"
-proof
-  fix a b show "lcm a \<circ> lcm b = lcm b \<circ> lcm a"
-    by (simp add: fun_eq_iff ac_simps)
-next
-  fix a show "lcm a \<circ> lcm a = lcm a" unfolding o_def
-    by (intro ext, simp add: lcm_left_idem)
-qed
-
-lemma dvd_Lcm [simp]: "a \<in> A \<Longrightarrow> a dvd Lcm A"
-  and Lcm_least: "(\<And>a. a \<in> A \<Longrightarrow> a dvd b) \<Longrightarrow> Lcm A dvd b"
-  and unit_factor_Lcm [simp]: 
-          "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)"
-proof -
-  have "(\<forall>a\<in>A. a dvd Lcm A) \<and> (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> Lcm A dvd l') \<and>
-    unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" (is ?thesis)
-  proof (cases "\<exists>l. l \<noteq>  0 \<and> (\<forall>a\<in>A. a dvd l)")
-    case False
-    hence "Lcm A = 0" by (auto simp: Lcm_Lcm_eucl Lcm_eucl_def)
-    with False show ?thesis by auto
-  next
-    case True
-    then obtain l\<^sub>0 where l\<^sub>0_props: "l\<^sub>0 \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l\<^sub>0)" by blast
-    def n \<equiv> "LEAST n. \<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
-    def l \<equiv> "SOME l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
-    have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l) \<and> euclidean_size l = n"
-      apply (subst n_def)
-      apply (rule LeastI[of _ "euclidean_size l\<^sub>0"])
-      apply (rule exI[of _ l\<^sub>0])
-      apply (simp add: l\<^sub>0_props)
-      done
-    from someI_ex[OF this] have "l \<noteq> 0" and "\<forall>a\<in>A. a dvd l" and "euclidean_size l = n" 
-      unfolding l_def by simp_all
-    {
-      fix l' assume "\<forall>a\<in>A. a dvd l'"
-      with \<open>\<forall>a\<in>A. a dvd l\<close> have "\<forall>a\<in>A. a dvd gcd l l'" by (auto intro: gcd_greatest)
-      moreover from \<open>l \<noteq> 0\<close> have "gcd l l' \<noteq> 0" by simp
-      ultimately have "\<exists>b. b \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd b) \<and> euclidean_size b = euclidean_size (gcd l l')"
-        by (intro exI[of _ "gcd l l'"], auto)
-      hence "euclidean_size (gcd l l') \<ge> n" by (subst n_def) (rule Least_le)
-      moreover have "euclidean_size (gcd l l') \<le> n"
-      proof -
-        have "gcd l l' dvd l" by simp
-        then obtain a where "l = gcd l l' * a" unfolding dvd_def by blast
-        with \<open>l \<noteq> 0\<close> have "a \<noteq> 0" by auto
-        hence "euclidean_size (gcd l l') \<le> euclidean_size (gcd l l' * a)"
-          by (rule size_mult_mono)
-        also have "gcd l l' * a = l" using \<open>l = gcd l l' * a\<close> ..
-        also note \<open>euclidean_size l = n\<close>
-        finally show "euclidean_size (gcd l l') \<le> n" .
-      qed
-      ultimately have *: "euclidean_size l = euclidean_size (gcd l l')" 
-        by (intro le_antisym, simp_all add: \<open>euclidean_size l = n\<close>)
-      from \<open>l \<noteq> 0\<close> have "l dvd gcd l l'"
-        by (rule dvd_euclidean_size_eq_imp_dvd) (auto simp add: *)
-      hence "l dvd l'" by (blast dest: dvd_gcd_D2)
-    }
-
-    with \<open>(\<forall>a\<in>A. a dvd l)\<close> and unit_factor_is_unit[OF \<open>l \<noteq> 0\<close>] and \<open>l \<noteq> 0\<close>
-      have "(\<forall>a\<in>A. a dvd normalize l) \<and> 
-        (\<forall>l'. (\<forall>a\<in>A. a dvd l') \<longrightarrow> normalize l dvd l') \<and>
-        unit_factor (normalize l) = 
-        (if normalize l = 0 then 0 else 1)"
-      by (auto simp: unit_simps)
-    also from True have "normalize l = Lcm A"
-      by (simp add: Lcm_Lcm_eucl Lcm_eucl_def Let_def n_def l_def)
-    finally show ?thesis .
-  qed
-  note A = this
-
-  {fix a assume "a \<in> A" then show "a dvd Lcm A" using A by blast}
-  {fix b assume "\<And>a. a \<in> A \<Longrightarrow> a dvd b" then show "Lcm A dvd b" using A by blast}
-  from A show "unit_factor (Lcm A) = (if Lcm A = 0 then 0 else 1)" by blast
-qed
-
-lemma normalize_Lcm [simp]:
-  "normalize (Lcm A) = Lcm A"
-proof (cases "Lcm A = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  have "unit_factor (Lcm A) * normalize (Lcm A) = Lcm A"
-    by (fact unit_factor_mult_normalize)
-  with False show ?thesis by simp
-qed
-
 lemma LcmI:
   assumes "\<And>a. a \<in> A \<Longrightarrow> a dvd b" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> a dvd c) \<Longrightarrow> b dvd c"
     and "normalize b = b" shows "b = Lcm A"
-  by (rule associated_eqI) (auto simp: assms intro: Lcm_least)
+  by (rule associated_eqI) (auto simp: assms dvd_Lcm intro: Lcm_least)
 
 lemma Lcm_subset:
   "A \<subseteq> B \<Longrightarrow> Lcm A dvd Lcm B"
@@ -1043,13 +911,6 @@
   apply simp
   done
 
-lemma Lcm_1_iff:
-  "Lcm A = 1 \<longleftrightarrow> (\<forall>a\<in>A. is_unit a)"
-proof
-  assume "Lcm A = 1"
-  then show "\<forall>a\<in>A. is_unit a" by auto
-qed (rule LcmI [symmetric], auto)
-
 lemma Lcm_no_units:
   "Lcm A = Lcm (A - {a. is_unit a})"
 proof -
@@ -1060,14 +921,6 @@
   finally show ?thesis by simp
 qed
 
-lemma Lcm_empty [simp]:
-  "Lcm {} = 1"
-  by (simp add: Lcm_1_iff)
-
-lemma Lcm_eq_0_I [simp]:
-  "0 \<in> A \<Longrightarrow> Lcm A = 0"
-  by (drule dvd_Lcm) simp
-
 lemma Lcm_0_iff':
   "Lcm A = 0 \<longleftrightarrow> \<not>(\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l))"
 proof
@@ -1092,27 +945,6 @@
   qed
 qed (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
 
-lemma Lcm_0_iff [simp]:
-  "finite A \<Longrightarrow> Lcm A = 0 \<longleftrightarrow> 0 \<in> A"
-proof -
-  assume "finite A"
-  have "0 \<in> A \<Longrightarrow> Lcm A = 0"  by (intro dvd_0_left dvd_Lcm)
-  moreover {
-    assume "0 \<notin> A"
-    hence "\<Prod>A \<noteq> 0" 
-      apply (induct rule: finite_induct[OF \<open>finite A\<close>]) 
-      apply simp
-      apply (subst setprod.insert, assumption, assumption)
-      apply (rule no_zero_divisors)
-      apply blast+
-      done
-    moreover from \<open>finite A\<close> have "\<forall>a\<in>A. a dvd \<Prod>A" by blast
-    ultimately have "\<exists>l. l \<noteq> 0 \<and> (\<forall>a\<in>A. a dvd l)" by blast
-    with Lcm_0_iff' have "Lcm A \<noteq> 0" by simp
-  }
-  ultimately show "Lcm A = 0 \<longleftrightarrow> 0 \<in> A" by blast
-qed
-
 lemma Lcm_no_multiple:
   "(\<forall>m. m \<noteq> 0 \<longrightarrow> (\<exists>a\<in>A. \<not>a dvd m)) \<Longrightarrow> Lcm A = 0"
 proof -
@@ -1121,14 +953,6 @@
   then show "Lcm A = 0" by (simp only: Lcm_Lcm_eucl Lcm_eucl_def if_False)
 qed
 
-lemma Lcm_insert [simp]:
-  "Lcm (insert a A) = lcm a (Lcm A)"
-proof (rule lcmI)
-  fix l assume "a dvd l" and "Lcm A dvd l"
-  then have "\<forall>a\<in>A. a dvd l" by (auto intro: dvd_trans [of _ "Lcm A" l])
-  with \<open>a dvd l\<close> show "Lcm (insert a A) dvd l" by (force intro: Lcm_least)
-qed (auto intro: Lcm_least dvd_Lcm)
- 
 lemma Lcm_finite:
   assumes "finite A"
   shows "Lcm A = Finite_Set.fold lcm 1 A"
@@ -1167,50 +991,17 @@
     \<Longrightarrow> Lcm A = normalize (\<Prod>A)"
   by (rule Lcm_coprime) (simp_all add: card_eq_0_iff)
 
-lemma Gcd_Lcm:
-  "Gcd A = Lcm {d. \<forall>a\<in>A. d dvd a}"
-  by (simp add: Gcd_Gcd_eucl Lcm_Lcm_eucl Gcd_eucl_def)
-
-lemma Gcd_dvd [simp]: "a \<in> A \<Longrightarrow> Gcd A dvd a"
-  and Gcd_greatest: "(\<And>a. a \<in> A \<Longrightarrow> b dvd a) \<Longrightarrow> b dvd Gcd A"
-  and unit_factor_Gcd [simp]: 
-    "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
+lemma unit_factor_Gcd [simp]: "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
 proof -
-  fix a assume "a \<in> A"
-  hence "Lcm {d. \<forall>a\<in>A. d dvd a} dvd a" by (intro Lcm_least) blast
-  then show "Gcd A dvd a" by (simp add: Gcd_Lcm)
-next
-  fix g' assume "\<And>a. a \<in> A \<Longrightarrow> g' dvd a"
-  hence "g' dvd Lcm {d. \<forall>a\<in>A. d dvd a}" by (intro dvd_Lcm) blast
-  then show "g' dvd Gcd A" by (simp add: Gcd_Lcm)
-next
   show "unit_factor (Gcd A) = (if Gcd A = 0 then 0 else 1)"
-    by (simp add: Gcd_Lcm)
+    by (simp add: Gcd_Lcm unit_factor_Lcm)
 qed
 
-lemma normalize_Gcd [simp]:
-  "normalize (Gcd A) = Gcd A"
-proof (cases "Gcd A = 0")
-  case True then show ?thesis by simp
-next
-  case False
-  have "unit_factor (Gcd A) * normalize (Gcd A) = Gcd A"
-    by (fact unit_factor_mult_normalize)
-  with False show ?thesis by simp
-qed
-
-subclass semiring_Gcd
-  by standard (auto intro: Gcd_greatest Lcm_least)
-
 lemma GcdI:
   assumes "\<And>a. a \<in> A \<Longrightarrow> b dvd a" and "\<And>c. (\<And>a. a \<in> A \<Longrightarrow> c dvd a) \<Longrightarrow> c dvd b"
     and "normalize b = b"
   shows "b = Gcd A"
-  by (rule associated_eqI) (auto simp: assms intro: Gcd_greatest)
-
-lemma Lcm_Gcd:
-  "Lcm A = Gcd {m. \<forall>a\<in>A. a dvd m}"
-  by (rule LcmI[symmetric]) (auto intro: Gcd_greatest Gcd_greatest)
+  by (rule associated_eqI) (auto simp: assms Gcd_dvd intro: Gcd_greatest)
 
 lemma Gcd_1:
   "1 \<in> A \<Longrightarrow> Gcd A = 1"
@@ -1232,6 +1023,21 @@
 lemma Gcd_2 [simp]: "Gcd {a,b} = gcd a b"
   by simp
 
+
+definition pairwise_coprime where
+  "pairwise_coprime A = (\<forall>x y. x \<in> A \<and> y \<in> A \<and> x \<noteq> y \<longrightarrow> coprime x y)"
+
+lemma pairwise_coprimeI [intro?]:
+  "(\<And>x y. x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y) \<Longrightarrow> pairwise_coprime A"
+  by (simp add: pairwise_coprime_def)
+
+lemma pairwise_coprimeD:
+  "pairwise_coprime A \<Longrightarrow> x \<in> A \<Longrightarrow> y \<in> A \<Longrightarrow> x \<noteq> y \<Longrightarrow> coprime x y"
+  by (simp add: pairwise_coprime_def)
+
+lemma pairwise_coprime_subset: "pairwise_coprime A \<Longrightarrow> B \<subseteq> A \<Longrightarrow> pairwise_coprime B"
+  by (force simp: pairwise_coprime_def)
+
 end
 
 text \<open>
@@ -1243,7 +1049,6 @@
 begin
 
 subclass euclidean_ring ..
-
 subclass ring_gcd ..
 
 lemma euclid_ext_gcd [simp]:
@@ -1325,6 +1130,7 @@
 
 end
 
+
 instantiation int :: euclidean_ring
 begin
 
@@ -1336,22 +1142,19 @@
 
 end
 
+
 instantiation poly :: (field) euclidean_ring
 begin
 
 definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
-  where "euclidean_size p = (if p = 0 then 0 else Suc (degree p))"
-
-lemma euclidenan_size_poly_minus_one_degree [simp]:
-  "euclidean_size p - 1 = degree p"
-  by (simp add: euclidean_size_poly_def)
+  where "euclidean_size p = (if p = 0 then 0 else 2 ^ degree p)"
 
 lemma euclidean_size_poly_0 [simp]:
   "euclidean_size (0::'a poly) = 0"
   by (simp add: euclidean_size_poly_def)
 
 lemma euclidean_size_poly_not_0 [simp]:
-  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = Suc (degree p)"
+  "p \<noteq> 0 \<Longrightarrow> euclidean_size p = 2 ^ degree p"
   by (simp add: euclidean_size_poly_def)
 
 instance
@@ -1369,23 +1172,82 @@
     by (rule degree_mult_right_le)
   with \<open>q \<noteq> 0\<close> show "euclidean_size p \<le> euclidean_size (p * q)"
     by (cases "p = 0") simp_all
-qed
+qed simp
 
 end
 
-(*instance nat :: euclidean_semiring_gcd
-proof (standard, auto intro!: ext)
-  fix m n :: nat
-  show *: "gcd m n = gcd_eucl m n"
-  proof (induct m n rule: gcd_eucl_induct)
-    case zero then show ?case by (simp add: gcd_eucl_0)
-  next
-    case (mod m n)
-    with gcd_eucl_non_0 [of n m, symmetric]
-    show ?case by (simp add: gcd_non_0_nat)
-  qed
-  show "lcm m n = lcm_eucl m n"
-    by (simp add: lcm_eucl_def lcm_gcd * [symmetric] lcm_nat_def)
-qed*)
+
+instance nat :: euclidean_semiring_gcd
+proof
+  show [simp]: "gcd = (gcd_eucl :: nat \<Rightarrow> _)" "Lcm = (Lcm_eucl :: nat set \<Rightarrow> _)"
+    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
+  show "lcm = (lcm_eucl :: nat \<Rightarrow> _)" "Gcd = (Gcd_eucl :: nat set \<Rightarrow> _)"
+    by (intro ext, simp add: lcm_eucl_def lcm_nat_def Gcd_nat_def Gcd_eucl_def)+
+qed
+
+instance int :: euclidean_ring_gcd
+proof
+  show [simp]: "gcd = (gcd_eucl :: int \<Rightarrow> _)" "Lcm = (Lcm_eucl :: int set \<Rightarrow> _)"
+    by (simp_all add: eq_gcd_euclI eq_Lcm_euclI)
+  show "lcm = (lcm_eucl :: int \<Rightarrow> _)" "Gcd = (Gcd_eucl :: int set \<Rightarrow> _)"
+    by (intro ext, simp add: lcm_eucl_def lcm_altdef_int 
+          semiring_Gcd_class.Gcd_Lcm Gcd_eucl_def abs_mult)+
+qed
+
+
+instantiation poly :: (field) euclidean_ring_gcd
+begin
+
+definition gcd_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  "gcd_poly = gcd_eucl"
+  
+definition lcm_poly :: "'a poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly" where
+  "lcm_poly = lcm_eucl"
+  
+definition Gcd_poly :: "'a poly set \<Rightarrow> 'a poly" where
+  "Gcd_poly = Gcd_eucl"
+  
+definition Lcm_poly :: "'a poly set \<Rightarrow> 'a poly" where
+  "Lcm_poly = Lcm_eucl"
+
+instance by standard (simp_all only: gcd_poly_def lcm_poly_def Gcd_poly_def Lcm_poly_def)
+end
+
+lemma poly_gcd_monic:
+  "lead_coeff (gcd x y) = (if x = 0 \<and> y = 0 then 0 else 1)"
+  using unit_factor_gcd[of x y]
+  by (simp add: unit_factor_poly_def monom_0 one_poly_def lead_coeff_def split: if_split_asm)
+
+lemma poly_dvd_antisym:
+  fixes p q :: "'a::idom poly"
+  assumes coeff: "coeff p (degree p) = coeff q (degree q)"
+  assumes dvd1: "p dvd q" and dvd2: "q dvd p" shows "p = q"
+proof (cases "p = 0")
+  case True with coeff show "p = q" by simp
+next
+  case False with coeff have "q \<noteq> 0" by auto
+  have degree: "degree p = degree q"
+    using \<open>p dvd q\<close> \<open>q dvd p\<close> \<open>p \<noteq> 0\<close> \<open>q \<noteq> 0\<close>
+    by (intro order_antisym dvd_imp_degree_le)
+
+  from \<open>p dvd q\<close> obtain a where a: "q = p * a" ..
+  with \<open>q \<noteq> 0\<close> have "a \<noteq> 0" by auto
+  with degree a \<open>p \<noteq> 0\<close> have "degree a = 0"
+    by (simp add: degree_mult_eq)
+  with coeff a show "p = q"
+    by (cases a, auto split: if_splits)
+qed
+
+lemma poly_gcd_unique:
+  fixes d x y :: "_ poly"
+  assumes dvd1: "d dvd x" and dvd2: "d dvd y"
+    and greatest: "\<And>k. k dvd x \<Longrightarrow> k dvd y \<Longrightarrow> k dvd d"
+    and monic: "coeff d (degree d) = (if x = 0 \<and> y = 0 then 0 else 1)"
+  shows "d = gcd x y"
+  using assms by (intro gcdI) (auto simp: normalize_poly_def split: if_split_asm)
+
+lemma poly_gcd_code [code]:
+  "gcd x y = (if y = 0 then normalize x else gcd y (x mod (y :: _ poly)))"
+  by (simp add: gcd_0 gcd_non_0)
 
 end