src/HOL/Algebra/UnivPoly.thy
 author wenzelm Sat Oct 10 16:26:23 2015 +0200 (2015-10-10) changeset 61382 efac889fccbc parent 61169 4de9ff3ea29a child 61384 9f5145281888 permissions -rw-r--r--
isabelle update_cartouches;
1 (*  Title:      HOL/Algebra/UnivPoly.thy
2     Author:     Clemens Ballarin, started 9 December 1996
5 Contributions, in particular on long division, by Jesus Aransay.
6 *)
8 theory UnivPoly
9 imports Module RingHom
10 begin
12 section \<open>Univariate Polynomials\<close>
14 text \<open>
15   Polynomials are formalised as modules with additional operations for
16   extracting coefficients from polynomials and for obtaining monomials
17   from coefficients and exponents (record @{text "up_ring"}).  The
18   carrier set is a set of bounded functions from Nat to the
19   coefficient domain.  Bounded means that these functions return zero
20   above a certain bound (the degree).  There is a chapter on the
21   formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
22   which was implemented with axiomatic type classes.  This was later
23   ported to Locales.
24 \<close>
27 subsection \<open>The Constructor for Univariate Polynomials\<close>
29 text \<open>
30   Functions with finite support.
31 \<close>
33 locale bound =
34   fixes z :: 'a
35     and n :: nat
36     and f :: "nat => 'a"
37   assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
39 declare bound.intro [intro!]
40   and bound.bound [dest]
42 lemma bound_below:
43   assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
44 proof (rule classical)
45   assume "~ ?thesis"
46   then have "m < n" by arith
47   with bound have "f n = z" ..
48   with nonzero show ?thesis by contradiction
49 qed
51 record ('a, 'p) up_ring = "('a, 'p) module" +
52   monom :: "['a, nat] => 'p"
53   coeff :: "['p, nat] => 'a"
55 definition
56   up :: "('a, 'm) ring_scheme => (nat => 'a) set"
57   where "up R = {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero>\<^bsub>R\<^esub> n f)}"
59 definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
60   where "UP R = \<lparr>
61    carrier = up R,
62    mult = (%p:up R. %q:up R. %n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
63    one = (%i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
64    zero = (%i. \<zero>\<^bsub>R\<^esub>),
65    add = (%p:up R. %q:up R. %i. p i \<oplus>\<^bsub>R\<^esub> q i),
66    smult = (%a:carrier R. %p:up R. %i. a \<otimes>\<^bsub>R\<^esub> p i),
67    monom = (%a:carrier R. %n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
68    coeff = (%p:up R. %n. p n)\<rparr>"
70 text \<open>
71   Properties of the set of polynomials @{term up}.
72 \<close>
74 lemma mem_upI [intro]:
75   "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
76   by (simp add: up_def Pi_def)
78 lemma mem_upD [dest]:
79   "f \<in> up R ==> f n \<in> carrier R"
80   by (simp add: up_def Pi_def)
82 context ring
83 begin
85 lemma bound_upD [dest]: "f \<in> up R ==> EX n. bound \<zero> n f" by (simp add: up_def)
87 lemma up_one_closed: "(%n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
89 lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R" by force
92   "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
93 proof
94   fix n
95   assume "p \<in> up R" and "q \<in> up R"
96   then show "p n \<oplus> q n \<in> carrier R"
97     by auto
98 next
99   assume UP: "p \<in> up R" "q \<in> up R"
100   show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
101   proof -
102     from UP obtain n where boundn: "bound \<zero> n p" by fast
103     from UP obtain m where boundm: "bound \<zero> m q" by fast
104     have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
105     proof
106       fix i
107       assume "max n m < i"
108       with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastforce
109     qed
110     then show ?thesis ..
111   qed
112 qed
114 lemma up_a_inv_closed:
115   "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
116 proof
117   assume R: "p \<in> up R"
118   then obtain n where "bound \<zero> n p" by auto
119   then have "bound \<zero> n (%i. \<ominus> p i)" by auto
120   then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
121 qed auto
123 lemma up_minus_closed:
124   "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<ominus> q i) \<in> up R"
125   using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed a_minus_def [of _ R]
126   by auto
128 lemma up_mult_closed:
129   "[| p \<in> up R; q \<in> up R |] ==>
130   (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
131 proof
132   fix n
133   assume "p \<in> up R" "q \<in> up R"
134   then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
135     by (simp add: mem_upD  funcsetI)
136 next
137   assume UP: "p \<in> up R" "q \<in> up R"
138   show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
139   proof -
140     from UP obtain n where boundn: "bound \<zero> n p" by fast
141     from UP obtain m where boundm: "bound \<zero> m q" by fast
142     have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
143     proof
144       fix k assume bound: "n + m < k"
145       {
146         fix i
147         have "p i \<otimes> q (k-i) = \<zero>"
148         proof (cases "n < i")
149           case True
150           with boundn have "p i = \<zero>" by auto
151           moreover from UP have "q (k-i) \<in> carrier R" by auto
152           ultimately show ?thesis by simp
153         next
154           case False
155           with bound have "m < k-i" by arith
156           with boundm have "q (k-i) = \<zero>" by auto
157           moreover from UP have "p i \<in> carrier R" by auto
158           ultimately show ?thesis by simp
159         qed
160       }
161       then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
163     qed
164     then show ?thesis by fast
165   qed
166 qed
168 end
171 subsection \<open>Effect of Operations on Coefficients\<close>
173 locale UP =
174   fixes R (structure) and P (structure)
175   defines P_def: "P == UP R"
177 locale UP_ring = UP + R: ring R
179 locale UP_cring = UP + R: cring R
181 sublocale UP_cring < UP_ring
182   by intro_locales [1] (rule P_def)
184 locale UP_domain = UP + R: "domain" R
186 sublocale UP_domain < UP_cring
187   by intro_locales [1] (rule P_def)
189 context UP
190 begin
192 text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
194 declare P_def [simp]
196 lemma up_eqI:
197   assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \<in> carrier P" "q \<in> carrier P"
198   shows "p = q"
199 proof
200   fix x
201   from prem and R show "p x = q x" by (simp add: UP_def)
202 qed
204 lemma coeff_closed [simp]:
205   "p \<in> carrier P ==> coeff P p n \<in> carrier R" by (auto simp add: UP_def)
207 end
209 context UP_ring
210 begin
212 (* Theorems generalised from commutative rings to rings by Jesus Aransay. *)
214 lemma coeff_monom [simp]:
215   "a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
216 proof -
217   assume R: "a \<in> carrier R"
218   then have "(%n. if n = m then a else \<zero>) \<in> up R"
219     using up_def by force
220   with R show ?thesis by (simp add: UP_def)
221 qed
223 lemma coeff_zero [simp]: "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" by (auto simp add: UP_def)
225 lemma coeff_one [simp]: "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
226   using up_one_closed by (simp add: UP_def)
228 lemma coeff_smult [simp]:
229   "[| a \<in> carrier R; p \<in> carrier P |] ==> coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
230   by (simp add: UP_def up_smult_closed)
233   "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
236 lemma coeff_mult [simp]:
237   "[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
238   by (simp add: UP_def up_mult_closed)
240 end
243 subsection \<open>Polynomials Form a Ring.\<close>
245 context UP_ring
246 begin
248 text \<open>Operations are closed over @{term P}.\<close>
250 lemma UP_mult_closed [simp]:
251   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
253 lemma UP_one_closed [simp]:
254   "\<one>\<^bsub>P\<^esub> \<in> carrier P" by (simp add: UP_def up_one_closed)
256 lemma UP_zero_closed [intro, simp]:
257   "\<zero>\<^bsub>P\<^esub> \<in> carrier P" by (auto simp add: UP_def)
259 lemma UP_a_closed [intro, simp]:
260   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_add_closed)
262 lemma monom_closed [simp]:
263   "a \<in> carrier R ==> monom P a n \<in> carrier P" by (auto simp add: UP_def up_def Pi_def)
265 lemma UP_smult_closed [simp]:
266   "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" by (simp add: UP_def up_smult_closed)
268 end
270 declare (in UP) P_def [simp del]
272 text \<open>Algebraic ring properties\<close>
274 context UP_ring
275 begin
277 lemma UP_a_assoc:
278   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
279   shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
281 lemma UP_l_zero [simp]:
282   assumes R: "p \<in> carrier P"
283   shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)
285 lemma UP_l_neg_ex:
286   assumes R: "p \<in> carrier P"
287   shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
288 proof -
289   let ?q = "%i. \<ominus> (p i)"
290   from R have closed: "?q \<in> carrier P"
291     by (simp add: UP_def P_def up_a_inv_closed)
292   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
293     by (simp add: UP_def P_def up_a_inv_closed)
294   show ?thesis
295   proof
296     show "?q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
297       by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
298   qed (rule closed)
299 qed
301 lemma UP_a_comm:
302   assumes R: "p \<in> carrier P" "q \<in> carrier P"
303   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)
305 lemma UP_m_assoc:
306   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
307   shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
308 proof (rule up_eqI)
309   fix n
310   {
311     fix k and a b c :: "nat=>'a"
312     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
313       "c \<in> UNIV -> carrier R"
314     then have "k <= n ==>
315       (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
316       (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
317       (is "_ \<Longrightarrow> ?eq k")
318     proof (induct k)
319       case 0 then show ?case by (simp add: Pi_def m_assoc)
320     next
321       case (Suc k)
322       then have "k <= n" by arith
323       from this R have "?eq k" by (rule Suc)
324       with R show ?case
325         by (simp cong: finsum_cong
326              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
327            (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
328     qed
329   }
330   with R show "coeff P ((p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r) n = coeff P (p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)) n"
334 lemma UP_r_one [simp]:
335   assumes R: "p \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub> = p"
336 proof (rule up_eqI)
337   fix n
338   show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n"
339   proof (cases n)
340     case 0
341     {
342       with R show ?thesis by simp
343     }
344   next
345     case Suc
346     {
347       (*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*)
348       fix nn assume Succ: "n = Suc nn"
349       have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
350       proof -
351         have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
352         also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
353           using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
354         also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
355         proof -
356           have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
357             using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R
358             unfolding Pi_def by simp
359           also have "\<dots> = \<zero>" by simp
360           finally show ?thesis using r_zero R by simp
361         qed
362         also have "\<dots> = coeff P p (Suc nn)" using R by simp
363         finally show ?thesis by simp
364       qed
365       then show ?thesis using Succ by simp
366     }
367   qed
370 lemma UP_l_one [simp]:
371   assumes R: "p \<in> carrier P"
372   shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
373 proof (rule up_eqI)
374   fix n
375   show "coeff P (\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p) n = coeff P p n"
376   proof (cases n)
377     case 0 with R show ?thesis by simp
378   next
379     case Suc with R show ?thesis
380       by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
381   qed
384 lemma UP_l_distr:
385   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
386   shows "(p \<oplus>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = (p \<otimes>\<^bsub>P\<^esub> r) \<oplus>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
387   by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
389 lemma UP_r_distr:
390   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
391   shows "r \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = (r \<otimes>\<^bsub>P\<^esub> p) \<oplus>\<^bsub>P\<^esub> (r \<otimes>\<^bsub>P\<^esub> q)"
392   by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R)
394 theorem UP_ring: "ring P"
395   by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc)
396     (auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)
398 end
401 subsection \<open>Polynomials Form a Commutative Ring.\<close>
403 context UP_cring
404 begin
406 lemma UP_m_comm:
407   assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
408 proof (rule up_eqI)
409   fix n
410   {
411     fix k and a b :: "nat=>'a"
412     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
413     then have "k <= n ==>
414       (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
415       (is "_ \<Longrightarrow> ?eq k")
416     proof (induct k)
417       case 0 then show ?case by (simp add: Pi_def)
418     next
419       case (Suc k) then show ?case
420         by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
421     qed
422   }
423   note l = this
424   from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
425     unfolding coeff_mult [OF R1 R2, of n]
426     unfolding coeff_mult [OF R2 R1, of n]
427     using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
428 qed (simp_all add: R1 R2)
431 subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
433 theorem UP_cring:
434   "cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
436 end
438 context UP_ring
439 begin
441 lemma UP_a_inv_closed [intro, simp]:
442   "p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P"
443   by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]])
445 lemma coeff_a_inv [simp]:
446   assumes R: "p \<in> carrier P"
447   shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)"
448 proof -
449   from R coeff_closed UP_a_inv_closed have
450     "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> coeff P p n \<oplus> (coeff P p n \<oplus> coeff P (\<ominus>\<^bsub>P\<^esub> p) n)"
451     by algebra
452   also from R have "... =  \<ominus> (coeff P p n)"
454       abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
455   finally show ?thesis .
456 qed
458 end
460 sublocale UP_ring < P: ring P using UP_ring .
461 sublocale UP_cring < P: cring P using UP_cring .
464 subsection \<open>Polynomials Form an Algebra\<close>
466 context UP_ring
467 begin
469 lemma UP_smult_l_distr:
470   "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
471   (a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
472   by (rule up_eqI) (simp_all add: R.l_distr)
474 lemma UP_smult_r_distr:
475   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
476   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"
477   by (rule up_eqI) (simp_all add: R.r_distr)
479 lemma UP_smult_assoc1:
480       "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
481       (a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
482   by (rule up_eqI) (simp_all add: R.m_assoc)
484 lemma UP_smult_zero [simp]:
485       "p \<in> carrier P ==> \<zero> \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
486   by (rule up_eqI) simp_all
488 lemma UP_smult_one [simp]:
489       "p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p"
490   by (rule up_eqI) simp_all
492 lemma UP_smult_assoc2:
493   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
494   (a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
495   by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
497 end
499 text \<open>
500   Interpretation of lemmas from @{term algebra}.
501 \<close>
503 lemma (in cring) cring:
504   "cring R" ..
506 lemma (in UP_cring) UP_algebra:
507   "algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
508     UP_smult_assoc1 UP_smult_assoc2)
510 sublocale UP_cring < algebra R P using UP_algebra .
513 subsection \<open>Further Lemmas Involving Monomials\<close>
515 context UP_ring
516 begin
518 lemma monom_zero [simp]:
519   "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" by (simp add: UP_def P_def)
521 lemma monom_mult_is_smult:
522   assumes R: "a \<in> carrier R" "p \<in> carrier P"
523   shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
524 proof (rule up_eqI)
525   fix n
526   show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
527   proof (cases n)
528     case 0 with R show ?thesis by simp
529   next
530     case Suc with R show ?thesis
531       using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
532   qed
535 lemma monom_one [simp]:
536   "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
537   by (rule up_eqI) simp_all
540   "[| a \<in> carrier R; b \<in> carrier R |] ==>
541   monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
542   by (rule up_eqI) simp_all
544 lemma monom_one_Suc:
545   "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
546 proof (rule up_eqI)
547   fix k
548   show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
549   proof (cases "k = Suc n")
550     case True show ?thesis
551     proof -
552       fix m
554         "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
555       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
556       also from True
557       have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
558         coeff P (monom P \<one> 1) (k - i))"
559         by (simp cong: R.finsum_cong add: Pi_def)
560       also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
561         coeff P (monom P \<one> 1) (k - i))"
562         by (simp only: ivl_disj_un_singleton)
563       also from True
564       have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
565         coeff P (monom P \<one> 1) (k - i))"
566         by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
567           order_less_imp_not_eq Pi_def)
568       also from True have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
570       finally show ?thesis .
571     qed
572   next
573     case False
574     note neq = False
575     let ?s =
576       "\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
577     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
578     also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
579     proof -
580       have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
581         by (simp cong: R.finsum_cong add: Pi_def)
582       from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
583         by (simp cong: R.finsum_cong add: Pi_def) arith
584       have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
585         by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
586       show ?thesis
587       proof (cases "k < n")
588         case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def)
589       next
590         case False then have n_le_k: "n <= k" by arith
591         show ?thesis
592         proof (cases "n = k")
593           case True
594           then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
595             by (simp cong: R.finsum_cong add: Pi_def)
596           also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
597             by (simp only: ivl_disj_un_singleton)
598           finally show ?thesis .
599         next
600           case False with n_le_k have n_less_k: "n < k" by arith
601           with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
602             by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
603           also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
604             by (simp only: ivl_disj_un_singleton)
605           also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
606             by (simp add: R.finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
607           also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
608             by (simp only: ivl_disj_un_one)
609           finally show ?thesis .
610         qed
611       qed
612     qed
613     also have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" by simp
614     finally show ?thesis .
615   qed
616 qed (simp_all)
618 lemma monom_one_Suc2:
619   "monom P \<one> (Suc n) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
620 proof (induct n)
621   case 0 show ?case by simp
622 next
623   case Suc
624   {
625     fix k:: nat
626     assume hypo: "monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
627     then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
628     proof -
629       have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
630         unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
631       note cl = monom_closed [OF R.one_closed, of 1]
632       note clk = monom_closed [OF R.one_closed, of k]
633       have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
634         unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc  [OF cl clk cl]] ..
635       from lhs rhs show ?thesis by simp
636     qed
637   }
638 qed
640 text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
641   and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
643 corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
644   unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
646 lemma monom_mult_smult:
647   "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
648   by (rule up_eqI) simp_all
650 lemma monom_one_mult:
651   "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m"
652 proof (induct n)
653   case 0 show ?case by simp
654 next
655   case Suc then show ?case
656     unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps
657     using m_assoc monom_one_comm [of m] by simp
658 qed
660 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"
661   unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all
663 lemma monom_mult [simp]:
664   assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R"
665   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
666 proof (rule up_eqI)
667   fix k
668   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"
669   proof (cases "n + m = k")
670     case True
671     {
672       show ?thesis
673         unfolding True [symmetric]
674           coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
675           coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
676         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>))"
677           "(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
678           a_in_R b_in_R
679         unfolding simp_implies_def
680         using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> b)"]
681         unfolding Pi_def by auto
682     }
683   next
684     case False
685     {
686       show ?thesis
687         unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False)
688         unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k]
689         unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False
690         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>)"]
691         unfolding Pi_def simp_implies_def using a_in_R b_in_R by force
692     }
693   qed
694 qed (simp_all add: a_in_R b_in_R)
696 lemma monom_a_inv [simp]:
697   "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
698   by (rule up_eqI) simp_all
700 lemma monom_inj:
701   "inj_on (%a. monom P a n) (carrier R)"
702 proof (rule inj_onI)
703   fix x y
704   assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
705   then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
706   with R show "x = y" by simp
707 qed
709 end
712 subsection \<open>The Degree Function\<close>
714 definition
715   deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
716   where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
718 context UP_ring
719 begin
721 lemma deg_aboveI:
722   "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
723   by (unfold deg_def P_def) (fast intro: Least_le)
725 (*
726 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
727 proof -
728   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
729   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
730   then show ?thesis ..
731 qed
733 lemma bound_coeff_obtain:
734   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
735 proof -
736   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
737   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
738   with prem show P .
739 qed
740 *)
742 lemma deg_aboveD:
743   assumes "deg R p < m" and "p \<in> carrier P"
744   shows "coeff P p m = \<zero>"
745 proof -
746   from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
747     by (auto simp add: UP_def P_def)
748   then have "bound \<zero> (deg R p) (coeff P p)"
749     by (auto simp: deg_def P_def dest: LeastI)
750   from this and \<open>deg R p < m\<close> show ?thesis ..
751 qed
753 lemma deg_belowI:
754   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
755     and R: "p \<in> carrier P"
756   shows "n <= deg R p"
757 -- \<open>Logically, this is a slightly stronger version of
758    @{thm [source] deg_aboveD}\<close>
759 proof (cases "n=0")
760   case True then show ?thesis by simp
761 next
762   case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
763   then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
764   then show ?thesis by arith
765 qed
767 lemma lcoeff_nonzero_deg:
768   assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
769   shows "coeff P p (deg R p) ~= \<zero>"
770 proof -
771   from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
772   proof -
773     have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
774       by arith
775     from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
776       by (unfold deg_def P_def) simp
777     then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
778     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
779       by (unfold bound_def) fast
780     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
781     then show ?thesis by (auto intro: that)
782   qed
783   with deg_belowI R have "deg R p = m" by fastforce
784   with m_coeff show ?thesis by simp
785 qed
787 lemma lcoeff_nonzero_nonzero:
788   assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
789   shows "coeff P p 0 ~= \<zero>"
790 proof -
791   have "EX m. coeff P p m ~= \<zero>"
792   proof (rule classical)
793     assume "~ ?thesis"
794     with R have "p = \<zero>\<^bsub>P\<^esub>" by (auto intro: up_eqI)
795     with nonzero show ?thesis by contradiction
796   qed
797   then obtain m where coeff: "coeff P p m ~= \<zero>" ..
798   from this and R have "m <= deg R p" by (rule deg_belowI)
799   then have "m = 0" by (simp add: deg)
800   with coeff show ?thesis by simp
801 qed
803 lemma lcoeff_nonzero:
804   assumes neq: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
805   shows "coeff P p (deg R p) ~= \<zero>"
806 proof (cases "deg R p = 0")
807   case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
808 next
809   case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
810 qed
812 lemma deg_eqI:
813   "[| !!m. n < m ==> coeff P p m = \<zero>;
814       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
815 by (fast intro: le_antisym deg_aboveI deg_belowI)
817 text \<open>Degree and polynomial operations\<close>
820   "p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
821   deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
824 lemma deg_monom_le:
825   "a \<in> carrier R ==> deg R (monom P a n) <= n"
826   by (intro deg_aboveI) simp_all
828 lemma deg_monom [simp]:
829   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
830   by (fastforce intro: le_antisym deg_aboveI deg_belowI)
832 lemma deg_const [simp]:
833   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
834 proof (rule le_antisym)
835   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
836 next
837   show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
838 qed
840 lemma deg_zero [simp]:
841   "deg R \<zero>\<^bsub>P\<^esub> = 0"
842 proof (rule le_antisym)
843   show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
844 next
845   show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
846 qed
848 lemma deg_one [simp]:
849   "deg R \<one>\<^bsub>P\<^esub> = 0"
850 proof (rule le_antisym)
851   show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
852 next
853   show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
854 qed
856 lemma deg_uminus [simp]:
857   assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
858 proof (rule le_antisym)
859   show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
860 next
861   show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
862     by (simp add: deg_belowI lcoeff_nonzero_deg
863       inj_on_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
864 qed
866 text\<open>The following lemma is later \emph{overwritten} by the most
867   specific one for domains, @{text deg_smult}.\<close>
869 lemma deg_smult_ring [simp]:
870   "[| a \<in> carrier R; p \<in> carrier P |] ==>
871   deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
872   by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
874 end
876 context UP_domain
877 begin
879 lemma deg_smult [simp]:
880   assumes R: "a \<in> carrier R" "p \<in> carrier P"
881   shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
882 proof (rule le_antisym)
883   show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
884     using R by (rule deg_smult_ring)
885 next
886   show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^bsub>P\<^esub> p)"
887   proof (cases "a = \<zero>")
888   qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
889 qed
891 end
893 context UP_ring
894 begin
896 lemma deg_mult_ring:
897   assumes R: "p \<in> carrier P" "q \<in> carrier P"
898   shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q"
899 proof (rule deg_aboveI)
900   fix m
901   assume boundm: "deg R p + deg R q < m"
902   {
903     fix k i
904     assume boundk: "deg R p + deg R q < k"
905     then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
906     proof (cases "deg R p < i")
907       case True then show ?thesis by (simp add: deg_aboveD R)
908     next
909       case False with boundk have "deg R q < k - i" by arith
910       then show ?thesis by (simp add: deg_aboveD R)
911     qed
912   }
913   with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
916 end
918 context UP_domain
919 begin
921 lemma deg_mult [simp]:
922   "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
923   deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
924 proof (rule le_antisym)
925   assume "p \<in> carrier P" " q \<in> carrier P"
926   then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_ring)
927 next
928   let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
929   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
930   have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
931   show "deg R p + deg R q <= deg R (p \<otimes>\<^bsub>P\<^esub> q)"
932   proof (rule deg_belowI, simp add: R)
933     have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
934       = (\<Oplus>i \<in> {..< deg R p} \<union> {deg R p .. deg R p + deg R q}. ?s i)"
935       by (simp only: ivl_disj_un_one)
936     also have "... = (\<Oplus>i \<in> {deg R p .. deg R p + deg R q}. ?s i)"
937       by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
939     also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
940       by (simp only: ivl_disj_un_singleton)
941     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
942       by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
943     finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
944       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
945     with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
946       by (simp add: integral_iff lcoeff_nonzero R)
948 qed
950 end
952 text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
954 context UP_ring
955 begin
957 lemma coeff_finsum:
958   assumes fin: "finite A"
959   shows "p \<in> A -> carrier P ==>
960     coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
961   using fin by induct (auto simp: Pi_def)
963 lemma up_repr:
964   assumes R: "p \<in> carrier P"
965   shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
966 proof (rule up_eqI)
967   let ?s = "(%i. monom P (coeff P p i) i)"
968   fix k
969   from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
970     by simp
971   show "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = coeff P p k"
972   proof (cases "k <= deg R p")
973     case True
974     hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
975           coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k} \<union> {k<..deg R p}. ?s i) k"
976       by (simp only: ivl_disj_un_one)
977     also from True
978     have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k}. ?s i) k"
979       by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint
980         ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
981     also
982     have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
983       by (simp only: ivl_disj_un_singleton)
984     also have "... = coeff P p k"
985       by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
986     finally show ?thesis .
987   next
988     case False
989     hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
990           coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
991       by (simp only: ivl_disj_un_singleton)
992     also from False have "... = coeff P p k"
993       by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
994     finally show ?thesis .
995   qed
996 qed (simp_all add: R Pi_def)
998 lemma up_repr_le:
999   "[| deg R p <= n; p \<in> carrier P |] ==>
1000   (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
1001 proof -
1002   let ?s = "(%i. monom P (coeff P p i) i)"
1003   assume R: "p \<in> carrier P" and "deg R p <= n"
1004   then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \<union> {deg R p<..n})"
1005     by (simp only: ivl_disj_un_one)
1006   also have "... = finsum P ?s {..deg R p}"
1007     by (simp cong: P.finsum_cong add: P.finsum_Un_disjoint ivl_disj_int_one
1008       deg_aboveD R Pi_def)
1009   also have "... = p" using R by (rule up_repr)
1010   finally show ?thesis .
1011 qed
1013 end
1016 subsection \<open>Polynomials over Integral Domains\<close>
1018 lemma domainI:
1019   assumes cring: "cring R"
1020     and one_not_zero: "one R ~= zero R"
1021     and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
1022       b \<in> carrier R |] ==> a = zero R | b = zero R"
1023   shows "domain R"
1024   by (auto intro!: domain.intro domain_axioms.intro cring.axioms assms
1025     del: disjCI)
1027 context UP_domain
1028 begin
1030 lemma UP_one_not_zero:
1031   "\<one>\<^bsub>P\<^esub> ~= \<zero>\<^bsub>P\<^esub>"
1032 proof
1033   assume "\<one>\<^bsub>P\<^esub> = \<zero>\<^bsub>P\<^esub>"
1034   hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp
1035   hence "\<one> = \<zero>" by simp
1036   with R.one_not_zero show "False" by contradiction
1037 qed
1039 lemma UP_integral:
1040   "[| p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>"
1041 proof -
1042   fix p q
1043   assume pq: "p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P" "q \<in> carrier P"
1044   show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>"
1045   proof (rule classical)
1046     assume c: "~ (p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>)"
1047     with R have "deg R p + deg R q = deg R (p \<otimes>\<^bsub>P\<^esub> q)" by simp
1048     also from pq have "... = 0" by simp
1049     finally have "deg R p + deg R q = 0" .
1050     then have f1: "deg R p = 0 & deg R q = 0" by simp
1051     from f1 R have "p = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P p i) i)"
1052       by (simp only: up_repr_le)
1053     also from R have "... = monom P (coeff P p 0) 0" by simp
1054     finally have p: "p = monom P (coeff P p 0) 0" .
1055     from f1 R have "q = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P q i) i)"
1056       by (simp only: up_repr_le)
1057     also from R have "... = monom P (coeff P q 0) 0" by simp
1058     finally have q: "q = monom P (coeff P q 0) 0" .
1059     from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^bsub>P\<^esub> q) 0" by simp
1060     also from pq have "... = \<zero>" by simp
1061     finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
1062     with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
1064     with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastforce
1065   qed
1066 qed
1068 theorem UP_domain:
1069   "domain P"
1070   by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
1072 end
1074 text \<open>
1075   Interpretation of theorems from @{term domain}.
1076 \<close>
1078 sublocale UP_domain < "domain" P
1079   by intro_locales (rule domain.axioms UP_domain)+
1082 subsection \<open>The Evaluation Homomorphism and Universal Property\<close>
1084 (* alternative congruence rule (possibly more efficient)
1085 lemma (in abelian_monoid) finsum_cong2:
1086   "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
1087   !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
1088   sorry*)
1090 lemma (in abelian_monoid) boundD_carrier:
1091   "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
1092   by auto
1094 context ring
1095 begin
1097 theorem diagonal_sum:
1098   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
1099   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1100   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1101 proof -
1102   assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
1103   {
1104     fix j
1105     have "j <= n + m ==>
1106       (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1107       (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
1108     proof (induct j)
1109       case 0 from Rf Rg show ?case by (simp add: Pi_def)
1110     next
1111       case (Suc j)
1112       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
1113         using Suc by (auto intro!: funcset_mem [OF Rg])
1114       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
1115         using Suc by (auto intro!: funcset_mem [OF Rg])
1116       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
1117         using Suc by (auto intro!: funcset_mem [OF Rf])
1118       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
1119         using Suc by (auto intro!: funcset_mem [OF Rg])
1120       have R11: "g 0 \<in> carrier R"
1121         using Suc by (auto intro!: funcset_mem [OF Rg])
1122       from Suc show ?case
1123         by (simp cong: finsum_cong add: Suc_diff_le a_ac
1124           Pi_def R6 R8 R9 R10 R11)
1125     qed
1126   }
1127   then show ?thesis by fast
1128 qed
1130 theorem cauchy_product:
1131   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
1132     and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
1133   shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1134     (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"      (* State reverse direction? *)
1135 proof -
1136   have f: "!!x. f x \<in> carrier R"
1137   proof -
1138     fix x
1139     show "f x \<in> carrier R"
1140       using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
1141   qed
1142   have g: "!!x. g x \<in> carrier R"
1143   proof -
1144     fix x
1145     show "g x \<in> carrier R"
1146       using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
1147   qed
1148   from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1149       (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1150     by (simp add: diagonal_sum Pi_def)
1151   also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1152     by (simp only: ivl_disj_un_one)
1153   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1154     by (simp cong: finsum_cong
1155       add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1156   also from f g
1157   have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m - k}. f k \<otimes> g i)"
1159   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
1160     by (simp cong: finsum_cong
1161       add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1162   also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"
1163     by (simp add: finsum_ldistr diagonal_sum Pi_def,
1164       simp cong: finsum_cong add: finsum_rdistr Pi_def)
1165   finally show ?thesis .
1166 qed
1168 end
1170 lemma (in UP_ring) const_ring_hom:
1171   "(%a. monom P a 0) \<in> ring_hom R P"
1172   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
1174 definition
1175   eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
1176            'a => 'b, 'b, nat => 'a] => 'b"
1177   where "eval R S phi s = (\<lambda>p \<in> carrier (UP R).
1178     \<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1180 context UP
1181 begin
1183 lemma eval_on_carrier:
1184   fixes S (structure)
1185   shows "p \<in> carrier P ==>
1186   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)"
1187   by (unfold eval_def, fold P_def) simp
1189 lemma eval_extensional:
1190   "eval R S phi p \<in> extensional (carrier P)"
1191   by (unfold eval_def, fold P_def) simp
1193 end
1195 text \<open>The universal property of the polynomial ring\<close>
1197 locale UP_pre_univ_prop = ring_hom_cring + UP_cring
1199 (* FIXME print_locale ring_hom_cring fails *)
1201 locale UP_univ_prop = UP_pre_univ_prop +
1202   fixes s and Eval
1203   assumes indet_img_carrier [simp, intro]: "s \<in> carrier S"
1204   defines Eval_def: "Eval == eval R S h s"
1206 text\<open>JE: I have moved the following lemma from Ring.thy and lifted then to the locale @{term ring_hom_ring} from @{term ring_hom_cring}.\<close>
1207 text\<open>JE: I was considering using it in @{text eval_ring_hom}, but that property does not hold for non commutative rings, so
1208   maybe it is not that necessary.\<close>
1210 lemma (in ring_hom_ring) hom_finsum [simp]:
1211   "f \<in> A -> carrier R ==>
1212   h (finsum R f A) = finsum S (h o f) A"
1213   by (induct A rule: infinite_finite_induct, auto simp: Pi_def)
1215 context UP_pre_univ_prop
1216 begin
1218 theorem eval_ring_hom:
1219   assumes S: "s \<in> carrier S"
1220   shows "eval R S h s \<in> ring_hom P S"
1221 proof (rule ring_hom_memI)
1222   fix p
1223   assume R: "p \<in> carrier P"
1224   then show "eval R S h s p \<in> carrier S"
1225     by (simp only: eval_on_carrier) (simp add: S Pi_def)
1226 next
1227   fix p q
1228   assume R: "p \<in> carrier P" "q \<in> carrier P"
1229   then show "eval R S h s (p \<oplus>\<^bsub>P\<^esub> q) = eval R S h s p \<oplus>\<^bsub>S\<^esub> eval R S h s q"
1230   proof (simp only: eval_on_carrier P.a_closed)
1231     from S R have
1232       "(\<Oplus>\<^bsub>S \<^esub>i\<in>{..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
1233       (\<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)}.
1234         h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1235       by (simp cong: S.finsum_cong
1237     also from R have "... =
1238         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
1239           h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1241     also from R S have "... =
1242       (\<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>
1243       (\<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)"
1244       by (simp cong: S.finsum_cong
1245         add: S.l_distr deg_aboveD ivl_disj_int_one Pi_def)
1246     also have "... =
1247         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
1248           h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
1249         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
1250           h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1251       by (simp only: ivl_disj_un_one max.cobounded1 max.cobounded2)
1252     also from R S have "... =
1253       (\<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>
1254       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1255       by (simp cong: S.finsum_cong
1256         add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
1257     finally show
1258       "(\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R (p \<oplus>\<^bsub>P\<^esub> q)}. h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
1259       (\<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>
1260       (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
1261   qed
1262 next
1263   show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
1264     by (simp only: eval_on_carrier UP_one_closed) simp
1265 next
1266   fix p q
1267   assume R: "p \<in> carrier P" "q \<in> carrier P"
1268   then show "eval R S h s (p \<otimes>\<^bsub>P\<^esub> q) = eval R S h s p \<otimes>\<^bsub>S\<^esub> eval R S h s q"
1269   proof (simp only: eval_on_carrier UP_mult_closed)
1270     from R S have
1271       "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
1272       (\<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}.
1273         h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1274       by (simp cong: S.finsum_cong
1275         add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def
1276         del: coeff_mult)
1277     also from R have "... =
1278       (\<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)"
1279       by (simp only: ivl_disj_un_one deg_mult_ring)
1280     also from R S have "... =
1281       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
1282          \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
1283            h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
1284            (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
1285       by (simp cong: S.finsum_cong add: S.nat_pow_mult Pi_def
1286         S.m_ac S.finsum_rdistr)
1287     also from R S have "... =
1288       (\<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>
1289       (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1290       by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
1291         Pi_def)
1292     finally show
1293       "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (p \<otimes>\<^bsub>P\<^esub> q)}. h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
1294       (\<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>
1295       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
1296   qed
1297 qed
1299 text \<open>
1300   The following lemma could be proved in @{text UP_cring} with the additional
1301   assumption that @{text h} is closed.\<close>
1303 lemma (in UP_pre_univ_prop) eval_const:
1304   "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
1305   by (simp only: eval_on_carrier monom_closed) simp
1307 text \<open>Further properties of the evaluation homomorphism.\<close>
1309 text \<open>The following proof is complicated by the fact that in arbitrary
1310   rings one might have @{term "one R = zero R"}.\<close>
1312 (* TODO: simplify by cases "one R = zero R" *)
1314 lemma (in UP_pre_univ_prop) eval_monom1:
1315   assumes S: "s \<in> carrier S"
1316   shows "eval R S h s (monom P \<one> 1) = s"
1317 proof (simp only: eval_on_carrier monom_closed R.one_closed)
1318    from S have
1319     "(\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) =
1320     (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
1321       h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1322     by (simp cong: S.finsum_cong del: coeff_monom
1323       add: deg_aboveD S.finsum_Un_disjoint ivl_disj_int_one Pi_def)
1324   also have "... =
1325     (\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1326     by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
1327   also have "... = s"
1328   proof (cases "s = \<zero>\<^bsub>S\<^esub>")
1329     case True then show ?thesis by (simp add: Pi_def)
1330   next
1331     case False then show ?thesis by (simp add: S Pi_def)
1332   qed
1333   finally show "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (monom P \<one> 1)}.
1334     h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" .
1335 qed
1337 end
1339 text \<open>Interpretation of ring homomorphism lemmas.\<close>
1341 sublocale UP_univ_prop < ring_hom_cring P S Eval
1342   unfolding Eval_def
1343   by unfold_locales (fast intro: eval_ring_hom)
1345 lemma (in UP_cring) monom_pow:
1346   assumes R: "a \<in> carrier R"
1347   shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)"
1348 proof (induct m)
1349   case 0 from R show ?case by simp
1350 next
1351   case Suc with R show ?case
1353 qed
1355 lemma (in ring_hom_cring) hom_pow [simp]:
1356   "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^bsub>S\<^esub> (n::nat)"
1357   by (induct n) simp_all
1359 lemma (in UP_univ_prop) Eval_monom:
1360   "r \<in> carrier R ==> Eval (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
1361 proof -
1362   assume R: "r \<in> carrier R"
1363   from R have "Eval (monom P r n) = Eval (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)"
1364     by (simp del: monom_mult add: monom_mult [THEN sym] monom_pow)
1365   also
1366   from R eval_monom1 [where s = s, folded Eval_def]
1367   have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
1368     by (simp add: eval_const [where s = s, folded Eval_def])
1369   finally show ?thesis .
1370 qed
1372 lemma (in UP_pre_univ_prop) eval_monom:
1373   assumes R: "r \<in> carrier R" and S: "s \<in> carrier S"
1374   shows "eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
1375 proof -
1376   interpret UP_univ_prop R S h P s "eval R S h s"
1377     using UP_pre_univ_prop_axioms P_def R S
1378     by (auto intro: UP_univ_prop.intro UP_univ_prop_axioms.intro)
1379   from R
1380   show ?thesis by (rule Eval_monom)
1381 qed
1383 lemma (in UP_univ_prop) Eval_smult:
1384   "[| r \<in> carrier R; p \<in> carrier P |] ==> Eval (r \<odot>\<^bsub>P\<^esub> p) = h r \<otimes>\<^bsub>S\<^esub> Eval p"
1385 proof -
1386   assume R: "r \<in> carrier R" and P: "p \<in> carrier P"
1387   then show ?thesis
1388     by (simp add: monom_mult_is_smult [THEN sym]
1389       eval_const [where s = s, folded Eval_def])
1390 qed
1392 lemma ring_hom_cringI:
1393   assumes "cring R"
1394     and "cring S"
1395     and "h \<in> ring_hom R S"
1396   shows "ring_hom_cring R S h"
1397   by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
1398     cring.axioms assms)
1400 context UP_pre_univ_prop
1401 begin
1403 lemma UP_hom_unique:
1404   assumes "ring_hom_cring P S Phi"
1405   assumes Phi: "Phi (monom P \<one> (Suc 0)) = s"
1406       "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
1407   assumes "ring_hom_cring P S Psi"
1408   assumes Psi: "Psi (monom P \<one> (Suc 0)) = s"
1409       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
1410     and P: "p \<in> carrier P" and S: "s \<in> carrier S"
1411   shows "Phi p = Psi p"
1412 proof -
1413   interpret ring_hom_cring P S Phi by fact
1414   interpret ring_hom_cring P S Psi by fact
1415   have "Phi p =
1416       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)"
1417     by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
1418   also
1419   have "... =
1420       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)"
1421     by (simp add: Phi Psi P Pi_def comp_def)
1422   also have "... = Psi p"
1423     by (simp add: up_repr P monom_mult [THEN sym] monom_pow del: monom_mult)
1424   finally show ?thesis .
1425 qed
1427 lemma ring_homD:
1428   assumes Phi: "Phi \<in> ring_hom P S"
1429   shows "ring_hom_cring P S Phi"
1430   by unfold_locales (rule Phi)
1432 theorem UP_universal_property:
1433   assumes S: "s \<in> carrier S"
1434   shows "EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
1435     Phi (monom P \<one> 1) = s &
1436     (ALL r : carrier R. Phi (monom P r 0) = h r)"
1437   using S eval_monom1
1438   apply (auto intro: eval_ring_hom eval_const eval_extensional)
1439   apply (rule extensionalityI)
1440   apply (auto intro: UP_hom_unique ring_homD)
1441   done
1443 end
1445 text\<open>JE: The following lemma was added by me; it might be even lifted to a simpler locale\<close>
1447 context monoid
1448 begin
1450 lemma nat_pow_eone[simp]: assumes x_in_G: "x \<in> carrier G" shows "x (^) (1::nat) = x"
1451   using nat_pow_Suc [of x 0] unfolding nat_pow_0 [of x] unfolding l_one [OF x_in_G] by simp
1453 end
1455 context UP_ring
1456 begin
1458 abbreviation lcoeff :: "(nat =>'a) => 'a" where "lcoeff p == coeff P p (deg R p)"
1460 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>"
1461   using lcoeff_nonzero [OF p_not_zero p_in_R] .
1464 subsection\<open>The long division algorithm: some previous facts.\<close>
1466 lemma coeff_minus [simp]:
1467   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"
1468   unfolding a_minus_def [OF p q] unfolding coeff_add [OF p a_inv_closed [OF q]] unfolding coeff_a_inv [OF q]
1469   using coeff_closed [OF p, of n] using coeff_closed [OF q, of n] by algebra
1471 lemma lcoeff_closed [simp]: assumes p: "p \<in> carrier P" shows "lcoeff p \<in> carrier R"
1472   using coeff_closed [OF p, of "deg R p"] by simp
1474 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"
1475   using deg_smult_ring [OF a_in_R f_in_P] by (cases "a = \<zero>", auto)
1477 lemma coeff_monom_mult: assumes R: "c \<in> carrier R" and P: "p \<in> carrier P"
1478   shows "coeff P (monom P c n \<otimes>\<^bsub>P\<^esub> p) (m + n) = c \<otimes> (coeff P p m)"
1479 proof -
1480   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))"
1481     unfolding coeff_mult [OF monom_closed [OF R, of n] P, of "m + n"] unfolding coeff_monom [OF R, of n] by simp
1482   also have "(\<Oplus>i\<in>{..m + n}. (if n = i then c else \<zero>) \<otimes> coeff P p (m + n - i)) =
1483     (\<Oplus>i\<in>{..m + n}. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"
1484     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))"
1485       "(\<lambda>i::nat. (if n = i then c \<otimes> coeff P p (m + n - i) else \<zero>))"]
1486     using coeff_closed [OF P] unfolding Pi_def simp_implies_def using R by auto
1487   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))"]
1488     unfolding Pi_def using coeff_closed [OF P] using P R by auto
1489   finally show ?thesis by simp
1490 qed
1492 lemma deg_lcoeff_cancel:
1493   assumes p_in_P: "p \<in> carrier P" and q_in_P: "q \<in> carrier P" and r_in_P: "r \<in> carrier P"
1494   and deg_r_nonzero: "deg R r \<noteq> 0"
1495   and deg_R_p: "deg R p \<le> deg R r" and deg_R_q: "deg R q \<le> deg R r"
1496   and coeff_R_p_eq_q: "coeff P p (deg R r) = \<ominus>\<^bsub>R\<^esub> (coeff P q (deg R r))"
1497   shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) < deg R r"
1498 proof -
1499   have deg_le: "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<le> deg R r"
1500   proof (rule deg_aboveI)
1501     fix m
1502     assume deg_r_le: "deg R r < m"
1503     show "coeff P (p \<oplus>\<^bsub>P\<^esub> q) m = \<zero>"
1504     proof -
1505       have slp: "deg R p < m" and "deg R q < m" using deg_R_p deg_R_q using deg_r_le by auto
1506       then have max_sl: "max (deg R p) (deg R q) < m" by simp
1507       then have "deg R (p \<oplus>\<^bsub>P\<^esub> q) < m" using deg_add [OF p_in_P q_in_P] by arith
1508       with deg_R_p deg_R_q show ?thesis using coeff_add [OF p_in_P q_in_P, of m]
1509         using deg_aboveD [of "p \<oplus>\<^bsub>P\<^esub> q" m] using p_in_P q_in_P by simp
1510     qed
1511   qed (simp add: p_in_P q_in_P)
1512   moreover have deg_ne: "deg R (p \<oplus>\<^bsub>P\<^esub> q) \<noteq> deg R r"
1513   proof (rule ccontr)
1514     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
1515     from deg_r_nonzero have r_nonzero: "r \<noteq> \<zero>\<^bsub>P\<^esub>" by (cases "r = \<zero>\<^bsub>P\<^esub>", simp_all)
1516     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
1517       using coeff_closed [OF p_in_P, of "deg R r"] coeff_closed [OF q_in_P, of "deg R r"] by algebra
1518     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
1519       using deg_r_nonzero by (cases "p \<oplus>\<^bsub>P\<^esub> q \<noteq> \<zero>\<^bsub>P\<^esub>", auto)
1520   qed
1521   ultimately show ?thesis by simp
1522 qed
1524 lemma monom_deg_mult:
1525   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"
1526   and a_in_R: "a \<in> carrier R"
1527   shows "deg R (g \<otimes>\<^bsub>P\<^esub> monom P a (deg R f - deg R g)) \<le> deg R f"
1528   using deg_mult_ring [OF g_in_P monom_closed [OF a_in_R, of "deg R f - deg R g"]]
1529   apply (cases "a = \<zero>") using g_in_P apply simp
1530   using deg_monom [OF _ a_in_R, of "deg R f - deg R g"] using deg_le by simp
1532 lemma deg_zero_impl_monom:
1533   assumes f_in_P: "f \<in> carrier P" and deg_f: "deg R f = 0"
1534   shows "f = monom P (coeff P f 0) 0"
1535   apply (rule up_eqI) using coeff_monom [OF coeff_closed [OF f_in_P], of 0 0]
1536   using f_in_P deg_f using deg_aboveD [of f _] by auto
1538 end
1541 subsection \<open>The long division proof for commutative rings\<close>
1543 context UP_cring
1544 begin
1546 lemma exI3: assumes exist: "Pred x y z"
1547   shows "\<exists> x y z. Pred x y z"
1548   using exist by blast
1550 text \<open>Jacobson's Theorem 2.14\<close>
1552 lemma long_div_theorem:
1553   assumes g_in_P [simp]: "g \<in> carrier P" and f_in_P [simp]: "f \<in> carrier P"
1554   and g_not_zero: "g \<noteq> \<zero>\<^bsub>P\<^esub>"
1555   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)"
1556   using f_in_P
1557 proof (induct "deg R f" arbitrary: "f" rule: nat_less_induct)
1558   case (1 f)
1559   note f_in_P [simp] = "1.prems"
1560   let ?pred = "(\<lambda> q r (k::nat).
1561     (q \<in> carrier P) \<and> (r \<in> carrier P)
1562     \<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))"
1563   let ?lg = "lcoeff g" and ?lf = "lcoeff f"
1564   show ?case
1565   proof (cases "deg R f < deg R g")
1566     case True
1567     have "?pred \<zero>\<^bsub>P\<^esub> f 0" using True by force
1568     then show ?thesis by blast
1569   next
1570     case False then have deg_g_le_deg_f: "deg R g \<le> deg R f" by simp
1571     {
1572       let ?k = "1::nat"
1573       let ?f1 = "(g \<otimes>\<^bsub>P\<^esub> (monom P (?lf) (deg R f - deg R g))) \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)"
1574       let ?q = "monom P (?lf) (deg R f - deg R g)"
1575       have f1_in_carrier: "?f1 \<in> carrier P" and q_in_carrier: "?q \<in> carrier P" by simp_all
1576       show ?thesis
1577       proof (cases "deg R f = 0")
1578         case True
1579         {
1580           have deg_g: "deg R g = 0" using True using deg_g_le_deg_f by simp
1581           have "?pred f \<zero>\<^bsub>P\<^esub> 1"
1582             using deg_zero_impl_monom [OF g_in_P deg_g]
1583             using sym [OF monom_mult_is_smult [OF coeff_closed [OF g_in_P, of 0] f_in_P]]
1584             using deg_g by simp
1585           then show ?thesis by blast
1586         }
1587       next
1588         case False note deg_f_nzero = False
1589         {
1590           have exist: "lcoeff g (^) ?k \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1"
1592               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"]])
1593           have deg_remainder_l_f: "deg R (\<ominus>\<^bsub>P\<^esub> ?f1) < deg R f"
1594           proof (unfold deg_uminus [OF f1_in_carrier])
1595             show "deg R ?f1 < deg R f"
1596             proof (rule deg_lcoeff_cancel)
1597               show "deg R (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) \<le> deg R f"
1598                 using deg_smult_ring [of ?lg f]
1599                 using lcoeff_nonzero2 [OF g_in_P g_not_zero] by simp
1600               show "deg R (g \<otimes>\<^bsub>P\<^esub> ?q) \<le> deg R f"
1601                 by (simp add: monom_deg_mult [OF f_in_P g_in_P deg_g_le_deg_f, of ?lf])
1602               show "coeff P (g \<otimes>\<^bsub>P\<^esub> ?q) (deg R f) = \<ominus> coeff P (\<ominus>\<^bsub>P\<^esub> (?lg \<odot>\<^bsub>P\<^esub> f)) (deg R f)"
1603                 unfolding coeff_mult [OF g_in_P monom_closed
1604                   [OF lcoeff_closed [OF f_in_P],
1605                     of "deg R f - deg R g"], of "deg R f"]
1606                 unfolding coeff_monom [OF lcoeff_closed
1607                   [OF f_in_P], of "(deg R f - deg R g)"]
1608                 using R.finsum_cong' [of "{..deg R f}" "{..deg R f}"
1609                   "(\<lambda>i. coeff P g i \<otimes> (if deg R f - deg R g = deg R f - i then ?lf else \<zero>))"
1610                   "(\<lambda>i. if deg R g = i then coeff P g i \<otimes> ?lf else \<zero>)"]
1611                 using R.finsum_singleton [of "deg R g" "{.. deg R f}" "(\<lambda>i. coeff P g i \<otimes> ?lf)"]
1612                 unfolding Pi_def using deg_g_le_deg_f by force
1614           qed
1615           then obtain q' r' k'
1616             where rem_desc: "?lg (^) (k'::nat) \<odot>\<^bsub>P\<^esub> (\<ominus>\<^bsub>P\<^esub> ?f1) = g \<otimes>\<^bsub>P\<^esub> q' \<oplus>\<^bsub>P\<^esub> r'"
1617             and rem_deg: "(r' = \<zero>\<^bsub>P\<^esub> \<or> deg R r' < deg R g)"
1618             and q'_in_carrier: "q' \<in> carrier P" and r'_in_carrier: "r' \<in> carrier P"
1619             using "1.hyps" using f1_in_carrier by blast
1620           show ?thesis
1621           proof (rule exI3 [of _ "((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q')" r' "Suc k'"], intro conjI)
1622             show "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = g \<otimes>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<oplus>\<^bsub>P\<^esub> r'"
1623             proof -
1624               have "(?lg (^) (Suc k')) \<odot>\<^bsub>P\<^esub> f = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> \<ominus>\<^bsub>P\<^esub> ?f1)"
1625                 using smult_assoc1 [OF _ _ f_in_P] using exist by simp
1626               also have "\<dots> = (?lg (^) k') \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q) \<oplus>\<^bsub>P\<^esub> ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ( \<ominus>\<^bsub>P\<^esub> ?f1))"
1627                 using UP_smult_r_distr by simp
1628               also have "\<dots> = (?lg (^) 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')"
1629                 unfolding rem_desc ..
1630               also have "\<dots> = (?lg (^) 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'"
1631                 using sym [OF a_assoc [of "?lg (^) k' \<odot>\<^bsub>P\<^esub> (g \<otimes>\<^bsub>P\<^esub> ?q)" "g \<otimes>\<^bsub>P\<^esub> q'" "r'"]]
1632                 using r'_in_carrier q'_in_carrier by simp
1633               also have "\<dots> = (?lg (^) 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'"
1634                 using q'_in_carrier by (auto simp add: m_comm)
1635               also have "\<dots> = (((?lg (^) 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'"
1636                 using smult_assoc2 q'_in_carrier "1.prems" by auto
1637               also have "\<dots> = ((?lg (^) k') \<odot>\<^bsub>P\<^esub> ?q \<oplus>\<^bsub>P\<^esub> q') \<otimes>\<^bsub>P\<^esub> g \<oplus>\<^bsub>P\<^esub> r'"
1638                 using sym [OF l_distr] and q'_in_carrier by auto
1639               finally show ?thesis using m_comm q'_in_carrier by auto
1640             qed
1641           qed (simp_all add: rem_deg q'_in_carrier r'_in_carrier)
1642         }
1643       qed
1644     }
1645   qed
1646 qed
1648 end
1651 text \<open>The remainder theorem as corollary of the long division theorem.\<close>
1653 context UP_cring
1654 begin
1656 lemma deg_minus_monom:
1657   assumes a: "a \<in> carrier R"
1658   and R_not_trivial: "(carrier R \<noteq> {\<zero>})"
1659   shows "deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = 1"
1660   (is "deg R ?g = 1")
1661 proof -
1662   have "deg R ?g \<le> 1"
1663   proof (rule deg_aboveI)
1664     fix m
1665     assume "(1::nat) < m"
1666     then show "coeff P ?g m = \<zero>"
1667       using coeff_minus using a by auto algebra
1669   moreover have "deg R ?g \<ge> 1"
1670   proof (rule deg_belowI)
1671     show "coeff P ?g 1 \<noteq> \<zero>"
1672       using a using R.carrier_one_not_zero R_not_trivial by simp algebra
1674   ultimately show ?thesis by simp
1675 qed
1677 lemma lcoeff_monom:
1678   assumes a: "a \<in> carrier R" and R_not_trivial: "(carrier R \<noteq> {\<zero>})"
1679   shows "lcoeff (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<one>"
1680   using deg_minus_monom [OF a R_not_trivial]
1681   using coeff_minus a by auto algebra
1683 lemma deg_nzero_nzero:
1684   assumes deg_p_nzero: "deg R p \<noteq> 0"
1685   shows "p \<noteq> \<zero>\<^bsub>P\<^esub>"
1686   using deg_zero deg_p_nzero by auto
1688 lemma deg_monom_minus:
1689   assumes a: "a \<in> carrier R"
1690   and R_not_trivial: "carrier R \<noteq> {\<zero>}"
1691   shows "deg R (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = 1"
1692   (is "deg R ?g = 1")
1693 proof -
1694   have "deg R ?g \<le> 1"
1695   proof (rule deg_aboveI)
1696     fix m::nat assume "1 < m" then show "coeff P ?g m = \<zero>"
1697       using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of m]
1698       using coeff_monom [OF R.one_closed, of 1 m] using coeff_monom [OF a, of 0 m] by auto algebra
1700   moreover have "1 \<le> deg R ?g"
1701   proof (rule deg_belowI)
1702     show "coeff P ?g 1 \<noteq> \<zero>"
1703       using coeff_minus [OF monom_closed [OF R.one_closed, of 1] monom_closed [OF a, of 0], of 1]
1704       using coeff_monom [OF R.one_closed, of 1 1] using coeff_monom [OF a, of 0 1]
1705       using R_not_trivial using R.carrier_one_not_zero
1706       by auto algebra
1708   ultimately show ?thesis by simp
1709 qed
1711 lemma eval_monom_expr:
1712   assumes a: "a \<in> carrier R"
1713   shows "eval R R id a (monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0) = \<zero>"
1714   (is "eval R R id a ?g = _")
1715 proof -
1716   interpret UP_pre_univ_prop R R id by unfold_locales simp
1717   have eval_ring_hom: "eval R R id a \<in> ring_hom P R" using eval_ring_hom [OF a] by simp
1718   interpret ring_hom_cring P R "eval R R id a" by unfold_locales (rule eval_ring_hom)
1719   have mon1_closed: "monom P \<one>\<^bsub>R\<^esub> 1 \<in> carrier P"
1720     and mon0_closed: "monom P a 0 \<in> carrier P"
1721     and min_mon0_closed: "\<ominus>\<^bsub>P\<^esub> monom P a 0 \<in> carrier P"
1722     using a R.a_inv_closed by auto
1723   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)"
1724     unfolding P.minus_eq [OF mon1_closed mon0_closed]
1725     unfolding hom_add [OF mon1_closed min_mon0_closed]
1726     unfolding hom_a_inv [OF mon0_closed]
1727     using R.minus_eq [symmetric] mon1_closed mon0_closed by auto
1728   also have "\<dots> = a \<ominus> a"
1729     using eval_monom [OF R.one_closed a, of 1] using eval_monom [OF a a, of 0] using a by simp
1730   also have "\<dots> = \<zero>"
1731     using a by algebra
1732   finally show ?thesis by simp
1733 qed
1735 lemma remainder_theorem_exist:
1736   assumes f: "f \<in> carrier P" and a: "a \<in> carrier R"
1737   and R_not_trivial: "carrier R \<noteq> {\<zero>}"
1738   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)"
1739   (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)")
1740 proof -
1741   let ?g = "monom P \<one>\<^bsub>R\<^esub> 1 \<ominus>\<^bsub>P\<^esub> monom P a 0"
1742   from deg_minus_monom [OF a R_not_trivial]
1743   have deg_g_nzero: "deg R ?g \<noteq> 0" by simp
1744   have "\<exists>q r (k::nat). q \<in> carrier P \<and> r \<in> carrier P \<and>
1745     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)"
1746     using long_div_theorem [OF _ f deg_nzero_nzero [OF deg_g_nzero]] a
1747     by auto
1748   then show ?thesis
1749     unfolding lcoeff_monom [OF a R_not_trivial]
1750     unfolding deg_monom_minus [OF a R_not_trivial]
1751     using smult_one [OF f] using deg_zero by force
1752 qed
1754 lemma remainder_theorem_expression:
1755   assumes f [simp]: "f \<in> carrier P" and a [simp]: "a \<in> carrier R"
1756   and q [simp]: "q \<in> carrier P" and r [simp]: "r \<in> carrier P"
1757   and R_not_trivial: "carrier R \<noteq> {\<zero>}"
1758   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"
1759   (is "f = ?g \<otimes>\<^bsub>P\<^esub> q \<oplus>\<^bsub>P\<^esub> r" is "f = ?gq \<oplus>\<^bsub>P\<^esub> r")
1760     and deg_r_0: "deg R r = 0"
1761     shows "r = monom P (eval R R id a f) 0"
1762 proof -
1763   interpret UP_pre_univ_prop R R id P by standard simp
1764   have eval_ring_hom: "eval R R id a \<in> ring_hom P R"
1765     using eval_ring_hom [OF a] by simp
1766   have "eval R R id a f = eval R R id a ?gq \<oplus>\<^bsub>R\<^esub> eval R R id a r"
1767     unfolding f_expr using ring_hom_add [OF eval_ring_hom] by auto
1768   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"
1769     using ring_hom_mult [OF eval_ring_hom] by auto
1770   also have "\<dots> = \<zero> \<oplus> eval R R id a r"
1771     unfolding eval_monom_expr [OF a] using eval_ring_hom
1772     unfolding ring_hom_def using q unfolding Pi_def by simp
1773   also have "\<dots> = eval R R id a r"
1774     using eval_ring_hom unfolding ring_hom_def using r unfolding Pi_def by simp
1775   finally have eval_eq: "eval R R id a f = eval R R id a r" by simp
1776   from deg_zero_impl_monom [OF r deg_r_0]
1777   have "r = monom P (coeff P r 0) 0" by simp
1778   with eval_const [OF a, of "coeff P r 0"] eval_eq
1779   show ?thesis by auto
1780 qed
1782 corollary remainder_theorem:
1783   assumes f [simp]: "f \<in> carrier P" and a [simp]: "a \<in> carrier R"
1784   and R_not_trivial: "carrier R \<noteq> {\<zero>}"
1785   shows "\<exists> q r. (q \<in> carrier P) \<and> (r \<in> carrier P) \<and>
1786      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"
1787   (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")
1788 proof -
1789   from remainder_theorem_exist [OF f a R_not_trivial]
1790   obtain q r
1791     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"
1792     and deg_r: "deg R r = 0" by force
1793   with remainder_theorem_expression [OF f a _ _ R_not_trivial, of q r]
1794   show ?thesis by auto
1795 qed
1797 end
1800 subsection \<open>Sample Application of Evaluation Homomorphism\<close>
1802 lemma UP_pre_univ_propI:
1803   assumes "cring R"
1804     and "cring S"
1805     and "h \<in> ring_hom R S"
1806   shows "UP_pre_univ_prop R S h"
1807   using assms
1808   by (auto intro!: UP_pre_univ_prop.intro ring_hom_cring.intro
1809     ring_hom_cring_axioms.intro UP_cring.intro)
1811 definition
1812   INTEG :: "int ring"
1813   where "INTEG = \<lparr>carrier = UNIV, mult = op *, one = 1, zero = 0, add = op +\<rparr>"
1815 lemma INTEG_cring: "cring INTEG"
1816   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
1817     left_minus distrib_right)
1819 lemma INTEG_id_eval:
1820   "UP_pre_univ_prop INTEG INTEG id"
1821   by (fast intro: UP_pre_univ_propI INTEG_cring id_ring_hom)
1823 text \<open>
1824   Interpretation now enables to import all theorems and lemmas
1825   valid in the context of homomorphisms between @{term INTEG} and @{term
1826   "UP INTEG"} globally.
1827 \<close>
1829 interpretation INTEG: UP_pre_univ_prop INTEG INTEG id "UP INTEG"
1830   using INTEG_id_eval by simp_all
1832 lemma INTEG_closed [intro, simp]:
1833   "z \<in> carrier INTEG"
1834   by (unfold INTEG_def) simp
1836 lemma INTEG_mult [simp]:
1837   "mult INTEG z w = z * w"
1838   by (unfold INTEG_def) simp
1840 lemma INTEG_pow [simp]:
1841   "pow INTEG z n = z ^ n"
1842   by (induct n) (simp_all add: INTEG_def nat_pow_def)
1844 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"