SSL UnivPoly.thy Sprache: Isabelle

(*  Title:      HOL/Algebra/UnivPoly.thy
    Author:     Clemens Ballarin, started 9 December 1996
    Copyright:  Clemens Ballarin

Contributions, in particular on long division, by Jesus Aransay.
*)

theory UnivPoly
imports Module RingHom
begin

section \<open>Univariate Polynomials\<close>

text \<open>
  Polynomials are formalised as modules with additional operations for
  extracting coefficients from polynomials and for obtaining monomials
  from coefficients and exponents (record \<open>up_ring\<close>).  The
  carrier set is a set of bounded functions from Nat to the
  coefficient domain.  Bounded means that these functions return zero
  above a certain bound (the degree).  There is a chapter on the
  formalisation of polynomials in the PhD thesis \<^cite>\<open>"Ballarin:1999"\<close>,
  which was implemented with axiomatic type classes.  This was later
  ported to Locales.
\<close>

subsection \<open>The Constructor for Univariate Polynomials\<close>

text \<open>
  Functions with finite support.
\<close>

locale bound =
  fixes z :: 'a
    and n :: nat
    and f :: "nat => 'a"
  assumes bound: "!!m. n < m \ f m = z"

declare bound.intro [intro!]
  and bound.bound [dest]

lemma bound_below:
  assumes bound: "bound z m f" and nonzero: "f n \ z" shows "n \ m"
proof (rule classical)
  assume "\ ?thesis"
  then have "m < n" by arith
  with bound have "f n = z" ..
  with nonzero show ?thesis by contradiction
qed

record ('a, 'p) up_ring = "('a, 'p) module" +
  monom :: "['a, nat] => 'p"
  coeff :: "['p, nat] => 'a"

definition
  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
  where "up R = {f. f \ UNIV \ carrier R \ (\n. bound \\<^bsub>R\<^esub> n f)}"

definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
  where "UP R = \
   carrier = up R,
   mult = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
   one = (\<lambda>i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
   zero = (\<lambda>i. \<zero>\<^bsub>R\<^esub>),
   add = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>i. p i \<oplus>\<^bsub>R\<^esub> q i),
   smult = (\<lambda>a\<in>carrier R. \<lambda>p\<in>up R. \<lambda>i. a \<otimes>\<^bsub>R\<^esub> p i),
   monom = (\<lambda>a\<in>carrier R. \<lambda>n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
   coeff = (\<lambda>p\<in>up R. \<lambda>n. p n)\<rparr>"

text \<open>
  Properties of the set of polynomials \<^term>\<open>up\<close>.
\<close>

lemma mem_upI [intro]:
  "[| \n. f n \ carrier R; \n. bound (zero R) n f |] ==> f \ up R"
  by (simp add: up_def Pi_def)

lemma mem_upD [dest]:
  "f \ up R ==> f n \ carrier R"
  by (simp add: up_def Pi_def)

context ring
begin

lemma bound_upD [dest]: "f \ up R \ \n. bound \ n f" by (simp add: up_def)

lemma up_one_closed: "(\n. if n = 0 then \ else \) \ up R" using up_def by force

lemma up_smult_closed: "[| a \ carrier R; p \ up R |] ==> (\i. a \ p i) \ up R" by force

lemma up_add_closed:
  "[| p \ up R; q \ up R |] ==> (\i. p i \ q i) \ up R"
proof
  fix n
  assume "p \ up R" and "q \ up R"
  then show "p n \ q n \ carrier R"
    by auto
next
  assume UP: "p \ up R" "q \ up R"
  show "\n. bound \ n (\i. p i \ q i)"
  proof -
    from UP obtain n where boundn: "bound \ n p" by fast
    from UP obtain m where boundm: "bound \ m q" by fast
    have "bound \ (max n m) (\i. p i \ q i)"
    proof
      fix i
      assume "max n m < i"
      with boundn and boundm and UP show "p i \ q i = \" by fastforce
    qed
    then show ?thesis ..
  qed
qed

lemma up_a_inv_closed:
  "p \ up R ==> (\i. \ (p i)) \ up R"
proof
  assume R: "p \ up R"
  then obtain n where "bound \ n p" by auto
  then have "bound \ n (\i. \ p i)"
    by (simp add: bound_def minus_equality)
  then show "\n. bound \ n (\i. \ p i)" by auto
qed auto

lemma up_minus_closed:
  "[| p \ up R; q \ up R |] ==> (\i. p i \ q i) \ up R"
  unfolding a_minus_def
  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed  by auto

lemma up_mult_closed:
  "[| p \ up R; q \ up R |] ==>
  (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
proof
  fix n
  assume "p \ up R" "q \ up R"
  then show "(\i \ {..n}. p i \ q (n-i)) \ carrier R"
    by (simp add: mem_upD  funcsetI)
next
  assume UP: "p \ up R" "q \ up R"
  show "\n. bound \ n (\n. \i \ {..n}. p i \ q (n-i))"
  proof -
    from UP obtain n where boundn: "bound \ n p" by fast
    from UP obtain m where boundm: "bound \ m q" by fast
    have "bound \ (n + m) (\n. \i \ {..n}. p i \ q (n - i))"
    proof
      fix k assume bound: "n + m < k"
      {
        fix i
        have "p i \ q (k-i) = \"
        proof (cases "n < i")
          case True
          with boundn have "p i = \" by auto
          moreover from UP have "q (k-i) \ carrier R" by auto
          ultimately show ?thesis by simp
        next
          case False
          with bound have "m < k-i" by arith
          with boundm have "q (k-i) = \" by auto
          moreover from UP have "p i \ carrier R" by auto
          ultimately show ?thesis by simp
        qed
      }
      then show "(\i \ {..k}. p i \ q (k-i)) = \"
        by (simp add: Pi_def)
    qed
    then show ?thesis by fast
  qed
qed

end

subsection \<open>Effect of Operations on Coefficients\<close>

locale UP =
  fixes R (structure) and P (structure)
  defines P_def: "P == UP R"

locale UP_ring = UP + R?: ring R

locale UP_cring = UP + R?: cring R

sublocale UP_cring < UP_ring
  by intro_locales [1] (rule P_def)

locale UP_domain = UP + R?: "domain" R

sublocale UP_domain < UP_cring
  by intro_locales [1] (rule P_def)

context UP
begin

text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>

declare P_def [simp]

lemma up_eqI:
  assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \ carrier P" "q \ carrier P"
  shows "p = q"
proof
  fix x
  from prem and R show "p x = q x" by (simp add: UP_def)
qed

lemma coeff_closed [simp]:
  "p \ carrier P ==> coeff P p n \ carrier R" by (auto simp add: UP_def)

end

context UP_ring
begin

(* Theorems generalised from commutative rings to rings by Jesus Aransay. *)

lemma coeff_monom [simp]:
  "a \ carrier R ==> coeff P (monom P a m) n = (if m=n then a else \)"
proof -
  assume R: "a \ carrier R"
  then have "(\n. if n = m then a else \) \ up R"
    using up_def by force
  with R show ?thesis by (simp add: UP_def)
qed

lemma coeff_zero [simp]: "coeff P \\<^bsub>P\<^esub> n = \" by (auto simp add: UP_def)

lemma coeff_one [simp]: "coeff P \\<^bsub>P\<^esub> n = (if n=0 then \ else \)"
  using up_one_closed by (simp add: UP_def)

lemma coeff_smult [simp]:
  "[| a \ carrier R; p \ carrier P |] ==> coeff P (a \\<^bsub>P\<^esub> p) n = a \ coeff P p n"
  by (simp add: UP_def up_smult_closed)

lemma coeff_add [simp]:
  "[| p \ carrier P; q \ carrier P |] ==> coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n"
  by (simp add: UP_def up_add_closed)

lemma coeff_mult [simp]:
  "[| p \ carrier P; q \ carrier P |] ==> coeff P (p \\<^bsub>P\<^esub> q) n = (\i \ {..n}. coeff P p i \ coeff P q (n-i))"
  by (simp add: UP_def up_mult_closed)

end

subsection \<open>Polynomials Form a Ring.\<close>

context UP_ring
begin

text \<open>Operations are closed over \<^term>\<open>P\<close>.\<close>

lemma UP_mult_closed [simp]:
  "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" by (simp add: UP_def up_mult_closed)

lemma UP_one_closed [simp]:
  "\\<^bsub>P\<^esub> \ carrier P" by (simp add: UP_def up_one_closed)

lemma UP_zero_closed [intro, simp]:
  "\\<^bsub>P\<^esub> \ carrier P" by (auto simp add: UP_def)

lemma UP_a_closed [intro, simp]:
  "[| p \ carrier P; q \ carrier P |] ==> p \\<^bsub>P\<^esub> q \ carrier P" by (simp add: UP_def up_add_closed)

lemma monom_closed [simp]:
  "a \ carrier R ==> monom P a n \ carrier P" by (auto simp add: UP_def up_def Pi_def)

lemma UP_smult_closed [simp]:
  "[| a \ carrier R; p \ carrier P |] ==> a \\<^bsub>P\<^esub> p \ carrier P" by (simp add: UP_def up_smult_closed)

end

declare (in UP) P_def [simp del]

text \<open>Algebraic ring properties\<close>

context UP_ring
begin

lemma UP_a_assoc:
  assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
  shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R)

lemma UP_l_zero [simp]:
  assumes R: "p \ carrier P"
  shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)

