# HG changeset patch
# User ballarin
# Date 1219075026 -7200
# Node ID 4b867f6a65d35adc281e48d5383deaf154e4b169
# Parent  7a28472be96b5360d4a69f72d237c161c440272d
Theorem on polynomial division and lemmas.

diff -r 7a28472be96b -r 4b867f6a65d3 src/HOL/Algebra/FiniteProduct.thy
--- a/src/HOL/Algebra/FiniteProduct.thy	Sun Aug 17 21:11:24 2008 +0200
+++ b/src/HOL/Algebra/FiniteProduct.thy	Mon Aug 18 17:57:06 2008 +0200
@@ -313,7 +313,9 @@
 declare funcsetI [intro]
   funcset_mem [dest]
 
-lemma (in comm_monoid) finprod_insert [simp]:
+context comm_monoid begin
+
+lemma finprod_insert [simp]:
   "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |] ==>
    finprod G f (insert a F) = f a \<otimes> finprod G f F"
   apply (rule trans)
@@ -331,7 +333,7 @@
   apply (auto simp add: finprod_def)
   done
 
-lemma (in comm_monoid) finprod_one [simp]:
+lemma finprod_one [simp]:
   "finite A ==> (\<Otimes>i:A. \<one>) = \<one>"
 proof (induct set: finite)
   case empty show ?case by simp
@@ -341,7 +343,7 @@
   with insert show ?case by simp
 qed
 
-lemma (in comm_monoid) finprod_closed [simp]:
+lemma finprod_closed [simp]:
   fixes A
   assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   shows "finprod G f A \<in> carrier G"
@@ -363,7 +365,7 @@
   "(f \<in> A Un B -> C) = (f \<in> A -> C & f \<in> B -> C)"
   by fast
 
-lemma (in comm_monoid) finprod_Un_Int:
+lemma finprod_Un_Int:
   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
      finprod G g (A Un B) \<otimes> finprod G g (A Int B) =
      finprod G g A \<otimes> finprod G g B"
@@ -379,7 +381,7 @@
           Int_mono2 Un_subset_iff) 
 qed
 
-lemma (in comm_monoid) finprod_Un_disjoint:
+lemma finprod_Un_disjoint:
   "[| finite A; finite B; A Int B = {};
       g \<in> A -> carrier G; g \<in> B -> carrier G |]
    ==> finprod G g (A Un B) = finprod G g A \<otimes> finprod G g B"
@@ -387,7 +389,7 @@
       apply (auto simp add: finprod_closed)
   done
 
-lemma (in comm_monoid) finprod_multf:
+lemma finprod_multf:
   "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
    finprod G (%x. f x \<otimes> g x) A = (finprod G f A \<otimes> finprod G g A)"
 proof (induct set: finite)
@@ -404,7 +406,7 @@
     by (simp add: insert fA fa gA ga fgA m_ac)
 qed
 
-lemma (in comm_monoid) finprod_cong':
+lemma finprod_cong':
   "[| A = B; g \<in> B -> carrier G;
       !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
 proof -
@@ -445,7 +447,7 @@
   qed
 qed
 
-lemma (in comm_monoid) finprod_cong:
+lemma finprod_cong:
   "[| A = B; f \<in> B -> carrier G = True;
       !!i. i \<in> B ==> f i = g i |] ==> finprod G f A = finprod G g B"
   (* This order of prems is slightly faster (3%) than the last two swapped. *)
@@ -458,19 +460,23 @@
   is not added to the simpset by default.
 *}
 
+end
+
 declare funcsetI [rule del]
   funcset_mem [rule del]
 
-lemma (in comm_monoid) finprod_0 [simp]:
+context comm_monoid begin
+
+lemma finprod_0 [simp]:
   "f \<in> {0::nat} -> carrier G ==> finprod G f {..0} = f 0"
 by (simp add: Pi_def)
 
-lemma (in comm_monoid) finprod_Suc [simp]:
+lemma finprod_Suc [simp]:
   "f \<in> {..Suc n} -> carrier G ==>
    finprod G f {..Suc n} = (f (Suc n) \<otimes> finprod G f {..n})"
 by (simp add: Pi_def atMost_Suc)
 
-lemma (in comm_monoid) finprod_Suc2:
+lemma finprod_Suc2:
   "f \<in> {..Suc n} -> carrier G ==>
    finprod G f {..Suc n} = (finprod G (%i. f (Suc i)) {..n} \<otimes> f 0)"
 proof (induct n)
@@ -479,7 +485,7 @@
   case Suc thus ?case by (simp add: m_assoc Pi_def)
 qed
 
