--- 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