# HG changeset patch
# User haftmann
# Date 1435237302 -7200
# Node ID c9fdf20804476cbda9f6b2cd70e8850b0f3ec4e4
# Parent  7ed2cde6806d32b8c7f1da73da93759a9ef7fdec
euclidean algorithm on polynomials

diff -r 7ed2cde6806d -r c9fdf2080447 src/HOL/Number_Theory/Euclidean_Algorithm.thy
--- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:42 2015 +0200
+++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:42 2015 +0200
@@ -3,7 +3,7 @@
 section \<open>Abstract euclidean algorithm\<close>
 
 theory Euclidean_Algorithm
-imports Complex_Main
+imports Complex_Main "~~/src/HOL/Library/Polynomial"
 begin
   
 text \<open>
@@ -1566,4 +1566,42 @@
 
 end
 
+instantiation poly :: (field) euclidean_semiring
+begin
+
+definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
+  where "euclidean_size = (degree :: 'a poly \<Rightarrow> nat)"
+
+definition normalization_factor_poly :: "'a poly \<Rightarrow> 'a poly"
+  where "normalization_factor p = monom (coeff p (degree p)) 0"
+
+instance
+proof (default, unfold euclidean_size_poly_def normalization_factor_poly_def)
+  fix p q :: "'a poly"
+  assume "q \<noteq> 0" and "\<not> q dvd p"
+  then show "degree (p mod q) < degree q"
+    using degree_mod_less [of q p] by (simp add: mod_eq_0_iff_dvd)
+next
+  fix p q :: "'a poly"
+  assume "q \<noteq> 0"
+  from \<open>q \<noteq> 0\<close> show "degree p \<le> degree (p * q)"
+    by (rule degree_mult_right_le)
+  from \<open>q \<noteq> 0\<close> show "is_unit (monom (coeff q (degree q)) 0)"
+    by (auto intro: is_unit_monom_0)
+next
+  fix p :: "'a poly"
+  show "monom (coeff p (degree p)) 0 = p" if "is_unit p"
+    using that by (fact is_unit_monom_trival)
+next
+  fix p q :: "'a poly"
+  show "monom (coeff (p * q) (degree (p * q))) 0 =
+    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
+    by (simp add: monom_0 coeff_degree_mult)
+next
+  show "monom (coeff 0 (degree 0)) 0 = 0"
+    by simp
+qed
+
 end
+
+end