src/HOL/Algebra/UnivPoly.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 16417 9bc16273c2d4 child 16639 5a89d3622ac0 permissions -rw-r--r--
Constant "If" is now local
1 (*
2   Title:     HOL/Algebra/UnivPoly.thy
3   Id:        \$Id\$
4   Author:    Clemens Ballarin, started 9 December 1996
5   Copyright: Clemens Ballarin
6 *)
8 header {* Univariate Polynomials *}
10 theory UnivPoly imports Module begin
12 text {*
13   Polynomials are formalised as modules with additional operations for
14   extracting coefficients from polynomials and for obtaining monomials
15   from coefficients and exponents (record @{text "up_ring"}).  The
16   carrier set is a set of bounded functions from Nat to the
17   coefficient domain.  Bounded means that these functions return zero
18   above a certain bound (the degree).  There is a chapter on the
19   formalisation of polynomials in the PhD thesis \cite{Ballarin:1999},
20   which was implemented with axiomatic type classes.  This was later
21   ported to Locales.
22 *}
25 subsection {* The Constructor for Univariate Polynomials *}
27 text {*
28   Functions with finite support.
29 *}
31 locale bound =
32   fixes z :: 'a
33     and n :: nat
34     and f :: "nat => 'a"
35   assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
37 declare bound.intro [intro!]
38   and bound.bound [dest]
40 lemma bound_below:
41   assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
42 proof (rule classical)
43   assume "~ ?thesis"
44   then have "m < n" by arith
45   with bound have "f n = z" ..
46   with nonzero show ?thesis by contradiction
47 qed
49 record ('a, 'p) up_ring = "('a, 'p) module" +
50   monom :: "['a, nat] => 'p"
51   coeff :: "['p, nat] => 'a"
53 constdefs (structure R)
54   up :: "('a, 'm) ring_scheme => (nat => 'a) set"
55   "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound \<zero> n f)}"
56   UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
57   "UP R == (|
58     carrier = up R,
59     mult = (%p:up R. %q:up R. %n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)),
60     one = (%i. if i=0 then \<one> else \<zero>),
61     zero = (%i. \<zero>),
62     add = (%p:up R. %q:up R. %i. p i \<oplus> q i),
63     smult = (%a:carrier R. %p:up R. %i. a \<otimes> p i),
64     monom = (%a:carrier R. %n i. if i=n then a else \<zero>),
65     coeff = (%p:up R. %n. p n) |)"
67 text {*
68   Properties of the set of polynomials @{term up}.
69 *}
71 lemma mem_upI [intro]:
72   "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
73   by (simp add: up_def Pi_def)
75 lemma mem_upD [dest]:
76   "f \<in> up R ==> f n \<in> carrier R"
77   by (simp add: up_def Pi_def)
79 lemma (in cring) bound_upD [dest]:
80   "f \<in> up R ==> EX n. bound \<zero> n f"
81   by (simp add: up_def)
83 lemma (in cring) up_one_closed:
84    "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
85   using up_def by force
87 lemma (in cring) up_smult_closed:
88   "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
89   by force
91 lemma (in cring) up_add_closed:
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 fastsimp
109     qed
110     then show ?thesis ..
111   qed
112 qed
114 lemma (in cring) 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 (in cring) up_mult_closed:
124   "[| p \<in> up R; q \<in> up R |] ==>
125   (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
126 proof
127   fix n
128   assume "p \<in> up R" "q \<in> up R"
129   then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
130     by (simp add: mem_upD  funcsetI)
131 next
132   assume UP: "p \<in> up R" "q \<in> up R"
133   show "EX n. bound \<zero> n (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
134   proof -
135     from UP obtain n where boundn: "bound \<zero> n p" by fast
136     from UP obtain m where boundm: "bound \<zero> m q" by fast
137     have "bound \<zero> (n + m) (%n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
138     proof
139       fix k assume bound: "n + m < k"
140       {
141         fix i
142         have "p i \<otimes> q (k-i) = \<zero>"
143         proof (cases "n < i")
144           case True
145           with boundn have "p i = \<zero>" by auto
146           moreover from UP have "q (k-i) \<in> carrier R" by auto
147           ultimately show ?thesis by simp
148         next
149           case False
150           with bound have "m < k-i" by arith
151           with boundm have "q (k-i) = \<zero>" by auto
152           moreover from UP have "p i \<in> carrier R" by auto
153           ultimately show ?thesis by simp
154         qed
155       }
156       then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
157         by (simp add: Pi_def)
158     qed
159     then show ?thesis by fast
160   qed
161 qed
164 subsection {* Effect of operations on coefficients *}
166 locale UP = struct R + struct P +
167   defines P_def: "P == UP R"
169 locale UP_cring = UP + cring R
171 locale UP_domain = UP_cring + "domain" R
173 text {*
174   Temporarily declare @{thm [locale=UP] P_def} as simp rule.
175 *}
177 declare (in UP) P_def [simp]
179 lemma (in UP_cring) coeff_monom [simp]:
180   "a \<in> carrier R ==>
181   coeff P (monom P a m) n = (if m=n then a else \<zero>)"
182 proof -
183   assume R: "a \<in> carrier R"
184   then have "(%n. if n = m then a else \<zero>) \<in> up R"
185     using up_def by force
186   with R show ?thesis by (simp add: UP_def)
187 qed
189 lemma (in UP_cring) coeff_zero [simp]:
190   "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>"
191   by (auto simp add: UP_def)
193 lemma (in UP_cring) coeff_one [simp]:
194   "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
195   using up_one_closed by (simp add: UP_def)
197 lemma (in UP_cring) coeff_smult [simp]:
198   "[| a \<in> carrier R; p \<in> carrier P |] ==>
199   coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
200   by (simp add: UP_def up_smult_closed)
202 lemma (in UP_cring) coeff_add [simp]:
203   "[| p \<in> carrier P; q \<in> carrier P |] ==>
204   coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
207 lemma (in UP_cring) coeff_mult [simp]:
208   "[| p \<in> carrier P; q \<in> carrier P |] ==>
209   coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
210   by (simp add: UP_def up_mult_closed)
212 lemma (in UP) up_eqI:
213   assumes prem: "!!n. coeff P p n = coeff P q n"
214     and R: "p \<in> carrier P" "q \<in> carrier P"
215   shows "p = q"
216 proof
217   fix x
218   from prem and R show "p x = q x" by (simp add: UP_def)
219 qed
221 subsection {* Polynomials form a commutative ring. *}
223 text {* Operations are closed over @{term P}. *}
225 lemma (in UP_cring) UP_mult_closed [simp]:
226   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P"
227   by (simp add: UP_def up_mult_closed)
229 lemma (in UP_cring) UP_one_closed [simp]:
230   "\<one>\<^bsub>P\<^esub> \<in> carrier P"
231   by (simp add: UP_def up_one_closed)
233 lemma (in UP_cring) UP_zero_closed [intro, simp]:
234   "\<zero>\<^bsub>P\<^esub> \<in> carrier P"
235   by (auto simp add: UP_def)
237 lemma (in UP_cring) UP_a_closed [intro, simp]:
238   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P"
241 lemma (in UP_cring) monom_closed [simp]:
242   "a \<in> carrier R ==> monom P a n \<in> carrier P"
243   by (auto simp add: UP_def up_def Pi_def)
245 lemma (in UP_cring) UP_smult_closed [simp]:
246   "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P"
247   by (simp add: UP_def up_smult_closed)
249 lemma (in UP) coeff_closed [simp]:
250   "p \<in> carrier P ==> coeff P p n \<in> carrier R"
251   by (auto simp add: UP_def)
253 declare (in UP) P_def [simp del]
255 text {* Algebraic ring properties *}
257 lemma (in UP_cring) UP_a_assoc:
258   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
259   shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)"
260   by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
262 lemma (in UP_cring) UP_l_zero [simp]:
263   assumes R: "p \<in> carrier P"
264   shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p"
265   by (rule up_eqI, simp_all add: R)
267 lemma (in UP_cring) UP_l_neg_ex:
268   assumes R: "p \<in> carrier P"
269   shows "EX q : carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
270 proof -
271   let ?q = "%i. \<ominus> (p i)"
272   from R have closed: "?q \<in> carrier P"
273     by (simp add: UP_def P_def up_a_inv_closed)
274   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
275     by (simp add: UP_def P_def up_a_inv_closed)
276   show ?thesis
277   proof
278     show "?q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
279       by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
280   qed (rule closed)
281 qed
283 lemma (in UP_cring) UP_a_comm:
284   assumes R: "p \<in> carrier P" "q \<in> carrier P"
285   shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p"
286   by (rule up_eqI, simp add: a_comm R, simp_all add: R)
288 ML_setup {*
289   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
290 *}
292 lemma (in UP_cring) UP_m_assoc:
293   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
294   shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
295 proof (rule up_eqI)
296   fix n
297   {
298     fix k and a b c :: "nat=>'a"
299     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
300       "c \<in> UNIV -> carrier R"
301     then have "k <= n ==>
302       (\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
303       (\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
304       (concl is "?eq k")
305     proof (induct k)
306       case 0 then show ?case by (simp add: Pi_def m_assoc)
307     next
308       case (Suc k)
309       then have "k <= n" by arith
310       then have "?eq k" by (rule Suc)
311       with R show ?case
312         by (simp cong: finsum_cong
313              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
314           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
315     qed
316   }
317   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"
318     by (simp add: Pi_def)
319 qed (simp_all add: R)
321 ML_setup {*
322   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
323 *}
325 lemma (in UP_cring) UP_l_one [simp]:
326   assumes R: "p \<in> carrier P"
327   shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
328 proof (rule up_eqI)
329   fix n
330   show "coeff P (\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p) n = coeff P p n"
331   proof (cases n)
332     case 0 with R show ?thesis by simp
333   next
334     case Suc with R show ?thesis
335       by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
336   qed
337 qed (simp_all add: R)
339 lemma (in UP_cring) UP_l_distr:
340   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
341   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)"
342   by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
344 lemma (in UP_cring) UP_m_comm:
345   assumes R: "p \<in> carrier P" "q \<in> carrier P"
346   shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
347 proof (rule up_eqI)
348   fix n
349   {
350     fix k and a b :: "nat=>'a"
351     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
352     then have "k <= n ==>
353       (\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) =
354       (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
355       (concl is "?eq k")
356     proof (induct k)
357       case 0 then show ?case by (simp add: Pi_def)
358     next
359       case (Suc k) then show ?case
360         by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
361     qed
362   }
363   note l = this
364   from R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n =  coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
365     apply (simp add: Pi_def)
366     apply (subst l)
367     apply (auto simp add: Pi_def)
368     apply (simp add: m_comm)
369     done
370 qed (simp_all add: R)
372 (*
373 Strange phenomenon in Isar:
375 theorem (in UP_cring) UP_cring:
376   "cring P"
377 proof (rule cringI)
378   show "abelian_group P" proof (rule abelian_groupI)
379   fix x y z
380   assume "x \<in> carrier P" and "y \<in> carrier P" and "z \<in> carrier P"
381   {
382   show "x \<oplus>\<^bsub>P\<^esub> y \<in> carrier P" sorry
383   next
384   show "x \<oplus>\<^bsub>P\<^esub> y \<oplus>\<^bsub>P\<^esub> z = x \<oplus>\<^bsub>P\<^esub> (y \<oplus>\<^bsub>P\<^esub> z)" sorry
385   next
386   show "x \<oplus>\<^bsub>P\<^esub> y = y \<oplus>\<^bsub>P\<^esub> x" sorry
387   next
388   show "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> x = x" sorry
389   next
390   show "\<exists>y\<in>carrier P. y \<oplus>\<^bsub>P\<^esub> x = \<zero>\<^bsub>P\<^esub>" sorry
391   next
392   show "\<zero>\<^bsub>P\<^esub> \<in> carrier P" sorry  last goal rejected!!!
393 *)
395 theorem (in UP_cring) UP_cring:
396   "cring P"
397   by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
398     UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
400 lemma (in UP_cring) UP_ring:  (* preliminary *)
401   "ring P"
402   by (auto intro: ring.intro cring.axioms UP_cring)
404 lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
405   "p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P"
406   by (rule abelian_group.a_inv_closed
407     [OF ring.is_abelian_group [OF UP_ring]])
409 lemma (in UP_cring) coeff_a_inv [simp]:
410   assumes R: "p \<in> carrier P"
411   shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)"
412 proof -
413   from R coeff_closed UP_a_inv_closed have
414     "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)"
415     by algebra
416   also from R have "... =  \<ominus> (coeff P p n)"
418       abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
419   finally show ?thesis .
420 qed
422 text {*
423   Instantiation of lemmas from @{term cring}.
424 *}
426 (* TODO: this should be automated with an instantiation command. *)
428 lemma (in UP_cring) UP_monoid:
429   "monoid P"
430   by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
431     UP_cring)
432 (* TODO: provide cring.is_monoid *)
434 lemma (in UP_cring) UP_comm_monoid:
435   "comm_monoid P"
436   by (fast intro!: cring.is_comm_monoid UP_cring)
438 lemma (in UP_cring) UP_abelian_monoid:
439   "abelian_monoid P"
440   by (fast intro!: abelian_group.axioms ring.is_abelian_group UP_ring)
442 lemma (in UP_cring) UP_abelian_group:
443   "abelian_group P"
444   by (fast intro!: ring.is_abelian_group UP_ring)
446 lemmas (in UP_cring) UP_r_one [simp] =
447   monoid.r_one [OF UP_monoid]
449 lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
450   monoid.nat_pow_closed [OF UP_monoid]
452 lemmas (in UP_cring) UP_nat_pow_0 [simp] =
453   monoid.nat_pow_0 [OF UP_monoid]
455 lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
456   monoid.nat_pow_Suc [OF UP_monoid]
458 lemmas (in UP_cring) UP_nat_pow_one [simp] =
459   monoid.nat_pow_one [OF UP_monoid]
461 lemmas (in UP_cring) UP_nat_pow_mult =
462   monoid.nat_pow_mult [OF UP_monoid]
464 lemmas (in UP_cring) UP_nat_pow_pow =
465   monoid.nat_pow_pow [OF UP_monoid]
467 lemmas (in UP_cring) UP_m_lcomm =
468   comm_monoid.m_lcomm [OF UP_comm_monoid]
470 lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
472 lemmas (in UP_cring) UP_nat_pow_distr =
473   comm_monoid.nat_pow_distr [OF UP_comm_monoid]
475 lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
477 lemmas (in UP_cring) UP_r_zero [simp] =
478   abelian_monoid.r_zero [OF UP_abelian_monoid]
480 lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
482 lemmas (in UP_cring) UP_finsum_empty [simp] =
483   abelian_monoid.finsum_empty [OF UP_abelian_monoid]
485 lemmas (in UP_cring) UP_finsum_insert [simp] =
486   abelian_monoid.finsum_insert [OF UP_abelian_monoid]
488 lemmas (in UP_cring) UP_finsum_zero [simp] =
489   abelian_monoid.finsum_zero [OF UP_abelian_monoid]
491 lemmas (in UP_cring) UP_finsum_closed [simp] =
492   abelian_monoid.finsum_closed [OF UP_abelian_monoid]
494 lemmas (in UP_cring) UP_finsum_Un_Int =
495   abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
497 lemmas (in UP_cring) UP_finsum_Un_disjoint =
498   abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
500 lemmas (in UP_cring) UP_finsum_addf =
501   abelian_monoid.finsum_addf [OF UP_abelian_monoid]
503 lemmas (in UP_cring) UP_finsum_cong' =
504   abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
506 lemmas (in UP_cring) UP_finsum_0 [simp] =
507   abelian_monoid.finsum_0 [OF UP_abelian_monoid]
509 lemmas (in UP_cring) UP_finsum_Suc [simp] =
510   abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
512 lemmas (in UP_cring) UP_finsum_Suc2 =
513   abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
515 lemmas (in UP_cring) UP_finsum_add [simp] =
516   abelian_monoid.finsum_add [OF UP_abelian_monoid]
518 lemmas (in UP_cring) UP_finsum_cong =
519   abelian_monoid.finsum_cong [OF UP_abelian_monoid]
521 lemmas (in UP_cring) UP_minus_closed [intro, simp] =
522   abelian_group.minus_closed [OF UP_abelian_group]
524 lemmas (in UP_cring) UP_a_l_cancel [simp] =
525   abelian_group.a_l_cancel [OF UP_abelian_group]
527 lemmas (in UP_cring) UP_a_r_cancel [simp] =
528   abelian_group.a_r_cancel [OF UP_abelian_group]
530 lemmas (in UP_cring) UP_l_neg =
531   abelian_group.l_neg [OF UP_abelian_group]
533 lemmas (in UP_cring) UP_r_neg =
534   abelian_group.r_neg [OF UP_abelian_group]
536 lemmas (in UP_cring) UP_minus_zero [simp] =
537   abelian_group.minus_zero [OF UP_abelian_group]
539 lemmas (in UP_cring) UP_minus_minus [simp] =
540   abelian_group.minus_minus [OF UP_abelian_group]
542 lemmas (in UP_cring) UP_minus_add =
543   abelian_group.minus_add [OF UP_abelian_group]
545 lemmas (in UP_cring) UP_r_neg2 =
546   abelian_group.r_neg2 [OF UP_abelian_group]
548 lemmas (in UP_cring) UP_r_neg1 =
549   abelian_group.r_neg1 [OF UP_abelian_group]
551 lemmas (in UP_cring) UP_r_distr =
552   ring.r_distr [OF UP_ring]
554 lemmas (in UP_cring) UP_l_null [simp] =
555   ring.l_null [OF UP_ring]
557 lemmas (in UP_cring) UP_r_null [simp] =
558   ring.r_null [OF UP_ring]
560 lemmas (in UP_cring) UP_l_minus =
561   ring.l_minus [OF UP_ring]
563 lemmas (in UP_cring) UP_r_minus =
564   ring.r_minus [OF UP_ring]
566 lemmas (in UP_cring) UP_finsum_ldistr =
567   cring.finsum_ldistr [OF UP_cring]
569 lemmas (in UP_cring) UP_finsum_rdistr =
570   cring.finsum_rdistr [OF UP_cring]
573 subsection {* Polynomials form an Algebra *}
575 lemma (in UP_cring) UP_smult_l_distr:
576   "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
577   (a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
578   by (rule up_eqI) (simp_all add: R.l_distr)
580 lemma (in UP_cring) UP_smult_r_distr:
581   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
582   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"
583   by (rule up_eqI) (simp_all add: R.r_distr)
585 lemma (in UP_cring) UP_smult_assoc1:
586       "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
587       (a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
588   by (rule up_eqI) (simp_all add: R.m_assoc)
590 lemma (in UP_cring) UP_smult_one [simp]:
591       "p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p"
592   by (rule up_eqI) simp_all
594 lemma (in UP_cring) UP_smult_assoc2:
595   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
596   (a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
597   by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
599 text {*
600   Instantiation of lemmas from @{term algebra}.
601 *}
603 (* TODO: this should be automated with an instantiation command. *)
605 (* TODO: move to CRing.thy, really a fact missing from the locales package *)
606 lemma (in cring) cring:
607   "cring R"
608   by (fast intro: cring.intro prems)
610 lemma (in UP_cring) UP_algebra:
611   "algebra R P"
612   by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr
613     UP_smult_assoc1 UP_smult_assoc2)
615 lemmas (in UP_cring) UP_smult_l_null [simp] =
616   algebra.smult_l_null [OF UP_algebra]
618 lemmas (in UP_cring) UP_smult_r_null [simp] =
619   algebra.smult_r_null [OF UP_algebra]
621 lemmas (in UP_cring) UP_smult_l_minus =
622   algebra.smult_l_minus [OF UP_algebra]
624 lemmas (in UP_cring) UP_smult_r_minus =
625   algebra.smult_r_minus [OF UP_algebra]
627 subsection {* Further lemmas involving monomials *}
629 lemma (in UP_cring) monom_zero [simp]:
630   "monom P \<zero> n = \<zero>\<^bsub>P\<^esub>"
631   by (simp add: UP_def P_def)
633 ML_setup {*
634   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
635 *}
637 lemma (in UP_cring) monom_mult_is_smult:
638   assumes R: "a \<in> carrier R" "p \<in> carrier P"
639   shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
640 proof (rule up_eqI)
641   fix n
642   have "coeff P (p \<otimes>\<^bsub>P\<^esub> monom P a 0) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
643   proof (cases n)
644     case 0 with R show ?thesis by (simp add: R.m_comm)
645   next
646     case Suc with R show ?thesis
647       by (simp cong: finsum_cong add: R.r_null Pi_def)
648         (simp add: m_comm)
649   qed
650   with R show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
651     by (simp add: UP_m_comm)
652 qed (simp_all add: R)
654 ML_setup {*
655   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
656 *}
658 lemma (in UP_cring) monom_add [simp]:
659   "[| a \<in> carrier R; b \<in> carrier R |] ==>
660   monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
661   by (rule up_eqI) simp_all
663 ML_setup {*
664   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
665 *}
667 lemma (in UP_cring) monom_one_Suc:
668   "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
669 proof (rule up_eqI)
670   fix k
671   show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
672   proof (cases "k = Suc n")
673     case True show ?thesis
674     proof -
675       from True have less_add_diff:
676         "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
677       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
678       also from True
679       have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
680         coeff P (monom P \<one> 1) (k - i))"
681         by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
682       also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
683         coeff P (monom P \<one> 1) (k - i))"
684         by (simp only: ivl_disj_un_singleton)
685       also from True
686       have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
687         coeff P (monom P \<one> 1) (k - i))"
688         by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
689           order_less_imp_not_eq Pi_def)
690       also from True have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
691         by (simp add: ivl_disj_un_one)
692       finally show ?thesis .
693     qed
694   next
695     case False
696     note neq = False
697     let ?s =
698       "\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
699     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
700     also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
701     proof -
702       have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
703         by (simp cong: finsum_cong add: Pi_def)
704       from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
705         by (simp cong: finsum_cong add: Pi_def) arith
706       have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
707         by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
708       show ?thesis
709       proof (cases "k < n")
710         case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
711       next
712         case False then have n_le_k: "n <= k" by arith
713         show ?thesis
714         proof (cases "n = k")
715           case True
716           then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
717             by (simp cong: finsum_cong add: finsum_Un_disjoint
718               ivl_disj_int_singleton Pi_def)
719           also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
720             by (simp only: ivl_disj_un_singleton)
721           finally show ?thesis .
722         next
723           case False with n_le_k have n_less_k: "n < k" by arith
724           with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
725             by (simp add: finsum_Un_disjoint f1 f2
726               ivl_disj_int_singleton Pi_def del: Un_insert_right)
727           also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
728             by (simp only: ivl_disj_un_singleton)
729           also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
730             by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
731           also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
732             by (simp only: ivl_disj_un_one)
733           finally show ?thesis .
734         qed
735       qed
736     qed
737     also have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" by simp
738     finally show ?thesis .
739   qed
740 qed (simp_all)
742 ML_setup {*
743   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
744 *}
746 lemma (in UP_cring) monom_mult_smult:
747   "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
748   by (rule up_eqI) simp_all
750 lemma (in UP_cring) monom_one [simp]:
751   "monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
752   by (rule up_eqI) simp_all
754 lemma (in UP_cring) monom_one_mult:
755   "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m"
756 proof (induct n)
757   case 0 show ?case by simp
758 next
759   case Suc then show ?case
760     by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac)
761 qed
763 lemma (in UP_cring) monom_mult [simp]:
764   assumes R: "a \<in> carrier R" "b \<in> carrier R"
765   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
766 proof -
767   from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
768   also from R have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> monom P \<one> (n + m)"
769     by (simp add: monom_mult_smult del: r_one)
770   also have "... = a \<otimes> b \<odot>\<^bsub>P\<^esub> (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m)"
771     by (simp only: monom_one_mult)
772   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))"
773     by (simp add: UP_smult_assoc1)
774   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))"
775     by (simp add: UP_m_comm)
776   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)"
777     by (simp add: UP_smult_assoc2)
778   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))"
779     by (simp add: UP_m_comm)
780   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)"
781     by (simp add: UP_smult_assoc2)
782   also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^bsub>P\<^esub> monom P (b \<otimes> \<one>) m"
783     by (simp add: monom_mult_smult del: r_one)
784   also from R have "... = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m" by simp
785   finally show ?thesis .
786 qed
788 lemma (in UP_cring) monom_a_inv [simp]:
789   "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
790   by (rule up_eqI) simp_all
792 lemma (in UP_cring) monom_inj:
793   "inj_on (%a. monom P a n) (carrier R)"
794 proof (rule inj_onI)
795   fix x y
796   assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
797   then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
798   with R show "x = y" by simp
799 qed
801 subsection {* The degree function *}
803 constdefs (structure R)
804   deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
805   "deg R p == LEAST n. bound \<zero> n (coeff (UP R) p)"
807 lemma (in UP_cring) deg_aboveI:
808   "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
809   by (unfold deg_def P_def) (fast intro: Least_le)
811 (*
812 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
813 proof -
814   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
815   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
816   then show ?thesis ..
817 qed
819 lemma bound_coeff_obtain:
820   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
821 proof -
822   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
823   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
824   with prem show P .
825 qed
826 *)
828 lemma (in UP_cring) deg_aboveD:
829   "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
830 proof -
831   assume R: "p \<in> carrier P" and "deg R p < m"
832   from R obtain n where "bound \<zero> n (coeff P p)"
833     by (auto simp add: UP_def P_def)
834   then have "bound \<zero> (deg R p) (coeff P p)"
835     by (auto simp: deg_def P_def dest: LeastI)
836   then show ?thesis ..
837 qed
839 lemma (in UP_cring) deg_belowI:
840   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
841     and R: "p \<in> carrier P"
842   shows "n <= deg R p"
843 -- {* Logically, this is a slightly stronger version of
844    @{thm [source] deg_aboveD} *}
845 proof (cases "n=0")
846   case True then show ?thesis by simp
847 next
848   case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
849   then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
850   then show ?thesis by arith
851 qed
853 lemma (in UP_cring) lcoeff_nonzero_deg:
854   assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
855   shows "coeff P p (deg R p) ~= \<zero>"
856 proof -
857   from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
858   proof -
859     have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
860       by arith
861 (* TODO: why does simplification below not work with "1" *)
862     from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
863       by (unfold deg_def P_def) arith
864     then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
865     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
866       by (unfold bound_def) fast
867     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
868     then show ?thesis by auto
869   qed
870   with deg_belowI R have "deg R p = m" by fastsimp
871   with m_coeff show ?thesis by simp
872 qed
874 lemma (in UP_cring) lcoeff_nonzero_nonzero:
875   assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
876   shows "coeff P p 0 ~= \<zero>"
877 proof -
878   have "EX m. coeff P p m ~= \<zero>"
879   proof (rule classical)
880     assume "~ ?thesis"
881     with R have "p = \<zero>\<^bsub>P\<^esub>" by (auto intro: up_eqI)
882     with nonzero show ?thesis by contradiction
883   qed
884   then obtain m where coeff: "coeff P p m ~= \<zero>" ..
885   then have "m <= deg R p" by (rule deg_belowI)
886   then have "m = 0" by (simp add: deg)
887   with coeff show ?thesis by simp
888 qed
890 lemma (in UP_cring) lcoeff_nonzero:
891   assumes neq: "p ~= \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
892   shows "coeff P p (deg R p) ~= \<zero>"
893 proof (cases "deg R p = 0")
894   case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
895 next
896   case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
897 qed
899 lemma (in UP_cring) deg_eqI:
900   "[| !!m. n < m ==> coeff P p m = \<zero>;
901       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
902 by (fast intro: le_anti_sym deg_aboveI deg_belowI)
904 (* Degree and polynomial operations *)
906 lemma (in UP_cring) deg_add [simp]:
907   assumes R: "p \<in> carrier P" "q \<in> carrier P"
908   shows "deg R (p \<oplus>\<^bsub>P\<^esub> q) <= max (deg R p) (deg R q)"
909 proof (cases "deg R p <= deg R q")
910   case True show ?thesis
911     by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
912 next
913   case False show ?thesis
914     by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
915 qed
917 lemma (in UP_cring) deg_monom_le:
918   "a \<in> carrier R ==> deg R (monom P a n) <= n"
919   by (intro deg_aboveI) simp_all
921 lemma (in UP_cring) deg_monom [simp]:
922   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
923   by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
925 lemma (in UP_cring) deg_const [simp]:
926   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
927 proof (rule le_anti_sym)
928   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
929 next
930   show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
931 qed
933 lemma (in UP_cring) deg_zero [simp]:
934   "deg R \<zero>\<^bsub>P\<^esub> = 0"
935 proof (rule le_anti_sym)
936   show "deg R \<zero>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
937 next
938   show "0 <= deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
939 qed
941 lemma (in UP_cring) deg_one [simp]:
942   "deg R \<one>\<^bsub>P\<^esub> = 0"
943 proof (rule le_anti_sym)
944   show "deg R \<one>\<^bsub>P\<^esub> <= 0" by (rule deg_aboveI) simp_all
945 next
946   show "0 <= deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
947 qed
949 lemma (in UP_cring) deg_uminus [simp]:
950   assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
951 proof (rule le_anti_sym)
952   show "deg R (\<ominus>\<^bsub>P\<^esub> p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
953 next
954   show "deg R p <= deg R (\<ominus>\<^bsub>P\<^esub> p)"
955     by (simp add: deg_belowI lcoeff_nonzero_deg
956       inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
957 qed
959 lemma (in UP_domain) deg_smult_ring:
960   "[| a \<in> carrier R; p \<in> carrier P |] ==>
961   deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
962   by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
964 lemma (in UP_domain) deg_smult [simp]:
965   assumes R: "a \<in> carrier R" "p \<in> carrier P"
966   shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
967 proof (rule le_anti_sym)
968   show "deg R (a \<odot>\<^bsub>P\<^esub> p) <= (if a = \<zero> then 0 else deg R p)"
969     by (rule deg_smult_ring)
970 next
971   show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^bsub>P\<^esub> p)"
972   proof (cases "a = \<zero>")
973   qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
974 qed
976 lemma (in UP_cring) deg_mult_cring:
977   assumes R: "p \<in> carrier P" "q \<in> carrier P"
978   shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q"
979 proof (rule deg_aboveI)
980   fix m
981   assume boundm: "deg R p + deg R q < m"
982   {
983     fix k i
984     assume boundk: "deg R p + deg R q < k"
985     then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
986     proof (cases "deg R p < i")
987       case True then show ?thesis by (simp add: deg_aboveD R)
988     next
989       case False with boundk have "deg R q < k - i" by arith
990       then show ?thesis by (simp add: deg_aboveD R)
991     qed
992   }
993   with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
994 qed (simp add: R)
996 ML_setup {*
997   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
998 *}
1000 lemma (in UP_domain) deg_mult [simp]:
1001   "[| p ~= \<zero>\<^bsub>P\<^esub>; q ~= \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
1002   deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
1003 proof (rule le_anti_sym)
1004   assume "p \<in> carrier P" " q \<in> carrier P"
1005   show "deg R (p \<otimes>\<^bsub>P\<^esub> q) <= deg R p + deg R q" by (rule deg_mult_cring)
1006 next
1007   let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
1008   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^bsub>P\<^esub>" "q ~= \<zero>\<^bsub>P\<^esub>"
1009   have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
1010   show "deg R p + deg R q <= deg R (p \<otimes>\<^bsub>P\<^esub> q)"
1011   proof (rule deg_belowI, simp add: R)
1012     have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
1013       = (\<Oplus>i \<in> {..< deg R p} \<union> {deg R p .. deg R p + deg R q}. ?s i)"
1014       by (simp only: ivl_disj_un_one)
1015     also have "... = (\<Oplus>i \<in> {deg R p .. deg R p + deg R q}. ?s i)"
1016       by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
1017         deg_aboveD less_add_diff R Pi_def)
1018     also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
1019       by (simp only: ivl_disj_un_singleton)
1020     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
1021       by (simp cong: finsum_cong add: finsum_Un_disjoint
1022         ivl_disj_int_singleton deg_aboveD R Pi_def)
1023     finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
1024       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
1025     with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
1026       by (simp add: integral_iff lcoeff_nonzero R)
1027     qed (simp add: R)
1028   qed
1030 lemma (in UP_cring) coeff_finsum:
1031   assumes fin: "finite A"
1032   shows "p \<in> A -> carrier P ==>
1033     coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
1034   using fin by induct (auto simp: Pi_def)
1036 ML_setup {*
1037   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
1038 *}
1040 lemma (in UP_cring) up_repr:
1041   assumes R: "p \<in> carrier P"
1042   shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
1043 proof (rule up_eqI)
1044   let ?s = "(%i. monom P (coeff P p i) i)"
1045   fix k
1046   from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
1047     by simp
1048   show "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = coeff P p k"
1049   proof (cases "k <= deg R p")
1050     case True
1051     hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
1052           coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k} \<union> {k<..deg R p}. ?s i) k"
1053       by (simp only: ivl_disj_un_one)
1054     also from True
1055     have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k}. ?s i) k"
1056       by (simp cong: finsum_cong add: finsum_Un_disjoint
1057         ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
1058     also
1059     have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
1060       by (simp only: ivl_disj_un_singleton)
1061     also have "... = coeff P p k"
1062       by (simp cong: finsum_cong add: setsum_Un_disjoint
1063         ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
1064     finally show ?thesis .
1065   next
1066     case False
1067     hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
1068           coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
1069       by (simp only: ivl_disj_un_singleton)
1070     also from False have "... = coeff P p k"
1071       by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
1072         coeff_finsum deg_aboveD R Pi_def)
1073     finally show ?thesis .
1074   qed
1075 qed (simp_all add: R Pi_def)
1077 lemma (in UP_cring) up_repr_le:
1078   "[| deg R p <= n; p \<in> carrier P |] ==>
1079   (\<Oplus>\<^bsub>P\<^esub> i \<in> {..n}. monom P (coeff P p i) i) = p"
1080 proof -
1081   let ?s = "(%i. monom P (coeff P p i) i)"
1082   assume R: "p \<in> carrier P" and "deg R p <= n"
1083   then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} \<union> {deg R p<..n})"
1084     by (simp only: ivl_disj_un_one)
1085   also have "... = finsum P ?s {..deg R p}"
1086     by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
1087       deg_aboveD R Pi_def)
1088   also have "... = p" by (rule up_repr)
1089   finally show ?thesis .
1090 qed
1092 ML_setup {*
1093   simpset_ref() := simpset() setsubgoaler asm_simp_tac;
1094 *}
1096 subsection {* Polynomials over an integral domain form an integral domain *}
1098 lemma domainI:
1099   assumes cring: "cring R"
1100     and one_not_zero: "one R ~= zero R"
1101     and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
1102       b \<in> carrier R |] ==> a = zero R | b = zero R"
1103   shows "domain R"
1104   by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
1105     del: disjCI)
1107 lemma (in UP_domain) UP_one_not_zero:
1108   "\<one>\<^bsub>P\<^esub> ~= \<zero>\<^bsub>P\<^esub>"
1109 proof
1110   assume "\<one>\<^bsub>P\<^esub> = \<zero>\<^bsub>P\<^esub>"
1111   hence "coeff P \<one>\<^bsub>P\<^esub> 0 = (coeff P \<zero>\<^bsub>P\<^esub> 0)" by simp
1112   hence "\<one> = \<zero>" by simp
1113   with one_not_zero show "False" by contradiction
1114 qed
1116 lemma (in UP_domain) UP_integral:
1117   "[| 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>"
1118 proof -
1119   fix p q
1120   assume pq: "p \<otimes>\<^bsub>P\<^esub> q = \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P" "q \<in> carrier P"
1121   show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>"
1122   proof (rule classical)
1123     assume c: "~ (p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>)"
1124     with R have "deg R p + deg R q = deg R (p \<otimes>\<^bsub>P\<^esub> q)" by simp
1125     also from pq have "... = 0" by simp
1126     finally have "deg R p + deg R q = 0" .
1127     then have f1: "deg R p = 0 & deg R q = 0" by simp
1128     from f1 R have "p = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P p i) i)"
1129       by (simp only: up_repr_le)
1130     also from R have "... = monom P (coeff P p 0) 0" by simp
1131     finally have p: "p = monom P (coeff P p 0) 0" .
1132     from f1 R have "q = (\<Oplus>\<^bsub>P\<^esub> i \<in> {..0}. monom P (coeff P q i) i)"
1133       by (simp only: up_repr_le)
1134     also from R have "... = monom P (coeff P q 0) 0" by simp
1135     finally have q: "q = monom P (coeff P q 0) 0" .
1136     from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^bsub>P\<^esub> q) 0" by simp
1137     also from pq have "... = \<zero>" by simp
1138     finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
1139     with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
1140       by (simp add: R.integral_iff)
1141     with p q show "p = \<zero>\<^bsub>P\<^esub> | q = \<zero>\<^bsub>P\<^esub>" by fastsimp
1142   qed
1143 qed
1145 theorem (in UP_domain) UP_domain:
1146   "domain P"
1147   by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
1149 text {*
1150   Instantiation of theorems from @{term domain}.
1151 *}
1153 (* TODO: this should be automated with an instantiation command. *)
1155 lemmas (in UP_domain) UP_zero_not_one [simp] =
1156   domain.zero_not_one [OF UP_domain]
1158 lemmas (in UP_domain) UP_integral_iff =
1159   domain.integral_iff [OF UP_domain]
1161 lemmas (in UP_domain) UP_m_lcancel =
1162   domain.m_lcancel [OF UP_domain]
1164 lemmas (in UP_domain) UP_m_rcancel =
1165   domain.m_rcancel [OF UP_domain]
1167 lemma (in UP_domain) smult_integral:
1168   "[| a \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>; a \<in> carrier R; p \<in> carrier P |] ==> a = \<zero> | p = \<zero>\<^bsub>P\<^esub>"
1169   by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
1170     inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
1173 subsection {* Evaluation Homomorphism and Universal Property*}
1175 (* alternative congruence rule (possibly more efficient)
1176 lemma (in abelian_monoid) finsum_cong2:
1177   "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
1178   !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
1179   sorry*)
1181 ML_setup {*
1182   simpset_ref() := simpset() setsubgoaler asm_full_simp_tac;
1183 *}
1185 theorem (in cring) diagonal_sum:
1186   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
1187   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1188   (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1189 proof -
1190   assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
1191   {
1192     fix j
1193     have "j <= n + m ==>
1194       (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1195       (\<Oplus>k \<in> {..j}. \<Oplus>i \<in> {..j - k}. f k \<otimes> g i)"
1196     proof (induct j)
1197       case 0 from Rf Rg show ?case by (simp add: Pi_def)
1198     next
1199       case (Suc j)
1200       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
1201         using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1202       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
1203         using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1204       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
1205         using Suc by (auto intro!: funcset_mem [OF Rf])
1206       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
1207         using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1208       have R11: "g 0 \<in> carrier R"
1209         using Suc by (auto intro!: funcset_mem [OF Rg])
1210       from Suc show ?case
1211         by (simp cong: finsum_cong add: Suc_diff_le a_ac
1212           Pi_def R6 R8 R9 R10 R11)
1213     qed
1214   }
1215   then show ?thesis by fast
1216 qed
1218 lemma (in abelian_monoid) boundD_carrier:
1219   "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
1220   by auto
1222 theorem (in cring) cauchy_product:
1223   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
1224     and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
1225   shows "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1226     (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"       (* State revese direction? *)
1227 proof -
1228   have f: "!!x. f x \<in> carrier R"
1229   proof -
1230     fix x
1231     show "f x \<in> carrier R"
1232       using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
1233   qed
1234   have g: "!!x. g x \<in> carrier R"
1235   proof -
1236     fix x
1237     show "g x \<in> carrier R"
1238       using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
1239   qed
1240   from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1241       (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1242     by (simp add: diagonal_sum Pi_def)
1243   also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1244     by (simp only: ivl_disj_un_one)
1245   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1246     by (simp cong: finsum_cong
1247       add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1248   also from f g
1249   have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m - k}. f k \<otimes> g i)"
1250     by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
1251   also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
1252     by (simp cong: finsum_cong
1253       add: bound.bound [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1254   also from f g have "... = (\<Oplus>i \<in> {..n}. f i) \<otimes> (\<Oplus>i \<in> {..m}. g i)"
1255     by (simp add: finsum_ldistr diagonal_sum Pi_def,
1256       simp cong: finsum_cong add: finsum_rdistr Pi_def)
1257   finally show ?thesis .
1258 qed
1260 lemma (in UP_cring) const_ring_hom:
1261   "(%a. monom P a 0) \<in> ring_hom R P"
1262   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
1264 constdefs (structure S)
1265   eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
1266            'a => 'b, 'b, nat => 'a] => 'b"
1267   "eval R S phi s == \<lambda>p \<in> carrier (UP R).
1268     \<Oplus>i \<in> {..deg R p}. phi (coeff (UP R) p i) \<otimes> s (^) i"
1270 locale UP_univ_prop = ring_hom_cring R S + UP_cring R
1272 lemma (in UP) eval_on_carrier:
1273   includes struct S
1274   shows  "p \<in> carrier P ==>
1275     eval R S phi s p =
1276     (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p}. phi (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1277   by (unfold eval_def, fold P_def) simp
1279 lemma (in UP) eval_extensional:
1280   "eval R S phi s \<in> extensional (carrier P)"
1281   by (unfold eval_def, fold P_def) simp
1283 theorem (in UP_univ_prop) eval_ring_hom:
1284   "s \<in> carrier S ==> eval R S h s \<in> ring_hom P S"
1285 proof (rule ring_hom_memI)
1286   fix p
1287   assume RS: "p \<in> carrier P" "s \<in> carrier S"
1288   then show "eval R S h s p \<in> carrier S"
1289     by (simp only: eval_on_carrier) (simp add: Pi_def)
1290 next
1291   fix p q
1292   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
1293   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"
1294   proof (simp only: eval_on_carrier UP_mult_closed)
1295     from RS have
1296       "(\<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) =
1297       (\<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}.
1298         h (coeff P (p \<otimes>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1299       by (simp cong: finsum_cong
1300         add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1301         del: coeff_mult)
1302     also from RS have "... =
1303       (\<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)"
1304       by (simp only: ivl_disj_un_one deg_mult_cring)
1305     also from RS have "... =
1306       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p + deg R q}.
1307          \<Oplus>\<^bsub>S\<^esub> k \<in> {..i}.
1308            h (coeff P p k) \<otimes>\<^bsub>S\<^esub> h (coeff P q (i - k)) \<otimes>\<^bsub>S\<^esub>
1309            (s (^)\<^bsub>S\<^esub> k \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> (i - k)))"
1310       by (simp cong: finsum_cong add: nat_pow_mult Pi_def
1311         S.m_ac S.finsum_rdistr)
1312     also from RS have "... =
1313       (\<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>
1314       (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1315       by (simp add: S.cauchy_product [THEN sym] bound.intro deg_aboveD S.m_ac
1316         Pi_def)
1317     finally show
1318       "(\<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) =
1319       (\<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>
1320       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
1321   qed
1322 next
1323   fix p q
1324   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
1325   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"
1326   proof (simp only: eval_on_carrier UP_a_closed)
1327     from RS have
1328       "(\<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) =
1329       (\<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)}.
1330         h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1331       by (simp cong: finsum_cong
1332         add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1334     also from RS have "... =
1335         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..max (deg R p) (deg R q)}.
1336           h (coeff P (p \<oplus>\<^bsub>P\<^esub> q) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1337       by (simp add: ivl_disj_un_one)
1338     also from RS have "... =
1339       (\<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>
1340       (\<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)"
1341       by (simp cong: finsum_cong
1342         add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1343     also have "... =
1344         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
1345           h (coeff P p i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) \<oplus>\<^bsub>S\<^esub>
1346         (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
1347           h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1348       by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
1349     also from RS have "... =
1350       (\<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>
1351       (\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1352       by (simp cong: finsum_cong
1353         add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1354     finally show
1355       "(\<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) =
1356       (\<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>
1357       (\<Oplus>\<^bsub>S\<^esub>i \<in> {..deg R q}. h (coeff P q i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)" .
1358   qed
1359 next
1360   assume S: "s \<in> carrier S"
1361   then show "eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
1362     by (simp only: eval_on_carrier UP_one_closed) simp
1363 qed
1365 text {* Instantiation of ring homomorphism lemmas. *}
1367 (* TODO: again, automate with instantiation command *)
1369 lemma (in UP_univ_prop) ring_hom_cring_P_S:
1370   "s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)"
1371   by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
1372     intro: ring_hom_cring_axioms.intro eval_ring_hom)
1374 (*
1375 lemma (in UP_univ_prop) UP_hom_closed [intro, simp]:
1376   "[| s \<in> carrier S; p \<in> carrier P |] ==> eval R S h s p \<in> carrier S"
1377   by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S])
1379 lemma (in UP_univ_prop) UP_hom_mult [simp]:
1380   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
1381   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"
1382   by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S])
1384 lemma (in UP_univ_prop) UP_hom_add [simp]:
1385   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
1386   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"
1387   by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S])
1389 lemma (in UP_univ_prop) UP_hom_one [simp]:
1390   "s \<in> carrier S ==> eval R S h s \<one>\<^bsub>P\<^esub> = \<one>\<^bsub>S\<^esub>"
1391   by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S])
1393 lemma (in UP_univ_prop) UP_hom_zero [simp]:
1394   "s \<in> carrier S ==> eval R S h s \<zero>\<^bsub>P\<^esub> = \<zero>\<^bsub>S\<^esub>"
1395   by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S])
1397 lemma (in UP_univ_prop) UP_hom_a_inv [simp]:
1398   "[| s \<in> carrier S; p \<in> carrier P |] ==>
1399   (eval R S h s) (\<ominus>\<^bsub>P\<^esub> p) = \<ominus>\<^bsub>S\<^esub> (eval R S h s) p"
1400   by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S])
1402 lemma (in UP_univ_prop) UP_hom_finsum [simp]:
1403   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
1404   (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A"
1405   by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S])
1407 lemma (in UP_univ_prop) UP_hom_finprod [simp]:
1408   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
1409   (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A"
1410   by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S])
1411 *)
1413 text {* Further properties of the evaluation homomorphism. *}
1415 (* The following lemma could be proved in UP\_cring with the additional
1416    assumption that h is closed. *)
1418 lemma (in UP_univ_prop) eval_const:
1419   "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
1420   by (simp only: eval_on_carrier monom_closed) simp
1422 text {* The following proof is complicated by the fact that in arbitrary
1423   rings one might have @{term "one R = zero R"}. *}
1425 (* TODO: simplify by cases "one R = zero R" *)
1427 lemma (in UP_univ_prop) eval_monom1:
1428   "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
1429 proof (simp only: eval_on_carrier monom_closed R.one_closed)
1430   assume S: "s \<in> carrier S"
1431   then have
1432     "(\<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) =
1433     (\<Oplus>\<^bsub>S\<^esub> i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
1434       h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1435     by (simp cong: finsum_cong del: coeff_monom
1436       add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1437   also have "... =
1438     (\<Oplus>\<^bsub>S\<^esub> i \<in> {..1}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i)"
1439     by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
1440   also have "... = s"
1441   proof (cases "s = \<zero>\<^bsub>S\<^esub>")
1442     case True then show ?thesis by (simp add: Pi_def)
1443   next
1444     case False with S show ?thesis by (simp add: Pi_def)
1445   qed
1446   finally show "(\<Oplus>\<^bsub>S\<^esub> i \<in> {..deg R (monom P \<one> 1)}.
1447     h (coeff P (monom P \<one> 1) i) \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> i) = s" .
1448 qed
1450 lemma (in UP_cring) monom_pow:
1451   assumes R: "a \<in> carrier R"
1452   shows "(monom P a n) (^)\<^bsub>P\<^esub> m = monom P (a (^) m) (n * m)"
1453 proof (induct m)
1454   case 0 from R show ?case by simp
1455 next
1456   case Suc with R show ?case
1457     by (simp del: monom_mult add: monom_mult [THEN sym] add_commute)
1458 qed
1460 lemma (in ring_hom_cring) hom_pow [simp]:
1461   "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^bsub>S\<^esub> (n::nat)"
1462   by (induct n) simp_all
1464 lemma (in UP_univ_prop) eval_monom:
1465   "[| s \<in> carrier S; r \<in> carrier R |] ==>
1466   eval R S h s (monom P r n) = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
1467 proof -
1468   assume S: "s \<in> carrier S" and R: "r \<in> carrier R"
1469   from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
1470     by - (rule ring_hom_cring.axioms, assumption)+
1471     (* why is simplifier invoked --- in done ??? *)
1472   from R S have "eval R S h s (monom P r n) =
1473     eval R S h s (monom P r 0 \<otimes>\<^bsub>P\<^esub> (monom P \<one> 1) (^)\<^bsub>P\<^esub> n)"
1474     by (simp del: monom_mult (* eval.hom_mult eval.hom_pow, delayed inst! *)
1475       add: monom_mult [THEN sym] monom_pow)
1476   also
1477   from R S eval_monom1 have "... = h r \<otimes>\<^bsub>S\<^esub> s (^)\<^bsub>S\<^esub> n"
1478     by (simp add: eval_const)
1479   finally show ?thesis .
1480 qed
1482 lemma (in UP_univ_prop) eval_smult:
1483   "[| s \<in> carrier S; r \<in> carrier R; p \<in> carrier P |] ==>
1484   eval R S h s (r \<odot>\<^bsub>P\<^esub> p) = h r \<otimes>\<^bsub>S\<^esub> eval R S h s p"
1485 proof -
1486   assume S: "s \<in> carrier S" and R: "r \<in> carrier R" and P: "p \<in> carrier P"
1487   from ring_hom_cring_P_S [OF S] interpret ring_hom_cring [P S "eval R S h s"]
1488     by - (rule ring_hom_cring.axioms, assumption)+
1489   from S R P show ?thesis
1490     by (simp add: monom_mult_is_smult [THEN sym] eval_const)
1491 qed
1493 lemma ring_hom_cringI:
1494   assumes "cring R"
1495     and "cring S"
1496     and "h \<in> ring_hom R S"
1497   shows "ring_hom_cring R S h"
1498   by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
1499     cring.axioms prems)
1501 lemma (in UP_univ_prop) UP_hom_unique:
1502   assumes Phi: "Phi \<in> ring_hom P S" "Phi (monom P \<one> (Suc 0)) = s"
1503       "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
1504     and Psi: "Psi \<in> ring_hom P S" "Psi (monom P \<one> (Suc 0)) = s"
1505       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
1506     and S: "s \<in> carrier S" and P: "p \<in> carrier P"
1507   shows "Phi p = Psi p"
1508 proof -
1509   from UP_cring interpret cring [P] by - (rule cring.axioms, assumption)+
1510   interpret Phi: ring_hom_cring [P S Phi]
1511     by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Phi)
1512   interpret Psi: ring_hom_cring [P S Psi]
1513     by (auto intro: ring_hom_cring.axioms ring_hom_cringI UP_cring S.cring Psi)
1515   have "Phi p =
1516       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)"
1517     by (simp add: up_repr P S monom_mult [THEN sym] monom_pow del: monom_mult)
1518   also
1519   have "... =
1520       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)"
1521     by (simp add: Phi Psi P S Pi_def comp_def)
1522 (* Without interpret, the following command would have been necessary.
1523     by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
1524       ring_hom_cring.hom_mult [OF Phi_hom]
1525       ring_hom_cring.hom_pow [OF Phi_hom] Phi
1526       ring_hom_cring.hom_finsum [OF Psi_hom]
1527       ring_hom_cring.hom_mult [OF Psi_hom]
1528       ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
1529 *)
1530   also have "... = Psi p"
1531     by (simp add: up_repr P S monom_mult [THEN sym] monom_pow del: monom_mult)
1532   finally show ?thesis .
1533 qed
1535 theorem (in UP_univ_prop) UP_universal_property:
1536   "s \<in> carrier S ==>
1537   EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
1538     Phi (monom P \<one> 1) = s &
1539     (ALL r : carrier R. Phi (monom P r 0) = h r)"
1540   using eval_monom1
1541   apply (auto intro: eval_ring_hom eval_const eval_extensional)
1542   apply (rule extensionalityI)
1543   apply (auto intro: UP_hom_unique)
1544   done
1546 subsection {* Sample application of evaluation homomorphism *}
1548 lemma UP_univ_propI:
1549   assumes "cring R"
1550     and "cring S"
1551     and "h \<in> ring_hom R S"
1552   shows "UP_univ_prop R S h"
1553   by (fast intro: UP_univ_prop.intro ring_hom_cring_axioms.intro
1554     cring.axioms prems)
1556 constdefs
1557   INTEG :: "int ring"
1558   "INTEG == (| carrier = UNIV, mult = op *, one = 1, zero = 0, add = op + |)"
1560 lemma INTEG_cring:
1561   "cring INTEG"
1562   by (unfold INTEG_def) (auto intro!: cringI abelian_groupI comm_monoidI
1565 lemma INTEG_id_eval:
1566   "UP_univ_prop INTEG INTEG id"
1567   by (fast intro: UP_univ_propI INTEG_cring id_ring_hom)
1569 text {*
1570   Interpretation allows now to import all theorems and lemmas
1571   valid in the context of homomorphisms between @{term INTEG} and @{term
1572   "UP INTEG"} globally.
1573 *}
1575 interpretation INTEG: UP_univ_prop [INTEG INTEG id]
1576   using INTEG_id_eval
1577   by - (rule UP_univ_prop.axioms, assumption)+
1579 lemma INTEG_closed [intro, simp]:
1580   "z \<in> carrier INTEG"
1581   by (unfold INTEG_def) simp
1583 lemma INTEG_mult [simp]:
1584   "mult INTEG z w = z * w"
1585   by (unfold INTEG_def) simp
1587 lemma INTEG_pow [simp]:
1588   "pow INTEG z n = z ^ n"
1589   by (induct n) (simp_all add: INTEG_def nat_pow_def)
1591 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
1592   by (simp add: INTEG.eval_monom)
1594 end