Quellcode-Bibliothek

^© Kompilation durch diese Firma

[Weder Korrektheit noch Funktionsfähigkeit der Software werden zugesichert.]

Datei: matrices.pvs Sprache: Isabelle

Original von: Isabelle^©

(*  Title:      HOL/Algebra/Polynomial_Divisibility.thy
    Author:     Paulo Emílio de Vilhena
*)

theory Polynomial_Divisibility
  imports Polynomials Embedded_Algebras "HOL-Library.Multiset"

begin

section \<open>Divisibility of Polynomials\<close>

subsection \<open>Definitions\<close>

abbreviation poly_ring :: "_ \ ('a list) ring"
  where "poly_ring R \ univ_poly R (carrier R)"

abbreviation pirreducible :: "_ \ 'a set \ 'a list \ bool" ("pirreducible\")
  where "pirreducible\<^bsub>R\<^esub> K p \ ring_irreducible\<^bsub>(univ_poly R K)\<^esub> p"

abbreviation pprime :: "_ \ 'a set \ 'a list \ bool" ("pprime\")
  where "pprime\<^bsub>R\<^esub> K p \ ring_prime\<^bsub>(univ_poly R K)\<^esub> p"

definition pdivides :: "_ \ 'a list \ 'a list \ bool" (infix "pdivides\" 65)
  where "p pdivides\<^bsub>R\<^esub> q = p divides\<^bsub>(univ_poly R (carrier R))\<^esub> q"

definition rupture :: "_ \ 'a set \ 'a list \ (('a list) set) ring" ("Rupt\")
  where "Rupt\<^bsub>R\<^esub> K p = (K[X]\<^bsub>R\<^esub>) Quot (PIdl\<^bsub>K[X]\<^bsub>R\<^esub>\<^esub> p)"

abbreviation (in ring) rupture_surj :: "'a set \ 'a list \ 'a list \ ('a list) set"
  where "rupture_surj K p \ (\q. (PIdl\<^bsub>K[X]\<^esub> p) +>\<^bsub>K[X]\<^esub> q)"

subsection \<open>Basic Properties\<close>

lemma (in ring) carrier_polynomial_shell [intro]:
  assumes "subring K R" and "p \ carrier (K[X])" shows "p \ carrier (poly_ring R)"
  using carrier_polynomial[OF assms(1), of p] assms(2) unfolding sym[OF univ_poly_carrier] by simp

lemma (in domain) pdivides_zero:
  assumes "subring K R" and "p \ carrier (K[X])" shows "p pdivides []"
  using ring.divides_zero[OF univ_poly_is_ring[OF carrier_is_subring]
         carrier_polynomial_shell[OF assms]]
  unfolding univ_poly_zero pdivides_def .

lemma (in domain) zero_pdivides_zero: "[] pdivides []"
  using pdivides_zero[OF carrier_is_subring] univ_poly_carrier by blast

lemma (in domain) zero_pdivides:
  shows "[] pdivides p \ p = []"
  using ring.zero_divides[OF univ_poly_is_ring[OF carrier_is_subring]]
  unfolding univ_poly_zero pdivides_def .

lemma (in domain) pprime_iff_pirreducible:
  assumes "subfield K R" and "p \ carrier (K[X])"
  shows "pprime K p \ pirreducible K p"
  using principal_domain.primeness_condition[OF univ_poly_is_principal] assms by simp

lemma (in domain) pirreducibleE:
  assumes "subring K R" "p \ carrier (K[X])" "pirreducible K p"
  shows "p \ []" "p \ Units (K[X])"
    and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \
                 p = q \<otimes>\<^bsub>K[X]\<^esub> r \<Longrightarrow> q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
  using domain.ring_irreducibleE[OF univ_poly_is_domain[OF assms(1)] _ assms(3)] assms(2)
  by (auto simp add: univ_poly_zero)

lemma (in domain) pirreducibleI:
  assumes "subring K R" "p \ carrier (K[X])" "p \ []" "p \ Units (K[X])"
    and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \
                 p = q \<otimes>\<^bsub>K[X]\<^esub> r \<Longrightarrow> q \<in> Units (K[X]) \<or> r \<in> Units (K[X])"
  shows "pirreducible K p"
  using domain.ring_irreducibleI[OF univ_poly_is_domain[OF assms(1)] _ assms(4)] assms(2-3,5)
  by (auto simp add: univ_poly_zero)

lemma (in domain) univ_poly_carrier_units_incl:
  shows "Units ((carrier R) [X]) \ { [ k ] | k. k \ carrier R - { \ } }"
proof
  fix p assume "p \ Units ((carrier R) [X])"
  then obtain q
    where p: "polynomial (carrier R) p" and q: "polynomial (carrier R) q" and pq: "poly_mult p q = [ \ ]"
    unfolding Units_def univ_poly_def by auto
  hence not_nil: "p \ []" and "q \ []"
    using poly_mult_integral[OF carrier_is_subring p q] poly_mult_zero[OF polynomial_incl[OF p]] by auto
  hence "degree p = 0"
    using poly_mult_degree_eq[OF carrier_is_subring p q] unfolding pq by simp
  hence "length p = 1"
    using not_nil by (metis One_nat_def Suc_pred length_greater_0_conv)
  then obtain k where k: "p = [ k ]"
    by (metis One_nat_def length_0_conv length_Suc_conv)
  hence "k \ carrier R - { \ }"
    using p unfolding polynomial_def by auto
  thus "p \ { [ k ] | k. k \ carrier R - { \ } }"
    unfolding k by blast
qed

lemma (in field) univ_poly_carrier_units:
  "Units ((carrier R) [X]) = { [ k ] | k. k \ carrier R - { \ } }"
proof
  show "Units ((carrier R) [X]) \ { [ k ] | k. k \ carrier R - { \ } }"
    using univ_poly_carrier_units_incl by simp
next
  show "{ [ k ] | k. k \ carrier R - { \ } } \ Units ((carrier R) [X])"
  proof (auto)
    fix k assume k: "k \ carrier R" "k \ \"
    hence inv_k: "inv k \ carrier R" "inv k \ \" and "k \ inv k = \" "inv k \ k = \"
      using subfield_m_inv[OF carrier_is_subfield, of k] by auto
    hence "poly_mult [ k ] [ inv k ] = [ \ ]" and "poly_mult [ inv k ] [ k ] = [ \ ]"
      by (auto simp add: k)
    moreover have "polynomial (carrier R) [ k ]" and "polynomial (carrier R) [ inv k ]"
      using const_is_polynomial k inv_k by auto
    ultimately show "[ k ] \ Units ((carrier R) [X])"
      unfolding Units_def univ_poly_def by (auto simp del: poly_mult.simps)
  qed
qed

lemma (in domain) univ_poly_units_incl:
  assumes "subring K R" shows "Units (K[X]) \ { [ k ] | k. k \ K - { \ } }"
  using domain.univ_poly_carrier_units_incl[OF subring_is_domain[OF assms]]
        univ_poly_consistent[OF assms] by auto

lemma (in ring) univ_poly_units:
  assumes "subfield K R" shows "Units (K[X]) = { [ k ] | k. k \ K - { \ } }"
  using field.univ_poly_carrier_units[OF subfield_iff(2)[OF assms]]
        univ_poly_consistent[OF subfieldE(1)[OF assms]] by auto

lemma (in domain) univ_poly_units':
  assumes "subfield K R" shows "p \ Units (K[X]) \ p \ carrier (K[X]) \ p \ [] \ degree p = 0"
  unfolding univ_poly_units[OF assms] sym[OF univ_poly_carrier] polynomial_def
  by (auto, metis hd_in_set le_0_eq le_Suc_eq length_0_conv length_Suc_conv list.sel(1) subsetD)

corollary (in domain) rupture_one_not_zero:
  assumes "subfield K R" and "p \ carrier (K[X])" and "degree p > 0"
  shows "\\<^bsub>Rupt K p\<^esub> \ \\<^bsub>Rupt K p\<^esub>"
proof (rule ccontr)
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  assume "\ \\<^bsub>Rupt K p\<^esub> \ \\<^bsub>Rupt K p\<^esub>"
  then have "PIdl\<^bsub>K[X]\<^esub> p +>\<^bsub>K[X]\<^esub> \\<^bsub>K[X]\<^esub> = PIdl\<^bsub>K[X]\<^esub> p"
    unfolding rupture_def FactRing_def by simp
  hence "\\<^bsub>K[X]\<^esub> \ PIdl\<^bsub>K[X]\<^esub> p"
    using ideal.rcos_const_imp_mem[OF UP.cgenideal_ideal[OF assms(2)]] by auto
  then obtain q where "q \ carrier (K[X])" and "\\<^bsub>K[X]\<^esub> = q \\<^bsub>K[X]\<^esub> p"
    using assms(2) unfolding cgenideal_def by auto
  hence "p \ Units (K[X])"
    unfolding Units_def using assms(2) UP.m_comm by auto
  hence "degree p = 0"
    unfolding univ_poly_units[OF assms(1)] by auto
  with \<open>degree p > 0\<close> show False
    by simp
qed

corollary (in ring) pirreducible_degree:
  assumes "subfield K R" "p \ carrier (K[X])" "pirreducible K p"
  shows "degree p \ 1"
proof (rule ccontr)
  assume "\ degree p \ 1" then have "length p \ 1"
    by simp
  moreover have "p \ []" and "p \ Units (K[X])"
    using assms(3) by (auto simp add: ring_irreducible_def irreducible_def univ_poly_zero)
  ultimately obtain k where k: "p = [ k ]"
    by (metis append_butlast_last_id butlast_take diff_is_0_eq le_refl self_append_conv2 take0 take_all)
  hence "k \ K" and "k \ \"
    using assms(2) by (auto simp add: polynomial_def univ_poly_def)
  hence "p \ Units (K[X])"
    using univ_poly_units[OF assms(1)] unfolding k by auto
  from \<open>p \<in> Units (K[X])\<close> and \<open>p \<notin> Units (K[X])\<close> show False by simp
qed

corollary (in domain) univ_poly_not_field:
  assumes "subring K R" shows "\ field (K[X])"
proof -
  have "X \ carrier (K[X]) - { \\<^bsub>(K[X])\<^esub> }" and "X \ { [ k ] | k. k \ K - { \ } }"
    using var_closed(1)[OF assms] unfolding univ_poly_zero var_def by auto
  thus ?thesis
    using field.field_Units[of "K[X]"] univ_poly_units_incl[OF assms] by blast
qed

lemma (in domain) rupture_is_field_iff_pirreducible:
  assumes "subfield K R" and "p \ carrier (K[X])"
  shows "field (Rupt K p) \ pirreducible K p"
proof
  assume "pirreducible K p" thus "field (Rupt K p)"
    using principal_domain.field_iff_prime[OF univ_poly_is_principal[OF assms(1)]] assms(2)
          pprime_iff_pirreducible[OF assms] pirreducibleE(1)[OF subfieldE(1)[OF assms(1)]]
    by (simp add: univ_poly_zero rupture_def)
next
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  assume field: "field (Rupt K p)"
  have "p \ []"
  proof (rule ccontr)
    assume "\ p \ []" then have p: "p = []"
      by simp
    hence "Rupt K p \ (K[X])"
      using UP.FactRing_zeroideal(1) UP.genideal_zero
            UP.cgenideal_eq_genideal[OF UP.zero_closed]
      by (simp add: rupture_def univ_poly_zero)
    then obtain h where h: "h \ ring_iso (Rupt K p) (K[X])"
      unfolding is_ring_iso_def by blast
    moreover have "ring (Rupt K p)"
      using field by (simp add: cring_def domain_def field_def)
    ultimately interpret R: ring_hom_ring "Rupt K p" "K[X]" h
      unfolding ring_hom_ring_def ring_hom_ring_axioms_def ring_iso_def
      using UP.ring_axioms by simp
    have "field (K[X])"
      using field.ring_iso_imp_img_field[OF field h] by simp
    thus False
      using univ_poly_not_field[OF subfieldE(1)[OF assms(1)]] by simp
  qed
  thus "pirreducible K p"
    using UP.field_iff_prime pprime_iff_pirreducible[OF assms] assms(2) field
    by (simp add: univ_poly_zero rupture_def)
qed

lemma (in domain) rupture_surj_hom:
  assumes "subring K R" and "p \ carrier (K[X])"
  shows "(rupture_surj K p) \ ring_hom (K[X]) (Rupt K p)"
    and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .
  interpret I: ideal "PIdl\<^bsub>K[X]\<^esub> p" "K[X]"
    using UP.cgenideal_ideal[OF assms(2)] .
  show "(rupture_surj K p) \ ring_hom (K[X]) (Rupt K p)"
   and "ring_hom_ring (K[X]) (Rupt K p) (rupture_surj K p)"
    using ring_hom_ring.intro[OF UP.ring_axioms I.quotient_is_ring] I.rcos_ring_hom
    unfolding symmetric[OF ring_hom_ring_axioms_def] rupture_def by auto
qed

corollary (in domain) rupture_surj_norm_is_hom:
  assumes "subring K R" and "p \ carrier (K[X])"
  shows "((rupture_surj K p) \ poly_of_const) \ ring_hom (R \ carrier := K \) (Rupt K p)"
  using ring_hom_trans[OF canonical_embedding_is_hom[OF assms(1)] rupture_surj_hom(1)[OF assms]] .

lemma (in domain) norm_map_in_poly_ring_carrier:
  assumes "p \ carrier (poly_ring R)" and "\a. a \ carrier R \ f a \ carrier (poly_ring R)"
  shows "ring.normalize (poly_ring R) (map f p) \ carrier (poly_ring (poly_ring R))"
proof -
  have "set p \ carrier R"
    using assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "set (map f p) \ carrier (poly_ring R)"
    using assms(2) by auto
  thus ?thesis
    using ring.normalize_gives_polynomial[OF univ_poly_is_ring[OF carrier_is_subring]]
    unfolding univ_poly_carrier by simp
qed

lemma (in domain) map_in_poly_ring_carrier:
  assumes "p \ carrier (poly_ring R)" and "\a. a \ carrier R \ f a \ carrier (poly_ring R)"
    and "\a. a \ \ \ f a \ []"
  shows "map f p \ carrier (poly_ring (poly_ring R))"
proof -
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .
  have "lead_coeff p \ \" if "p \ []"
    using that assms(1) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence "ring.normalize (poly_ring R) (map f p) = map f p"
    by (cases p) (simp_all add: assms(3) univ_poly_zero)
  thus ?thesis
    using norm_map_in_poly_ring_carrier[of p f] assms(1-2) by simp
qed

lemma (in domain) map_norm_in_poly_ring_carrier:
  assumes "subring K R" and "p \ carrier (K[X])"
  shows "map poly_of_const p \ carrier (poly_ring (K[X]))"
  using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]]
proof -
  have "\a. a \ K \ poly_of_const a \ carrier (K[X])"
   and "\a. a \ \ \ poly_of_const a \ []"
    using ring_hom_memE(1)[OF canonical_embedding_is_hom[OF assms(1)]]
    by (auto simp: poly_of_const_def)
  thus ?thesis
    using domain.map_in_poly_ring_carrier[OF subring_is_domain[OF assms(1)]] assms(2)
    unfolding univ_poly_consistent[OF assms(1)] by simp
qed

lemma (in domain) polynomial_rupture:
  assumes "subring K R" and "p \ carrier (K[X])"
  shows "(ring.eval (Rupt K p)) (map ((rupture_surj K p) \ poly_of_const) p) (rupture_surj K p X) = \\<^bsub>Rupt K p\<^esub>"
proof -
  let ?surj = "rupture_surj K p"

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .
  interpret Hom: ring_hom_ring "K[X]" "Rupt K p" ?surj
    using rupture_surj_hom(2)[OF assms] .

  have "(Hom.S.eval) (map (?surj \ poly_of_const) p) (?surj X) = ?surj ((UP.eval) (map poly_of_const p) X)"
    using Hom.eval_hom[OF UP.carrier_is_subring var_closed(1)[OF assms(1)]
          map_norm_in_poly_ring_carrier[OF assms]] by simp
  also have " ... = ?surj p"
    unfolding sym[OF eval_rewrite[OF assms]] ..
  also have " ... = \\<^bsub>Rupt K p\<^esub>"
    using UP.a_rcos_zero[OF UP.cgenideal_ideal[OF assms(2)] UP.cgenideal_self[OF assms(2)]]
    unfolding rupture_def FactRing_def by simp
  finally show ?thesis .
qed

subsection \<open>Division\<close>

definition (in ring) long_divides :: "'a list \ 'a list \ ('a list \ 'a list) \ bool"
  where "long_divides p q t \
           \<comment> \<open>i\<close>   (t \<in> carrier (poly_ring R) \<times> carrier (poly_ring R)) \<and>
           \<comment> \<open>ii\<close>  (p = (q \<otimes>\<^bsub>poly_ring R\<^esub> (fst t)) \<oplus>\<^bsub>poly_ring R\<^esub> (snd t)) \<and>
           \<comment> \<open>iii\<close> (snd t = [] \<or> degree (snd t) < degree q)"

definition (in ring) long_division :: "'a list \ 'a list \ ('a list \ 'a list)"
  where "long_division p q = (THE t. long_divides p q t)"

definition (in ring) pdiv :: "'a list \ 'a list \ 'a list" (infixl "pdiv" 65)
  where "p pdiv q = (if q = [] then [] else fst (long_division p q))"

definition (in ring) pmod :: "'a list \ 'a list \ 'a list" (infixl "pmod" 65)
  where "p pmod q = (if q = [] then p else snd (long_division p q))"

lemma (in ring) long_dividesI:
  assumes "b \ carrier (poly_ring R)" and "r \ carrier (poly_ring R)"
      and "p = (q \\<^bsub>poly_ring R\<^esub> b) \\<^bsub>poly_ring R\<^esub> r" and "r = [] \ degree r < degree q"
    shows "long_divides p q (b, r)"
  using assms unfolding long_divides_def by auto

lemma (in domain) exists_long_division:
  assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []"
  obtains b r where "b \ carrier (K[X])" and "r \ carrier (K[X])" and "long_divides p q (b, r)"
  using subfield_long_division_theorem_shell[OF assms(1-3)] assms(4)
        carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]]
  unfolding long_divides_def univ_poly_zero univ_poly_add univ_poly_mult by auto