lemma UP_l_neg_ex:
  assumes R: "p \ carrier P"
  shows "\q \ carrier P. q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>"
proof -
  let ?q = "\i. \ (p i)"
  from R have closed: "?q \ carrier P"
    by (simp add: UP_def P_def up_a_inv_closed)
  from R have coeff: "!!n. coeff P ?q n = \ (coeff P p n)"
    by (simp add: UP_def P_def up_a_inv_closed)
  show ?thesis
  proof
    show "?q \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>"
      by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
  qed (rule closed)
qed

lemma UP_a_comm:
  assumes R: "p \ carrier P" "q \ carrier P"
  shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R)

lemma UP_m_assoc:
  assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
  shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)"
proof (rule up_eqI)
  fix n
  {
    fix k and a b c :: "nat=>'a"
    assume R: "a \ UNIV \ carrier R" "b \ UNIV \ carrier R"
      "c \ UNIV \ carrier R"
    then have "k <= n ==>
      (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
      (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
      (is "_ \ ?eq k")
    proof (induct k)
      case 0 then show ?case by (simp add: Pi_def m_assoc)
    next
      case (Suc k)
      then have "k <= n" by arith
      from this R have "?eq k" by (rule Suc)
      with R show ?case
        by (simp cong: finsum_cong
             add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
    qed
  }
  with R show "coeff P ((p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r) n = coeff P (p \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)) n"
    by (simp add: Pi_def)
qed (simp_all add: R)

lemma UP_r_one [simp]:
  assumes R: "p \ carrier P" shows "p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> = p"
proof (rule up_eqI)
  fix n
  show "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) n = coeff P p n"
  proof (cases n)
    case 0
    {
      with R show ?thesis by simp
    }
  next
    case Suc
    {
      (*JE: in the locale UP_cring the proof was solved only with "by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)", but I did not get it to work here*)
      fix nn assume Succ: "n = Suc nn"
      have "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
      proof -
        have "coeff P (p \\<^bsub>P\<^esub> \\<^bsub>P\<^esub>) (Suc nn) = (\i\{..Suc nn}. coeff P p i \ (if Suc nn \ i then \ else \))" using R by simp
        also have "\ = coeff P p (Suc nn) \ (if Suc nn \ Suc nn then \ else \) \ (\i\{..nn}. coeff P p i \ (if Suc nn \ i then \ else \))"
          using finsum_Suc [of "(\i::nat. coeff P p i \ (if Suc nn \ i then \ else \))" "nn"] unfolding Pi_def using R by simp
        also have "\ = coeff P p (Suc nn) \ (if Suc nn \ Suc nn then \ else \)"
        proof -
          have "(\i\{..nn}. coeff P p i \ (if Suc nn \ i then \ else \)) = (\i\{..nn}. \)"
            using finsum_cong [of "{..nn}" "{..nn}" "(\i::nat. coeff P p i \ (if Suc nn \ i then \ else \))" "(\i::nat. \)"] using R
            unfolding Pi_def by simp
          also have "\ = \" by simp
          finally show ?thesis using r_zero R by simp
        qed
        also have "\ = coeff P p (Suc nn)" using R by simp
        finally show ?thesis by simp
      qed
      then show ?thesis using Succ by simp
    }
  qed
qed (simp_all add: R)

lemma UP_l_one [simp]:
  assumes R: "p \ carrier P"
  shows "\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p = p"
proof (rule up_eqI)
  fix n
  show "coeff P (\\<^bsub>P\<^esub> \\<^bsub>P\<^esub> p) n = coeff P p n"
  proof (cases n)
    case 0 with R show ?thesis by simp
  next
    case Suc with R show ?thesis
      by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
  qed
qed (simp_all add: R)

lemma UP_l_distr:
  assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
  shows "(p \\<^bsub>P\<^esub> q) \\<^bsub>P\<^esub> r = (p \\<^bsub>P\<^esub> r) \\<^bsub>P\<^esub> (q \\<^bsub>P\<^esub> r)"
  by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)

lemma UP_r_distr:
  assumes R: "p \ carrier P" "q \ carrier P" "r \ carrier P"
  shows "r \\<^bsub>P\<^esub> (p \\<^bsub>P\<^esub> q) = (r \\<^bsub>P\<^esub> p) \\<^bsub>P\<^esub> (r \\<^bsub>P\<^esub> q)"
  by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R)

theorem UP_ring: "ring P"
  by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc)
    (auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)

end

subsection \<open>Polynomials Form a Commutative Ring.\<close>

context UP_cring
begin

lemma UP_m_comm:
  assumes R1: "p \ carrier P" and R2: "q \ carrier P" shows "p \\<^bsub>P\<^esub> q = q \\<^bsub>P\<^esub> p"
proof (rule up_eqI)
  fix n
  have l: "(\i \ {..k}. a i \ b (n-i)) = (\i \ {..k}. a (k-i) \ b (i+n-k))" (is "?eq k")
    if "a \ UNIV \ carrier R" "b \ UNIV \ carrier R" and "k <= n"
    for k and a b :: "nat=>'a"
  using that
  proof (induct k)
    case 0 then show ?case by (simp add: Pi_def)
  next
    case (Suc k) then show ?case
      by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
  qed
  from R1 R2 show "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P (q \\<^bsub>P\<^esub> p) n"
    unfolding coeff_mult [OF R1 R2, of n]
    unfolding coeff_mult [OF R2 R1, of n]
    using l [of "(\i. coeff P p i)" "(\i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
qed (simp_all add: R1 R2)

subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>

theorem UP_cring:
  "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)

end

context UP_ring
begin

lemma UP_a_inv_closed [intro, simp]:
  "p \ carrier P ==> \\<^bsub>P\<^esub> p \ carrier P"
  by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]])

lemma coeff_a_inv [simp]:
  assumes R: "p \ carrier P"
  shows "coeff P (\\<^bsub>P\<^esub> p) n = \ (coeff P p n)"
