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