lemma (in domain) exists_unique_long_division:
  assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []"
  shows "\!t. long_divides p q t"
proof -
  let ?padd   = "\a b. a \\<^bsub>poly_ring R\<^esub> b"
  let ?pmult  = "\a b. a \\<^bsub>poly_ring R\<^esub> b"
  let ?pminus = "\a b. a \\<^bsub>poly_ring R\<^esub> b"

  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  obtain b r where ldiv: "long_divides p q (b, r)"
    using exists_long_division[OF assms] by metis

  moreover have "(b, r) = (b', r')" if "long_divides p q (b', r')" for b' r'
  proof -
    have q: "q \ carrier (poly_ring R)" "q \ []"
      using assms(3-4) carrier_polynomial[OF subfieldE(1)[OF assms(1)]]
      unfolding univ_poly_carrier by auto
    hence in_carrier: "q \ carrier (poly_ring R)"
      "b \ carrier (poly_ring R)" "r \ carrier (poly_ring R)"
      "b' \ carrier (poly_ring R)" "r' \ carrier (poly_ring R)"
      using assms(3) that ldiv unfolding long_divides_def by auto
    have "?pminus (?padd (?pmult q b) r) r' = ?pminus (?padd (?pmult q b') r') r'"
      using ldiv and that unfolding long_divides_def by auto
    hence eq: "?padd (?pmult q (?pminus b b')) (?pminus r r') = \\<^bsub>poly_ring R\<^esub>"
      using in_carrier by algebra
    have "b = b'"
    proof (rule ccontr)
      assume "b \ b'"
      hence pminus: "?pminus b b' \ \\<^bsub>poly_ring R\<^esub>" "?pminus b b' \ carrier (poly_ring R)"
        using in_carrier(2,4) by (metis UP.add.inv_closed UP.l_neg UP.minus_eq UP.minus_unique, algebra)
      hence degree_ge: "degree (?pmult q (?pminus b b')) \ degree q"
        using poly_mult_degree_eq[OF carrier_is_subring, of q "?pminus b b'"] q
        unfolding univ_poly_zero univ_poly_carrier univ_poly_mult by simp

      have "?pminus b b' = \\<^bsub>poly_ring R\<^esub>" if "?pminus r r' = \\<^bsub>poly_ring R\<^esub>"
        using eq pminus(2) q UP.integral univ_poly_zero unfolding that by auto
      hence "?pminus r r' \ []"
        using pminus(1) unfolding univ_poly_zero by blast
      moreover have "?pminus r r' = []" if "r = []" and "r' = []"
        using univ_poly_a_inv_def'[OF carrier_is_subring UP.zero_closed] that
        unfolding a_minus_def univ_poly_add univ_poly_zero by auto
      ultimately have "r \ [] \ r' \ []"
        by blast
      hence "max (degree r) (degree r') < degree q"
        using ldiv and that unfolding long_divides_def by auto
      moreover have "degree (?pminus r r') \ max (degree r) (degree r')"
        using poly_add_degree[of r "map (a_inv R) r'"]
        unfolding a_minus_def univ_poly_add univ_poly_a_inv_def'[OF carrier_is_subring in_carrier(5)]
        by auto
      ultimately have degree_lt: "degree (?pminus r r') < degree q"
        by linarith
      have is_poly: "polynomial (carrier R) (?pmult q (?pminus b b'))" "polynomial (carrier R) (?pminus r r')"
        using in_carrier pminus(2) unfolding univ_poly_carrier by algebra+

      have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = degree (?pmult q (?pminus b b'))"
        using poly_add_degree_eq[OF carrier_is_subring is_poly] degree_ge degree_lt
        unfolding univ_poly_carrier sym[OF univ_poly_add[of R "carrier R"]] max_def by simp
      hence "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) > 0"
        using degree_ge degree_lt by simp
      moreover have "degree (?padd (?pmult q (?pminus b b')) (?pminus r r')) = 0"
        using eq unfolding univ_poly_zero by simp
      ultimately show False by simp
    qed
    hence "?pminus r r' = \\<^bsub>poly_ring R\<^esub>"
      using in_carrier eq by algebra
    hence "r = r'"
      using in_carrier by (metis UP.add.inv_closed UP.add.right_cancel UP.minus_eq UP.r_neg)
    with \<open>b = b'\<close> show ?thesis
      by simp
  qed

  ultimately show ?thesis
    by auto
qed

lemma (in domain) long_divisionE:
  assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []"
  shows "long_divides p q (p pdiv q, p pmod q)"
  using theI'[OF exists_unique_long_division[OF assms]] assms(4)
  unfolding pmod_def pdiv_def long_division_def by auto

lemma (in domain) long_divisionI:
  assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []"
  shows "long_divides p q (b, r) \ (b, r) = (p pdiv q, p pmod q)"
  using exists_unique_long_division[OF assms] long_divisionE[OF assms] by metis

lemma (in domain) long_division_closed:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])"
proof -
  have "p pdiv q \ carrier (K[X]) \ p pmod q \ carrier (K[X])"
    using assms univ_poly_zero_closed[of R] long_divisionI[of K] exists_long_division[OF assms]
    by (cases "q = []") (simp add: pdiv_def pmod_def, metis Pair_inject)+
  thus "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])"
    by auto