proof -
  from R coeff_closed UP_a_inv_closed have
    "coeff P (\\<^bsub>P\<^esub> p) n = \ coeff P p n \ (coeff P p n \ coeff P (\\<^bsub>P\<^esub> p) n)"
    by algebra
  also from R have "... = \ (coeff P p n)"
    by (simp del: coeff_add add: coeff_add [THEN sym]
      abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
  finally show ?thesis .
qed

end

sublocale UP_ring < P?: ring P using UP_ring .
sublocale UP_cring < P?: cring P using UP_cring .

subsection \<open>Polynomials Form an Algebra\<close>

context UP_ring
begin

lemma UP_smult_l_distr:
  "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==>
  (a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
  by (rule up_eqI) (simp_all add: R.l_distr)

lemma UP_smult_r_distr:
  "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==>
  a \<odot>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> q"
  by (rule up_eqI) (simp_all add: R.r_distr)

lemma UP_smult_assoc1:
      "[| a \ carrier R; b \ carrier R; p \ carrier P |] ==>
      (a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
  by (rule up_eqI) (simp_all add: R.m_assoc)

lemma UP_smult_zero [simp]:
      "p \ carrier P ==> \ \\<^bsub>P\<^esub> p = \\<^bsub>P\<^esub>"
  by (rule up_eqI) simp_all

lemma UP_smult_one [simp]:
      "p \ carrier P ==> \ \\<^bsub>P\<^esub> p = p"
  by (rule up_eqI) simp_all

lemma UP_smult_assoc2:
  "[| a \ carrier R; p \ carrier P; q \ carrier P |] ==>
  (a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
  by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)

end

text \<open>
  Interpretation of lemmas from \<^term>\<open>algebra\<close>.
\<close>

lemma (in UP_cring) UP_algebra:
  "algebra R P" by (auto intro!: algebraI R.cring_axioms UP_cring UP_smult_l_distr UP_smult_r_distr
    UP_smult_assoc1 UP_smult_assoc2)

sublocale UP_cring < algebra R P using UP_algebra .

subsection \<open>Further Lemmas Involving Monomials\<close>

context UP_ring
begin

lemma monom_zero [simp]:
  "monom P \ n = \\<^bsub>P\<^esub>" by (simp add: UP_def P_def)

lemma monom_mult_is_smult:
  assumes R: "a \ carrier R" "p \ carrier P"
  shows "monom P a 0 \\<^bsub>P\<^esub> p = a \\<^bsub>P\<^esub> p"
proof (rule up_eqI)
  fix n
  show "coeff P (monom P a 0 \\<^bsub>P\<^esub> p) n = coeff P (a \\<^bsub>P\<^esub> p) n"
  proof (cases n)
    case 0 with R show ?thesis by simp
  next
    case Suc with R show ?thesis
      using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
  qed
qed (simp_all add: R)

lemma monom_one [simp]:
  "monom P \ 0 = \\<^bsub>P\<^esub>"
  by (rule up_eqI) simp_all

lemma monom_add [simp]:
  "[| a \ carrier R; b \ carrier R |] ==>
  monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
  by (rule up_eqI) simp_all

lemma monom_one_Suc:
  "monom P \ (Suc n) = monom P \ n \\<^bsub>P\<^esub> monom P \ 1"
proof (rule up_eqI)
  fix k
  show "coeff P (monom P \ (Suc n)) k = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k"
  proof (cases "k = Suc n")
    case True show ?thesis
    proof -
      fix m
      from True have less_add_diff:
        "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
      from True have "coeff P (monom P \ (Suc n)) k = \" by simp
      also from True
      have "... = (\i \ {.. {n}. coeff P (monom P \ n) i \
        coeff P (monom P \<one> 1) (k - i))"
        by (simp cong: R.finsum_cong add: Pi_def)
      also have "... = (\i \ {..n}. coeff P (monom P \ n) i \
        coeff P (monom P \<one> 1) (k - i))"
        by (simp only: ivl_disj_un_singleton)
      also from True
      have "... = (\i \ {..n} \ {n<..k}. coeff P (monom P \ n) i \
        coeff P (monom P \<one> 1) (k - i))"
        by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
          order_less_imp_not_eq Pi_def)
      also from True have "... = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k"
        by (simp add: ivl_disj_un_one)
      finally show ?thesis .
    qed
  next
    case False
    note neq = False
    let ?s =
      "\i. (if n = i then \ else \) \ (if Suc 0 = k - i then \ else \)"
    from neq have "coeff P (monom P \ (Suc n)) k = \" by simp
    also have "... = (\i \ {..k}. ?s i)"
    proof -
      have f1: "(\i \ {.."
        by (simp cong: R.finsum_cong add: Pi_def)
      from neq have f2: "(\i \ {n}. ?s i) = \"
        by (simp cong: R.finsum_cong add: Pi_def) arith
      have f3: "n < k ==> (\i \ {n<..k}. ?s i) = \"
        by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
      show ?thesis
      proof (cases "k < n")
        case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def)
      next
        case False then have n_le_k: "n <= k" by arith
        show ?thesis
        proof (cases "n = k")
          case True
          then have "\ = (\i \ {.. {n}. ?s i)"
            by (simp cong: R.finsum_cong add: Pi_def)
          also from True have "... = (\i \ {..k}. ?s i)"
            by (simp only: ivl_disj_un_singleton)
          finally show ?thesis .
        next
          case False with n_le_k have n_less_k: "n < k" by arith
          with neq have "\ = (\i \ {.. {n}. ?s i)"
            by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
          also have "... = (\i \ {..n}. ?s i)"
            by (simp only: ivl_disj_un_singleton)
          also from n_less_k neq have "... = (\i \ {..n} \ {n<..k}. ?s i)"
            by (simp add: R.finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
          also from n_less_k have "... = (\i \ {..k}. ?s i)"
            by (simp only: ivl_disj_un_one)
          finally show ?thesis .
        qed
      qed
    qed
    also have "... = coeff P (monom P \ n \\<^bsub>P\<^esub> monom P \ 1) k" by simp
    finally show ?thesis .
  qed
qed (simp_all)

lemma monom_one_Suc2:
  "monom P \ (Suc n) = monom P \ 1 \\<^bsub>P\<^esub> monom P \ n"
proof (induct n)
  case 0 show ?case by simp
next
  case Suc
  {
    fix k:: nat
    assume hypo: "monom P \ (Suc k) = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k"
    then show "monom P \ (Suc (Suc k)) = monom P \ 1 \\<^bsub>P\<^esub> monom P \ (Suc k)"
    proof -
      have lhs: "monom P \ (Suc (Suc k)) = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k \\<^bsub>P\<^esub> monom P \ 1"
        unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
      note cl = monom_closed [OF R.one_closed, of 1]
      note clk = monom_closed [OF R.one_closed, of k]
      have rhs: "monom P \ 1 \\<^bsub>P\<^esub> monom P \ (Suc k) = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k \\<^bsub>P\<^esub> monom P \ 1"
        unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
      from lhs rhs show ?thesis by simp
    qed
  }
qed

text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
  and @{thm "monom_one_Suc2"}, and is trivial in \<^term>\<open>UP_cring\<close>\<close>

corollary monom_one_comm: shows "monom P \ k \\<^bsub>P\<^esub> monom P \ 1 = monom P \ 1 \\<^bsub>P\<^esub> monom P \ k"
  unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..

lemma monom_mult_smult:
  "[| a \ carrier R; b \ carrier R |] ==> monom P (a \ b) n = a \\<^bsub>P\<^esub> monom P b n"
  by (rule up_eqI) simp_all

lemma monom_one_mult:
  "monom P \ (n + m) = monom P \ n \\<^bsub>P\<^esub> monom P \ m"
proof (induct n)
  case 0 show ?case by simp
next
  case Suc then show ?case
    unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps
    using m_assoc monom_one_comm [of m] by simp
qed

lemma monom_one_mult_comm: "monom P \ n \\<^bsub>P\<^esub> monom P \ m = monom P \ m \\<^bsub>P\<^esub> monom P \ n"
  unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all

lemma monom_mult [simp]:
  assumes a_in_R: "a \ carrier R" and b_in_R: "b \ carrier R"
  shows "monom P (a \ b) (n + m) = monom P a n \\<^bsub>P\<^esub> monom P b m"
proof (rule up_eqI)
  fix k
  show "coeff P (monom P (a \ b) (n + m)) k = coeff P (monom P a n \\<^bsub>P\<^esub> monom P b m) k"
  proof (cases "n + m = k")
    case True
    {
      show ?thesis
        unfolding True [symmetric]
          coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
          coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
        using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\i. (if n = i then a else \) \ (if m = n + m - i then b else \))"
          "(\i. if n = i then a \ b else \)"]
          a_in_R b_in_R
        unfolding simp_implies_def
        using R.finsum_singleton [of n "{.. n + m}" "(\i. a \ b)"]
        unfolding Pi_def by auto
    }
  next
    case False
    {
      show ?thesis
        unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False)
        unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k]
        unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False
        using R.finsum_cong [of "{..k}" "{..k}" "(\i. (if n = i then a else \) \ (if m = k - i then b else \))" "(\i. \)"]
        unfolding Pi_def simp_implies_def using a_in_R b_in_R by force
    }
  qed