-lemma (in comm_monoid) finprod_mult [simp]:
+lemma finprod_mult [simp]:
   "[| f \<in> {..n} -> carrier G; g \<in> {..n} -> carrier G |] ==>
      finprod G (%i. f i \<otimes> g i) {..n::nat} =
      finprod G f {..n} \<otimes> finprod G g {..n}"
@@ -487,7 +493,7 @@
 
 (* The following two were contributed by Jeremy Avigad. *)
 
-lemma (in comm_monoid) finprod_reindex:
+lemma finprod_reindex:
   assumes fin: "finite A"
     shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
         inj_on h A ==> finprod G f (h ` A) = finprod G (%x. f (h x)) A"
@@ -495,7 +501,7 @@
   apply (auto simp add: finprod_insert Pi_def)
 done
 
-lemma (in comm_monoid) finprod_const:
+lemma finprod_const:
   assumes fin [simp]: "finite A"
       and a [simp]: "a : carrier G"
     shows "finprod G (%x. a) A = a (^) card A"
@@ -508,4 +514,16 @@
   apply auto
 done
 
+(* The following lemma was contributed by Jesus Aransay. *)
+
+lemma finprod_singleton:
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
+  shows "(\<Otimes>j\<in>A. if i = j then f j else \<one>) = f i"
+  using i_in_A G.finprod_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<one>)"]
+    fin_A f_Pi G.finprod_one [of "A - {i}"]
+    G.finprod_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<one>)" "(\<lambda>i. \<one>)"] 
+  unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
+
 end
+
+end
diff -r 7a28472be96b -r 4b867f6a65d3 src/HOL/Algebra/Ring.thy
--- a/src/HOL/Algebra/Ring.thy	Sun Aug 17 21:11:24 2008 +0200
+++ b/src/HOL/Algebra/Ring.thy	Mon Aug 18 17:57:06 2008 +0200
@@ -216,13 +216,15 @@
   "\<Oplus>\<index>i:A. b" == "finsum \<struct>\<index> (%i. b) A"
   -- {* Beware of argument permutation! *}
 
+context abelian_monoid begin
+
 (*
-  lemmas (in abelian_monoid) finsum_empty [simp] =
+  lemmas finsum_empty [simp] =
     comm_monoid.finprod_empty [OF a_comm_monoid, simplified]
   is dangeous, because attributes (like simplified) are applied upon opening
   the locale, simplified refers to the simpset at that time!!!
 
-  lemmas (in abelian_monoid) finsum_empty [simp] =
+  lemmas finsum_empty [simp] =
     abelian_monoid.finprod_empty [OF a_abelian_monoid, folded finsum_def,
       simplified monoid_record_simps]
   makes the locale slow, because proofs are repeated for every
@@ -231,23 +233,23 @@
   from 110 secs to 60 secs.
 *)
 
-lemma (in abelian_monoid) finsum_empty [simp]:
+lemma finsum_empty [simp]:
   "finsum G f {} = \<zero>"
   by (rule comm_monoid.finprod_empty [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_insert [simp]:
+lemma finsum_insert [simp]:
   "[| finite F; a \<notin> F; f \<in> F -> carrier G; f a \<in> carrier G |]
   ==> finsum G f (insert a F) = f a \<oplus> finsum G f F"
   by (rule comm_monoid.finprod_insert [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_zero [simp]:
+lemma finsum_zero [simp]:
   "finite A ==> (\<Oplus>i\<in>A. \<zero>) = \<zero>"
   by (rule comm_monoid.finprod_one [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_closed [simp]:
+lemma finsum_closed [simp]:
   fixes A
   assumes fin: "finite A" and f: "f \<in> A -> carrier G" 
   shows "finsum G f A \<in> carrier G"
@@ -257,57 +259,57 @@
   apply (rule f)
   done
 
-lemma (in abelian_monoid) finsum_Un_Int:
+lemma finsum_Un_Int:
   "[| finite A; finite B; g \<in> A -> carrier G; g \<in> B -> carrier G |] ==>
      finsum G g (A Un B) \<oplus> finsum G g (A Int B) =
      finsum G g A \<oplus> finsum G g B"
   by (rule comm_monoid.finprod_Un_Int [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_Un_disjoint:
+lemma finsum_Un_disjoint:
   "[| finite A; finite B; A Int B = {};
       g \<in> A -> carrier G; g \<in> B -> carrier G |]
    ==> finsum G g (A Un B) = finsum G g A \<oplus> finsum G g B"
   by (rule comm_monoid.finprod_Un_disjoint [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_addf:
+lemma finsum_addf:
   "[| finite A; f \<in> A -> carrier G; g \<in> A -> carrier G |] ==>
    finsum G (%x. f x \<oplus> g x) A = (finsum G f A \<oplus> finsum G g A)"
   by (rule comm_monoid.finprod_multf [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_cong':
+lemma finsum_cong':
   "[| A = B; g : B -> carrier G;
       !!i. i : B ==> f i = g i |] ==> finsum G f A = finsum G g B"
   by (rule comm_monoid.finprod_cong' [OF a_comm_monoid,
     folded finsum_def, simplified monoid_record_simps]) auto
 
-lemma (in abelian_monoid) finsum_0 [simp]:
+lemma finsum_0 [simp]:
   "f : {0::nat} -> carrier G ==> finsum G f {..0} = f 0"
   by (rule comm_monoid.finprod_0 [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_Suc [simp]:
+lemma finsum_Suc [simp]:
   "f : {..Suc n} -> carrier G ==>
    finsum G f {..Suc n} = (f (Suc n) \<oplus> finsum G f {..n})"
   by (rule comm_monoid.finprod_Suc [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_Suc2:
+lemma finsum_Suc2:
   "f : {..Suc n} -> carrier G ==>
    finsum G f {..Suc n} = (finsum G (%i. f (Suc i)) {..n} \<oplus> f 0)"
   by (rule comm_monoid.finprod_Suc2 [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_add [simp]:
+lemma finsum_add [simp]:
   "[| f : {..n} -> carrier G; g : {..n} -> carrier G |] ==>
      finsum G (%i. f i \<oplus> g i) {..n::nat} =
      finsum G f {..n} \<oplus> finsum G g {..n}"
   by (rule comm_monoid.finprod_mult [OF a_comm_monoid, folded finsum_def,
     simplified monoid_record_simps])
 
-lemma (in abelian_monoid) finsum_cong:
+lemma finsum_cong:
   "[| A = B; f : B -> carrier G;
       !!i. i : B =simp=> f i = g i |] ==> finsum G f A = finsum G g B"
   by (rule comm_monoid.finprod_cong [OF a_comm_monoid, folded finsum_def,
@@ -317,7 +319,7 @@
    the reason is that the premise @{text "g \<in> B -> carrier G"} cannot be shown.
    Adding @{thm [source] Pi_def} to the simpset is often useful. *}
 
-lemma (in abelian_monoid) finsum_reindex:
+lemma finsum_reindex:
   assumes fin: "finite A"
     shows "f : (h ` A) \<rightarrow> carrier G \<Longrightarrow> 
         inj_on h A ==> finsum G f (h ` A) = finsum G (%x. f (h x)) A"
@@ -328,7 +330,7 @@
 (* The following is wrong.  Needed is the equivalent of (^) for addition,
   or indeed the canonical embedding from Nat into the monoid.
 
-lemma (in abelian_monoid) finsum_const:
+lemma finsum_const:
   assumes fin [simp]: "finite A"
       and a [simp]: "a : carrier G"
     shows "finsum G (%x. a) A = a (^) card A"
@@ -342,6 +344,18 @@
 done
 *)
 
+(* By Jesus Aransay. *)
+
+lemma finsum_singleton:
+  assumes i_in_A: "i \<in> A" and fin_A: "finite A" and f_Pi: "f \<in> A \<rightarrow> carrier G"
+  shows "(\<Oplus>j\<in>A. if i = j then f j else \<zero>) = f i"
+  using i_in_A finsum_insert [of "A - {i}" i "(\<lambda>j. if i = j then f j else \<zero>)"]
+    fin_A f_Pi finsum_zero [of "A - {i}"]
+    finsum_cong [of "A - {i}" "A - {i}" "(\<lambda>j. if i = j then f j else \<zero>)" "(\<lambda>i. \<zero>)"] 
+  unfolding Pi_def simp_implies_def by (force simp add: insert_absorb)
+
+end
+
 
 subsection {* Rings: Basic Definitions *}
 
diff -r 7a28472be96b -r 4b867f6a65d3 src/HOL/Algebra/UnivPoly.thy
--- a/src/HOL/Algebra/UnivPoly.thy	Sun Aug 17 21:11:24 2008 +0200
+++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 18 17:57:06 2008 +0200
@@ -4,7 +4,7 @@
   Author:    Clemens Ballarin, started 9 December 1996
   Copyright: Clemens Ballarin
 
-Contributions by Jesus Aransay.
+Contributions, in particular on long division, by Jesus Aransay.
 *)
 
 theory UnivPoly imports Module RingHom begin
@@ -53,19 +53,19 @@
   monom :: "['a, nat] => 'p"
   coeff :: "['p, nat] => 'a"
 
-constdefs (structure R)
-  up :: "('a, 'm) ring_scheme => (nat => 'a) set"
-  "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
-  UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
-  "UP R == (|
-    carrier = up R,
-    mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
-    one = (%i. if i=0 then \<one> else \<zero>),
-    zero = (%i. \<zero>),
-    add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
-    smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
-    monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
-    coeff = (%p:up R. %n. p n) |)"
+definition up :: "('a, 'm) ring_scheme => (nat => 'a) set"
+  where up_def: "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
+
+definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
+  where UP_def: "UP R == (|
+   carrier = up R,
+   mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
+   one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
+   zero = (%i. \<zero>\<^bsub>R\<^esub>),
+   add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i),
+   smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i),
+   monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
+   coeff = (%p:up R. %n. p n) |)"
 
 text {*
   Properties of the set of polynomials @{term up}.
@@ -120,6 +120,11 @@
   then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
 qed auto
 
+lemma up_minus_closed:
+  "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<ominus> q i) \<in> up R"
+  using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
+  by auto
+
 lemma up_mult_closed:
   "[| p \<in> up R; q \<in> up R |] ==>
   (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
@@ -204,7 +209,7 @@
 context UP_ring 
 begin
 
-(* Theorems generalised to rings by Jesus Aransay. *)
+(* Theorems generalised from commutative rings to rings by Jesus Aransay. *)
 
 lemma coeff_monom [simp]:
   "a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
@@ -297,12 +302,6 @@
   assumes R: "p \<in> carrier P" "q \<in> carrier P"
   shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R)
 
-end
-
-
-context UP_ring
-begin
-
 lemma UP_m_assoc:
   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
   shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
@@ -345,8 +344,7 @@
   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*)
+      (*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 \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
       proof -
@@ -395,11 +393,12 @@
 
 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)
+    (auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)
 
 end
 
-subsection {* Polynomials form a commutative Ring. *}
+
+subsection {* Polynomials Form a Commutative Ring. *}
 
 context UP_cring
 begin
@@ -662,42 +661,38 @@
 lemma monom_one_mult_comm: "monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m = monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
   unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all
 
-end
-
-context UP_cring
-begin
-
-(* Could got to UP_ring?  *)
-
 lemma monom_mult [simp]:
-  assumes R: "a \<in> carrier R" "b \<in> carrier R"
+  assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R"
   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
-proof -
-  from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
-  also from R have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> monom P \<one> (n + m)"
-    by (simp add: monom_mult_smult del: R.r_one)
-  also have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m)"
-    by (simp only: monom_one_mult)
-  also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m))"
-    by (simp add: UP_smult_assoc1)
-  also from R have "... = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> (monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n))"
-    unfolding monom_one_mult_comm by simp
-  also from R have "... = a \<odot>\<^bsub>P\<^esub> ((b \<odot>\<^bsub>P\<^esub> monom P \<one> m) \<otimes>\<^bsub>P\<^esub> monom P \<one> n)"
-    by (simp add: UP_smult_assoc2)
-  also from R have "... = a \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m))"
-    using monom_one_mult_comm [of n m] by (simp add: P.m_comm)
-  also from R have "... = (a \<odot>\<^bsub>P\<^esub> monom P \<one> n) \<otimes>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> monom P \<one> m)"
-    by (simp add: UP_smult_assoc2)
-  also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^bsub>P\<^esub> monom P (b \<otimes> \<one>) m"
-    by (simp add: monom_mult_smult del: R.r_one)
-  also from R have "... = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m" by simp
-  finally show ?thesis .
-qed
-
-end
-
-context UP_ring
-begin
+proof (rule up_eqI)
+  fix k 
+  show "coeff P (monom P (a \<otimes> b) (n + m)) k = coeff P (monom P a n \<otimes>\<^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}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))" 
+	  "(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
+	  a_in_R b_in_R
+	unfolding simp_implies_def
+	using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> 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}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = k - i then b else \<zero>))" "(\<lambda>i. \<zero>)"]
+	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 \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
@@ -717,9 +712,8 @@
 
 subsection {* The Degree Function *}
 
-constdefs (structure R)
-  deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
-  "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
+definition deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
+  where "deg R p == LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p)"
 
 context UP_ring
 begin
@@ -1186,11 +1180,11 @@
   "(%a. monom P a 0) \<in> ring_hom R P"
   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
 
-constdefs (structure S)
+definition
   eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
            'a => 'b, 'b, nat => 'a] => 'b"
-  "eval R S phi s == \<lambda>p \<in> carrier (UP R).
-    \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> s (^) i"
+  where "eval R S phi s == \<lambda>p \<in> 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
@@ -1468,6 +1462,398 @@
 
 end
 
+text{*JE: The following lemma was added by me; it might be even lifted to a simpler locale*}
+
+context monoid
+begin
+
+lemma nat_pow_eone[simp]: assumes x_in_G: "x \<in> 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 \<in> carrier P" and p_not_zero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" shows "lcoeff p \<noteq> \<zero>" 
+  using lcoeff_nonzero [OF p_not_zero p_in_R] .
+
+subsection{*The long division algorithm: some previous facts.*}
+
+lemma coeff_minus [simp]:
+  assumes p: "p \<in> carrier P" and q: "q \<in> carrier P" shows "coeff P (p \<ominus>\<^bsub>P\<^esub> q) n = coeff P p n \<ominus> coeff P q n" 
+  unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
+  using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
+
+lemma lcoeff_closed [simp]: assumes p: "p \<in> carrier P" shows "lcoeff p \<in> carrier R"
+  using coeff_closed [OF p, of "deg R p"] by simp
+
+lemma deg_smult_decr: assumes a_in_R: "a \<in> carrier R" and f_in_P: "f \<in> carrier P" shows "deg R (a \<odot>\<^bsub>P\<^esub> f) \<le> deg R f"
+  using deg_smult_ring [OF a_in_R f_in_P] by (cases "a = \<zero>", auto)
+
+lemma coeff_monom_mult: assumes R: "c \<in> carrier R" and P: "p \<in> carrier P" 
+  shows "coeff P (monom P c n \<otimes>\<^bsub>P\<^esub> p) (m + n) = c \<otimes> (coeff P p m)"
+proof -
+  have "coeff P (monom P c n \<otimes>\<^bsub>P\<^esub> p) (m + n) = (\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> 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 "(\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> 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}" "(\<lambda>i::nat. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i))" 
+      "(\<lambda>i::nat. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"]
+    using coeff_closed [OF P] unfolding Pi_def simp_implies_def using R by auto
+  also have "\<dots> = c \<otimes> coeff P p m" using R.finsum_singleton [of n "{..m + n}" "(\<lambda>i. c \<otimes> 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 \<in> carrier P" and q_in_P: "q \<in> carrier P" and r_in_P: "r \<in> carrier P" 
+  and deg_r_nonzero: "deg R r \<noteq> 0"
+  and deg_R_p: "deg R p \<le> deg R r" and deg_R_q: "deg R q \<le> deg R r" 
+  and coeff_R_p_eq_q: "coeff P p (deg R r) = \<ominus>\<^bsub>R\<^esub> (coeff P q (deg R r))"
+  shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) < deg R r"
+proof -
+  have deg_le: "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<le> deg R r"
+  proof (rule deg_aboveI)
+    fix m
+    assume deg_r_le: "deg R r < m"
+    show "coeff P (p \<oplus>\<^bsub>P\<^esub> q) m = \<zero>"
+    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 \<oplus>\<^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 \<oplus>\<^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 \<oplus>\<^bsub>P\<^esub> q) \<noteq> deg R r"
+  proof (rule ccontr)
+    assume nz: "\<not> deg R (p \<oplus>\<^bsub>P\<^esub> q) \<noteq> deg R r" then have deg_eq: "deg R (p \<oplus>\<^bsub>P\<^esub> q) = deg R r" by simp
+    from deg_r_nonzero have r_nonzero: "r \<noteq> \<zero>\<^bsub>P\<^esub>" by (cases "r = \<zero>\<^bsub>P\<^esub>", simp_all)
+    have "coeff P (p \<oplus>\<^bsub>P\<^esub> q) (deg R r) = \<zero>\<^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 \<oplus>\<^bsub>P\<^esub> q"] using p_in_P q_in_P
+      using deg_r_nonzero by (cases "p \<oplus>\<^bsub>P\<^esub> q \<noteq> \<zero>\<^bsub>P\<^esub>", auto)
+  qed
+  ultimately show ?thesis by simp
+qed
+
+lemma monom_deg_mult: 
+  assumes f_in_P: "f \<in> carrier P" and g_in_P: "g \<in> carrier P" and deg_le: "deg R g \<le> deg R f"
+  and a_in_R: "a \<in> carrier R"
+  shows "deg R (g \<otimes>\<^bsub>P\<^esub> monom P a (deg R f - deg R g)) \<le> 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 = \<zero>") 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 \<in> 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 {* The long division proof for commutative rings *}
+
+context UP_cring
+begin
+
+lemma exI3: assumes exist: "Pred x y z" 
+  shows "\<exists> x y z. Pred x y z"
+  using exist by blast
+
+text {* Jacobson's Theorem 2.14 *}
+
+lemma long_div_theorem: 
+  assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
+  and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
+  shows "\<exists> 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> | deg R r < deg R g)"
+proof -
+  let ?pred = "(\<lambda> 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> | deg R r < deg R g))"
+    and ?lg = "lcoeff g"
+  show ?thesis
+    (*JE: we distinguish some particular cases where the solution is almost direct.*)
+  proof (cases "deg R f < deg R g")
+    case True     
+      (*JE: if the degree of f is smaller than the one of g the solution is straightforward.*)
+      (* CB: avoid exI3 *)
+      have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
+      then show ?thesis by fast
+  next
+    case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
+    {
+      (*JE: we now apply the induction hypothesis with some additional facts required*)
+      from f_in_P deg_g_le_deg_f show ?thesis
+      proof (induct n \<equiv> "deg R f" arbitrary: "f" rule: nat_less_induct)
+	fix n f
+	assume hypo: "\<forall>m<n. \<forall>x. x \<in> carrier P \<longrightarrow>
+          deg R g \<le> deg R x \<longrightarrow> 
+	  m = deg R x \<longrightarrow>
+	  (\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> x = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g))"
+	  and prem: "n = deg R f" and f_in_P [simp]: "f \<in> carrier P"
+	  and deg_g_le_deg_f: "deg R g \<le> deg R f"
+	let ?k = "1::nat" and ?r = "(g \<otimes>\<^bsub>P\<^esub> (monom P (lcoeff f) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)"
+	  and ?q = "monom P (lcoeff f) (deg R f - deg R g)"
+	show "\<exists> q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and> lcoeff g (^) k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r & (r = \<zero>\<^bsub>P\<^esub> | deg R r < deg R g)"
+	proof -
+	  (*JE: we first extablish the existence of a triple satisfying the previous equation. 
+	    Then we will have to prove the second part of the predicate.*)
+	  have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r"
+	    using minus_add
+	    using sym [OF a_assoc [of "g \<otimes>\<^bsub>P\<^esub> ?q" "\<ominus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "lcoeff g \<odot>\<^bsub>P\<^esub> f"]]
+	    using r_neg by auto
+	  show ?thesis
+	  proof (cases "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g")
+	    (*JE: if the degree of the remainder satisfies the statement property we are done*)
+	    case True
+	    {
+	      show ?thesis
+	      proof (rule exI3 [of _ ?q "\<ominus>\<^bsub>P\<^esub> ?r" ?k], intro conjI)
+		show "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r" using exist by simp
+		show "\<ominus>\<^bsub>P\<^esub> ?r = \<zero>\<^bsub>P\<^esub> \<or> deg R (\<ominus>\<^bsub>P\<^esub> ?r) < deg R g" using True by simp
+	      qed (simp_all)
+	    }
+	  next
+	    case False note n_deg_r_l_deg_g = False
+	    {
+	      (*JE: otherwise, we verify the conditions of the induction hypothesis.*)
+	      show ?thesis
+	      proof (cases "deg R f = 0")
+		(*JE: the solutions are different if the degree of f is zero or not*)
+		case True
+		{
+		  have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
+		  have "lcoeff g (^) (1::nat) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> f \<oplus>\<^bsub>P\<^esub> \<zero>\<^bsub>P\<^esub>"
+		    unfolding deg_g apply simp
+		    unfolding sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
+		    using deg_zero_impl_monom [OF g_in_P deg_g] by simp
+		  then show ?thesis using f_in_P by blast
+		}
+	      next
+		case False note deg_f_nzero = False
+		{
+		  (*JE: now it only remains the case where the induction hypothesis can be used.*)
+		  (*JE: we first prove that the degree of the remainder is smaller than the one of f*)
+		  have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n"
+		  proof -
+		    have "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = deg R ?r" using deg_uminus [of ?r] by simp
+		    also have "\<dots> < deg R f"
+		    proof (rule deg_lcoeff_cancel)
+		      show "deg R (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
+			using deg_smult_ring [of "lcoeff g" f] using prem
+			using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
+		      show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
+			using monom_deg_mult [OF _ g_in_P, of f "lcoeff f"] and deg_g_le_deg_f
+			by simp
+		      show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (lcoeff g \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
+			unfolding coeff_mult [OF g_in_P monom_closed [OF lcoeff_closed [OF f_in_P], of "deg R f - deg R g"], of "deg R f"]
+			unfolding coeff_monom [OF lcoeff_closed [OF f_in_P], of "(deg R f - deg R g)"]
+			using R.finsum_cong' [of "{..deg R f}" "{..deg R f}" 
+			  "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then lcoeff f else \<zero>))" 
+			  "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> lcoeff f else \<zero>)"]
+			using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> lcoeff f)"]
+			unfolding Pi_def using deg_g_le_deg_f by force
+		    qed (simp_all add: deg_f_nzero)
+		    finally show "deg R (\<ominus>\<^bsub>P\<^esub> ?r) < n" unfolding prem .
+		  qed
+		  moreover have "\<ominus>\<^bsub>P\<^esub> ?r \<in> carrier P" by simp
+		  moreover obtain m where deg_rem_eq_m: "deg R (\<ominus>\<^bsub>P\<^esub> ?r) = m" by auto
+		  moreover have "deg R g \<le> deg R (\<ominus>\<^bsub>P\<^esub> ?r)" using n_deg_r_l_deg_g by simp
+		    (*JE: now, by applying the induction hypothesis, we obtain new quotient, remainder and exponent.*)
+		  ultimately obtain q' r' k'
+		    where rem_desc: "lcoeff g (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?r) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
+		    and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
+		    using hypo by blast
+		      (*JE: we now prove that the new quotient, remainder and exponent can be used to get 
+		      the quotient, remainder and exponent of the long division theorem*)
+		  show ?thesis
+		  proof (rule exI3 [of _ "((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
+		    show "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
+		    proof -
+		      have "(lcoeff g (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?r)" 
+			using smult_assoc1 exist by simp
+		      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?r))"
+			using UP_smult_r_distr by simp
+		      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r')"
+			using rem_desc by simp
+		      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
+			using sym [OF a_assoc [of "lcoeff g (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
+			using q'_in_carrier r'_in_carrier by simp
+		      also have "\<dots> = (lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> (?q \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+			using q'_in_carrier by (auto simp add: m_comm)
+		      also have "\<dots> = (((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q) \<otimes>\<^bsub>P\<^esub> g) \<oplus>\<^bsub>P\<^esub> q' \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'" 
+			using smult_assoc2 q'_in_carrier by auto
+		      also have "\<dots> = ((lcoeff g (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
+			using sym [OF l_distr] and q'_in_carrier by auto
+		      finally show ?thesis using m_comm q'_in_carrier by auto
+		    qed
+		  qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
+		}
+	      qed
+	    }
+	  qed
+	qed
+      qed
+    }
+  qed
+qed
+
+end
+
+
+text {*The remainder theorem as corollary of the long division theorem.*}
+
+context UP_cring
+begin
+
+lemma deg_minus_monom:
+  assumes a: "a \<in> carrier R"
+  and R_not_trivial: "(carrier R \<noteq> {\<zero>})"
+  shows "deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = 1"
+  (is "deg R ?g = 1")
+proof -
+  have "deg R ?g \<le> 1"
+  proof (rule deg_aboveI)
+    fix m
+    assume "(1::nat) < m" 
+    then show "coeff P ?g m = \<zero>" 
+      using coeff_minus using a by auto algebra
+  qed (simp add: a)
+  moreover have "deg R ?g \<ge> 1"
+  proof (rule deg_belowI)
+    show "coeff P ?g 1 \<noteq> \<zero>"
+      using a using R.carrier_one_not_zero R_not_trivial by simp algebra
+  qed (simp add: a)
+  ultimately show ?thesis by simp
+qed
+
+lemma lcoeff_monom:
+  assumes a: "a \<in> carrier R" and R_not_trivial: "(carrier R \<noteq> {\<zero>})"
+  shows "lcoeff (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<one>"
+  using deg_minus_monom [OF a R_not_trivial]
+  using coeff_minus a by auto algebra
+
+lemma deg_nzero_nzero:
+  assumes deg_p_nzero: "deg R p \<noteq> 0"
+  shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"
+  using deg_zero deg_p_nzero by auto
+
+lemma deg_monom_minus:
+  assumes a: "a \<in> carrier R"
+  and R_not_trivial: "carrier R \<noteq> {\<zero>}"
+  shows "deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = 1"
+  (is "deg R ?g = 1")
+proof -
+  have "deg R ?g \<le> 1"
+  proof (rule deg_aboveI)
+    fix m::nat assume "1 < m" then show "coeff P ?g m = \<zero>" 
+      using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of m] 
+      using coeff_monom [OF R.one_closed, of 1 m] using coeff_monom [OF a, of 0 m] by auto algebra
+  qed (simp add: a)
+  moreover have "1 \<le> deg R ?g"
+  proof (rule deg_belowI)
+    show "coeff P ?g 1 \<noteq> \<zero>" 
+      using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of 1]
+      using coeff_monom [OF R.one_closed, of 1 1] using coeff_monom [OF a, of 0 1] 
+      using R_not_trivial using R.carrier_one_not_zero
+      by auto algebra
+  qed (simp add: a)
+  ultimately show ?thesis by simp
+qed
+
+lemma eval_monom_expr:
+  assumes a: "a \<in> carrier R"
+  shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
+  (is "eval R R id a ?g = _")
+proof -
+  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+  have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
+  interpret ring_hom_cring [P R "eval R R id a"] by unfold_locales (simp add: eval_ring_hom)
+  have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P" 
+    and mon0_closed: "monom P a 0 \<in> carrier P" 
+    and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
+    using a R.a_inv_closed by auto
+  have "eval R R id a ?g = eval R R id a (monom P \<one> 1) \<ominus> eval R R id a (monom P a 0)"
+    unfolding P.minus_eq [OF mon1_closed mon0_closed]
+    unfolding R_S_h.hom_add [OF mon1_closed min_mon0_closed]
+    unfolding R_S_h.hom_a_inv [OF mon0_closed] 
+    using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
+  also have "\<dots> = a \<ominus> a"
+    using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
+  also have "\<dots> = \<zero>"
+    using a by algebra
+  finally show ?thesis by simp
+qed
+
+lemma remainder_theorem_exist:
+  assumes f: "f \<in> carrier P" and a: "a \<in> carrier R"
+  and R_not_trivial: "carrier R \<noteq> {\<zero>}"
+  shows "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (deg R r = 0)"
+  (is "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r \<and> (deg R r = 0)")
+proof -
+  let ?g = "monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0"
+  from deg_minus_monom [OF a R_not_trivial]
+  have deg_g_nzero: "deg R ?g \<noteq> 0" by simp
+  have "\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and>
+    lcoeff ?g (^) 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)"
+    using long_div_theorem [OF _ f deg_nzero_nzero [OF deg_g_nzero]] a
+    by auto
+  then show ?thesis
+    unfolding lcoeff_monom [OF a R_not_trivial]
+    unfolding deg_monom_minus [OF a R_not_trivial]
+    using smult_one [OF f] using deg_zero by force
+qed
+
+lemma remainder_theorem_expression:
+  assumes f [simp]: "f \<in> carrier P" and a [simp]: "a \<in> carrier R"
+  and q [simp]: "q \<in> carrier P" and r [simp]: "r \<in> carrier P"
+  and R_not_trivial: "carrier R \<noteq> {\<zero>}"
+  and f_expr: "f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r"
+  (is "f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r" is "f = ?gq \<oplus>\<^bsub>P\<^esub> r")
+    and deg_r_0: "deg R r = 0"
+    shows "r = monom P (eval R R id a f) 0"
+proof -
+  interpret UP_pre_univ_prop [R R id P] by unfold_locales simp
+  have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
+    using eval_ring_hom [OF a] by simp
+  have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
+    unfolding f_expr using ring_hom_add [OF eval_ring_hom] by auto
+  also have "\<dots> = ((eval R R id a ?g) \<otimes> (eval R R id a q)) \<oplus>\<^bsub>R\<^esub> eval R R id a r"
+    using ring_hom_mult [OF eval_ring_hom] by auto
+  also have "\<dots> = \<zero> \<oplus> eval R R id a r"
+    unfolding eval_monom_expr [OF a] using eval_ring_hom 
+    unfolding ring_hom_def using q unfolding Pi_def by simp
+  also have "\<dots> = eval R R id a r"
+    using eval_ring_hom unfolding ring_hom_def using r unfolding Pi_def by simp
+  finally have eval_eq: "eval R R id a f = eval R R id a r" by simp
+  from deg_zero_impl_monom [OF r deg_r_0]
+  have "r = monom P (coeff P r 0) 0" by simp
+  with eval_const [OF a, of "coeff P r 0"] eval_eq 
+  show ?thesis by auto
+qed
+
+corollary remainder_theorem:
+  assumes f [simp]: "f \<in> carrier P" and a [simp]: "a \<in> carrier R"
+  and R_not_trivial: "carrier R \<noteq> {\<zero>}"
+  shows "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> 
+     f = (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0"
+  (is "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> monom P (eval R R id a f) 0")
+proof -
+  from remainder_theorem_exist [OF f a R_not_trivial]
+  obtain q r
+    where q_r: "q \<in> carrier P \<and> r \<in> carrier P \<and> f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r"
+    and deg_r: "deg R r = 0" by force
+  with remainder_theorem_expression [OF f a _ _ R_not_trivial, of q r]
+  show ?thesis by auto
+qed
+
+end
+
 
 subsection {* Sample Application of Evaluation Homomorphism *}