qed

lemma (in domain) pdiv_pmod:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "p = (q \\<^bsub>K[X]\<^esub> (p pdiv q)) \\<^bsub>K[X]\<^esub> (p pmod q)"
proof (cases)
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .
  assume "q = []" thus ?thesis
    using assms(2) unfolding pdiv_def pmod_def sym[OF univ_poly_zero[of R K]] by simp
next
  assume "q \ []" thus ?thesis
    using long_divisionE[OF assms] unfolding long_divides_def univ_poly_mult univ_poly_add by simp
qed

lemma (in domain) pmod_degree:
  assumes "subfield K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])" "q \ []"
  shows "p pmod q = [] \ degree (p pmod q) < degree q"
  using long_divisionE[OF assms] unfolding long_divides_def by auto

lemma (in domain) pmod_const:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" and "degree q > degree p"
  shows "p pdiv q = []" and "p pmod q = p"
proof -
  have "p pdiv q = [] \ p pmod q = p"
  proof (cases)
    interpret UP: ring "K[X]"
      using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

    assume "q \ []"
    have "p = (q \\<^bsub>K[X]\<^esub> []) \\<^bsub>K[X]\<^esub> p"
      using assms(2-3) unfolding sym[OF univ_poly_zero[of R K]] by simp
    moreover have "([], p) \ carrier (poly_ring R) \ carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] by auto
    ultimately have "long_divides p q ([], p)"
      using assms(4) unfolding long_divides_def univ_poly_mult univ_poly_add by auto
    with \<open>q \<noteq> []\<close> show ?thesis
      using long_divisionI[OF assms(1-3)] by auto
  qed (simp add: pmod_def pdiv_def)
  thus "p pdiv q = []" and "p pmod q = p"
    by auto
qed

lemma (in domain) long_division_zero:
  assumes "subfield K R" and "q \ carrier (K[X])" shows "[] pdiv q = []" and "[] pmod q = []"
proof -
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .

  have "[] pdiv q = [] \ [] pmod q = []"
  proof (cases)
    assume "q \ []"
    have "q \ carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)] assms(2)] .
    hence "long_divides [] q ([], [])"
      unfolding long_divides_def sym[OF univ_poly_zero[of R "carrier R"]] by auto
    with \<open>q \<noteq> []\<close> show ?thesis
      using long_divisionI[OF assms(1) univ_poly_zero_closed assms(2)] by simp
  qed (simp add: pmod_def pdiv_def)
  thus "[] pdiv q = []" and "[] pmod q = []"
    by auto
qed

lemma (in domain) long_division_a_inv:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "((\\<^bsub>K[X]\<^esub> p) pdiv q) = \\<^bsub>K[X]\<^esub> (p pdiv q)" (is "?pdiv")
    and "((\\<^bsub>K[X]\<^esub> p) pmod q) = \\<^bsub>K[X]\<^esub> (p pmod q)" (is "?pmod")