qed (simp_all add: a_in_R b_in_R)

lemma monom_a_inv [simp]:
  "a \ carrier R ==> monom P (\ a) n = \\<^bsub>P\<^esub> monom P a n"
  by (rule up_eqI) auto

lemma monom_inj:
  "inj_on (\a. monom P a n) (carrier R)"
proof (rule inj_onI)
  fix x y
  assume R: "x \ carrier R" "y \ carrier R" and eq: "monom P x n = monom P y n"
  then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
  with R show "x = y" by simp
qed

end

subsection \<open>The Degree Function\<close>

definition
  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
  where "deg R p = (LEAST n. bound \\<^bsub>R\<^esub> n (coeff (UP R) p))"

context UP_ring
begin

lemma deg_aboveI:
  "[| (!!m. n < m ==> coeff P p m = \); p \ carrier P |] ==> deg R p <= n"
  by (unfold deg_def P_def) (fast intro: Least_le)

(*
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
proof -
  have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  then show ?thesis ..
qed

lemma bound_coeff_obtain:
  assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
proof -
  have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
  then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
  with prem show P .
qed
*)

lemma deg_aboveD:
  assumes "deg R p < m" and "p \ carrier P"
  shows "coeff P p m = \"
proof -
  from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
    by (auto simp add: UP_def P_def)
  then have "bound \ (deg R p) (coeff P p)"
    by (auto simp: deg_def P_def dest: LeastI)
  from this and \<open>deg R p < m\<close> show ?thesis ..
qed

lemma deg_belowI:
  assumes non_zero: "n \ 0 \ coeff P p n \ \"
    and R: "p \ carrier P"
  shows "n \ deg R p"
\<comment> \<open>Logically, this is a slightly stronger version of
   @{thm [source] deg_aboveD}\<close>
proof (cases "n=0")
  case True then show ?thesis by simp
next
  case False then have "coeff P p n \ \" by (rule non_zero)
  then have "\ deg R p < n" by (fast dest: deg_aboveD intro: R)
  then show ?thesis by arith
qed

lemma lcoeff_nonzero_deg:
  assumes deg: "deg R p \ 0" and R: "p \ carrier P"
  shows "coeff P p (deg R p) \ \"
proof -
  from R obtain m where "deg R p \ m" and m_coeff: "coeff P p m \ \"
  proof -
    have minus: "\(n::nat) m. n \ 0 \ (n - Suc 0 < m) = (n \ m)"
      by arith
    from deg have "deg R p - 1 < (LEAST n. bound \ n (coeff P p))"
      by (unfold deg_def P_def) simp
    then have "\ bound \ (deg R p - 1) (coeff P p)" by (rule not_less_Least)
    then have "\m. deg R p - 1 < m \ coeff P p m \ \"
      by (unfold bound_def) fast
    then have "\m. deg R p \ m \ coeff P p m \ \" by (simp add: deg minus)
    then show ?thesis by (auto intro: that)
  qed
  with deg_belowI R have "deg R p = m" by fastforce
  with m_coeff show ?thesis by simp
qed

lemma lcoeff_nonzero_nonzero:
  assumes deg: "deg R p = 0" and nonzero: "p \ \\<^bsub>P\<^esub>" and R: "p \ carrier P"
  shows "coeff P p 0 \ \"
proof -
  have "\m. coeff P p m \ \"
  proof (rule classical)
    assume "\ ?thesis"
    with R have "p = \\<^bsub>P\<^esub>" by (auto intro: up_eqI)
    with nonzero show ?thesis by contradiction
  qed
  then obtain m where coeff: "coeff P p m \ \" ..
  from this and R have "m \ deg R p" by (rule deg_belowI)
  then have "m = 0" by (simp add: deg)
  with coeff show ?thesis by simp
qed

lemma lcoeff_nonzero:
  assumes neq: "p \ \\<^bsub>P\<^esub>" and R: "p \ carrier P"
  shows "coeff P p (deg R p) \ \"
proof (cases "deg R p = 0")
  case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
next
  case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
qed

lemma deg_eqI:
  "[| \m. n < m \ coeff P p m = \;
      \<And>n. n \<noteq> 0 \<Longrightarrow> coeff P p n \<noteq> \<zero>; p \<in> carrier P |] ==> deg R p = n"
by (fast intro: le_antisym deg_aboveI deg_belowI)

text \<open>Degree and polynomial operations\<close>

lemma deg_add [simp]:
  "p \ carrier P \ q \ carrier P \
  deg R (p \<oplus>\<^bsub>P\<^esub> q) \<le> max (deg R p) (deg R q)"
by(rule deg_aboveI)(simp_all add: deg_aboveD)

lemma deg_monom_le:
  "a \ carrier R \ deg R (monom P a n) \ n"
  by (intro deg_aboveI) simp_all

lemma deg_monom [simp]:
  "[| a \ \; a \ carrier R |] ==> deg R (monom P a n) = n"
  by (fastforce intro: le_antisym deg_aboveI deg_belowI)

lemma deg_const [simp]:
  assumes R: "a \ carrier R" shows "deg R (monom P a 0) = 0"
proof (rule le_antisym)
  show "deg R (monom P a 0) \ 0" by (rule deg_aboveI) (simp_all add: R)
next
  show "0 \ deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
qed

lemma deg_zero [simp]:
  "deg R \\<^bsub>P\<^esub> = 0"
proof (rule le_antisym)
  show "deg R \\<^bsub>P\<^esub> \ 0" by (rule deg_aboveI) simp_all
next
  show "0 \ deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
qed

lemma deg_one [simp]:
  "deg R \\<^bsub>P\<^esub> = 0"
proof (rule le_antisym)
  show "deg R \\<^bsub>P\<^esub> \ 0" by (rule deg_aboveI) simp_all
next
  show "0 \ deg R \\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
qed

lemma deg_uminus [simp]:
  assumes R: "p \ carrier P" shows "deg R (\\<^bsub>P\<^esub> p) = deg R p"
proof (rule le_antisym)
  show "deg R (\\<^bsub>P\<^esub> p) \ deg R p" by (simp add: deg_aboveI deg_aboveD R)
