src/HOL/Number_Theory/Euclidean_Algorithm.thy
changeset 60571 c9fdf2080447
parent 60569 f2f1f6860959
child 60572 718b1ba06429
     1.1 --- a/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:42 2015 +0200
     1.2 +++ b/src/HOL/Number_Theory/Euclidean_Algorithm.thy	Thu Jun 25 15:01:42 2015 +0200
     1.3 @@ -3,7 +3,7 @@
     1.4  section \<open>Abstract euclidean algorithm\<close>
     1.5  
     1.6  theory Euclidean_Algorithm
     1.7 -imports Complex_Main
     1.8 +imports Complex_Main "~~/src/HOL/Library/Polynomial"
     1.9  begin
    1.10    
    1.11  text \<open>
    1.12 @@ -1566,4 +1566,42 @@
    1.13  
    1.14  end
    1.15  
    1.16 +instantiation poly :: (field) euclidean_semiring
    1.17 +begin
    1.18 +
    1.19 +definition euclidean_size_poly :: "'a poly \<Rightarrow> nat"
    1.20 +  where "euclidean_size = (degree :: 'a poly \<Rightarrow> nat)"
    1.21 +
    1.22 +definition normalization_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    1.23 +  where "normalization_factor p = monom (coeff p (degree p)) 0"
    1.24 +
    1.25 +instance
    1.26 +proof (default, unfold euclidean_size_poly_def normalization_factor_poly_def)
    1.27 +  fix p q :: "'a poly"
    1.28 +  assume "q \<noteq> 0" and "\<not> q dvd p"
    1.29 +  then show "degree (p mod q) < degree q"
    1.30 +    using degree_mod_less [of q p] by (simp add: mod_eq_0_iff_dvd)
    1.31 +next
    1.32 +  fix p q :: "'a poly"
    1.33 +  assume "q \<noteq> 0"
    1.34 +  from \<open>q \<noteq> 0\<close> show "degree p \<le> degree (p * q)"
    1.35 +    by (rule degree_mult_right_le)
    1.36 +  from \<open>q \<noteq> 0\<close> show "is_unit (monom (coeff q (degree q)) 0)"
    1.37 +    by (auto intro: is_unit_monom_0)
    1.38 +next
    1.39 +  fix p :: "'a poly"
    1.40 +  show "monom (coeff p (degree p)) 0 = p" if "is_unit p"
    1.41 +    using that by (fact is_unit_monom_trival)
    1.42 +next
    1.43 +  fix p q :: "'a poly"
    1.44 +  show "monom (coeff (p * q) (degree (p * q))) 0 =
    1.45 +    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
    1.46 +    by (simp add: monom_0 coeff_degree_mult)
    1.47 +next
    1.48 +  show "monom (coeff 0 (degree 0)) 0 = 0"
    1.49 +    by simp
    1.50 +qed
    1.51 +
    1.52  end
    1.53 +
    1.54 +end