proof -
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

  have "?pdiv \ ?pmod"
  proof (cases)
    assume "q = []" thus ?thesis
      unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp
  next
    assume not_nil: "q \ []"
    have "\\<^bsub>K[X]\<^esub> p = \\<^bsub>K[X]\<^esub> ((q \\<^bsub>K[X]\<^esub> (p pdiv q)) \\<^bsub>K[X]\<^esub> (p pmod q))"
      using pdiv_pmod[OF assms] by simp
    hence "\\<^bsub>K[X]\<^esub> p = (q \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> (p pdiv q))) \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> (p pmod q))"
      using assms(2-3) long_division_closed[OF assms] by algebra
    moreover have "\\<^bsub>K[X]\<^esub> (p pdiv q) \ carrier (K[X])" "\\<^bsub>K[X]\<^esub> (p pmod q) \ carrier (K[X])"
      using long_division_closed[OF assms] by algebra+
    hence "(\\<^bsub>K[X]\<^esub> (p pdiv q), \\<^bsub>K[X]\<^esub> (p pmod q)) \ carrier (poly_ring R) \ carrier (poly_ring R)"
      using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
    moreover have "\\<^bsub>K[X]\<^esub> (p pmod q) = [] \ degree (\\<^bsub>K[X]\<^esub> (p pmod q)) < degree q"
      using univ_poly_a_inv_length[OF subfieldE(1)[OF assms(1)]
            long_division_closed(2)[OF assms]] pmod_degree[OF assms not_nil]
      by auto
    ultimately have "long_divides (\\<^bsub>K[X]\<^esub> p) q (\\<^bsub>K[X]\<^esub> (p pdiv q), \\<^bsub>K[X]\<^esub> (p pmod q))"
      unfolding long_divides_def univ_poly_mult univ_poly_add by simp
    thus ?thesis
      using long_divisionI[OF assms(1) UP.a_inv_closed[OF assms(2)] assms(3) not_nil] by simp
  qed
  thus ?pdiv and ?pmod
    by auto
qed

lemma (in domain) long_division_add:
  assumes "subfield K R" and "a \ carrier (K[X])" "b \ carrier (K[X])" "q \ carrier (K[X])"
  shows "(a \\<^bsub>K[X]\<^esub> b) pdiv q = (a pdiv q) \\<^bsub>K[X]\<^esub> (b pdiv q)" (is "?pdiv")
    and "(a \\<^bsub>K[X]\<^esub> b) pmod q = (a pmod q) \\<^bsub>K[X]\<^esub> (b pmod q)" (is "?pmod")
proof -
  let ?pdiv_add = "(a pdiv q) \\<^bsub>K[X]\<^esub> (b pdiv q)"
  let ?pmod_add = "(a pmod q) \\<^bsub>K[X]\<^esub> (b pmod q)"

  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .

  have "?pdiv \ ?pmod"
  proof (cases)
    assume "q = []" thus ?thesis
      using assms(2-3) unfolding pmod_def pdiv_def sym[OF univ_poly_zero[of R K]] by simp
  next
    note in_carrier = long_division_closed[OF assms(1,2,4)]
                      long_division_closed[OF assms(1,3,4)]

    assume "q \ []"
    have "a \\<^bsub>K[X]\<^esub> b = ((q \\<^bsub>K[X]\<^esub> (a pdiv q)) \\<^bsub>K[X]\<^esub> (a pmod q)) \\<^bsub>K[X]\<^esub>
                         ((q \<otimes>\<^bsub>K[X]\<^esub> (b pdiv q)) \<oplus>\<^bsub>K[X]\<^esub> (b pmod q))"
      using assms(2-3)[THEN pdiv_pmod[OF assms(1) _ assms(4)]] by simp
    hence "a \\<^bsub>K[X]\<^esub> b = (q \\<^bsub>K[X]\<^esub> ?pdiv_add) \\<^bsub>K[X]\<^esub> ?pmod_add"
      using assms(4) in_carrier by algebra
    moreover have "(?pdiv_add, ?pmod_add) \ carrier (poly_ring R) \ carrier (poly_ring R)"
      using in_carrier carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
    moreover have "?pmod_add = [] \ degree ?pmod_add < degree q"
    proof (cases)
      assume "?pmod_add \ []"
      hence "a pmod q \ [] \ b pmod q \ []"
        using in_carrier(2,4) unfolding sym[OF univ_poly_zero[of R K]] by auto
      moreover from \<open>q \<noteq> []\<close>
      have "a pmod q = [] \ degree (a pmod q) < degree q" and "b pmod q = [] \ degree (b pmod q) < degree q"
        using assms(2-3)[THEN pmod_degree[OF assms(1) _ assms(4)]] by auto
      ultimately have "max (degree (a pmod q)) (degree (b pmod q)) < degree q"
        by auto
      thus ?thesis
        using poly_add_degree le_less_trans unfolding univ_poly_add by blast
    qed simp
    ultimately have "long_divides (a \\<^bsub>K[X]\<^esub> b) q (?pdiv_add, ?pmod_add)"
      unfolding long_divides_def univ_poly_mult univ_poly_add by simp
    with \<open>q \<noteq> []\<close> show ?thesis
      using long_divisionI[OF assms(1) UP.a_closed[OF assms(2-3)] assms(4)] by simp
  qed
  thus ?pdiv and ?pmod
    by auto
qed

lemma (in domain) long_division_add_iff:
  assumes "subfield K R"
    and "a \ carrier (K[X])" "b \ carrier (K[X])" "c \ carrier (K[X])" "q \ carrier (K[X])"
  shows "a pmod q = b pmod q \ (a \\<^bsub>K[X]\<^esub> c) pmod q = (b \\<^bsub>K[X]\<^esub> c) pmod q"
proof -
  interpret UP: ring "K[X]"
    using univ_poly_is_ring[OF subfieldE(1)[OF assms(1)]] .
  show ?thesis
    using assms(2-4)[THEN long_division_closed(2)[OF assms(1) _ assms(5)]]
    unfolding assms(2-3)[THEN long_division_add(2)[OF assms(1) _ assms(4-5)]] by auto
qed

lemma (in domain) pdivides_iff:
  assumes "subfield K R" and "polynomial K p" "polynomial K q"
  shows "p pdivides q \ p divides\<^bsub>K[X]\<^esub> q"
proof
  show "p divides\<^bsub>K [X]\<^esub> q \ p pdivides q"
    using carrier_polynomial[OF subfieldE(1)[OF assms(1)]]
    unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by auto
next
  interpret UP: ring "poly_ring R"
    using univ_poly_is_ring[OF carrier_is_subring] .

  have in_carrier: "p \ carrier (poly_ring R)" "q \ carrier (poly_ring R)"
    using carrier_polynomial[OF subfieldE(1)[OF assms(1)]] assms
    unfolding univ_poly_carrier by auto

  assume "p pdivides q"
  then obtain b where "b \ carrier (poly_ring R)" and "q = p \\<^bsub>poly_ring R\<^esub> b"
      unfolding pdivides_def factor_def by blast
  show "p divides\<^bsub>K[X]\<^esub> q"
  proof (cases)
    assume "p = []"
    with \<open>b \<in> carrier (poly_ring R)\<close> and \<open>q = p \<otimes>\<^bsub>poly_ring R\<^esub> b\<close> have "q = []"
      unfolding univ_poly_mult sym[OF univ_poly_carrier]
      using poly_mult_zero(1)[OF polynomial_incl] by simp
    with \<open>p = []\<close> show ?thesis
      using poly_mult_zero(2)[of "[]"]
      unfolding factor_def univ_poly_mult by auto
  next
    interpret UP: ring "poly_ring R"
      using univ_poly_is_ring[OF carrier_is_subring] .

    assume "p \ []"
    from \<open>p pdivides q\<close> obtain b where "b \<in> carrier (poly_ring R)" and "q = p \<otimes>\<^bsub>poly_ring R\<^esub> b"
      unfolding pdivides_def factor_def by blast
    moreover have "p \ carrier (poly_ring R)" and "q \ carrier (poly_ring R)"
      using assms carrier_polynomial[OF subfieldE(1)[OF assms(1)]] unfolding univ_poly_carrier by auto
    ultimately have "q = (p \\<^bsub>poly_ring R\<^esub> b) \\<^bsub>poly_ring R\<^esub> \\<^bsub>poly_ring R\<^esub>"
      by algebra
    with \<open>b \<in> carrier (poly_ring R)\<close> have "long_divides q p (b, [])"
      unfolding long_divides_def univ_poly_zero by auto
    with \<open>p \<noteq> []\<close> have "b \<in> carrier (K[X])"
      using long_divisionI[of K q p b] long_division_closed[of K q p] assms
      unfolding univ_poly_carrier by auto
    with \<open>q = p \<otimes>\<^bsub>poly_ring R\<^esub> b\<close> show ?thesis
      unfolding factor_def univ_poly_mult by blast
  qed
qed

lemma (in domain) pdivides_iff_shell:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "p pdivides q \ p divides\<^bsub>K[X]\<^esub> q"
  using pdivides_iff assms by (simp add: univ_poly_carrier)