next
  show "deg R p \ deg R (\\<^bsub>P\<^esub> p)"
    by (simp add: deg_belowI lcoeff_nonzero_deg
      inj_on_eq_iff [OF R.a_inv_inj, of _ "\", simplified] R)
qed

text\<open>The following lemma is later \emph{overwritten} by the most
  specific one for domains, \<open>deg_smult\<close>.\<close>

lemma deg_smult_ring [simp]:
  "[| a \ carrier R; p \ carrier P |] ==>
  deg R (a \<odot>\<^bsub>P\<^esub> p) \<le> (if a = \<zero> then 0 else deg R p)"
  by (cases "a = \") (simp add: deg_aboveI deg_aboveD)+

end

context UP_domain
begin

lemma deg_smult [simp]:
  assumes R: "a \ carrier R" "p \ carrier P"
  shows "deg R (a \\<^bsub>P\<^esub> p) = (if a = \ then 0 else deg R p)"
proof (rule le_antisym)
  show "deg R (a \\<^bsub>P\<^esub> p) \ (if a = \ then 0 else deg R p)"
    using R by (rule deg_smult_ring)
next
  show "(if a = \ then 0 else deg R p) \ deg R (a \\<^bsub>P\<^esub> p)"
  proof (cases "a = \")
  qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
qed

end

context UP_ring
begin

lemma deg_mult_ring:
  assumes R: "p \ carrier P" "q \ carrier P"
  shows "deg R (p \\<^bsub>P\<^esub> q) \ deg R p + deg R q"
proof (rule deg_aboveI)
  fix m
  assume boundm: "deg R p + deg R q < m"
  {
    fix k i
    assume boundk: "deg R p + deg R q < k"
    then have "coeff P p i \ coeff P q (k - i) = \"
    proof (cases "deg R p < i")
      case True then show ?thesis by (simp add: deg_aboveD R)
    next
      case False with boundk have "deg R q < k - i" by arith
      then show ?thesis by (simp add: deg_aboveD R)
    qed
  }
  with boundm R show "coeff P (p \\<^bsub>P\<^esub> q) m = \" by simp
qed (simp add: R)

end

context UP_domain
begin

lemma deg_mult [simp]:
  "[| p \ \\<^bsub>P\<^esub>; q \ \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==>
  deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
proof (rule le_antisym)
  assume "p \ carrier P" " q \ carrier P"
  then show "deg R (p \\<^bsub>P\<^esub> q) \ deg R p + deg R q" by (rule deg_mult_ring)
next
  let ?s = "(\i. coeff P p i \ coeff P q (deg R p + deg R q - i))"
  assume R: "p \ carrier P" "q \ carrier P" and nz: "p \ \\<^bsub>P\<^esub>" "q \ \\<^bsub>P\<^esub>"
  have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
  show "deg R p + deg R q \ deg R (p \\<^bsub>P\<^esub> q)"
  proof (rule deg_belowI, simp add: R)
    have "(\i \ {.. deg R p + deg R q}. ?s i)
      = (\<Oplus>i \<in> {..< deg R p} \<union> {deg R p .. deg R p + deg R q}. ?s i)"
      by (simp only: ivl_disj_un_one)
    also have "... = (\i \ {deg R p .. deg R p + deg R q}. ?s i)"
      by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
        deg_aboveD less_add_diff R Pi_def)
    also have "...= (\i \ {deg R p} \ {deg R p <.. deg R p + deg R q}. ?s i)"
      by (simp only: ivl_disj_un_singleton)
    also have "... = coeff P p (deg R p) \ coeff P q (deg R q)"
      by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
    finally have "(\i \ {.. deg R p + deg R q}. ?s i)
      = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
    with nz show "(\i \ {.. deg R p + deg R q}. ?s i) \ \"
      by (simp add: integral_iff lcoeff_nonzero R)
  qed (simp add: R)
qed

end

text\<open>The following lemmas also can be lifted to \<^term>\<open>UP_ring\<close>.\<close>

context UP_ring
begin

lemma coeff_finsum:
  assumes fin: "finite A"
  shows "p \ A \ carrier P ==>
    coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
  using fin by induct (auto simp: Pi_def)

lemma up_repr:
  assumes R: "p \ carrier P"
  shows "(\\<^bsub>P\<^esub> i \ {..deg R p}. monom P (coeff P p i) i) = p"
proof (rule up_eqI)
  let ?s = "(\i. monom P (coeff P p i) i)"
  fix k
  from R have RR: "!!i. (if i = k then coeff P p i else \) \ carrier R"
    by simp
  show "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k = coeff P p k"
  proof (cases "k \ deg R p")
    case True
    hence "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k =
          coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k} \<union> {k<..deg R p}. ?s i) k"
      by (simp only: ivl_disj_un_one)
    also from True
    have "... = coeff P (\\<^bsub>P\<^esub> i \ {..k}. ?s i) k"
      by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint
        ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
    also
    have "... = coeff P (\\<^bsub>P\<^esub> i \ {.. {k}. ?s i) k"
      by (simp only: ivl_disj_un_singleton)
    also have "... = coeff P p k"
      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
    finally show ?thesis .
  next
    case False
    hence "coeff P (\\<^bsub>P\<^esub> i \ {..deg R p}. ?s i) k =
          coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
      by (simp only: ivl_disj_un_singleton)
    also from False have "... = coeff P p k"
      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
    finally show ?thesis .
  qed
qed (simp_all add: R Pi_def)

lemma up_repr_le:
  "[| deg R p <= n; p \ carrier P |] ==>
  (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
proof -
  let ?s = "(\i. monom P (coeff P p i) i)"
  assume R: "p \ carrier P" and "deg R p <= n"
  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \ {deg R p<..n})"
    by (simp only: ivl_disj_un_one)
  also have "... = finsum P ?s {..deg R p}"
    by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one
      deg_aboveD R Pi_def)
  also have "... = p" using R by (rule up_repr)
  finally show ?thesis .
qed

end

subsection \<open>Polynomials over Integral Domains\<close>

lemma domainI:
  assumes cring: "cring R"
    and one_not_zero: "one R \ zero R"
    and integral: "\a b. [| mult R a b = zero R; a \ carrier R;
      b \<in> carrier R |] ==> a = zero R \<or> b = zero R"
  shows "domain R"
  by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
    del: disjCI)

context UP_domain
begin

lemma UP_one_not_zero:
  "\\<^bsub>P\<^esub> \ \\<^bsub>P\<^esub>"
proof
  assume "\\<^bsub>P\<^esub> = \\<^bsub>P\<^esub>"
  hence "coeff P \\<^bsub>P\<^esub> 0 = (coeff P \\<^bsub>P\<^esub> 0)" by simp
  hence "\ = \" by simp
  with R.one_not_zero show "False" by contradiction
qed

lemma UP_integral:
  "[| p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>; p \ carrier P; q \ carrier P |] ==> p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>"
proof -
  fix p q
  assume pq: "p \\<^bsub>P\<^esub> q = \\<^bsub>P\<^esub>" and R: "p \ carrier P" "q \ carrier P"
  show "p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>"
  proof (rule classical)
    assume c: "\ (p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>)"
    with R have "deg R p + deg R q = deg R (p \\<^bsub>P\<^esub> q)" by simp
    also from pq have "... = 0" by simp
    finally have "deg R p + deg R q = 0" .
    then have f1: "deg R p = 0 \ deg R q = 0" by simp
    from f1 R have "p = (\\<^bsub>P\<^esub> i \ {..0}. monom P (coeff P p i) i)"
      by (simp only: up_repr_le)
    also from R have "... = monom P (coeff P p 0) 0" by simp
    finally have p: "p = monom P (coeff P p 0) 0" .
    from f1 R have "q = (\\<^bsub>P\<^esub> i \ {..0}. monom P (coeff P q i) i)"
      by (simp only: up_repr_le)
    also from R have "... = monom P (coeff P q 0) 0" by simp
    finally have q: "q = monom P (coeff P q 0) 0" .
    from R have "coeff P p 0 \ coeff P q 0 = coeff P (p \\<^bsub>P\<^esub> q) 0" by simp
    also from pq have "... = \" by simp
    finally have "coeff P p 0 \ coeff P q 0 = \" .
    with R have "coeff P p 0 = \ \ coeff P q 0 = \"
      by (simp add: R.integral_iff)
    with p q show "p = \\<^bsub>P\<^esub> \ q = \\<^bsub>P\<^esub>" by fastforce
  qed
