src/HOL/Library/Polynomial.thy
changeset 60685 cb21b7022b00
parent 60679 ade12ef2773c
child 60686 ea5bc46c11e6
     1.1 --- a/src/HOL/Library/Polynomial.thy	Wed Jul 08 00:04:15 2015 +0200
     1.2 +++ b/src/HOL/Library/Polynomial.thy	Wed Jul 08 14:01:34 2015 +0200
     1.3 @@ -7,7 +7,7 @@
     1.4  section \<open>Polynomials as type over a ring structure\<close>
     1.5  
     1.6  theory Polynomial
     1.7 -imports Main GCD "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
     1.8 +imports Main "~~/src/HOL/GCD" "~~/src/HOL/Library/More_List" "~~/src/HOL/Library/Infinite_Set"
     1.9  begin
    1.10  
    1.11  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    1.12 @@ -1495,6 +1495,63 @@
    1.13    shows "monom (coeff p (degree p)) 0 = p"
    1.14    using assms by (cases p) (simp_all add: monom_0 is_unit_pCons_iff)
    1.15  
    1.16 +lemma is_unit_polyE:
    1.17 +  assumes "is_unit p"
    1.18 +  obtains a where "p = monom a 0" and "a \<noteq> 0"
    1.19 +proof -
    1.20 +  obtain a q where "p = pCons a q" by (cases p)
    1.21 +  with assms have "p = [:a:]" and "a \<noteq> 0"
    1.22 +    by (simp_all add: is_unit_pCons_iff)
    1.23 +  with that show thesis by (simp add: monom_0)
    1.24 +qed
    1.25 +
    1.26 +instantiation poly :: (field) normalization_semidom
    1.27 +begin
    1.28 +
    1.29 +definition normalize_poly :: "'a poly \<Rightarrow> 'a poly"
    1.30 +  where "normalize_poly p = smult (1 / coeff p (degree p)) p"
    1.31 +
    1.32 +definition unit_factor_poly :: "'a poly \<Rightarrow> 'a poly"
    1.33 +  where "unit_factor_poly p = monom (coeff p (degree p)) 0"
    1.34 +
    1.35 +instance
    1.36 +proof
    1.37 +  fix p :: "'a poly"
    1.38 +  show "unit_factor p * normalize p = p"
    1.39 +    by (simp add: normalize_poly_def unit_factor_poly_def)
    1.40 +      (simp only: mult_smult_left [symmetric] smult_monom, simp)
    1.41 +next
    1.42 +  show "normalize 0 = (0::'a poly)"
    1.43 +    by (simp add: normalize_poly_def)
    1.44 +next
    1.45 +  show "unit_factor 0 = (0::'a poly)"
    1.46 +    by (simp add: unit_factor_poly_def)
    1.47 +next
    1.48 +  fix p :: "'a poly"
    1.49 +  assume "is_unit p"
    1.50 +  then obtain a where "p = monom a 0" and "a \<noteq> 0"
    1.51 +    by (rule is_unit_polyE)
    1.52 +  then show "normalize p = 1"
    1.53 +    by (auto simp add: normalize_poly_def smult_monom degree_monom_eq)
    1.54 +next
    1.55 +  fix p q :: "'a poly"
    1.56 +  assume "q \<noteq> 0"
    1.57 +  from \<open>q \<noteq> 0\<close> have "is_unit (monom (coeff q (degree q)) 0)"
    1.58 +    by (auto intro: is_unit_monom_0)
    1.59 +  then show "is_unit (unit_factor q)"
    1.60 +    by (simp add: unit_factor_poly_def)
    1.61 +next
    1.62 +  fix p q :: "'a poly"
    1.63 +  have "monom (coeff (p * q) (degree (p * q))) 0 =
    1.64 +    monom (coeff p (degree p)) 0 * monom (coeff q (degree q)) 0"
    1.65 +    by (simp add: monom_0 coeff_degree_mult)
    1.66 +  then show "unit_factor (p * q) =
    1.67 +    unit_factor p * unit_factor q"
    1.68 +    by (simp add: unit_factor_poly_def)
    1.69 +qed
    1.70 +
    1.71 +end
    1.72 +
    1.73  lemma degree_mod_less:
    1.74    "y \<noteq> 0 \<Longrightarrow> x mod y = 0 \<or> degree (x mod y) < degree y"
    1.75    using pdivmod_rel [of x y]