lemma (in domain) pmod_zero_iff_pdivides:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "p pmod q = [] \ q pdivides p"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] .

  show ?thesis
  proof
    assume pmod: "p pmod q = []"
    have "p pdiv q \ carrier (K[X])" and "p pmod q \ carrier (K[X])"
      using long_division_closed[OF assms] by auto
    hence "p = q \\<^bsub>K[X]\<^esub> (p pdiv q)"
      using pdiv_pmod[OF assms] assms(3) unfolding pmod sym[OF univ_poly_zero[of R K]] by algebra
    with \<open>p pdiv q \<in> carrier (K[X])\<close> show "q pdivides p"
      unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast
  next
    assume "q pdivides p" show "p pmod q = []"
    proof (cases)
      assume "q = []" with \<open>q pdivides p\<close> show ?thesis
        using zero_pdivides unfolding pmod_def by simp
    next
      assume "q \ []"
      from \<open>q pdivides p\<close> obtain r where "r \<in> carrier (K[X])" and "p = q \<otimes>\<^bsub>K[X]\<^esub> r"
        unfolding pdivides_iff_shell[OF assms(1,3,2)] factor_def by blast
      hence "p = (q \\<^bsub>K[X]\<^esub> r) \\<^bsub>K[X]\<^esub> []"
        using assms(2) unfolding sym[OF univ_poly_zero[of R K]] by simp
      moreover from \<open>r \<in> carrier (K[X])\<close> have "r \<in> carrier (poly_ring R)"
        using carrier_polynomial_shell[OF subfieldE(1)[OF assms(1)]] by auto
      ultimately have "long_divides p q (r, [])"
        unfolding long_divides_def univ_poly_mult univ_poly_add by auto
      with \<open>q \<noteq> []\<close> show ?thesis
        using long_divisionI[OF assms] by simp
    qed
  qed
qed

lemma (in domain) same_pmod_iff_pdivides:
  assumes "subfield K R" and "a \ carrier (K[X])" "b \ carrier (K[X])" "q \ carrier (K[X])"
  shows "a pmod q = b pmod q \ q pdivides (a \\<^bsub>K[X]\<^esub> b)"
proof -
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] .

  have "a pmod q = b pmod q \ (a \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> b)) pmod q = (b \\<^bsub>K[X]\<^esub> (\\<^bsub>K[X]\<^esub> b)) pmod q"
    using long_division_add_iff[OF assms(1-3) UP.a_inv_closed[OF assms(3)] assms(4)] .
  also have " ... \ (a \\<^bsub>K[X]\<^esub> b) pmod q = \\<^bsub>K[X]\<^esub> pmod q"
    using assms(2-3) by algebra
  also have " ... \ q pdivides (a \\<^bsub>K[X]\<^esub> b)"
    using pmod_zero_iff_pdivides[OF assms(1) UP.minus_closed[OF assms(2-3)] assms(4)]
    unfolding univ_poly_zero long_division_zero(2)[OF assms(1,4)] .
  finally show ?thesis .
qed

lemma (in domain) pdivides_imp_degree_le:
  assumes "subring K R" and "p \ carrier (K[X])" "q \ carrier (K[X])" "q \ []"
  shows "p pdivides q \ degree p \ degree q"
proof -
  assume "p pdivides q"
  then obtain r where r: "polynomial (carrier R) r" "q = poly_mult p r"
    unfolding pdivides_def factor_def univ_poly_mult univ_poly_carrier by blast
  moreover have p: "polynomial (carrier R) p"
    using assms(2) carrier_polynomial[OF assms(1)] unfolding univ_poly_carrier by auto
  moreover have "p \ []" and "r \ []"
    using poly_mult_zero(2)[OF polynomial_incl[OF p]] r(2) assms(4) by auto
  ultimately show "degree p \ degree q"
    using poly_mult_degree_eq[OF carrier_is_subring, of p r] by auto
qed

lemma (in domain) pprimeE:
  assumes "subfield K R" "p \ carrier (K[X])" "pprime K p"
  shows "p \ []" "p \ Units (K[X])"
    and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \
                 p pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<Longrightarrow> p pdivides q \<or> p pdivides r"
  using assms(2-3) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)]
  unfolding ring_prime_def prime_def
  by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero)

lemma (in domain) pprimeI:
  assumes "subfield K R" "p \ carrier (K[X])" "p \ []" "p \ Units (K[X])"
    and "\q r. \ q \ carrier (K[X]); r \ carrier (K[X])\ \
                 p pdivides (q \<otimes>\<^bsub>K[X]\<^esub> r) \<Longrightarrow> p pdivides q \<or> p pdivides r"
  shows "pprime K p"
  using assms(2-5) poly_mult_closed[OF subfieldE(1)[OF assms(1)]] pdivides_iff[OF assms(1)]
  unfolding ring_prime_def prime_def
  by (auto simp add: univ_poly_mult univ_poly_carrier univ_poly_zero)

lemma (in domain) associated_polynomials_iff:
  assumes "subfield K R" and "p \ carrier (K[X])" "q \ carrier (K[X])"
  shows "p \\<^bsub>K[X]\<^esub> q \ (\k \ K - { \ }. p = [ k ] \\<^bsub>K[X]\<^esub> q)"
  using domain.ring_associated_iff[OF univ_poly_is_domain[OF subfieldE(1)[OF assms(1)]] assms(2-3)]
  unfolding univ_poly_units[OF assms(1)] by auto

corollary (in domain) associated_polynomials_imp_same_length: (* stronger than "imp_same_degree" *)
  assumes "subring K R" and "p \ carrier (K[X])" and "q \ carrier (K[X])"
  shows "p \\<^bsub>K[X]\<^esub> q \ length p = length q"
proof -
  { fix p q
    assume p: "p \ carrier (K[X])" and q: "q \ carrier (K[X])" and "p \\<^bsub>K[X]\<^esub> q"
    have "length p \ length q"
    proof (cases "q = []")
      case True with \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p = []"
        unfolding associated_def True factor_def univ_poly_def by auto
      thus ?thesis
        using True by simp
    next
      case False
      from \<open>p \<sim>\<^bsub>K[X]\<^esub> q\<close> have "p divides\<^bsub>K [X]\<^esub> q"
        unfolding associated_def by simp
      hence "p divides\<^bsub>poly_ring R\<^esub> q"
        using carrier_polynomial[OF assms(1)]
        unfolding factor_def univ_poly_carrier univ_poly_mult by auto
      with \<open>q \<noteq> []\<close> have "degree p \<le> degree q"
        using pdivides_imp_degree_le[OF assms(1) p q] unfolding pdivides_def by simp
      with \<open>q \<noteq> []\<close> show ?thesis
        by (cases "p = []", auto simp add: Suc_leI le_diff_iff)
    qed
  } note aux_lemma = this

  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .

  assume "p \\<^bsub>K[X]\<^esub> q" thus ?thesis
    using aux_lemma[OF assms(2-3)] aux_lemma[OF assms(3,2) UP.associated_sym] by simp
qed

lemma (in ring) divides_pirreducible_condition:
  assumes "pirreducible K q" and "p \ carrier (K[X])"
  shows "p divides\<^bsub>K[X]\<^esub> q \ p \ Units (K[X]) \ p \\<^bsub>K[X]\<^esub> q"
  using divides_irreducible_condition[of "K[X]" q p] assms
  unfolding ring_irreducible_def by auto

subsection \<open>Polynomial Power\<close>

lemma (in domain) polynomial_pow_not_zero:
  assumes "p \ carrier (poly_ring R)" and "p \ []"
  shows "p [^]\<^bsub>poly_ring R\<^esub> (n::nat) \ []"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  from assms UP.integral show ?thesis
    unfolding sym[OF univ_poly_zero[of R "carrier R"]]
    by (induction n, auto)
qed

lemma (in domain) subring_polynomial_pow_not_zero:
  assumes "subring K R" and "p \ carrier (K[X])" and "p \ []"
  shows "p [^]\<^bsub>K[X]\<^esub> (n::nat) \ []"
  using domain.polynomial_pow_not_zero[OF subring_is_domain, of K p n] assms
  unfolding univ_poly_consistent[OF assms(1)] by simp

lemma (in domain) polynomial_pow_degree:
  assumes "p \ carrier (poly_ring R)"
  shows "degree (p [^]\<^bsub>poly_ring R\<^esub> n) = n * degree p"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  show ?thesis
  proof (induction n)
    case 0 thus ?case
      using UP.nat_pow_0 unfolding univ_poly_one by auto
  next
    let ?ppow = "\n. p [^]\<^bsub>poly_ring R\<^esub> n"
    case (Suc n) thus ?case
    proof (cases "p = []")
      case True thus ?thesis
        using univ_poly_zero[of R "carrier R"] UP.r_null assms by auto
    next
      case False
      hence "?ppow n \ carrier (poly_ring R)" and "?ppow n \ []" and "p \ []"
        using polynomial_pow_not_zero[of p n] assms by (auto simp add: univ_poly_one)
      thus ?thesis
        using poly_mult_degree_eq[OF carrier_is_subring, of "?ppow n" p] Suc assms
        unfolding univ_poly_carrier univ_poly_zero
        by (auto simp add: add.commute univ_poly_mult)
    qed
  qed
qed

lemma (in domain) subring_polynomial_pow_degree:
  assumes "subring K R" and "p \ carrier (K[X])"
  shows "degree (p [^]\<^bsub>K[X]\<^esub> n) = n * degree p"
  using domain.polynomial_pow_degree[OF subring_is_domain, of K p n] assms
  unfolding univ_poly_consistent[OF assms(1)] by simp

lemma (in domain) polynomial_pow_division:
  assumes "p \ carrier (poly_ring R)" and "(n::nat) \ m"
  shows "(p [^]\<^bsub>poly_ring R\<^esub> n) pdivides (p [^]\<^bsub>poly_ring R\<^esub> m)"