qed

theorem UP_domain:
  "domain P"
  by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)

end

text \<open>
  Interpretation of theorems from \<^term>\<open>domain\<close>.
\<close>

sublocale UP_domain < "domain" P
  by intro_locales (rule domain.axioms UP_domain)+

subsection \<open>The Evaluation Homomorphism and Universal Property\<close>

(* alternative congruence rule (possibly more efficient)
lemma (in abelian_monoid) finsum_cong2:
  "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
  !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
  sorry*)

lemma (in abelian_monoid) boundD_carrier:
  "[| bound \ n f; n < m |] ==> f m \ carrier G"
  by auto

context ring
begin

theorem diagonal_sum:
  "[| f \ {..n + m::nat} \ carrier R; g \ {..n + m} \ carrier R |] ==>
  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
  (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
proof -
  assume Rf: "f \ {..n + m} \ carrier R" and Rg: "g \ {..n + m} \ carrier R"
  {
    fix j
    have "j <= n + m ==>
      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
      (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
    proof (induct j)
      case 0 from Rf Rg show ?case by (simp add: Pi_def)
    next
      case (Suc j)
      have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \ carrier R"
        using Suc by (auto intro!: funcset_mem [OF Rg])
      have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \ carrier R"
        using Suc by (auto intro!: funcset_mem [OF Rg])
      have R9: "!!i k. [| k <= Suc j |] ==> f k \ carrier R"
        using Suc by (auto intro!: funcset_mem [OF Rf])
      have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \ carrier R"
        using Suc by (auto intro!: funcset_mem [OF Rg])
      have R11: "g 0 \ carrier R"
        using Suc by (auto intro!: funcset_mem [OF Rg])
      from Suc show ?case
        by (simp cong: finsum_cong add: Suc_diff_le a_ac
          Pi_def R6 R8 R9 R10 R11)
    qed
  }
  then show ?thesis by fast
qed

theorem cauchy_product:
  assumes bf: "bound \ n f" and bg: "bound \ m g"
    and Rf: "f \ {..n} \ carrier R" and Rg: "g \ {..m} \ carrier R"
  shows "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) =
    (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"      (* State reverse direction? *)
proof -
  have f: "!!x. f x \ carrier R"
  proof -
    fix x
    show "f x \ carrier R"
      using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
  qed
  have g: "!!x. g x \ carrier R"
  proof -
    fix x
    show "g x \ carrier R"
      using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
  qed
  from f g have "(\k \ {..n + m}. \i \ {..k}. f i \ g (k - i)) =
      (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
    by (simp add: diagonal_sum Pi_def)
  also have "... = (\k \ {..n} \ {n<..n + m}. \i \ {..n + m - k}. f k \ g i)"
    by (simp only: ivl_disj_un_one)
  also from f g have "... = (\k \ {..n}. \i \ {..n + m - k}. f k \ g i)"
    by (simp cong: finsum_cong
      add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  also from f g
  have "... = (\k \ {..n}. \i \ {..m} \ {m<..n + m - k}. f k \ g i)"
    by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
  also from f g have "... = (\k \ {..n}. \i \ {..m}. f k \ g i)"
    by (simp cong: finsum_cong
      add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
  also from f g have "... = (\i \ {..n}. f i) \ (\i \ {..m}. g i)"
    by (simp add: finsum_ldistr diagonal_sum Pi_def,
      simp cong: finsum_cong add: finsum_rdistr Pi_def)
  finally show ?thesis .
qed

end

lemma (in UP_ring) const_ring_hom:
  "(\a. monom P a 0) \ ring_hom R P"
  by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)

definition
  eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
           'a => 'b, 'b, nat => 'a] => 'b"
  where "eval R S phi s = (\p \ carrier (UP R).
    \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"

context UP
begin

lemma eval_on_carrier:
  fixes S (structure)
  shows "p \ carrier P ==>
  eval R S phi s p = (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
  by (unfold eval_def, fold P_def) simp

lemma eval_extensional:
  "eval R S phi p \ extensional (carrier P)"
  by (unfold eval_def, fold P_def) simp

end

text \<open>The universal property of the polynomial ring\<close>

locale UP_pre_univ_prop = ring_hom_cring + UP_cring

locale UP_univ_prop = UP_pre_univ_prop +
  fixes s and Eval
  assumes indet_img_carrier [simp, intro]: "s \ carrier S"
  defines Eval_def: "Eval == eval R S h s"

text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale \<^term>\<open>ring_hom_ring\<close> from \<^term>\<open>ring_hom_cring\<close>.\<close>
text\<open>JE: I was considering using it in \<open>eval_ring_hom\<close>, but that property does not hold for non commutative rings, so
  maybe it is not that necessary.\<close>

lemma (in ring_hom_ring) hom_finsum [simp]:
  "f \ A \ carrier R \
  h (finsum R f A) = finsum S (h \<circ> f) A"
  by (induct A rule: infinite_finite_induct, auto simp: Pi_def)

context UP_pre_univ_prop
begin

theorem eval_ring_hom:
  assumes S: "s \ carrier S"
  shows "eval R S h s \ ring_hom P S"
proof (rule ring_hom_memI)
  fix p
  assume R: "p \ carrier P"
  then show "eval R S h s p \ carrier S"
    by (simp only: eval_on_carrier) (simp add: S Pi_def)
next
  fix p q
  assume R: "p \ carrier P" "q \ carrier P"
  then show "eval R S h s (p \\<^bsub>P\<^esub> q) = eval R S h s p \\<^bsub>S\<^esub> eval R S h s q"
  proof (simp only: eval_on_carrier P.a_closed)
    from S R have
      "(\\<^bsub>S \<^esub>i\{..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
      (\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<oplus>\<^bsub>P\<^esub> q)<..max (deg R p) (deg R q)}.
        h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp cong: S.finsum_cong
        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def del: coeff_add)
    also from R have "... =
        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
          h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp add: ivl_disj_un_one)
    also from R S have "... =
      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
      (\<Oplus>\<^bsub>S\<^esub>i\<in>{..max (deg R p) (deg R q)}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp cong: S.finsum_cong
        add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def)
    also have "... =
        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
          h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
        (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
          h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
    also from R S have "... =
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp cong: S.finsum_cong
        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
    finally show
      "(\\<^bsub>S\<^esub>i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
      (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)" .
  qed
next
  show "eval R S h s \\<^bsub>P\<^esub> = \\<^bsub>S\<^esub>"
    by (simp only: eval_on_carrier UP_one_closed) simp
next
  fix p q
  assume R: "p \ carrier P" "q \ carrier P"
  then show "eval R S h s (p \\<^bsub>P\<^esub> q) = eval R S h s p \\<^bsub>S\<^esub> eval R S h s q"
  proof (simp only: eval_on_carrier UP_mult_closed)
    from R S have
      "(\\<^bsub>S\<^esub> i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)} \<union> {deg R (p \<otimes>\<^bsub>P\<^esub> q)<..deg R p + deg R q}.
        h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp cong: S.finsum_cong
        add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
        del: coeff_mult)
    also from R have "... =
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp only: ivl_disj_un_one deg_mult_ring)
    also from R S have "... =
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
         \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
           h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
           (s [^]\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> (i - k)))"
      by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
        S.m_ac S.finsum_rdistr)
    also from R S have "... =
      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
      (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
      by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
        Pi_def)
    finally show
      "(\\<^bsub>S\<^esub> i \ {..deg R (p \\<^bsub>P\<^esub> q)}. h (coeff P (p \\<^bsub>P\<^esub> q) i) \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) \<otimes>\<^bsub>S\<^esub>
      (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)" .
  qed
