Polynomial_Factorial does not depend on Field_as_Ring as such
authorhaftmann
Sun Oct 08 22:28:21 2017 +0200 (19 months ago)
changeset 66805274b4edca859
parent 66804 3f9bb52082c4
child 66806 a4e82b58d833
Polynomial_Factorial does not depend on Field_as_Ring as such
NEWS
src/HOL/Computational_Algebra/Computational_Algebra.thy
src/HOL/Computational_Algebra/Polynomial.thy
src/HOL/Computational_Algebra/Polynomial_Factorial.thy
src/HOL/ROOT
     1.1 --- a/NEWS	Sun Oct 08 22:28:20 2017 +0200
     1.2 +++ b/NEWS	Sun Oct 08 22:28:21 2017 +0200
     1.3 @@ -44,6 +44,11 @@
     1.4      higher-order quantifiers. An 'smt_explicit_application' option has been
     1.5      added to control this. INCOMPATIBILITY.
     1.6  
     1.7 +* Theory HOL-Computational_Algebra.Polynomial_Factorial does not
     1.8 +provide instances of rat, real, complex as factorial rings etc.
     1.9 +Import HOL-Computational_Algebra.Field_as_Ring explicitly in case of
    1.10 +need. INCOMPATIBILITY.
    1.11 +
    1.12  * Fact mod_mult_self4 (on nat) renamed to mod_mult_self3', to avoid clash
    1.13  with fact mod_mult_self4 (on more generic semirings). INCOMPATIBILITY.
    1.14  
     2.1 --- a/src/HOL/Computational_Algebra/Computational_Algebra.thy	Sun Oct 08 22:28:20 2017 +0200
     2.2 +++ b/src/HOL/Computational_Algebra/Computational_Algebra.thy	Sun Oct 08 22:28:21 2017 +0200
     2.3 @@ -12,6 +12,7 @@
     2.4    Nth_Powers
     2.5    Polynomial_FPS
     2.6    Polynomial
     2.7 +  Polynomial_Factorial
     2.8    Primes
     2.9    Squarefree
    2.10  begin
     3.1 --- a/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:20 2017 +0200
     3.2 +++ b/src/HOL/Computational_Algebra/Polynomial.thy	Sun Oct 08 22:28:21 2017 +0200
     3.3 @@ -12,6 +12,7 @@
     3.4    HOL.Deriv
     3.5    "HOL-Library.More_List"
     3.6    "HOL-Library.Infinite_Set"
     3.7 +  Factorial_Ring
     3.8  begin
     3.9  
    3.10  subsection \<open>Auxiliary: operations for lists (later) representing coefficients\<close>
    3.11 @@ -2881,167 +2882,6 @@
    3.12  qed
    3.13  
    3.14  
    3.15 -subsection \<open>Content and primitive part of a polynomial\<close>
    3.16 -
    3.17 -definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
    3.18 -  where "content p = gcd_list (coeffs p)"
    3.19 -
    3.20 -lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
    3.21 -  by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
    3.22 -
    3.23 -lemma content_0 [simp]: "content 0 = 0"
    3.24 -  by (simp add: content_def)
    3.25 -
    3.26 -lemma content_1 [simp]: "content 1 = 1"
    3.27 -  by (simp add: content_def)
    3.28 -
    3.29 -lemma content_const [simp]: "content [:c:] = normalize c"
    3.30 -  by (simp add: content_def cCons_def)
    3.31 -
    3.32 -lemma const_poly_dvd_iff_dvd_content: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
    3.33 -  for c :: "'a::semiring_gcd"
    3.34 -proof (cases "p = 0")
    3.35 -  case True
    3.36 -  then show ?thesis by simp
    3.37 -next
    3.38 -  case False
    3.39 -  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
    3.40 -    by (rule const_poly_dvd_iff)
    3.41 -  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
    3.42 -  proof safe
    3.43 -    fix n :: nat
    3.44 -    assume "\<forall>a\<in>set (coeffs p). c dvd a"
    3.45 -    then show "c dvd coeff p n"
    3.46 -      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
    3.47 -  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
    3.48 -  also have "\<dots> \<longleftrightarrow> c dvd content p"
    3.49 -    by (simp add: content_def dvd_Gcd_fin_iff dvd_mult_unit_iff)
    3.50 -  finally show ?thesis .
    3.51 -qed
    3.52 -
    3.53 -lemma content_dvd [simp]: "[:content p:] dvd p"
    3.54 -  by (subst const_poly_dvd_iff_dvd_content) simp_all
    3.55 -
    3.56 -lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
    3.57 -proof (cases "p = 0")
    3.58 -  case True
    3.59 -  then show ?thesis
    3.60 -    by simp
    3.61 -next
    3.62 -  case False
    3.63 -  then show ?thesis
    3.64 -    by (cases "n \<le> degree p")
    3.65 -      (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd)
    3.66 -qed
    3.67 -
    3.68 -lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
    3.69 -  by (simp add: content_def Gcd_fin_dvd)
    3.70 -
    3.71 -lemma normalize_content [simp]: "normalize (content p) = content p"
    3.72 -  by (simp add: content_def)
    3.73 -
    3.74 -lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
    3.75 -proof
    3.76 -  assume "is_unit (content p)"
    3.77 -  then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
    3.78 -  then show "content p = 1" by simp
    3.79 -qed auto
    3.80 -
    3.81 -lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
    3.82 -  by (simp add: content_def coeffs_smult Gcd_fin_mult)
    3.83 -
    3.84 -lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
    3.85 -  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
    3.86 -
    3.87 -definition primitive_part :: "'a :: semiring_gcd poly \<Rightarrow> 'a poly"
    3.88 -  where "primitive_part p = map_poly (\<lambda>x. x div content p) p"
    3.89 -
    3.90 -lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
    3.91 -  by (simp add: primitive_part_def)
    3.92 -
    3.93 -lemma content_times_primitive_part [simp]: "smult (content p) (primitive_part p) = p"
    3.94 -  for p :: "'a :: semiring_gcd poly"
    3.95 -proof (cases "p = 0")
    3.96 -  case True
    3.97 -  then show ?thesis by simp
    3.98 -next
    3.99 -  case False
   3.100 -  then show ?thesis
   3.101 -  unfolding primitive_part_def
   3.102 -  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
   3.103 -      intro: map_poly_idI)
   3.104 -qed
   3.105 -
   3.106 -lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   3.107 -proof (cases "p = 0")
   3.108 -  case True
   3.109 -  then show ?thesis by simp
   3.110 -next
   3.111 -  case False
   3.112 -  then have "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   3.113 -    by (simp add:  primitive_part_def)
   3.114 -  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   3.115 -    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   3.116 -  finally show ?thesis
   3.117 -    using False by simp
   3.118 -qed
   3.119 -
   3.120 -lemma content_primitive_part [simp]:
   3.121 -  assumes "p \<noteq> 0"
   3.122 -  shows "content (primitive_part p) = 1"
   3.123 -proof -
   3.124 -  have "p = smult (content p) (primitive_part p)"
   3.125 -    by simp
   3.126 -  also have "content \<dots> = content (primitive_part p) * content p"
   3.127 -    by (simp del: content_times_primitive_part add: ac_simps)
   3.128 -  finally have "1 * content p = content (primitive_part p) * content p"
   3.129 -    by simp
   3.130 -  then have "1 * content p div content p = content (primitive_part p) * content p div content p"
   3.131 -    by simp
   3.132 -  with assms show ?thesis
   3.133 -    by simp
   3.134 -qed
   3.135 -
   3.136 -lemma content_decompose:
   3.137 -  obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
   3.138 -proof (cases "p = 0")
   3.139 -  case True
   3.140 -  then show ?thesis by (intro that[of 1]) simp_all
   3.141 -next
   3.142 -  case False
   3.143 -  from content_dvd[of p] obtain r where r: "p = [:content p:] * r"
   3.144 -    by (rule dvdE)
   3.145 -  have "content p * 1 = content p * content r"
   3.146 -    by (subst r) simp
   3.147 -  with False have "content r = 1"
   3.148 -    by (subst (asm) mult_left_cancel) simp_all
   3.149 -  with r show ?thesis
   3.150 -    by (intro that[of r]) simp_all
   3.151 -qed
   3.152 -
   3.153 -lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q"
   3.154 -  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   3.155 -
   3.156 -lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   3.157 -  by (simp add: primitive_part_def map_poly_pCons)
   3.158 -
   3.159 -lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   3.160 -  by (auto simp: primitive_part_def)
   3.161 -
   3.162 -lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   3.163 -proof (cases "p = 0")
   3.164 -  case True
   3.165 -  then show ?thesis by simp
   3.166 -next
   3.167 -  case False
   3.168 -  have "p = smult (content p) (primitive_part p)"
   3.169 -    by simp
   3.170 -  also from False have "degree \<dots> = degree (primitive_part p)"
   3.171 -    by (subst degree_smult_eq) simp_all
   3.172 -  finally show ?thesis ..
   3.173 -qed
   3.174 -
   3.175 -
   3.176  subsection \<open>Division of polynomials\<close>
   3.177  
   3.178  subsubsection \<open>Division in general\<close>
   3.179 @@ -3649,16 +3489,6 @@
   3.180    finally show ?thesis .
   3.181  qed
   3.182  
   3.183 -lemma smult_content_normalize_primitive_part [simp]:
   3.184 -  "smult (content p) (normalize (primitive_part p)) = normalize p"
   3.185 -proof -
   3.186 -  have "smult (content p) (normalize (primitive_part p)) =
   3.187 -      normalize ([:content p:] * primitive_part p)"
   3.188 -    by (subst normalize_mult) (simp_all add: normalize_const_poly)
   3.189 -  also have "[:content p:] * primitive_part p = p" by simp
   3.190 -  finally show ?thesis .
   3.191 -qed
   3.192 -
   3.193  inductive eucl_rel_poly :: "'a::field poly \<Rightarrow> 'a poly \<Rightarrow> 'a poly \<times> 'a poly \<Rightarrow> bool"
   3.194    where
   3.195      eucl_rel_poly_by0: "eucl_rel_poly x 0 (0, x)"
   3.196 @@ -4502,6 +4332,387 @@
   3.197    qed
   3.198  qed
   3.199  
   3.200 +
   3.201 +subsection \<open>Primality and irreducibility in polynomial rings\<close>
   3.202 +
   3.203 +lemma prod_mset_const_poly: "(\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
   3.204 +  by (induct A) (simp_all add: ac_simps)
   3.205 +
   3.206 +lemma irreducible_const_poly_iff:
   3.207 +  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
   3.208 +  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
   3.209 +proof
   3.210 +  assume A: "irreducible c"
   3.211 +  show "irreducible [:c:]"
   3.212 +  proof (rule irreducibleI)
   3.213 +    fix a b assume ab: "[:c:] = a * b"
   3.214 +    hence "degree [:c:] = degree (a * b)" by (simp only: )
   3.215 +    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
   3.216 +    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
   3.217 +    finally have "degree a = 0" "degree b = 0" by auto
   3.218 +    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
   3.219 +    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
   3.220 +    hence "c = a' * b'" by (simp add: ab' mult_ac)
   3.221 +    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
   3.222 +    with ab' show "a dvd 1 \<or> b dvd 1"
   3.223 +      by (auto simp add: is_unit_const_poly_iff)
   3.224 +  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
   3.225 +next
   3.226 +  assume A: "irreducible [:c:]"
   3.227 +  then have "c \<noteq> 0" and "\<not> c dvd 1"
   3.228 +    by (auto simp add: irreducible_def is_unit_const_poly_iff)
   3.229 +  then show "irreducible c"
   3.230 +  proof (rule irreducibleI)
   3.231 +    fix a b assume ab: "c = a * b"
   3.232 +    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
   3.233 +    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
   3.234 +    then show "a dvd 1 \<or> b dvd 1"
   3.235 +      by (auto simp add: is_unit_const_poly_iff)
   3.236 +  qed
   3.237 +qed
   3.238 +
   3.239 +lemma lift_prime_elem_poly:
   3.240 +  assumes "prime_elem (c :: 'a :: semidom)"
   3.241 +  shows   "prime_elem [:c:]"
   3.242 +proof (rule prime_elemI)
   3.243 +  fix a b assume *: "[:c:] dvd a * b"
   3.244 +  from * have dvd: "c dvd coeff (a * b) n" for n
   3.245 +    by (subst (asm) const_poly_dvd_iff) blast
   3.246 +  {
   3.247 +    define m where "m = (GREATEST m. \<not>c dvd coeff b m)"
   3.248 +    assume "\<not>[:c:] dvd b"
   3.249 +    hence A: "\<exists>i. \<not>c dvd coeff b i" by (subst (asm) const_poly_dvd_iff) blast
   3.250 +    have B: "\<forall>i. \<not>c dvd coeff b i \<longrightarrow> i \<le> degree b"
   3.251 +      by (auto intro: le_degree)
   3.252 +    have coeff_m: "\<not>c dvd coeff b m" unfolding m_def by (rule GreatestI_ex_nat[OF A B])
   3.253 +    have "i \<le> m" if "\<not>c dvd coeff b i" for i
   3.254 +      unfolding m_def by (rule Greatest_le_nat[OF that B])
   3.255 +    hence dvd_b: "c dvd coeff b i" if "i > m" for i using that by force
   3.256 +
   3.257 +    have "c dvd coeff a i" for i
   3.258 +    proof (induction i rule: nat_descend_induct[of "degree a"])
   3.259 +      case (base i)
   3.260 +      thus ?case by (simp add: coeff_eq_0)
   3.261 +    next
   3.262 +      case (descend i)
   3.263 +      let ?A = "{..i+m} - {i}"
   3.264 +      have "c dvd coeff (a * b) (i + m)" by (rule dvd)
   3.265 +      also have "coeff (a * b) (i + m) = (\<Sum>k\<le>i + m. coeff a k * coeff b (i + m - k))"
   3.266 +        by (simp add: coeff_mult)
   3.267 +      also have "{..i+m} = insert i ?A" by auto
   3.268 +      also have "(\<Sum>k\<in>\<dots>. coeff a k * coeff b (i + m - k)) =
   3.269 +                   coeff a i * coeff b m + (\<Sum>k\<in>?A. coeff a k * coeff b (i + m - k))"
   3.270 +        (is "_ = _ + ?S")
   3.271 +        by (subst sum.insert) simp_all
   3.272 +      finally have eq: "c dvd coeff a i * coeff b m + ?S" .
   3.273 +      moreover have "c dvd ?S"
   3.274 +      proof (rule dvd_sum)
   3.275 +        fix k assume k: "k \<in> {..i+m} - {i}"
   3.276 +        show "c dvd coeff a k * coeff b (i + m - k)"
   3.277 +        proof (cases "k < i")
   3.278 +          case False
   3.279 +          with k have "c dvd coeff a k" by (intro descend.IH) simp
   3.280 +          thus ?thesis by simp
   3.281 +        next
   3.282 +          case True
   3.283 +          hence "c dvd coeff b (i + m - k)" by (intro dvd_b) simp
   3.284 +          thus ?thesis by simp
   3.285 +        qed
   3.286 +      qed
   3.287 +      ultimately have "c dvd coeff a i * coeff b m"
   3.288 +        by (simp add: dvd_add_left_iff)
   3.289 +      with assms coeff_m show "c dvd coeff a i"
   3.290 +        by (simp add: prime_elem_dvd_mult_iff)
   3.291 +    qed
   3.292 +    hence "[:c:] dvd a" by (subst const_poly_dvd_iff) blast
   3.293 +  }
   3.294 +  then show "[:c:] dvd a \<or> [:c:] dvd b" by blast
   3.295 +next
   3.296 +  from assms show "[:c:] \<noteq> 0" and "\<not> [:c:] dvd 1"
   3.297 +    by (simp_all add: prime_elem_def is_unit_const_poly_iff)
   3.298 +qed
   3.299 +
   3.300 +lemma prime_elem_const_poly_iff:
   3.301 +  fixes c :: "'a :: semidom"
   3.302 +  shows   "prime_elem [:c:] \<longleftrightarrow> prime_elem c"
   3.303 +proof
   3.304 +  assume A: "prime_elem [:c:]"
   3.305 +  show "prime_elem c"
   3.306 +  proof (rule prime_elemI)
   3.307 +    fix a b assume "c dvd a * b"
   3.308 +    hence "[:c:] dvd [:a:] * [:b:]" by (simp add: mult_ac)
   3.309 +    from A and this have "[:c:] dvd [:a:] \<or> [:c:] dvd [:b:]" by (rule prime_elem_dvd_multD)
   3.310 +    thus "c dvd a \<or> c dvd b" by simp
   3.311 +  qed (insert A, auto simp: prime_elem_def is_unit_poly_iff)
   3.312 +qed (auto intro: lift_prime_elem_poly)
   3.313 +
   3.314 +
   3.315 +subsection \<open>Content and primitive part of a polynomial\<close>
   3.316 +
   3.317 +definition content :: "'a::semiring_gcd poly \<Rightarrow> 'a"
   3.318 +  where "content p = gcd_list (coeffs p)"
   3.319 +
   3.320 +lemma content_eq_fold_coeffs [code]: "content p = fold_coeffs gcd p 0"
   3.321 +  by (simp add: content_def Gcd_fin.set_eq_fold fold_coeffs_def foldr_fold fun_eq_iff ac_simps)
   3.322 +
   3.323 +lemma content_0 [simp]: "content 0 = 0"
   3.324 +  by (simp add: content_def)
   3.325 +
   3.326 +lemma content_1 [simp]: "content 1 = 1"
   3.327 +  by (simp add: content_def)
   3.328 +
   3.329 +lemma content_const [simp]: "content [:c:] = normalize c"
   3.330 +  by (simp add: content_def cCons_def)
   3.331 +
   3.332 +lemma const_poly_dvd_iff_dvd_content: "[:c:] dvd p \<longleftrightarrow> c dvd content p"
   3.333 +  for c :: "'a::semiring_gcd"
   3.334 +proof (cases "p = 0")
   3.335 +  case True
   3.336 +  then show ?thesis by simp
   3.337 +next
   3.338 +  case False
   3.339 +  have "[:c:] dvd p \<longleftrightarrow> (\<forall>n. c dvd coeff p n)"
   3.340 +    by (rule const_poly_dvd_iff)
   3.341 +  also have "\<dots> \<longleftrightarrow> (\<forall>a\<in>set (coeffs p). c dvd a)"
   3.342 +  proof safe
   3.343 +    fix n :: nat
   3.344 +    assume "\<forall>a\<in>set (coeffs p). c dvd a"
   3.345 +    then show "c dvd coeff p n"
   3.346 +      by (cases "n \<le> degree p") (auto simp: coeff_eq_0 coeffs_def split: if_splits)
   3.347 +  qed (auto simp: coeffs_def simp del: upt_Suc split: if_splits)
   3.348 +  also have "\<dots> \<longleftrightarrow> c dvd content p"
   3.349 +    by (simp add: content_def dvd_Gcd_fin_iff dvd_mult_unit_iff)
   3.350 +  finally show ?thesis .
   3.351 +qed
   3.352 +
   3.353 +lemma content_dvd [simp]: "[:content p:] dvd p"
   3.354 +  by (subst const_poly_dvd_iff_dvd_content) simp_all
   3.355 +
   3.356 +lemma content_dvd_coeff [simp]: "content p dvd coeff p n"
   3.357 +proof (cases "p = 0")
   3.358 +  case True
   3.359 +  then show ?thesis
   3.360 +    by simp
   3.361 +next
   3.362 +  case False
   3.363 +  then show ?thesis
   3.364 +    by (cases "n \<le> degree p")
   3.365 +      (auto simp add: content_def not_le coeff_eq_0 coeff_in_coeffs intro: Gcd_fin_dvd)
   3.366 +qed
   3.367 +
   3.368 +lemma content_dvd_coeffs: "c \<in> set (coeffs p) \<Longrightarrow> content p dvd c"
   3.369 +  by (simp add: content_def Gcd_fin_dvd)
   3.370 +
   3.371 +lemma normalize_content [simp]: "normalize (content p) = content p"
   3.372 +  by (simp add: content_def)
   3.373 +
   3.374 +lemma is_unit_content_iff [simp]: "is_unit (content p) \<longleftrightarrow> content p = 1"
   3.375 +proof
   3.376 +  assume "is_unit (content p)"
   3.377 +  then have "normalize (content p) = 1" by (simp add: is_unit_normalize del: normalize_content)
   3.378 +  then show "content p = 1" by simp
   3.379 +qed auto
   3.380 +
   3.381 +lemma content_smult [simp]: "content (smult c p) = normalize c * content p"
   3.382 +  by (simp add: content_def coeffs_smult Gcd_fin_mult)
   3.383 +
   3.384 +lemma content_eq_zero_iff [simp]: "content p = 0 \<longleftrightarrow> p = 0"
   3.385 +  by (auto simp: content_def simp: poly_eq_iff coeffs_def)
   3.386 +
   3.387 +definition primitive_part :: "'a :: semiring_gcd poly \<Rightarrow> 'a poly"
   3.388 +  where "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   3.389 +
   3.390 +lemma primitive_part_0 [simp]: "primitive_part 0 = 0"
   3.391 +  by (simp add: primitive_part_def)
   3.392 +
   3.393 +lemma content_times_primitive_part [simp]: "smult (content p) (primitive_part p) = p"
   3.394 +  for p :: "'a :: semiring_gcd poly"
   3.395 +proof (cases "p = 0")
   3.396 +  case True
   3.397 +  then show ?thesis by simp
   3.398 +next
   3.399 +  case False
   3.400 +  then show ?thesis
   3.401 +  unfolding primitive_part_def
   3.402 +  by (auto simp: smult_conv_map_poly map_poly_map_poly o_def content_dvd_coeffs
   3.403 +      intro: map_poly_idI)
   3.404 +qed
   3.405 +
   3.406 +lemma primitive_part_eq_0_iff [simp]: "primitive_part p = 0 \<longleftrightarrow> p = 0"
   3.407 +proof (cases "p = 0")
   3.408 +  case True
   3.409 +  then show ?thesis by simp
   3.410 +next
   3.411 +  case False
   3.412 +  then have "primitive_part p = map_poly (\<lambda>x. x div content p) p"
   3.413 +    by (simp add:  primitive_part_def)
   3.414 +  also from False have "\<dots> = 0 \<longleftrightarrow> p = 0"
   3.415 +    by (intro map_poly_eq_0_iff) (auto simp: dvd_div_eq_0_iff content_dvd_coeffs)
   3.416 +  finally show ?thesis
   3.417 +    using False by simp
   3.418 +qed
   3.419 +
   3.420 +lemma content_primitive_part [simp]:
   3.421 +  assumes "p \<noteq> 0"
   3.422 +  shows "content (primitive_part p) = 1"
   3.423 +proof -
   3.424 +  have "p = smult (content p) (primitive_part p)"
   3.425 +    by simp
   3.426 +  also have "content \<dots> = content (primitive_part p) * content p"
   3.427 +    by (simp del: content_times_primitive_part add: ac_simps)
   3.428 +  finally have "1 * content p = content (primitive_part p) * content p"
   3.429 +    by simp
   3.430 +  then have "1 * content p div content p = content (primitive_part p) * content p div content p"
   3.431 +    by simp
   3.432 +  with assms show ?thesis
   3.433 +    by simp
   3.434 +qed
   3.435 +
   3.436 +lemma content_decompose:
   3.437 +  obtains p' :: "'a::semiring_gcd poly" where "p = smult (content p) p'" "content p' = 1"
   3.438 +proof (cases "p = 0")
   3.439 +  case True
   3.440 +  then show ?thesis by (intro that[of 1]) simp_all
   3.441 +next
   3.442 +  case False
   3.443 +  from content_dvd[of p] obtain r where r: "p = [:content p:] * r"
   3.444 +    by (rule dvdE)
   3.445 +  have "content p * 1 = content p * content r"
   3.446 +    by (subst r) simp
   3.447 +  with False have "content r = 1"
   3.448 +    by (subst (asm) mult_left_cancel) simp_all
   3.449 +  with r show ?thesis
   3.450 +    by (intro that[of r]) simp_all
   3.451 +qed
   3.452 +
   3.453 +lemma content_dvd_contentI [intro]: "p dvd q \<Longrightarrow> content p dvd content q"
   3.454 +  using const_poly_dvd_iff_dvd_content content_dvd dvd_trans by blast
   3.455 +
   3.456 +lemma primitive_part_const_poly [simp]: "primitive_part [:x:] = [:unit_factor x:]"
   3.457 +  by (simp add: primitive_part_def map_poly_pCons)
   3.458 +
   3.459 +lemma primitive_part_prim: "content p = 1 \<Longrightarrow> primitive_part p = p"
   3.460 +  by (auto simp: primitive_part_def)
   3.461 +
   3.462 +lemma degree_primitive_part [simp]: "degree (primitive_part p) = degree p"
   3.463 +proof (cases "p = 0")
   3.464 +  case True
   3.465 +  then show ?thesis by simp
   3.466 +next
   3.467 +  case False
   3.468 +  have "p = smult (content p) (primitive_part p)"
   3.469 +    by simp
   3.470 +  also from False have "degree \<dots> = degree (primitive_part p)"
   3.471 +    by (subst degree_smult_eq) simp_all
   3.472 +  finally show ?thesis ..
   3.473 +qed
   3.474 +
   3.475 +lemma smult_content_normalize_primitive_part [simp]:
   3.476 +  "smult (content p) (normalize (primitive_part p)) = normalize p"
   3.477 +proof -
   3.478 +  have "smult (content p) (normalize (primitive_part p)) =
   3.479 +      normalize ([:content p:] * primitive_part p)"
   3.480 +    by (subst normalize_mult) (simp_all add: normalize_const_poly)
   3.481 +  also have "[:content p:] * primitive_part p = p" by simp
   3.482 +  finally show ?thesis .
   3.483 +qed
   3.484 +
   3.485 +lemma content_mult:
   3.486 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   3.487 +  shows "content (p * q) = content p * content q"
   3.488 +proof -
   3.489 +  from content_decompose[of p] guess p' . note p = this
   3.490 +  from content_decompose[of q] guess q' . note q = this
   3.491 +  have "content (p * q) = content p * content q * content (p' * q')"
   3.492 +    by (subst p, subst q) (simp add: mult_ac normalize_mult)
   3.493 +  also have "content (p' * q') = 1"
   3.494 +  proof (cases "p' * q' = 0")
   3.495 +    case True
   3.496 +    with \<open>content p' = 1\<close> \<open>content q' = 1\<close> show ?thesis
   3.497 +      by auto
   3.498 +  next  
   3.499 +    case False
   3.500 +    from \<open>content p' = 1\<close> \<open>content q' = 1\<close>
   3.501 +    have "p' \<noteq> 0" "q' \<noteq> 0"
   3.502 +      by auto
   3.503 +    then have "p' * q' \<noteq> 0"
   3.504 +      by auto
   3.505 +    have "is_unit (content (p' * q'))"
   3.506 +    proof (rule ccontr)      
   3.507 +      assume "\<not> is_unit (content (p' * q'))"
   3.508 +      with False have "\<exists>p. p dvd content (p' * q') \<and> prime p"
   3.509 +        by (intro prime_divisor_exists) simp_all
   3.510 +      then obtain p where "p dvd content (p' * q')" "prime p"
   3.511 +        by blast
   3.512 +      from \<open>p dvd content (p' * q')\<close> have "[:p:] dvd p' * q'"
   3.513 +        by (simp add: const_poly_dvd_iff_dvd_content)
   3.514 +      moreover from \<open>prime p\<close> have "prime_elem [:p:]"
   3.515 +        by (simp add: lift_prime_elem_poly)
   3.516 +      ultimately have "[:p:] dvd p' \<or> [:p:] dvd q'"
   3.517 +        by (simp add: prime_elem_dvd_mult_iff)
   3.518 +      with \<open>content p' = 1\<close> \<open>content q' = 1\<close> have "is_unit p"
   3.519 +        by (simp add: const_poly_dvd_iff_dvd_content)
   3.520 +      with \<open>prime p\<close> show False
   3.521 +        by simp
   3.522 +    qed    
   3.523 +    then have "normalize (content (p' * q')) = 1"
   3.524 +      by (simp add: is_unit_normalize del: normalize_content)
   3.525 +    then show ?thesis
   3.526 +      by simp
   3.527 +  qed
   3.528 +  finally show ?thesis
   3.529 +    by simp
   3.530 +qed
   3.531 +
   3.532 +lemma primitive_part_mult:
   3.533 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   3.534 +  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
   3.535 +proof -
   3.536 +  have "primitive_part (p * q) = p * q div [:content (p * q):]"
   3.537 +    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   3.538 +  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
   3.539 +    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
   3.540 +  also have "\<dots> = primitive_part p * primitive_part q"
   3.541 +    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
   3.542 +  finally show ?thesis .
   3.543 +qed
   3.544 +
   3.545 +lemma primitive_part_smult:
   3.546 +  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   3.547 +  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
   3.548 +proof -
   3.549 +  have "smult a p = [:a:] * p" by simp
   3.550 +  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
   3.551 +    by (subst primitive_part_mult) simp_all
   3.552 +  finally show ?thesis .
   3.553 +qed  
   3.554 +
   3.555 +lemma primitive_part_dvd_primitive_partI [intro]:
   3.556 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
   3.557 +  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
   3.558 +  by (auto elim!: dvdE simp: primitive_part_mult)
   3.559 +
   3.560 +lemma content_prod_mset: 
   3.561 +  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
   3.562 +  shows "content (prod_mset A) = prod_mset (image_mset content A)"
   3.563 +  by (induction A) (simp_all add: content_mult mult_ac)
   3.564 +
   3.565 +lemma content_prod_eq_1_iff: 
   3.566 +  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   3.567 +  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
   3.568 +proof safe
   3.569 +  assume A: "content (p * q) = 1"
   3.570 +  {
   3.571 +    fix p q :: "'a poly" assume "content p * content q = 1"
   3.572 +    hence "1 = content p * content q" by simp
   3.573 +    hence "content p dvd 1" by (rule dvdI)
   3.574 +    hence "content p = 1" by simp
   3.575 +  } note B = this
   3.576 +  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
   3.577 +    by (simp_all add: content_mult mult_ac)
   3.578 +qed (auto simp: content_mult)
   3.579 +
   3.580 +
   3.581  no_notation cCons (infixr "##" 65)
   3.582  
   3.583  end
     4.1 --- a/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:20 2017 +0200
     4.2 +++ b/src/HOL/Computational_Algebra/Polynomial_Factorial.thy	Sun Oct 08 22:28:21 2017 +0200
     4.3 @@ -1,61 +1,20 @@
     4.4  (*  Title:      HOL/Computational_Algebra/Polynomial_Factorial.thy
     4.5 -    Author:     Brian Huffman
     4.6 -    Author:     Clemens Ballarin
     4.7 -    Author:     Amine Chaieb
     4.8 -    Author:     Florian Haftmann
     4.9      Author:     Manuel Eberl
    4.10  *)
    4.11  
    4.12 +section \<open>Polynomials, fractions and rings\<close>
    4.13 +
    4.14  theory Polynomial_Factorial
    4.15  imports 
    4.16    Complex_Main
    4.17    Polynomial
    4.18    Normalized_Fraction
    4.19 -  Field_as_Ring
    4.20  begin
    4.21  
    4.22 -subsection \<open>Various facts about polynomials\<close>
    4.23 -
    4.24 -lemma prod_mset_const_poly: " (\<Prod>x\<in>#A. [:f x:]) = [:prod_mset (image_mset f A):]"
    4.25 -  by (induct A) (simp_all add: ac_simps)
    4.26 -
    4.27 -lemma irreducible_const_poly_iff:
    4.28 -  fixes c :: "'a :: {comm_semiring_1,semiring_no_zero_divisors}"
    4.29 -  shows "irreducible [:c:] \<longleftrightarrow> irreducible c"
    4.30 -proof
    4.31 -  assume A: "irreducible c"
    4.32 -  show "irreducible [:c:]"
    4.33 -  proof (rule irreducibleI)
    4.34 -    fix a b assume ab: "[:c:] = a * b"
    4.35 -    hence "degree [:c:] = degree (a * b)" by (simp only: )
    4.36 -    also from A ab have "a \<noteq> 0" "b \<noteq> 0" by auto
    4.37 -    hence "degree (a * b) = degree a + degree b" by (simp add: degree_mult_eq)
    4.38 -    finally have "degree a = 0" "degree b = 0" by auto
    4.39 -    then obtain a' b' where ab': "a = [:a':]" "b = [:b':]" by (auto elim!: degree_eq_zeroE)
    4.40 -    from ab have "coeff [:c:] 0 = coeff (a * b) 0" by (simp only: )
    4.41 -    hence "c = a' * b'" by (simp add: ab' mult_ac)
    4.42 -    from A and this have "a' dvd 1 \<or> b' dvd 1" by (rule irreducibleD)
    4.43 -    with ab' show "a dvd 1 \<or> b dvd 1"
    4.44 -      by (auto simp add: is_unit_const_poly_iff)
    4.45 -  qed (insert A, auto simp: irreducible_def is_unit_poly_iff)
    4.46 -next
    4.47 -  assume A: "irreducible [:c:]"
    4.48 -  then have "c \<noteq> 0" and "\<not> c dvd 1"
    4.49 -    by (auto simp add: irreducible_def is_unit_const_poly_iff)
    4.50 -  then show "irreducible c"
    4.51 -  proof (rule irreducibleI)
    4.52 -    fix a b assume ab: "c = a * b"
    4.53 -    hence "[:c:] = [:a:] * [:b:]" by (simp add: mult_ac)
    4.54 -    from A and this have "[:a:] dvd 1 \<or> [:b:] dvd 1" by (rule irreducibleD)
    4.55 -    then show "a dvd 1 \<or> b dvd 1"
    4.56 -      by (auto simp add: is_unit_const_poly_iff)
    4.57 -  qed
    4.58 -qed
    4.59 -
    4.60 -
    4.61  subsection \<open>Lifting elements into the field of fractions\<close>
    4.62  
    4.63 -definition to_fract :: "'a :: idom \<Rightarrow> 'a fract" where "to_fract x = Fract x 1"
    4.64 +definition to_fract :: "'a :: idom \<Rightarrow> 'a fract"
    4.65 +  where "to_fract x = Fract x 1"
    4.66    \<comment> \<open>FIXME: name \<open>of_idom\<close>, abbreviation\<close>
    4.67  
    4.68  lemma to_fract_0 [simp]: "to_fract 0 = 0"
    4.69 @@ -429,39 +388,6 @@
    4.70    finally show ?thesis by simp
    4.71  qed
    4.72  
    4.73 -lemma primitive_part_mult:
    4.74 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
    4.75 -  shows "primitive_part (p * q) = primitive_part p * primitive_part q"
    4.76 -proof -
    4.77 -  have "primitive_part (p * q) = p * q div [:content (p * q):]"
    4.78 -    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
    4.79 -  also have "\<dots> = (p div [:content p:]) * (q div [:content q:])"
    4.80 -    by (subst div_mult_div_if_dvd) (simp_all add: content_mult mult_ac)
    4.81 -  also have "\<dots> = primitive_part p * primitive_part q"
    4.82 -    by (simp add: primitive_part_def div_const_poly_conv_map_poly)
    4.83 -  finally show ?thesis .
    4.84 -qed
    4.85 -
    4.86 -lemma primitive_part_smult:
    4.87 -  fixes p :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
    4.88 -  shows "primitive_part (smult a p) = smult (unit_factor a) (primitive_part p)"
    4.89 -proof -
    4.90 -  have "smult a p = [:a:] * p" by simp
    4.91 -  also have "primitive_part \<dots> = smult (unit_factor a) (primitive_part p)"
    4.92 -    by (subst primitive_part_mult) simp_all
    4.93 -  finally show ?thesis .
    4.94 -qed  
    4.95 -
    4.96 -lemma primitive_part_dvd_primitive_partI [intro]:
    4.97 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd, ring_gcd, idom_divide} poly"
    4.98 -  shows "p dvd q \<Longrightarrow> primitive_part p dvd primitive_part q"
    4.99 -  by (auto elim!: dvdE simp: primitive_part_mult)
   4.100 -
   4.101 -lemma content_prod_mset: 
   4.102 -  fixes A :: "'a :: {factorial_semiring, semiring_Gcd} poly multiset"
   4.103 -  shows "content (prod_mset A) = prod_mset (image_mset content A)"
   4.104 -  by (induction A) (simp_all add: content_mult mult_ac)
   4.105 -
   4.106  lemma fract_poly_dvdD:
   4.107    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   4.108    assumes "fract_poly p dvd fract_poly q" "content p = 1"
   4.109 @@ -481,104 +407,80 @@
   4.110    thus ?thesis by (rule dvdI)
   4.111  qed
   4.112  
   4.113 -lemma content_prod_eq_1_iff: 
   4.114 -  fixes p q :: "'a :: {factorial_semiring, semiring_Gcd} poly"
   4.115 -  shows "content (p * q) = 1 \<longleftrightarrow> content p = 1 \<and> content q = 1"
   4.116 -proof safe
   4.117 -  assume A: "content (p * q) = 1"
   4.118 -  {
   4.119 -    fix p q :: "'a poly" assume "content p * content q = 1"
   4.120 -    hence "1 = content p * content q" by simp
   4.121 -    hence "content p dvd 1" by (rule dvdI)
   4.122 -    hence "content p = 1" by simp
   4.123 -  } note B = this
   4.124 -  from A B[of p q] B [of q p] show "content p = 1" "content q = 1" 
   4.125 -    by (simp_all add: content_mult mult_ac)
   4.126 -qed (auto simp: content_mult)
   4.127 -
   4.128  end
   4.129  
   4.130  
   4.131  subsection \<open>Polynomials over a field are a Euclidean ring\<close>
   4.132  
   4.133 -definition unit_factor_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
   4.134 -  "unit_factor_field_poly p = [:lead_coeff p:]"
   4.135 -
   4.136 -definition normalize_field_poly :: "'a :: field poly \<Rightarrow> 'a poly" where
   4.137 -  "normalize_field_poly p = smult (inverse (lead_coeff p)) p"
   4.138 -
   4.139 -definition euclidean_size_field_poly :: "'a :: field poly \<Rightarrow> nat" where
   4.140 -  "euclidean_size_field_poly p = (if p = 0 then 0 else 2 ^ degree p)" 
   4.141 -
   4.142 -lemma dvd_field_poly: "dvd.dvd (op * :: 'a :: field poly \<Rightarrow> _) = op dvd"
   4.143 -  by (intro ext) (simp_all add: dvd.dvd_def dvd_def)
   4.144 +context
   4.145 +begin
   4.146  
   4.147  interpretation field_poly: 
   4.148    unique_euclidean_ring where zero = "0 :: 'a :: field poly"
   4.149 -    and one = 1 and plus = plus and uminus = uminus and minus = minus
   4.150 +    and one = 1 and plus = plus
   4.151 +    and uminus = uminus and minus = minus
   4.152      and times = times
   4.153 -    and normalize = normalize_field_poly and unit_factor = unit_factor_field_poly
   4.154 -    and euclidean_size = euclidean_size_field_poly
   4.155 +    and normalize = "\<lambda>p. smult (inverse (lead_coeff p)) p"
   4.156 +    and unit_factor = "\<lambda>p. [:lead_coeff p:]"
   4.157 +    and euclidean_size = "\<lambda>p. if p = 0 then 0 else 2 ^ degree p"
   4.158      and uniqueness_constraint = top
   4.159      and divide = divide and modulo = modulo
   4.160 -proof (standard, unfold dvd_field_poly)
   4.161 -  fix p :: "'a poly"
   4.162 -  show "unit_factor_field_poly p * normalize_field_poly p = p"
   4.163 -    by (cases "p = 0") 
   4.164 -       (simp_all add: unit_factor_field_poly_def normalize_field_poly_def)
   4.165 -next
   4.166 -  fix p :: "'a poly" assume "is_unit p"
   4.167 -  then show "unit_factor_field_poly p = p"
   4.168 -    by (elim is_unit_polyE) (auto simp: unit_factor_field_poly_def monom_0 one_poly_def field_simps)
   4.169 -next
   4.170 -  fix p :: "'a poly" assume "p \<noteq> 0"
   4.171 -  thus "is_unit (unit_factor_field_poly p)"
   4.172 -    by (simp add: unit_factor_field_poly_def is_unit_pCons_iff)
   4.173 -next
   4.174 -  fix p q s :: "'a poly" assume "s \<noteq> 0"
   4.175 -  moreover assume "euclidean_size_field_poly p < euclidean_size_field_poly q"
   4.176 -  ultimately show "euclidean_size_field_poly (p * s) < euclidean_size_field_poly (q * s)"
   4.177 -    by (auto simp add: euclidean_size_field_poly_def degree_mult_eq)
   4.178 -next
   4.179 -  fix p q r :: "'a poly" assume "p \<noteq> 0"
   4.180 -  moreover assume "euclidean_size_field_poly r < euclidean_size_field_poly p"
   4.181 -  ultimately show "(q * p + r) div p = q"
   4.182 -    by (cases "r = 0")
   4.183 -      (auto simp add: unit_factor_field_poly_def euclidean_size_field_poly_def div_poly_less)
   4.184 -qed (auto simp: unit_factor_field_poly_def normalize_field_poly_def lead_coeff_mult 
   4.185 -       euclidean_size_field_poly_def Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
   4.186 +  rewrites "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
   4.187 +    and "comm_monoid_mult.prod_mset times 1 = prod_mset"
   4.188 +    and "comm_semiring_1.irreducible times 1 0 = irreducible"
   4.189 +    and "comm_semiring_1.prime_elem times 1 0 = prime_elem"
   4.190 +proof -
   4.191 +  show "dvd.dvd (times :: 'a poly \<Rightarrow> _) = Rings.dvd"
   4.192 +    by (simp add: dvd_dict)
   4.193 +  show "comm_monoid_mult.prod_mset times 1 = prod_mset"
   4.194 +    by (simp add: prod_mset_dict)
   4.195 +  show "comm_semiring_1.irreducible times 1 0 = irreducible"
   4.196 +    by (simp add: irreducible_dict)
   4.197 +  show "comm_semiring_1.prime_elem times 1 0 = prime_elem"
   4.198 +    by (simp add: prime_elem_dict)
   4.199 +  show "class.unique_euclidean_ring divide plus minus (0 :: 'a poly) times 1 modulo
   4.200 +    (\<lambda>p. [:lead_coeff p:]) (\<lambda>p. smult (inverse (lead_coeff p)) p)
   4.201 +    (\<lambda>p. if p = 0 then 0 else 2 ^ degree p) uminus top"
   4.202 +  proof (standard, fold dvd_dict)
   4.203 +    fix p :: "'a poly"
   4.204 +    show "[:lead_coeff p:] * smult (inverse (lead_coeff p)) p = p"
   4.205 +      by (cases "p = 0") simp_all
   4.206 +  next
   4.207 +    fix p :: "'a poly" assume "is_unit p"
   4.208 +    then show "[:lead_coeff p:] = p"
   4.209 +      by (elim is_unit_polyE) (auto simp: monom_0 one_poly_def field_simps)
   4.210 +  next
   4.211 +    fix p :: "'a poly" assume "p \<noteq> 0"
   4.212 +    then show "is_unit [:lead_coeff p:]"
   4.213 +      by (simp add: is_unit_pCons_iff)
   4.214 +  next
   4.215 +    fix p q s :: "'a poly" assume "s \<noteq> 0"
   4.216 +    moreover assume "(if p = 0 then (0::nat) else 2 ^ degree p) < (if q = 0 then 0 else 2 ^ degree q)"
   4.217 +    ultimately show "(if p * s = 0 then (0::nat) else 2 ^ degree (p * s)) < (if q * s = 0 then 0 else 2 ^ degree (q * s))"
   4.218 +      by (auto simp add: degree_mult_eq)
   4.219 +  next
   4.220 +    fix p q r :: "'a poly" assume "p \<noteq> 0"
   4.221 +    moreover assume "(if r = 0 then (0::nat) else 2 ^ degree r)
   4.222 +    < (if p = 0 then 0 else 2 ^ degree p)"
   4.223 +    ultimately show "(q * p + r) div p = q"
   4.224 +      by (cases "r = 0") (auto simp add: div_poly_less)
   4.225 +  qed (auto simp: lead_coeff_mult Rings.div_mult_mod_eq intro!: degree_mod_less' degree_mult_right_le)
   4.226 +qed
   4.227  
   4.228  lemma field_poly_irreducible_imp_prime:
   4.229 -  assumes "irreducible (p :: 'a :: field poly)"
   4.230 -  shows   "prime_elem p"
   4.231 -proof -
   4.232 -  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   4.233 -  from field_poly.irreducible_imp_prime_elem[of p] assms
   4.234 -    show ?thesis unfolding irreducible_def prime_elem_def dvd_field_poly
   4.235 -      comm_semiring_1.irreducible_def[OF A] comm_semiring_1.prime_elem_def[OF A] by blast
   4.236 -qed
   4.237 +  "prime_elem p" if "irreducible p" for p :: "'a :: field poly"
   4.238 +  using that by (fact field_poly.irreducible_imp_prime_elem)
   4.239  
   4.240  lemma field_poly_prod_mset_prime_factorization:
   4.241 -  assumes "(x :: 'a :: field poly) \<noteq> 0"
   4.242 -  shows   "prod_mset (field_poly.prime_factorization x) = normalize_field_poly x"
   4.243 -proof -
   4.244 -  have A: "class.comm_monoid_mult op * (1 :: 'a poly)" ..
   4.245 -  have "comm_monoid_mult.prod_mset op * (1 :: 'a poly) = prod_mset"
   4.246 -    by (intro ext) (simp add: comm_monoid_mult.prod_mset_def[OF A] prod_mset_def)
   4.247 -  with field_poly.prod_mset_prime_factorization[OF assms] show ?thesis by simp
   4.248 -qed
   4.249 +  "prod_mset (field_poly.prime_factorization p) = smult (inverse (lead_coeff p)) p"
   4.250 +  if "p \<noteq> 0" for p :: "'a :: field poly"
   4.251 +  using that by (fact field_poly.prod_mset_prime_factorization)
   4.252  
   4.253  lemma field_poly_in_prime_factorization_imp_prime:
   4.254 -  assumes "(p :: 'a :: field poly) \<in># field_poly.prime_factorization x"
   4.255 -  shows   "prime_elem p"
   4.256 -proof -
   4.257 -  have A: "class.comm_semiring_1 op * 1 op + (0 :: 'a poly)" ..
   4.258 -  have B: "class.normalization_semidom op div op + op - (0 :: 'a poly) op * 1 
   4.259 -             unit_factor_field_poly normalize_field_poly" ..
   4.260 -  from field_poly.in_prime_factors_imp_prime [of p x] assms
   4.261 -    show ?thesis unfolding prime_elem_def dvd_field_poly
   4.262 -      comm_semiring_1.prime_elem_def[OF A] normalization_semidom.prime_def[OF B] by blast
   4.263 -qed
   4.264 +  "prime_elem p" if "p \<in># field_poly.prime_factorization x"
   4.265 +  for p :: "'a :: field poly"
   4.266 +  by (rule field_poly.prime_imp_prime_elem, rule field_poly.in_prime_factors_imp_prime)
   4.267 +    (fact that)
   4.268  
   4.269  
   4.270  subsection \<open>Primality and irreducibility in polynomial rings\<close>
   4.271 @@ -658,9 +560,6 @@
   4.272    qed
   4.273  qed
   4.274  
   4.275 -context
   4.276 -begin
   4.277 -
   4.278  private lemma irreducible_imp_prime_poly:
   4.279    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   4.280    assumes "irreducible p"
   4.281 @@ -686,7 +585,6 @@
   4.282    qed (insert assms, auto simp: irreducible_def)
   4.283  qed
   4.284  
   4.285 -
   4.286  lemma degree_primitive_part_fract [simp]:
   4.287    "degree (primitive_part_fract p) = degree p"
   4.288  proof -
   4.289 @@ -749,14 +647,9 @@
   4.290    shows "b \<noteq> 0 \<Longrightarrow> coprime a b \<Longrightarrow> prime_elem [:a,b:]"
   4.291    by (rule irreducible_imp_prime_poly, rule irreducible_linear_poly)
   4.292  
   4.293 -end
   4.294 -
   4.295   
   4.296  subsection \<open>Prime factorisation of polynomials\<close>   
   4.297  
   4.298 -context
   4.299 -begin 
   4.300 -
   4.301  private lemma poly_prime_factorization_exists_content_1:
   4.302    fixes p :: "'a :: {factorial_semiring,semiring_Gcd,ring_gcd,idom_divide} poly"
   4.303    assumes "p \<noteq> 0" "content p = 1"
   4.304 @@ -775,11 +668,12 @@
   4.305    finally have content_e: "content e = 1"
   4.306      by simp    
   4.307    
   4.308 -  have "fract_poly p = unit_factor_field_poly (fract_poly p) * 
   4.309 -          normalize_field_poly (fract_poly p)" by simp
   4.310 -  also have "unit_factor_field_poly (fract_poly p) = [:to_fract (lead_coeff p):]" 
   4.311 -    by (simp add: unit_factor_field_poly_def monom_0 degree_map_poly coeff_map_poly)
   4.312 -  also from assms have "normalize_field_poly (fract_poly p) = prod_mset ?P" 
   4.313 +  from \<open>p \<noteq> 0\<close> have "fract_poly p = [:lead_coeff (fract_poly p):] * 
   4.314 +    smult (inverse (lead_coeff (fract_poly p))) (fract_poly p)"
   4.315 +    by simp 
   4.316 +  also have "[:lead_coeff (fract_poly p):] = [:to_fract (lead_coeff p):]" 
   4.317 +    by (simp add: monom_0 degree_map_poly coeff_map_poly)
   4.318 +  also from assms have "smult (inverse (lead_coeff (fract_poly p))) (fract_poly p) = prod_mset ?P" 
   4.319      by (subst field_poly_prod_mset_prime_factorization) simp_all
   4.320    also have "\<dots> = prod_mset (image_mset id ?P)" by simp
   4.321    also have "image_mset id ?P = 
     5.1 --- a/src/HOL/ROOT	Sun Oct 08 22:28:20 2017 +0200
     5.2 +++ b/src/HOL/ROOT	Sun Oct 08 22:28:21 2017 +0200
     5.3 @@ -71,7 +71,6 @@
     5.4      Computational_Algebra
     5.5      (*conflicting type class instantiations and dependent applications*)
     5.6      Field_as_Ring
     5.7 -    Polynomial_Factorial
     5.8  
     5.9  session "HOL-Hahn_Banach" in Hahn_Banach = "HOL-Library" +
    5.10    description {*