proof -
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  let ?ppow = "\n. p [^]\<^bsub>poly_ring R\<^esub> n"

  have "?ppow n \\<^bsub>poly_ring R\<^esub> ?ppow k = ?ppow (n + k)" for k
    using assms(1) by (simp add: UP.nat_pow_mult)
  thus ?thesis
    using dividesI[of "?ppow (m - n)" "poly_ring R" "?ppow m" "?ppow n"] assms
    unfolding pdivides_def by auto
qed

lemma (in domain) subring_polynomial_pow_division:
  assumes "subring K R" and "p \ carrier (K[X])" and "(n::nat) \ m"
  shows "(p [^]\<^bsub>K[X]\<^esub> n) divides\<^bsub>K[X]\<^esub> (p [^]\<^bsub>K[X]\<^esub> m)"
  using domain.polynomial_pow_division[OF subring_is_domain, of K p n m] assms
  unfolding univ_poly_consistent[OF assms(1)] pdivides_def by simp

lemma (in domain) pirreducible_pow_pdivides_iff:
  assumes "subfield K R" "p \ carrier (K[X])" "q \ carrier (K[X])" "r \ carrier (K[X])"
    and "pirreducible K p" and "\ (p pdivides q)"
  shows "(p [^]\<^bsub>K[X]\<^esub> (n :: nat)) pdivides (q \\<^bsub>K[X]\<^esub> r) \ (p [^]\<^bsub>K[X]\<^esub> n) pdivides r"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  show ?thesis
  proof (cases "r = []")
    case True with \<open>q \<in> carrier (K[X])\<close> have "q \<otimes>\<^bsub>K[X]\<^esub> r = []" and "r = []"
      unfolding  sym[OF univ_poly_zero[of R K]] by auto
    thus ?thesis
      using pdivides_zero[OF subfieldE(1),of K] assms by auto
  next
    case False then have not_zero: "p \ []" "q \ []" "r \ []" "q \\<^bsub>K[X]\<^esub> r \ []"
      using subfieldE(1) pdivides_zero[OF _ assms(2)] assms(1-2,5-6) pirreducibleE(1)
            UP.integral_iff[OF assms(3-4)] univ_poly_zero[of R K] by auto
    from \<open>p \<noteq> []\<close>
    have ppow: "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \ []" "p [^]\<^bsub>K[X]\<^esub> (n :: nat) \ carrier (K[X])"
      using subring_polynomial_pow_not_zero[OF subfieldE(1)] assms(1-2) by auto
    have not_pdiv: "\ (p divides\<^bsub>mult_of (K[X])\<^esub> q)"
      using assms(6) pdivides_iff_shell[OF assms(1-3)] unfolding pdivides_def by auto
    have prime: "prime (mult_of (K[X])) p"
      using assms(5) pprime_iff_pirreducible[OF assms(1-2)]
      unfolding sym[OF UP.prime_eq_prime_mult[OF assms(2)]] ring_prime_def by simp
    have "a pdivides b \ a divides\<^bsub>mult_of (K[X])\<^esub> b"
      if "a \ carrier (K[X])" "a \ \\<^bsub>K[X]\<^esub>" "b \ carrier (K[X])" "b \ \\<^bsub>K[X]\<^esub>" for a b
      using that UP.divides_imp_divides_mult[of a b] divides_mult_imp_divides[of "K[X]" a b]
      unfolding pdivides_iff_shell[OF assms(1) that(1,3)] by blast
    thus ?thesis
      using UP.mult_of.prime_pow_divides_iff[OF _ _ _ prime not_pdiv, of r] ppow not_zero assms(2-4)
      unfolding nat_pow_mult_of carrier_mult_of mult_mult_of sym[OF univ_poly_zero[of R K]]
      by (metis DiffI UP.m_closed singletonD)
  qed
qed

lemma (in domain) subring_degree_one_imp_pirreducible:
  assumes "subring K R" and "a \ Units (R \ carrier := K \)" and "b \ K"
  shows "pirreducible K [ a, b ]"
proof (rule pirreducibleI[OF assms(1)])
  have "a \ K" and "a \ \"
    using assms(2) subringE(1)[OF assms(1)] unfolding Units_def by auto
  thus "[ a, b ] \ carrier (K[X])" and "[ a, b ] \ []" and "[ a, b ] \ Units (K [X])"
    using univ_poly_units_incl[OF assms(1)] assms(2-3)
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
next
  interpret UP: domain "K[X]"
    using univ_poly_is_domain[OF assms(1)] .

  { fix q r
    assume q: "q \ carrier (K[X])" and r: "r \ carrier (K[X])" and "[ a, b ] = q \\<^bsub>K[X]\<^esub> r"
    hence not_zero: "q \ []" "r \ []"
      by (metis UP.integral_iff list.distinct(1) univ_poly_zero)+
    have "degree (q \\<^bsub>K[X]\<^esub> r) = degree q + degree r"
      using not_zero poly_mult_degree_eq[OF assms(1)] q r
      by (simp add: univ_poly_carrier univ_poly_mult)
    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "degree q + degree r = 1" and "q \<noteq> []" "r \<noteq> []"
      using not_zero by auto
  } note aux_lemma1 = this

  { fix q r
    assume q: "q \ carrier (K[X])" "q \ []" and r: "r \ carrier (K[X])" "r \ []"
      and "[ a, b ] = q \\<^bsub>K[X]\<^esub> r" and "degree q = 1" and "degree r = 0"
    hence "length q = Suc (Suc 0)" and "length r = Suc 0"
      by (linarith, metis add.right_neutral add_eq_if length_0_conv)
    from \<open>length q = Suc (Suc 0)\<close> obtain c d where q_def: "q = [ c, d ]"
      by (metis length_0_conv length_Cons list.exhaust nat.inject)
    from \<open>length r = Suc 0\<close> obtain e where r_def: "r = [ e ]"
      by (metis length_0_conv length_Suc_conv)
    from \<open>r = [ e ]\<close> and \<open>q = [ c, d ]\<close>
    have c: "c \ K" "c \ \" and d: "d \ K" and e: "e \ K" "e \ \"
      using r q subringE(1)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    with sym[OF \<open>[ a, b ] = q \<otimes>\<^bsub>K[X]\<^esub> r\<close>] have "a = c \<otimes> e"
      using poly_mult_lead_coeff[OF assms(1), of q r]
      unfolding polynomial_def sym[OF univ_poly_mult[of R K]] r_def q_def by auto
    obtain inv_a where a: "a \ K" and inv_a: "inv_a \ K" "a \ inv_a = \" "inv_a \ a = \"
      using assms(2) unfolding Units_def by auto
    hence "a \ \" and "inv_a \ \"
      using subringE(1)[OF assms(1)] integral_iff by auto
    with \<open>c \<in> K\<close> and \<open>c \<noteq> \<zero>\<close> have in_carrier: "[ c \<otimes> inv_a ] \<in> carrier (K[X])"
      using subringE(1,6)[OF assms(1)] inv_a integral
      unfolding sym[OF univ_poly_carrier] polynomial_def
      by (auto, meson subsetD)
    moreover have "[ c \ inv_a ] \\<^bsub>K[X]\<^esub> r = [ \ ]"
      using \<open>a = c \<otimes> e\<close> a inv_a c e subsetD[OF subringE(1)[OF assms(1)]]
      unfolding r_def univ_poly_mult by (auto) (simp add: m_assoc m_lcomm integral_iff)+
    ultimately have "r \ Units (K[X])"
      using r(1) UP.m_comm[OF in_carrier r(1)] unfolding sym[OF univ_poly_one[of R K]] Units_def by auto
  } note aux_lemma2 = this

  fix q r
  assume q: "q \ carrier (K[X])" and r: "r \ carrier (K[X])" and qr: "[ a, b ] = q \\<^bsub>K[X]\<^esub> r"
  thus "q \ Units (K[X]) \ r \ Units (K[X])"
    using aux_lemma1[OF q r qr] aux_lemma2[of q r] aux_lemma2[of r q] UP.m_comm add_is_1 by auto
qed

lemma (in domain) degree_one_imp_pirreducible:
  assumes "subfield K R" and "p \ carrier (K[X])" and "degree p = 1"
  shows "pirreducible K p"
proof -
  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where p: "p = [ a, b ]"
    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
  with \<open>p \<in> carrier (K[X])\<close> show ?thesis
    using subring_degree_one_imp_pirreducible[OF subfieldE(1)[OF assms(1)], of a b]
          subfield.subfield_Units[OF assms(1)]
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
qed

lemma (in ring) degree_oneE[elim]:
  assumes "p \ carrier (K[X])" and "degree p = 1"
    and "\a b. \ a \ K; a \ \; b \ K; p = [ a, b ] \ \ P"
  shows P
proof -
  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where "p = [ a, b ]"
    by (metis length_0_conv length_Cons nat.inject neq_Nil_conv)
  with \<open>p \<in> carrier (K[X])\<close> have "a \<in> K" and "a \<noteq> \<zero>" and "b \<in> K"
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  with \<open>p = [ a, b ]\<close> show ?thesis
    using assms(3) by simp
qed