qed

text \<open>
  The following lemma could be proved in \<open>UP_cring\<close> with the additional
  assumption that \<open>h\<close> is closed.\<close>

lemma (in UP_pre_univ_prop) eval_const:
  "[| s \ carrier S; r \ carrier R |] ==> eval R S h s (monom P r 0) = h r"
  by (simp only: eval_on_carrier monom_closed) simp

text \<open>Further properties of the evaluation homomorphism.\<close>

text \<open>The following proof is complicated by the fact that in arbitrary
  rings one might have \<^term>\<open>one R = zero R\<close>.\<close>

(* TODO: simplify by cases "one R = zero R" *)

lemma (in UP_pre_univ_prop) eval_monom1:
  assumes S: "s \ carrier S"
  shows "eval R S h s (monom P \ 1) = s"
proof (simp only: eval_on_carrier monom_closed R.one_closed)
   from S have
    "(\\<^bsub>S\<^esub> i\{..deg R (monom P \ 1)}. h (coeff P (monom P \ 1) i) \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) =
    (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
      h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    by (simp cong: S.finsum_cong del: coeff_monom
      add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
  also have "... =
    (\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i)"
    by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
  also have "... = s"
  proof (cases "s = \\<^bsub>S\<^esub>")
    case True then show ?thesis by (simp add: Pi_def)
  next
    case False then show ?thesis by (simp add: S Pi_def)
  qed
  finally show "(\\<^bsub>S\<^esub> i \ {..deg R (monom P \ 1)}.
    h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> i) = s" .
qed

end

text \<open>Interpretation of ring homomorphism lemmas.\<close>

sublocale UP_univ_prop < ring_hom_cring P S Eval
  unfolding Eval_def
  by unfold_locales (fast intro: eval_ring_hom)

lemma (in UP_cring) monom_pow:
  assumes R: "a \ carrier R"
  shows "(monom P a n) [^]\<^bsub>P\<^esub> m = monom P (a [^] m) (n * m)"
proof (induct m)
  case 0 from R show ?case by simp
next
  case Suc with R show ?case
    by (simp del: monom_mult add: monom_mult [THEN sym] add.commute)
qed

lemma (in ring_hom_cring) hom_pow [simp]:
  "x \ carrier R ==> h (x [^] n) = h x [^]\<^bsub>S\<^esub> (n::nat)"
  by (induct n) simp_all

lemma (in UP_univ_prop) Eval_monom:
  "r \ carrier R ==> Eval (monom P r n) = h r \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
proof -
  assume R: "r \ carrier R"
  from R have "Eval (monom P r n) = Eval (monom P r 0 \\<^bsub>P\<^esub> (monom P \ 1) [^]\<^bsub>P\<^esub> n)"
    by (simp del: monom_mult add: monom_mult [THEN sym] monom_pow)
  also
  from R eval_monom1 [where s = s, folded Eval_def]
  have "... = h r \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
    by (simp add: eval_const [where s = s, folded Eval_def])
  finally show ?thesis .
qed

lemma (in UP_pre_univ_prop) eval_monom:
  assumes R: "r \ carrier R" and S: "s \ carrier S"
  shows "eval R S h s (monom P r n) = h r \\<^bsub>S\<^esub> s [^]\<^bsub>S\<^esub> n"
proof -
  interpret UP_univ_prop R S h P s "eval R S h s"
    using UP_pre_univ_prop_axioms P_def R S
    by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
  from R
  show ?thesis by (rule Eval_monom)
qed

lemma (in UP_univ_prop) Eval_smult:
  "[| r \ carrier R; p \ carrier P |] ==> Eval (r \\<^bsub>P\<^esub> p) = h r \\<^bsub>S\<^esub> Eval p"
proof -
  assume R: "r \ carrier R" and P: "p \ carrier P"
  then show ?thesis
    by (simp add: monom_mult_is_smult [THEN sym]
      eval_const [where s = s, folded Eval_def])
qed

lemma ring_hom_cringI:
  assumes "cring R"
    and "cring S"
    and "h \ ring_hom R S"
  shows "ring_hom_cring R S h"
  by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
    cring.axioms assms)

context UP_pre_univ_prop
begin

lemma UP_hom_unique:
  assumes "ring_hom_cring P S Phi"
  assumes Phi: "Phi (monom P \ (Suc 0)) = s"
      "!!r. r \ carrier R ==> Phi (monom P r 0) = h r"
  assumes "ring_hom_cring P S Psi"
  assumes Psi: "Psi (monom P \ (Suc 0)) = s"
      "!!r. r \ carrier R ==> Psi (monom P r 0) = h r"
    and P: "p \ carrier P" and S: "s \ carrier S"
  shows "Phi p = Psi p"