lemma (in domain) subring_degree_one_associatedI:
  assumes "subring K R" and "a \ K" "a' \ K" and "b \ K" and "a \ a' = \"
  shows "[ a , b ] \\<^bsub>K[X]\<^esub> [ \, a' \ b ]"
proof -
  from \<open>a \<otimes> a' = \<one>\<close> have not_zero: "a \<noteq> \<zero>" "a' \<noteq> \<zero>"
    using subringE(1)[OF assms(1)] assms(2-3) by auto
  hence "[ a, b ] = [ a ] \\<^bsub>K[X]\<^esub> [ \, a' \ b ]"
    using assms(2-4)[THEN subsetD[OF subringE(1)[OF assms(1)]]] assms(5) m_assoc
    unfolding univ_poly_mult by fastforce
  moreover have "[ a, b ] \ carrier (K[X])" and "[ \, a' \ b ] \ carrier (K[X])"
    using subringE(1,3,6)[OF assms(1)] not_zero one_not_zero assms
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  moreover have "[ a ] \ Units (K[X])"
  proof -
    from \<open>a \<noteq> \<zero>\<close> and \<open>a' \<noteq> \<zero>\<close> have "[ a ] \<in> carrier (K[X])" and "[ a' ] \<in> carrier (K[X])"
      using assms(2-3) unfolding sym[OF univ_poly_carrier] polynomial_def by auto
    moreover have "a' \ a = \"
      using subsetD[OF subringE(1)[OF assms(1)]] assms m_comm by simp
    hence "[ a ] \\<^bsub>K[X]\<^esub> [ a' ] = [ \ ]" and "[ a' ] \\<^bsub>K[X]\<^esub> [ a ] = [ \ ]"
      using assms unfolding univ_poly_mult by auto
    ultimately show ?thesis
      unfolding sym[OF univ_poly_one[of R K]] Units_def by blast
  qed
  ultimately show ?thesis
    using domain.ring_associated_iff[OF univ_poly_is_domain[OF assms(1)]] by blast
qed

lemma (in domain) degree_one_associatedI:
  assumes "subfield K R" and "p \ carrier (K[X])" and "degree p = 1"
  shows "p \\<^bsub>K[X]\<^esub> [ \, inv (lead_coeff p) \ (const_term p) ]"
proof -
  from \<open>p \<in> carrier (K[X])\<close> and \<open>degree p = 1\<close>
  obtain a b where "p = [ a, b ]" and "a \ K" "a \ \" and "b \ K"
    by auto
  thus ?thesis
    using subring_degree_one_associatedI[OF subfieldE(1)[OF assms(1)]]
          subfield_m_inv[OF assms(1)] subsetD[OF subfieldE(3)[OF assms(1)]]
    unfolding const_term_def
    by auto
qed

subsection \<open>Ideals\<close>

lemma (in domain) exists_unique_gen:
  assumes "subfield K R" "ideal I (K[X])" "I \ { [] }"
  shows "\!p \ carrier (K[X]). lead_coeff p = \ \ I = PIdl\<^bsub>K[X]\<^esub> p"
    (is "\!p. ?generator p")
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .
  obtain q where q: "q \ carrier (K[X])" "I = PIdl\<^bsub>K[X]\<^esub> q"
    using UP.exists_gen[OF assms(2)] by blast
  hence not_nil: "q \ []"
    using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3)
    by (auto simp add: univ_poly_zero)
  hence "lead_coeff q \ K - { \ }"
    using q(1) unfolding univ_poly_def polynomial_def by auto
  hence inv_lc_q: "inv (lead_coeff q) \ K - { \ }" "inv (lead_coeff q) \ lead_coeff q = \"
    using subfield_m_inv[OF assms(1)] by auto

  define p where "p = [ inv (lead_coeff q) ] \\<^bsub>K[X]\<^esub> q"
  have is_poly: "polynomial K [ inv (lead_coeff q) ]" "polynomial K q"
    using inv_lc_q(1) q(1) unfolding univ_poly_def polynomial_def by auto
  hence in_carrier: "p \ carrier (K[X])"
    using UP.m_closed unfolding univ_poly_carrier p_def by simp
  have lc_p: "lead_coeff p = \"
    using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)] is_poly _ not_nil] inv_lc_q(2)
    unfolding p_def univ_poly_mult[of R K] by simp
  moreover have PIdl_p: "I = PIdl\<^bsub>K[X]\<^esub> p"
    using UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) inv_lc_q(1) p_def
          associated_polynomials_iff[OF assms(1) in_carrier q(1)]
    by auto
  ultimately have "?generator p"
    using in_carrier by simp

  moreover
  have "\r. \ r \ carrier (K[X]); lead_coeff r = \; I = PIdl\<^bsub>K[X]\<^esub> r \ \ r = p"
  proof -
    fix r assume r: "r \ carrier (K[X])" "lead_coeff r = \" "I = PIdl\<^bsub>K[X]\<^esub> r"
    have "subring K R"
      by (simp add: \<open>subfield K R\<close> subfieldE(1))
    obtain k where k: "k \ K - { \ }" "r = [ k ] \\<^bsub>K[X]\<^esub> p"
      using UP.associated_iff_same_ideal[OF r(1) in_carrier] PIdl_p r(3)
            associated_polynomials_iff[OF assms(1) r(1) in_carrier]
      by auto
    hence "polynomial K [ k ]"
      unfolding polynomial_def by simp
    moreover have "p \ []"
      using not_nil UP.associated_iff_same_ideal[OF in_carrier q(1)] q(2) PIdl_p
            associated_polynomials_imp_same_length[OF \<open>subring K R\<close> in_carrier q(1)] by auto
    ultimately have "lead_coeff r = k \ (lead_coeff p)"
      using poly_mult_lead_coeff[OF subfieldE(1)[OF assms(1)]] in_carrier k(2)
      unfolding univ_poly_def by (auto simp del: poly_mult.simps)
    hence "k = \"
      using lc_p r(2) k(1) subfieldE(3)[OF assms(1)] by auto
    hence "r = map ((\) \) p"
      using poly_mult_const(1)[OF subfieldE(1)[OF assms(1)] _ k(1), of p] in_carrier
      unfolding k(2) univ_poly_carrier[of R K] univ_poly_mult[of R K] by auto
    moreover have "set p \ carrier R"
      using polynomial_in_carrier[OF subfieldE(1)[OF assms(1)]]
            in_carrier univ_poly_carrier[of R K] by auto
    hence "map ((\) \) p = p"
      by (induct p) (auto)
    ultimately show "r = p" by simp
  qed

  ultimately show ?thesis by blast
qed

proposition (in domain) exists_unique_pirreducible_gen:
  assumes "subfield K R" "ring_hom_ring (K[X]) R h"
    and "a_kernel (K[X]) R h \ { [] }" "a_kernel (K[X]) R h \ carrier (K[X])"
  shows "\!p \ carrier (K[X]). pirreducible K p \ lead_coeff p = \ \ a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> p"
    (is "\!p. ?generator p")
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  have "ideal (a_kernel (K[X]) R h) (K[X])"
    using ring_hom_ring.kernel_is_ideal[OF assms(2)] .
  then obtain p
    where p: "p \ carrier (K[X])" "lead_coeff p = \" "a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> p"
      and unique:
      "\q. \ q \ carrier (K[X]); lead_coeff q = \; a_kernel (K[X]) R h = PIdl\<^bsub>K[X]\<^esub> q \ \ q = p"
    using exists_unique_gen[OF assms(1) _ assms(3)] by metis

  have "p \ carrier (K[X]) - { [] }"
      using UP.genideal_zero UP.cgenideal_eq_genideal[OF UP.zero_closed] assms(3) p(1,3)
      by (auto simp add: univ_poly_zero)
  hence "pprime K p"
    using ring_hom_ring.primeideal_vimage[OF assms(2) UP.is_cring zeroprimeideal]
          UP.primeideal_iff_prime[of p]
    unfolding univ_poly_zero sym[OF p(3)] a_kernel_def' by simp
  hence "pirreducible K p"
    using pprime_iff_pirreducible[OF assms(1) p(1)] by simp
  thus ?thesis
    using p unique by metis
qed

lemma (in domain) cgenideal_pirreducible:
  assumes "subfield K R" and "p \ carrier (K[X])" "pirreducible K p"
  shows "\ pirreducible K q; q \ PIdl\<^bsub>K[X]\<^esub> p \ \ p \\<^bsub>K[X]\<^esub> q"
proof -
  interpret UP: principal_domain "K[X]"
    using univ_poly_is_principal[OF assms(1)] .

  assume q: "pirreducible K q" "q \ PIdl\<^bsub>K[X]\<^esub> p"
  hence in_carrier: "q \ carrier (K[X])"
    using additive_subgroup.a_subset[OF ideal.axioms(1)[OF UP.cgenideal_ideal[OF assms(2)]]] by auto
  hence "p divides\<^bsub>K[X]\<^esub> q"
    by (meson q assms(2) UP.cgenideal_ideal UP.cgenideal_minimal UP.to_contain_is_to_divide)
  then obtain r where r: "r \ carrier (K[X])" "q = p \\<^bsub>K[X]\<^esub> r"
    by auto
  hence "r \ Units (K[X])"
    using pirreducibleE(3)[OF _ in_carrier q(1) assms(2) r(1)] subfieldE(1)[OF assms(1)]
          pirreducibleE(2)[OF _ assms(2-3)] by auto
  thus "p \\<^bsub>K[X]\<^esub> q"
    using UP.ring_associated_iff[OF in_carrier assms(2)] r(2) UP.associated_sym
    unfolding UP.m_comm[OF assms(2) r(1)] by auto