proof -
  interpret ring_hom_cring P S Phi by fact
  interpret ring_hom_cring P S Psi by fact
  have "Phi p =
      Phi (\<Oplus>\<^bsub>P \<^esub>i \<in> {..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 [^]\<^bsub>P\<^esub> i)"
    by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
  also
  have "... =
      Psi (\<Oplus>\<^bsub>P \<^esub>i\<in>{..deg R p}. monom P (coeff P p i) 0 \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 [^]\<^bsub>P\<^esub> i)"
    by (simp add: Phi Psi P Pi_def comp_def)
  also have "... = Psi p"
    by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
  finally show ?thesis .
qed

lemma ring_homD:
  assumes Phi: "Phi \ ring_hom P S"
  shows "ring_hom_cring P S Phi"
  by unfold_locales (rule Phi)

theorem UP_universal_property:
  assumes S: "s \ carrier S"
  shows "\!Phi. Phi \ ring_hom P S \ extensional (carrier P) \
    Phi (monom P \<one> 1) = s \<and>
    (\<forall>r \<in> carrier R. Phi (monom P r 0) = h r)"
  using S eval_monom1
  apply (auto intro: eval_ring_hom eval_const eval_extensional)
  apply (rule extensionalityI)
  apply (auto intro: UP_hom_unique ring_homD)
  done

end

text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>

context monoid
begin

lemma nat_pow_eone[simp]: assumes x_in_G: "x \ carrier G" shows "x [^] (1::nat) = x"
  using nat_pow_Suc [of x 0] unfolding nat_pow_0 [of x] unfolding l_one [OF x_in_G] by simp

end

context UP_ring
begin

abbreviation lcoeff :: "(nat =>'a) => 'a" where "lcoeff p == coeff P p (deg R p)"

lemma lcoeff_nonzero2: assumes p_in_R: "p \ carrier P" and p_not_zero: "p \ \\<^bsub>P\<^esub>" shows "lcoeff p \ \"
  using lcoeff_nonzero [OF p_not_zero p_in_R] .

subsection\<open>The long division algorithm: some previous facts.\<close>

lemma coeff_minus [simp]:
  assumes p: "p \ carrier P" and q: "q \ carrier P"
  shows "coeff P (p \\<^bsub>P\<^esub> q) n = coeff P p n \ coeff P q n"
  by (simp add: a_minus_def p q)

lemma lcoeff_closed [simp]: assumes p: "p \ carrier P" shows "lcoeff p \ carrier R"
  using coeff_closed [OF p, of "deg R p"] by simp

lemma deg_smult_decr: assumes a_in_R: "a \ carrier R" and f_in_P: "f \ carrier P" shows "deg R (a \\<^bsub>P\<^esub> f) \ deg R f"
  using deg_smult_ring [OF a_in_R f_in_P] by (cases "a = \", auto)

lemma coeff_monom_mult: assumes R: "c \ carrier R" and P: "p \ carrier P"
  shows "coeff P (monom P c n \\<^bsub>P\<^esub> p) (m + n) = c \ (coeff P p m)"
proof -
  have "coeff P (monom P c n \\<^bsub>P\<^esub> p) (m + n) = (\i\{..m + n}. (if n = i then c else \) \ coeff P p (m + n - i))"
    unfolding coeff_mult [OF monom_closed [OF R, of n] P, of "m + n"] unfolding coeff_monom [OF R, of n] by simp
  also have "(\i\{..m + n}. (if n = i then c else \) \ coeff P p (m + n - i)) =
    (\<Oplus>i\<in>{..m + n}. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"
    using  R.finsum_cong [of "{..m + n}" "{..m + n}" "(\i::nat. (if n = i then c else \) \ coeff P p (m + n - i))"
      "(\i::nat. (if n = i then c \ coeff P p (m + n - i) else \))"]
    using coeff_closed [OF P] unfolding Pi_def simp_implies_def using R by auto
  also have "\ = c \ coeff P p m" using R.finsum_singleton [of n "{..m + n}" "(\i. c \ coeff P p (m + n - i))"]
    unfolding Pi_def using coeff_closed [OF P] using P R by auto
  finally show ?thesis by simp
qed

lemma deg_lcoeff_cancel:
  assumes p_in_P: "p \ carrier P" and q_in_P: "q \ carrier P" and r_in_P: "r \ carrier P"
  and deg_r_nonzero: "deg R r \ 0"
  and deg_R_p: "deg R p \ deg R r" and deg_R_q: "deg R q \ deg R r"
  and coeff_R_p_eq_q: "coeff P p (deg R r) = \\<^bsub>R\<^esub> (coeff P q (deg R r))"
  shows "deg R (p \\<^bsub>P\<^esub> q) < deg R r"
proof -
  have deg_le: "deg R (p \\<^bsub>P\<^esub> q) \ deg R r"
  proof (rule deg_aboveI)
    fix m
    assume deg_r_le: "deg R r < m"
    show "coeff P (p \\<^bsub>P\<^esub> q) m = \"
    proof -
      have slp: "deg R p < m" and "deg R q < m" using deg_R_p deg_R_q using deg_r_le by auto
      then have max_sl: "max (deg R p) (deg R q) < m" by simp
      then have "deg R (p \\<^bsub>P\<^esub> q) < m" using deg_add [OF p_in_P q_in_P] by arith
      with deg_R_p deg_R_q show ?thesis using coeff_add [OF p_in_P q_in_P, of m]
        using deg_aboveD [of "p \\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp
    qed
  qed (simp add: p_in_P q_in_P)
  moreover have deg_ne: "deg R (p \\<^bsub>P\<^esub> q) \ deg R r"
  proof (rule ccontr)
    assume nz: "\ deg R (p \\<^bsub>P\<^esub> q) \ deg R r" then have deg_eq: "deg R (p \\<^bsub>P\<^esub> q) = deg R r" by simp
    from deg_r_nonzero have r_nonzero: "r \ \\<^bsub>P\<^esub>" by (cases "r = \\<^bsub>P\<^esub>", simp_all)
    have "coeff P (p \\<^bsub>P\<^esub> q) (deg R r) = \\<^bsub>R\<^esub>" using coeff_add [OF p_in_P q_in_P, of "deg R r"] using coeff_R_p_eq_q
      using coeff_closed [OF p_in_P, of "deg R r"] coeff_closed [OF q_in_P, of "deg R r"] by algebra
    with lcoeff_nonzero [OF r_nonzero r_in_P]  and deg_eq show False using lcoeff_nonzero [of "p \\<^bsub>P\<^esub> q"] using p_in_P q_in_P
      using deg_r_nonzero by (cases "p \\<^bsub>P\<^esub> q \ \\<^bsub>P\<^esub>", auto)
  qed
  ultimately show ?thesis by simp
qed

lemma monom_deg_mult:
  assumes f_in_P: "f \ carrier P" and g_in_P: "g \ carrier P" and deg_le: "deg R g \ deg R f"
  and a_in_R: "a \ carrier R"
  shows "deg R (g \\<^bsub>P\<^esub> monom P a (deg R f - deg R g)) \ deg R f"
  using deg_mult_ring [OF g_in_P monom_closed [OF a_in_R, of "deg R f - deg R g"]]
  apply (cases "a = \") using g_in_P apply simp
  using deg_monom [OF _ a_in_R, of "deg R f - deg R g"] using deg_le by simp

lemma deg_zero_impl_monom:
  assumes f_in_P: "f \ carrier P" and deg_f: "deg R f = 0"
  shows "f = monom P (coeff P f 0) 0"
  apply (rule up_eqI) using coeff_monom [OF coeff_closed [OF f_in_P], of 0 0]
  using f_in_P deg_f using deg_aboveD [of f _] by auto

end

subsection \<open>The long division proof for commutative rings\<close>

context UP_cring
begin

lemma exI3: assumes exist: "Pred x y z"
  shows "\ x y z. Pred x y z"
  using exist by blast

text \<open>Jacobson's Theorem 2.14\<close>

lemma long_div_theorem:
  assumes g_in_P [simp]: "g \ carrier P" and f_in_P [simp]: "f \ carrier P"
  and g_not_zero: "g \ \\<^bsub>P\<^esub>"
  shows "\q r (k::nat). (q \ carrier P) \ (r \ carrier P) \ (lcoeff g)[^]\<^bsub>R\<^esub>k \\<^bsub>P\<^esub> f = g \\<^bsub>P\<^esub> q \\<^bsub>P\<^esub> r \ (r = \\<^bsub>P\<^esub> \ deg R r < deg R g)"
  using f_in_P
proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
  case (1 f)
  note f_in_P [simp] = "1.prems"
  let ?pred = "(\ q r (k::nat).
    (q \<in> carrier P) \<and> (r \<in> carrier P)
    \<and> (lcoeff g)[^]\<^bsub>R\<^esub>k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (r = \<zero>\<^bsub>P\<^esub> \<or> deg R r < deg R g))"
  let ?lg = "lcoeff g" and ?lf = "lcoeff f"
  show ?case
  proof (cases "deg R f < deg R g")
    case True
    have "?pred \\<^bsub>P\<^esub> f 0" using True by force
    then show ?thesis by blast
  next
    case False then have deg_g_le_deg_f: "deg R g \ deg R f" by simp
    {
      let ?k = "1::nat"
      let ?f1 = "(g \\<^bsub>P\<^esub> (monom P (?lf) (deg R f - deg R g))) \\<^bsub>P\<^esub> \\<^bsub>P\<^esub> (?lg \\<^bsub>P\<^esub> f)"
      let ?q = "monom P (?lf) (deg R f - deg R g)"
      have f1_in_carrier: "?f1 \ carrier P" and q_in_carrier: "?q \ carrier P" by simp_all
      show ?thesis
      proof (cases "deg R f = 0")
        case True
        {
--> --------------------

--> maximum size reached

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

quality100%

¤ Dauer der Verarbeitung: 0.81 Sekunden (vorverarbeitet) ¤

Wurzel

Suchen

Beweissystem der NASA

Beweissystem Isabelle

NIST Cobol Testsuite

Cephes Mathematical Library

Wiener Entwicklungsmethode

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.