qed

subsection \<open>Roots and Multiplicity\<close>

definition (in ring) is_root :: "'a list \ 'a \ bool"
  where "is_root p x \ (x \ carrier R \ eval p x = \ \ p \ [])"

definition (in ring) alg_mult :: "'a list \ 'a \ nat"
  where "alg_mult p x =
           (if p = [] then 0 else
             (if x \<in> carrier R then Greatest (\<lambda> n. ([ \<one>, \<ominus> x ] [^]\<^bsub>poly_ring R\<^esub> n) pdivides p) else 0))"

definition (in ring) roots :: "'a list \ 'a multiset"
  where "roots p = Abs_multiset (alg_mult p)"

definition (in ring) roots_on :: "'a set \ 'a list \ 'a multiset"
  where "roots_on K p = roots p \# mset_set K"

definition (in ring) splitted :: "'a list \ bool"
  where "splitted p \ size (roots p) = degree p"

definition (in ring) splitted_on :: "'a set \ 'a list \ bool"
  where "splitted_on K p \ size (roots_on K p) = degree p"

lemma (in domain) pdivides_imp_root_sharing:
  assumes "p \ carrier (poly_ring R)" "p pdivides q" and "a \ carrier R"
  shows "eval p a = \ \ eval q a = \"
proof -
  from \<open>p pdivides q\<close> obtain r where r: "q = p \<otimes>\<^bsub>poly_ring R\<^esub> r" "r \<in> carrier (poly_ring R)"
    unfolding pdivides_def factor_def by auto
  hence "eval q a = (eval p a) \ (eval r a)"
    using ring_hom_memE(2)[OF eval_is_hom[OF carrier_is_subring assms(3)] assms(1) r(2)] by simp
  thus "eval p a = \ \ eval q a = \"
    using ring_hom_memE(1)[OF eval_is_hom[OF carrier_is_subring assms(3)] r(2)] by auto
qed

lemma (in domain) degree_one_root:
  assumes "subfield K R" and "p \ carrier (K[X])" and "degree p = 1"
  shows "eval p (\ (inv (lead_coeff p) \ (const_term p))) = \"
    and "inv (lead_coeff p) \ (const_term p) \ K"
proof -
  from \<open>degree p = 1\<close> have "length p = Suc (Suc 0)"
    by simp
  then obtain a b where p: "p = [ a, b ]"
    by (metis (no_types, hide_lams) Suc_length_conv length_0_conv)
  hence "a \ K - { \ }" "b \ K" and in_carrier: "a \ carrier R" "b \ carrier R"
    using assms(2) subfieldE(3)[OF assms(1)] unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  hence inv_a: "inv a \ carrier R" "a \ inv a = \" and "inv a \ K"
    using subfield_m_inv(1-2)[OF assms(1), of a] subfieldE(3)[OF assms(1)] by auto
  hence "eval p (\ (inv a \ b)) = a \ (\ (inv a \ b)) \ b"
    using in_carrier unfolding p by simp
  also have " ... = \ (a \ (inv a \ b)) \ b"
    using inv_a in_carrier by (simp add: r_minus)
  also have " ... = \"
    using in_carrier(2) unfolding sym[OF m_assoc[OF in_carrier(1) inv_a(1) in_carrier(2)]] inv_a(2) by algebra
  finally have "eval p (\ (inv a \ b)) = \" .
  moreover have ct: "const_term p = b"
    using in_carrier unfolding p const_term_def by auto
  ultimately show "eval p (\ (inv (lead_coeff p) \ (const_term p))) = \"
    unfolding p by simp
  from \<open>inv a \<in> K\<close> and \<open>b \<in> K\<close>
  show "inv (lead_coeff p) \ (const_term p) \ K"
    using p subringE(6)[OF subfieldE(1)[OF assms(1)]] unfolding ct by auto
qed
lemma (in domain) is_root_imp_pdivides:
  assumes "p \ carrier (poly_ring R)"
  shows "is_root p x \ [ \, \ x ] pdivides p"
proof -
  let ?b = "[ \ , \ x ]"

  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  assume "is_root p x" hence x: "x \ carrier R" and is_root: "eval p x = \"
    unfolding is_root_def by auto
  hence b: "?b \ carrier (poly_ring R)"
    unfolding sym[OF univ_poly_carrier] polynomial_def by auto
  then obtain q r where q: "q \ carrier (poly_ring R)" and r: "r \ carrier (poly_ring R)"
    and long_divides: "p = (?b \\<^bsub>poly_ring R\<^esub> q) \\<^bsub>poly_ring R\<^esub> r" "r = [] \ degree r < degree ?b"
    using long_division_theorem[OF carrier_is_subring, of p ?b] assms by (auto simp add: univ_poly_carrier)

  show ?thesis
  proof (cases "r = []")
    case True then have "r = \\<^bsub>poly_ring R\<^esub>"
      unfolding univ_poly_zero[of R "carrier R"] .
    thus ?thesis
      using long_divides(1) q r b dividesI[OF q, of p ?b] by (simp add: pdivides_def)
  next
    case False then have "length r = Suc 0"
      using long_divides(2) le_SucE by fastforce
    then obtain a where "r = [ a ]" and a: "a \ carrier R" and "a \ \"
      using r unfolding sym[OF univ_poly_carrier] polynomial_def
      by (metis False length_0_conv length_Suc_conv list.sel(1) list.set_sel(1) subset_code(1))

    have "eval p x = ((eval ?b x) \ (eval q x)) \ (eval r x)"
      using long_divides(1) ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] by (simp add: b q r)
    also have " ... = eval r x"
      using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring x]] x b q r by (auto, algebra)
    finally have "a = \"
      using a unfolding \<open>r = [ a ]\<close> is_root by simp
    with \<open>a \<noteq> \<zero>\<close> have False .. thus ?thesis ..
  qed
qed

lemma (in domain) pdivides_imp_is_root:
  assumes "p \ []" and "x \ carrier R"
  shows "[ \, \ x ] pdivides p \ is_root p x"
proof -
  assume "[ \, \ x ] pdivides p"
  then obtain q where q: "q \ carrier (poly_ring R)" and pdiv: "p = [ \, \ x ] \\<^bsub>poly_ring R\<^esub> q"
    unfolding pdivides_def by auto
  moreover have "[ \, \ x ] \ carrier (poly_ring R)"
    using assms(2) unfolding sym[OF univ_poly_carrier] polynomial_def by simp
  ultimately have "eval p x = \"
    using ring_hom_memE[OF eval_is_hom[OF carrier_is_subring, of x]] assms(2) by (auto, algebra)
  with \<open>p \<noteq> []\<close> and \<open>x \<in> carrier R\<close> show "is_root p x"
    unfolding is_root_def by simp
qed

lemma (in domain) associated_polynomials_imp_same_is_root:
  assumes "p \ carrier (poly_ring R)" and "q \ carrier (poly_ring R)" and "p \\<^bsub>poly_ring R\<^esub> q"
  shows "is_root p x \ is_root q x"
proof (cases "p = []")
  case True with \<open>p \<sim>\<^bsub>poly_ring R\<^esub> q\<close> have "q = []"
    unfolding associated_def True factor_def univ_poly_def by auto
  thus ?thesis
    using True unfolding is_root_def by simp
next
  case False
  interpret UP: domain "poly_ring R"
    using univ_poly_is_domain[OF carrier_is_subring] .

  { fix p q
    assume p: "p \ carrier (poly_ring R)" and q: "q \ carrier (poly_ring R)" and pq: "p \\<^bsub>poly_ring R\<^esub> q"
    have "is_root p x \ is_root q x"
    proof -
      assume is_root: "is_root p x"
      then have "[ \, \ x ] pdivides p" and "p \ []" and "x \ carrier R"
        using is_root_imp_pdivides[OF p] unfolding is_root_def by auto
      moreover have "[ \, \ x ] \ carrier (poly_ring R)"
        using is_root unfolding is_root_def sym[OF univ_poly_carrier] polynomial_def by simp
      ultimately have "[ \, \ x ] pdivides q"
        using UP.divides_cong_r[OF _ pq ] unfolding pdivides_def by simp
--> --------------------

--> maximum size reached

--> --------------------

¤ Dauer der Verarbeitung: 0.52 Sekunden (vorverarbeitet) ¤

Druckansicht unsichere Verbindung
Druckansicht sprechenden Kalenders
in der Quellcodebibliothek suchen

Haftungshinweis

Die Informationen auf dieser Webseite wurden nach bestem Wissen sorgfältig zusammengestellt. Es wird jedoch weder Vollständigkeit, noch Richtigkeit, noch Qualität der bereit gestellten Informationen zugesichert.

Bemerkung:

Die farbliche Syntaxdarstellung ist noch experimentell.