src/HOL/Algebra/UnivPoly.thy
 author ballarin Wed Apr 30 18:32:06 2003 +0200 (2003-04-30) changeset 13940 c67798653056 child 13949 0ce528cd6f19 permissions -rw-r--r--
HOL-Algebra: New polynomial development added.
1 (*
2   Title:     Univariate Polynomials
3   Id:        \$Id\$
4   Author:    Clemens Ballarin, started 9 December 1996
5   Copyright: Clemens Ballarin
6 *)
8 theory UnivPoly = Module:
10 section {* Univariate Polynomials *}
12 subsection
13   {* Definition of the Constructor for Univariate Polynomials @{term UP} *}
15 (* Could alternatively use locale ...
16 locale bound = cring + var bound +
17   defines ...
18 *)
20 constdefs
21   bound  :: "['a, nat, nat => 'a] => bool"
22   "bound z n f == (ALL i. n < i --> f i = z)"
24 lemma boundI [intro!]:
25   "[| !! m. n < m ==> f m = z |] ==> bound z n f"
26   by (unfold bound_def) fast
28 lemma boundE [elim?]:
29   "[| bound z n f; (!! m. n < m ==> f m = z) ==> P |] ==> P"
30   by (unfold bound_def) fast
32 lemma boundD [dest]:
33   "[| bound z n f; n < m |] ==> f m = z"
34   by (unfold bound_def) fast
36 lemma bound_below:
37   assumes bound: "bound z m f" and nonzero: "f n ~= z" shows "n <= m"
38 proof (rule classical)
39   assume "~ ?thesis"
40   then have "m < n" by arith
41   with bound have "f n = z" ..
42   with nonzero show ?thesis by contradiction
43 qed
45 record ('a, 'p) up_ring = "('a, 'p) module" +
46   monom :: "['a, nat] => 'p"
47   coeff :: "['p, nat] => 'a"
49 constdefs
50   up :: "('a, 'm) ring_scheme => (nat => 'a) set"
51   "up R == {f. f \<in> UNIV -> carrier R & (EX n. bound (zero R) n f)}"
52   UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
53   "UP R == (|
54     carrier = up R,
55     mult = (%p:up R. %q:up R. %n. finsum R (%i. mult R (p i) (q (n-i))) {..n}),
56     one = (%i. if i=0 then one R else zero R),
57     zero = (%i. zero R),
58     add = (%p:up R. %q:up R. %i. add R (p i) (q i)),
59     smult = (%a:carrier R. %p:up R. %i. mult R a (p i)),
60     monom = (%a:carrier R. %n i. if i=n then a else zero R),
61     coeff = (%p:up R. %n. p n) |)"
63 text {*
64   Properties of the set of polynomials @{term up}.
65 *}
67 lemma mem_upI [intro]:
68   "[| !!n. f n \<in> carrier R; EX n. bound (zero R) n f |] ==> f \<in> up R"
69   by (simp add: up_def Pi_def)
71 lemma mem_upD [dest]:
72   "f \<in> up R ==> f n \<in> carrier R"
73   by (simp add: up_def Pi_def)
75 lemma (in cring) bound_upD [dest]:
76   "f \<in> up R ==> EX n. bound \<zero> n f"
77   by (simp add: up_def)
79 lemma (in cring) up_one_closed:
80    "(%n. if n = 0 then \<one> else \<zero>) \<in> up R"
81   using up_def by force
83 lemma (in cring) up_smult_closed:
84   "[| a \<in> carrier R; p \<in> up R |] ==> (%i. a \<otimes> p i) \<in> up R"
85   by force
87 lemma (in cring) up_add_closed:
88   "[| p \<in> up R; q \<in> up R |] ==> (%i. p i \<oplus> q i) \<in> up R"
89 proof
90   fix n
91   assume "p \<in> up R" and "q \<in> up R"
92   then show "p n \<oplus> q n \<in> carrier R"
93     by auto
94 next
95   assume UP: "p \<in> up R" "q \<in> up R"
96   show "EX n. bound \<zero> n (%i. p i \<oplus> q i)"
97   proof -
98     from UP obtain n where boundn: "bound \<zero> n p" by fast
99     from UP obtain m where boundm: "bound \<zero> m q" by fast
100     have "bound \<zero> (max n m) (%i. p i \<oplus> q i)"
101     proof
102       fix i
103       assume "max n m < i"
104       with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastsimp
105     qed
106     then show ?thesis ..
107   qed
108 qed
110 lemma (in cring) up_a_inv_closed:
111   "p \<in> up R ==> (%i. \<ominus> (p i)) \<in> up R"
112 proof
113   assume R: "p \<in> up R"
114   then obtain n where "bound \<zero> n p" by auto
115   then have "bound \<zero> n (%i. \<ominus> p i)" by auto
116   then show "EX n. bound \<zero> n (%i. \<ominus> p i)" by auto
117 qed auto
119 lemma (in cring) up_mult_closed:
120   "[| p \<in> up R; q \<in> up R |] ==>
121   (%n. finsum R (%i. p i \<otimes> q (n-i)) {..n}) \<in> up R"
122 proof
123   fix n
124   assume "p \<in> up R" "q \<in> up R"
125   then show "finsum R (%i. p i \<otimes> q (n-i)) {..n} \<in> carrier R"
126     by (simp add: mem_upD  funcsetI)
127 next
128   assume UP: "p \<in> up R" "q \<in> up R"
129   show "EX n. bound \<zero> n (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
130   proof -
131     from UP obtain n where boundn: "bound \<zero> n p" by fast
132     from UP obtain m where boundm: "bound \<zero> m q" by fast
133     have "bound \<zero> (n + m) (%n. finsum R (%i. p i \<otimes> q (n - i)) {..n})"
134     proof
135       fix k
136       assume bound: "n + m < k"
137       {
138 	fix i
139 	have "p i \<otimes> q (k-i) = \<zero>"
140 	proof (cases "n < i")
141 	  case True
142 	  with boundn have "p i = \<zero>" by auto
143           moreover from UP have "q (k-i) \<in> carrier R" by auto
144 	  ultimately show ?thesis by simp
145 	next
146 	  case False
147 	  with bound have "m < k-i" by arith
148 	  with boundm have "q (k-i) = \<zero>" by auto
149 	  moreover from UP have "p i \<in> carrier R" by auto
150 	  ultimately show ?thesis by simp
151 	qed
152       }
153       then show "finsum R (%i. p i \<otimes> q (k-i)) {..k} = \<zero>"
154 	by (simp add: Pi_def)
155     qed
156     then show ?thesis by fast
157   qed
158 qed
160 subsection {* Effect of operations on coefficients *}
162 locale UP = struct R + struct P +
163   defines P_def: "P == UP R"
165 locale UP_cring = UP + cring R
167 locale UP_domain = UP_cring + "domain" R
169 text {*
170   Temporarily declare UP.P\_def as simp rule.
171 *}
172 (* TODO: use antiquotation once text (in locale) is supported. *)
174 declare (in UP) P_def [simp]
176 lemma (in UP_cring) coeff_monom [simp]:
177   "a \<in> carrier R ==>
178   coeff P (monom P a m) n = (if m=n then a else \<zero>)"
179 proof -
180   assume R: "a \<in> carrier R"
181   then have "(%n. if n = m then a else \<zero>) \<in> up R"
182     using up_def by force
183   with R show ?thesis by (simp add: UP_def)
184 qed
186 lemma (in UP_cring) coeff_zero [simp]:
187   "coeff P \<zero>\<^sub>2 n = \<zero>"
188   by (auto simp add: UP_def)
190 lemma (in UP_cring) coeff_one [simp]:
191   "coeff P \<one>\<^sub>2 n = (if n=0 then \<one> else \<zero>)"
192   using up_one_closed by (simp add: UP_def)
194 lemma (in UP_cring) coeff_smult [simp]:
195   "[| a \<in> carrier R; p \<in> carrier P |] ==>
196   coeff P (a \<odot>\<^sub>2 p) n = a \<otimes> coeff P p n"
197   by (simp add: UP_def up_smult_closed)
199 lemma (in UP_cring) coeff_add [simp]:
200   "[| p \<in> carrier P; q \<in> carrier P |] ==>
201   coeff P (p \<oplus>\<^sub>2 q) n = coeff P p n \<oplus> coeff P q n"
204 lemma (in UP_cring) coeff_mult [simp]:
205   "[| p \<in> carrier P; q \<in> carrier P |] ==>
206   coeff P (p \<otimes>\<^sub>2 q) n = finsum R (%i. coeff P p i \<otimes> coeff P q (n-i)) {..n}"
207   by (simp add: UP_def up_mult_closed)
209 lemma (in UP) up_eqI:
210   assumes prem: "!!n. coeff P p n = coeff P q n"
211     and R: "p \<in> carrier P" "q \<in> carrier P"
212   shows "p = q"
213 proof
214   fix x
215   from prem and R show "p x = q x" by (simp add: UP_def)
216 qed
218 subsection {* Polynomials form a commutative ring. *}
220 text {* Operations are closed over @{term "P"}. *}
222 lemma (in UP_cring) UP_mult_closed [simp]:
223   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^sub>2 q \<in> carrier P"
224   by (simp add: UP_def up_mult_closed)
226 lemma (in UP_cring) UP_one_closed [simp]:
227   "\<one>\<^sub>2 \<in> carrier P"
228   by (simp add: UP_def up_one_closed)
230 lemma (in UP_cring) UP_zero_closed [intro, simp]:
231   "\<zero>\<^sub>2 \<in> carrier P"
232   by (auto simp add: UP_def)
234 lemma (in UP_cring) UP_a_closed [intro, simp]:
235   "[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^sub>2 q \<in> carrier P"
238 lemma (in UP_cring) monom_closed [simp]:
239   "a \<in> carrier R ==> monom P a n \<in> carrier P"
240   by (auto simp add: UP_def up_def Pi_def)
242 lemma (in UP_cring) UP_smult_closed [simp]:
243   "[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^sub>2 p \<in> carrier P"
244   by (simp add: UP_def up_smult_closed)
246 lemma (in UP) coeff_closed [simp]:
247   "p \<in> carrier P ==> coeff P p n \<in> carrier R"
248   by (auto simp add: UP_def)
250 declare (in UP) P_def [simp del]
252 text {* Algebraic ring properties *}
254 lemma (in UP_cring) UP_a_assoc:
255   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
256   shows "(p \<oplus>\<^sub>2 q) \<oplus>\<^sub>2 r = p \<oplus>\<^sub>2 (q \<oplus>\<^sub>2 r)"
257   by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
259 lemma (in UP_cring) UP_l_zero [simp]:
260   assumes R: "p \<in> carrier P"
261   shows "\<zero>\<^sub>2 \<oplus>\<^sub>2 p = p"
262   by (rule up_eqI, simp_all add: R)
264 lemma (in UP_cring) UP_l_neg_ex:
265   assumes R: "p \<in> carrier P"
266   shows "EX q : carrier P. q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
267 proof -
268   let ?q = "%i. \<ominus> (p i)"
269   from R have closed: "?q \<in> carrier P"
270     by (simp add: UP_def P_def up_a_inv_closed)
271   from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
272     by (simp add: UP_def P_def up_a_inv_closed)
273   show ?thesis
274   proof
275     show "?q \<oplus>\<^sub>2 p = \<zero>\<^sub>2"
276       by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
277   qed (rule closed)
278 qed
280 lemma (in UP_cring) UP_a_comm:
281   assumes R: "p \<in> carrier P" "q \<in> carrier P"
282   shows "p \<oplus>\<^sub>2 q = q \<oplus>\<^sub>2 p"
283   by (rule up_eqI, simp add: a_comm R, simp_all add: R)
285 ML_setup {*
286 Context.>> (fn thy => (simpset_ref_of thy :=
287   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
289 lemma (in UP_cring) UP_m_assoc:
290   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
291   shows "(p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r = p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)"
292 proof (rule up_eqI)
293   fix n
294   {
295     fix k and a b c :: "nat=>'a"
296     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
297       "c \<in> UNIV -> carrier R"
298     then have "k <= n ==>
299       finsum R (%j. finsum R (%i. a i \<otimes> b (j-i)) {..j} \<otimes> c (n-j)) {..k} =
300       finsum R (%j. a j \<otimes> finsum R (%i. b i \<otimes> c (n-j-i)) {..k-j}) {..k}"
301       (is "_ ==> ?eq k")
302     proof (induct k)
303       case 0 then show ?case by (simp add: Pi_def m_assoc)
304     next
305       case (Suc k)
306       then have "k <= n" by arith
307       then have "?eq k" by (rule Suc)
308       with R show ?case
309 	by (simp cong: finsum_cong
310              add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
311           (simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
312     qed
313   }
314   with R show "coeff P ((p \<otimes>\<^sub>2 q) \<otimes>\<^sub>2 r) n = coeff P (p \<otimes>\<^sub>2 (q \<otimes>\<^sub>2 r)) n"
315     by (simp add: Pi_def)
316 qed (simp_all add: R)
318 ML_setup {*
319 Context.>> (fn thy => (simpset_ref_of thy :=
320   simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
322 lemma (in UP_cring) UP_l_one [simp]:
323   assumes R: "p \<in> carrier P"
324   shows "\<one>\<^sub>2 \<otimes>\<^sub>2 p = p"
325 proof (rule up_eqI)
326   fix n
327   show "coeff P (\<one>\<^sub>2 \<otimes>\<^sub>2 p) n = coeff P p n"
328   proof (cases n)
329     case 0 with R show ?thesis by simp
330   next
331     case Suc with R show ?thesis
332       by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
333   qed
334 qed (simp_all add: R)
336 lemma (in UP_cring) UP_l_distr:
337   assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
338   shows "(p \<oplus>\<^sub>2 q) \<otimes>\<^sub>2 r = (p \<otimes>\<^sub>2 r) \<oplus>\<^sub>2 (q \<otimes>\<^sub>2 r)"
339   by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
341 lemma (in UP_cring) UP_m_comm:
342   assumes R: "p \<in> carrier P" "q \<in> carrier P"
343   shows "p \<otimes>\<^sub>2 q = q \<otimes>\<^sub>2 p"
344 proof (rule up_eqI)
345   fix n
346   {
347     fix k and a b :: "nat=>'a"
348     assume R: "a \<in> UNIV -> carrier R" "b \<in> UNIV -> carrier R"
349     then have "k <= n ==>
350       finsum R (%i. a i \<otimes> b (n-i)) {..k} =
351       finsum R (%i. a (k-i) \<otimes> b (i+n-k)) {..k}"
352       (is "_ ==> ?eq k")
353     proof (induct k)
354       case 0 then show ?case by (simp add: Pi_def)
355     next
356       case (Suc k) then show ?case
357 	by (subst finsum_Suc2) (simp add: Pi_def a_comm)+
358     qed
359   }
360   note l = this
361   from R show "coeff P (p \<otimes>\<^sub>2 q) n =  coeff P (q \<otimes>\<^sub>2 p) n"
362     apply (simp add: Pi_def)
363     apply (subst l)
364     apply (auto simp add: Pi_def)
365     apply (simp add: m_comm)
366     done
367 qed (simp_all add: R)
369 theorem (in UP_cring) UP_cring:
370   "cring P"
371   by (auto intro!: cringI abelian_groupI comm_monoidI UP_a_assoc UP_l_zero
372     UP_l_neg_ex UP_a_comm UP_m_assoc UP_l_one UP_m_comm UP_l_distr)
374 lemma (in UP_cring) UP_a_inv_closed [intro, simp]:
375   "p \<in> carrier P ==> \<ominus>\<^sub>2 p \<in> carrier P"
376   by (rule abelian_group.a_inv_closed
377     [OF cring.is_abelian_group [OF UP_cring]])
379 lemma (in UP_cring) coeff_a_inv [simp]:
380   assumes R: "p \<in> carrier P"
381   shows "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> (coeff P p n)"
382 proof -
383   from R coeff_closed UP_a_inv_closed have
384     "coeff P (\<ominus>\<^sub>2 p) n = \<ominus> coeff P p n \<oplus> (coeff P p n \<oplus> coeff P (\<ominus>\<^sub>2 p) n)"
385     by algebra
386   also from R have "... =  \<ominus> (coeff P p n)"
388       abelian_group.r_neg [OF cring.is_abelian_group [OF UP_cring]])
389   finally show ?thesis .
390 qed
392 text {*
393   Instantiation of lemmas from @{term cring}.
394 *}
396 lemma (in UP_cring) UP_monoid:
397   "monoid P"
398   by (fast intro!: cring.is_comm_monoid comm_monoid.axioms monoid.intro
399     UP_cring)
400 (* TODO: provide cring.is_monoid *)
402 lemma (in UP_cring) UP_comm_semigroup:
403   "comm_semigroup P"
404   by (fast intro!: cring.is_comm_monoid comm_monoid.axioms comm_semigroup.intro
405     UP_cring)
407 lemma (in UP_cring) UP_comm_monoid:
408   "comm_monoid P"
409   by (fast intro!: cring.is_comm_monoid UP_cring)
411 lemma (in UP_cring) UP_abelian_monoid:
412   "abelian_monoid P"
413   by (fast intro!: abelian_group.axioms cring.is_abelian_group UP_cring)
415 lemma (in UP_cring) UP_abelian_group:
416   "abelian_group P"
417   by (fast intro!: cring.is_abelian_group UP_cring)
419 lemmas (in UP_cring) UP_r_one [simp] =
420   monoid.r_one [OF UP_monoid]
422 lemmas (in UP_cring) UP_nat_pow_closed [intro, simp] =
423   monoid.nat_pow_closed [OF UP_monoid]
425 lemmas (in UP_cring) UP_nat_pow_0 [simp] =
426   monoid.nat_pow_0 [OF UP_monoid]
428 lemmas (in UP_cring) UP_nat_pow_Suc [simp] =
429   monoid.nat_pow_Suc [OF UP_monoid]
431 lemmas (in UP_cring) UP_nat_pow_one [simp] =
432   monoid.nat_pow_one [OF UP_monoid]
434 lemmas (in UP_cring) UP_nat_pow_mult =
435   monoid.nat_pow_mult [OF UP_monoid]
437 lemmas (in UP_cring) UP_nat_pow_pow =
438   monoid.nat_pow_pow [OF UP_monoid]
440 lemmas (in UP_cring) UP_m_lcomm =
441   comm_semigroup.m_lcomm [OF UP_comm_semigroup]
443 lemmas (in UP_cring) UP_m_ac = UP_m_assoc UP_m_comm UP_m_lcomm
445 lemmas (in UP_cring) UP_nat_pow_distr =
446   comm_monoid.nat_pow_distr [OF UP_comm_monoid]
448 lemmas (in UP_cring) UP_a_lcomm = abelian_monoid.a_lcomm [OF UP_abelian_monoid]
450 lemmas (in UP_cring) UP_r_zero [simp] =
451   abelian_monoid.r_zero [OF UP_abelian_monoid]
453 lemmas (in UP_cring) UP_a_ac = UP_a_assoc UP_a_comm UP_a_lcomm
455 lemmas (in UP_cring) UP_finsum_empty [simp] =
456   abelian_monoid.finsum_empty [OF UP_abelian_monoid]
458 lemmas (in UP_cring) UP_finsum_insert [simp] =
459   abelian_monoid.finsum_insert [OF UP_abelian_monoid]
461 lemmas (in UP_cring) UP_finsum_zero [simp] =
462   abelian_monoid.finsum_zero [OF UP_abelian_monoid]
464 lemmas (in UP_cring) UP_finsum_closed [simp] =
465   abelian_monoid.finsum_closed [OF UP_abelian_monoid]
467 lemmas (in UP_cring) UP_finsum_Un_Int =
468   abelian_monoid.finsum_Un_Int [OF UP_abelian_monoid]
470 lemmas (in UP_cring) UP_finsum_Un_disjoint =
471   abelian_monoid.finsum_Un_disjoint [OF UP_abelian_monoid]
473 lemmas (in UP_cring) UP_finsum_addf =
474   abelian_monoid.finsum_addf [OF UP_abelian_monoid]
476 lemmas (in UP_cring) UP_finsum_cong' =
477   abelian_monoid.finsum_cong' [OF UP_abelian_monoid]
479 lemmas (in UP_cring) UP_finsum_0 [simp] =
480   abelian_monoid.finsum_0 [OF UP_abelian_monoid]
482 lemmas (in UP_cring) UP_finsum_Suc [simp] =
483   abelian_monoid.finsum_Suc [OF UP_abelian_monoid]
485 lemmas (in UP_cring) UP_finsum_Suc2 =
486   abelian_monoid.finsum_Suc2 [OF UP_abelian_monoid]
488 lemmas (in UP_cring) UP_finsum_add [simp] =
489   abelian_monoid.finsum_add [OF UP_abelian_monoid]
491 lemmas (in UP_cring) UP_finsum_cong =
492   abelian_monoid.finsum_cong [OF UP_abelian_monoid]
494 lemmas (in UP_cring) UP_minus_closed [intro, simp] =
495   abelian_group.minus_closed [OF UP_abelian_group]
497 lemmas (in UP_cring) UP_a_l_cancel [simp] =
498   abelian_group.a_l_cancel [OF UP_abelian_group]
500 lemmas (in UP_cring) UP_a_r_cancel [simp] =
501   abelian_group.a_r_cancel [OF UP_abelian_group]
503 lemmas (in UP_cring) UP_l_neg =
504   abelian_group.l_neg [OF UP_abelian_group]
506 lemmas (in UP_cring) UP_r_neg =
507   abelian_group.r_neg [OF UP_abelian_group]
509 lemmas (in UP_cring) UP_minus_zero [simp] =
510   abelian_group.minus_zero [OF UP_abelian_group]
512 lemmas (in UP_cring) UP_minus_minus [simp] =
513   abelian_group.minus_minus [OF UP_abelian_group]
515 lemmas (in UP_cring) UP_minus_add =
516   abelian_group.minus_add [OF UP_abelian_group]
518 lemmas (in UP_cring) UP_r_neg2 =
519   abelian_group.r_neg2 [OF UP_abelian_group]
521 lemmas (in UP_cring) UP_r_neg1 =
522   abelian_group.r_neg1 [OF UP_abelian_group]
524 lemmas (in UP_cring) UP_r_distr =
525   cring.r_distr [OF UP_cring]
527 lemmas (in UP_cring) UP_l_null [simp] =
528   cring.l_null [OF UP_cring]
530 lemmas (in UP_cring) UP_r_null [simp] =
531   cring.r_null [OF UP_cring]
533 lemmas (in UP_cring) UP_l_minus =
534   cring.l_minus [OF UP_cring]
536 lemmas (in UP_cring) UP_r_minus =
537   cring.r_minus [OF UP_cring]
539 lemmas (in UP_cring) UP_finsum_ldistr =
540   cring.finsum_ldistr [OF UP_cring]
542 lemmas (in UP_cring) UP_finsum_rdistr =
543   cring.finsum_rdistr [OF UP_cring]
545 subsection {* Polynomials form an Algebra *}
547 lemma (in UP_cring) UP_smult_l_distr:
548   "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
549   (a \<oplus> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 b \<odot>\<^sub>2 p"
550   by (rule up_eqI) (simp_all add: R.l_distr)
552 lemma (in UP_cring) UP_smult_r_distr:
553   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
554   a \<odot>\<^sub>2 (p \<oplus>\<^sub>2 q) = a \<odot>\<^sub>2 p \<oplus>\<^sub>2 a \<odot>\<^sub>2 q"
555   by (rule up_eqI) (simp_all add: R.r_distr)
557 lemma (in UP_cring) UP_smult_assoc1:
558       "[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
559       (a \<otimes> b) \<odot>\<^sub>2 p = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 p)"
560   by (rule up_eqI) (simp_all add: R.m_assoc)
562 lemma (in UP_cring) UP_smult_one [simp]:
563       "p \<in> carrier P ==> \<one> \<odot>\<^sub>2 p = p"
564   by (rule up_eqI) simp_all
566 lemma (in UP_cring) UP_smult_assoc2:
567   "[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
568   (a \<odot>\<^sub>2 p) \<otimes>\<^sub>2 q = a \<odot>\<^sub>2 (p \<otimes>\<^sub>2 q)"
569   by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
571 text {*
572   Instantiation of lemmas from @{term algebra}.
573 *}
575 (* TODO: move to CRing.thy, really a fact missing from the locales package *)
577 lemma (in cring) cring:
578   "cring R"
579   by (fast intro: cring.intro prems)
581 lemma (in UP_cring) UP_algebra:
582   "algebra R P"
583   by (auto intro: algebraI cring UP_cring UP_smult_l_distr UP_smult_r_distr
584     UP_smult_assoc1 UP_smult_assoc2)
586 lemmas (in UP_cring) UP_smult_l_null [simp] =
587   algebra.smult_l_null [OF UP_algebra]
589 lemmas (in UP_cring) UP_smult_r_null [simp] =
590   algebra.smult_r_null [OF UP_algebra]
592 lemmas (in UP_cring) UP_smult_l_minus =
593   algebra.smult_l_minus [OF UP_algebra]
595 lemmas (in UP_cring) UP_smult_r_minus =
596   algebra.smult_r_minus [OF UP_algebra]
598 subsection {* Further Lemmas Involving @{term monom} *}
600 lemma (in UP_cring) monom_zero [simp]:
601   "monom P \<zero> n = \<zero>\<^sub>2"
602   by (simp add: UP_def P_def)
604 ML_setup {*
605 Context.>> (fn thy => (simpset_ref_of thy :=
606   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
608 lemma (in UP_cring) monom_mult_is_smult:
609   assumes R: "a \<in> carrier R" "p \<in> carrier P"
610   shows "monom P a 0 \<otimes>\<^sub>2 p = a \<odot>\<^sub>2 p"
611 proof (rule up_eqI)
612   fix n
613   have "coeff P (p \<otimes>\<^sub>2 monom P a 0) n = coeff P (a \<odot>\<^sub>2 p) n"
614   proof (cases n)
615     case 0 with R show ?thesis by (simp add: R.m_comm)
616   next
617     case Suc with R show ?thesis
618       by (simp cong: finsum_cong add: R.r_null Pi_def)
619         (simp add: m_comm)
620   qed
621   with R show "coeff P (monom P a 0 \<otimes>\<^sub>2 p) n = coeff P (a \<odot>\<^sub>2 p) n"
622     by (simp add: UP_m_comm)
623 qed (simp_all add: R)
625 ML_setup {*
626 Context.>> (fn thy => (simpset_ref_of thy :=
627   simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
629 lemma (in UP_cring) monom_add [simp]:
630   "[| a \<in> carrier R; b \<in> carrier R |] ==>
631   monom P (a \<oplus> b) n = monom P a n \<oplus>\<^sub>2 monom P b n"
632   by (rule up_eqI) simp_all
634 ML_setup {*
635 Context.>> (fn thy => (simpset_ref_of thy :=
636   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
638 lemma (in UP_cring) monom_one_Suc:
639   "monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1"
640 proof (rule up_eqI)
641   fix k
642   show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
643   proof (cases "k = Suc n")
644     case True show ?thesis
645     proof -
646       from True have less_add_diff:
647 	"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
648       from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
649       also from True
650       have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
651 	coeff P (monom P \<one> 1) (k - i)) ({..n(} Un {n})"
652 	by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
653       also have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
654 	coeff P (monom P \<one> 1) (k - i)) {..n}"
655 	by (simp only: ivl_disj_un_singleton)
656       also from True have "... = finsum R (%i. coeff P (monom P \<one> n) i \<otimes>
657 	coeff P (monom P \<one> 1) (k - i)) ({..n} Un {)n..k})"
658 	by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
659 	  order_less_imp_not_eq Pi_def)
660       also from True have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k"
661 	by (simp add: ivl_disj_un_one)
662       finally show ?thesis .
663     qed
664   next
665     case False
666     note neq = False
667     let ?s =
668       "(\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>))"
669     from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
670     also have "... = finsum R ?s {..k}"
671     proof -
672       have f1: "finsum R ?s {..n(} = \<zero>" by (simp cong: finsum_cong add: Pi_def)
673       from neq have f2: "finsum R ?s {n} = \<zero>"
674 	by (simp cong: finsum_cong add: Pi_def) arith
675       have f3: "n < k ==> finsum R ?s {)n..k} = \<zero>"
676 	by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
677       show ?thesis
678       proof (cases "k < n")
679 	case True then show ?thesis by (simp cong: finsum_cong add: Pi_def)
680       next
681 	case False then have n_le_k: "n <= k" by arith
682 	show ?thesis
683 	proof (cases "n = k")
684 	  case True
685 	  then have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
686 	    by (simp cong: finsum_cong add: finsum_Un_disjoint
687 	      ivl_disj_int_singleton Pi_def)
688 	  also from True have "... = finsum R ?s {..k}"
689 	    by (simp only: ivl_disj_un_singleton)
690 	  finally show ?thesis .
691 	next
692 	  case False with n_le_k have n_less_k: "n < k" by arith
693 	  with neq have "\<zero> = finsum R ?s ({..n(} \<union> {n})"
694 	    by (simp add: finsum_Un_disjoint f1 f2
695 	      ivl_disj_int_singleton Pi_def del: Un_insert_right)
696 	  also have "... = finsum R ?s {..n}"
697 	    by (simp only: ivl_disj_un_singleton)
698 	  also from n_less_k neq have "... = finsum R ?s ({..n} \<union> {)n..k})"
699 	    by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
700 	  also from n_less_k have "... = finsum R ?s {..k}"
701 	    by (simp only: ivl_disj_un_one)
702 	  finally show ?thesis .
703 	qed
704       qed
705     qed
706     also have "... = coeff P (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> 1) k" by simp
707     finally show ?thesis .
708   qed
709 qed (simp_all)
711 ML_setup {*
712 Context.>> (fn thy => (simpset_ref_of thy :=
713   simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
715 lemma (in UP_cring) monom_mult_smult:
716   "[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^sub>2 monom P b n"
717   by (rule up_eqI) simp_all
719 lemma (in UP_cring) monom_one [simp]:
720   "monom P \<one> 0 = \<one>\<^sub>2"
721   by (rule up_eqI) simp_all
723 lemma (in UP_cring) monom_one_mult:
724   "monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m"
725 proof (induct n)
726   case 0 show ?case by simp
727 next
728   case Suc then show ?case
729     by (simp only: add_Suc monom_one_Suc) (simp add: UP_m_ac)
730 qed
732 lemma (in UP_cring) monom_mult [simp]:
733   assumes R: "a \<in> carrier R" "b \<in> carrier R"
734   shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^sub>2 monom P b m"
735 proof -
736   from R have "monom P (a \<otimes> b) (n + m) = monom P (a \<otimes> b \<otimes> \<one>) (n + m)" by simp
737   also from R have "... = a \<otimes> b \<odot>\<^sub>2 monom P \<one> (n + m)"
738     by (simp add: monom_mult_smult del: r_one)
739   also have "... = a \<otimes> b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m)"
740     by (simp only: monom_one_mult)
741   also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 monom P \<one> m))"
742     by (simp add: UP_smult_assoc1)
743   also from R have "... = a \<odot>\<^sub>2 (b \<odot>\<^sub>2 (monom P \<one> m \<otimes>\<^sub>2 monom P \<one> n))"
744     by (simp add: UP_m_comm)
745   also from R have "... = a \<odot>\<^sub>2 ((b \<odot>\<^sub>2 monom P \<one> m) \<otimes>\<^sub>2 monom P \<one> n)"
746     by (simp add: UP_smult_assoc2)
747   also from R have "... = a \<odot>\<^sub>2 (monom P \<one> n \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m))"
748     by (simp add: UP_m_comm)
749   also from R have "... = (a \<odot>\<^sub>2 monom P \<one> n) \<otimes>\<^sub>2 (b \<odot>\<^sub>2 monom P \<one> m)"
750     by (simp add: UP_smult_assoc2)
751   also from R have "... = monom P (a \<otimes> \<one>) n \<otimes>\<^sub>2 monom P (b \<otimes> \<one>) m"
752     by (simp add: monom_mult_smult del: r_one)
753   also from R have "... = monom P a n \<otimes>\<^sub>2 monom P b m" by simp
754   finally show ?thesis .
755 qed
757 lemma (in UP_cring) monom_a_inv [simp]:
758   "a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^sub>2 monom P a n"
759   by (rule up_eqI) simp_all
761 lemma (in UP_cring) monom_inj:
762   "inj_on (%a. monom P a n) (carrier R)"
763 proof (rule inj_onI)
764   fix x y
765   assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
766   then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
767   with R show "x = y" by simp
768 qed
770 subsection {* The Degree Function *}
772 constdefs
773   deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
774   "deg R p == LEAST n. bound (zero R) n (coeff (UP R) p)"
776 lemma (in UP_cring) deg_aboveI:
777   "[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
778   by (unfold deg_def P_def) (fast intro: Least_le)
779 (*
780 lemma coeff_bound_ex: "EX n. bound n (coeff p)"
781 proof -
782   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
783   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
784   then show ?thesis ..
785 qed
787 lemma bound_coeff_obtain:
788   assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
789 proof -
790   have "(%n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
791   then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
792   with prem show P .
793 qed
794 *)
795 lemma (in UP_cring) deg_aboveD:
796   "[| deg R p < m; p \<in> carrier P |] ==> coeff P p m = \<zero>"
797 proof -
798   assume R: "p \<in> carrier P" and "deg R p < m"
799   from R obtain n where "bound \<zero> n (coeff P p)"
800     by (auto simp add: UP_def P_def)
801   then have "bound \<zero> (deg R p) (coeff P p)"
802     by (auto simp: deg_def P_def dest: LeastI)
803   then show ?thesis by (rule boundD)
804 qed
806 lemma (in UP_cring) deg_belowI:
807   assumes non_zero: "n ~= 0 ==> coeff P p n ~= \<zero>"
808     and R: "p \<in> carrier P"
809   shows "n <= deg R p"
810 -- {* Logically, this is a slightly stronger version of
811   @{thm [source] deg_aboveD} *}
812 proof (cases "n=0")
813   case True then show ?thesis by simp
814 next
815   case False then have "coeff P p n ~= \<zero>" by (rule non_zero)
816   then have "~ deg R p < n" by (fast dest: deg_aboveD intro: R)
817   then show ?thesis by arith
818 qed
820 lemma (in UP_cring) lcoeff_nonzero_deg:
821   assumes deg: "deg R p ~= 0" and R: "p \<in> carrier P"
822   shows "coeff P p (deg R p) ~= \<zero>"
823 proof -
824   from R obtain m where "deg R p <= m" and m_coeff: "coeff P p m ~= \<zero>"
825   proof -
826     have minus: "!!(n::nat) m. n ~= 0 ==> (n - Suc 0 < m) = (n <= m)"
827       by arith
828 (* TODO: why does proof not work with "1" *)
829     from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
830       by (unfold deg_def P_def) arith
831     then have "~ bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
832     then have "EX m. deg R p - 1 < m & coeff P p m ~= \<zero>"
833       by (unfold bound_def) fast
834     then have "EX m. deg R p <= m & coeff P p m ~= \<zero>" by (simp add: deg minus)
835     then show ?thesis by auto
836   qed
837   with deg_belowI R have "deg R p = m" by fastsimp
838   with m_coeff show ?thesis by simp
839 qed
841 lemma (in UP_cring) lcoeff_nonzero_nonzero:
842   assumes deg: "deg R p = 0" and nonzero: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
843   shows "coeff P p 0 ~= \<zero>"
844 proof -
845   have "EX m. coeff P p m ~= \<zero>"
846   proof (rule classical)
847     assume "~ ?thesis"
848     with R have "p = \<zero>\<^sub>2" by (auto intro: up_eqI)
849     with nonzero show ?thesis by contradiction
850   qed
851   then obtain m where coeff: "coeff P p m ~= \<zero>" ..
852   then have "m <= deg R p" by (rule deg_belowI)
853   then have "m = 0" by (simp add: deg)
854   with coeff show ?thesis by simp
855 qed
857 lemma (in UP_cring) lcoeff_nonzero:
858   assumes neq: "p ~= \<zero>\<^sub>2" and R: "p \<in> carrier P"
859   shows "coeff P p (deg R p) ~= \<zero>"
860 proof (cases "deg R p = 0")
861   case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
862 next
863   case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
864 qed
866 lemma (in UP_cring) deg_eqI:
867   "[| !!m. n < m ==> coeff P p m = \<zero>;
868       !!n. n ~= 0 ==> coeff P p n ~= \<zero>; p \<in> carrier P |] ==> deg R p = n"
869 by (fast intro: le_anti_sym deg_aboveI deg_belowI)
871 (* Degree and polynomial operations *)
873 lemma (in UP_cring) deg_add [simp]:
874   assumes R: "p \<in> carrier P" "q \<in> carrier P"
875   shows "deg R (p \<oplus>\<^sub>2 q) <= max (deg R p) (deg R q)"
876 proof (cases "deg R p <= deg R q")
877   case True show ?thesis
878     by (rule deg_aboveI) (simp_all add: True R deg_aboveD)
879 next
880   case False show ?thesis
881     by (rule deg_aboveI) (simp_all add: False R deg_aboveD)
882 qed
884 lemma (in UP_cring) deg_monom_le:
885   "a \<in> carrier R ==> deg R (monom P a n) <= n"
886   by (intro deg_aboveI) simp_all
888 lemma (in UP_cring) deg_monom [simp]:
889   "[| a ~= \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
890   by (fastsimp intro: le_anti_sym deg_aboveI deg_belowI)
892 lemma (in UP_cring) deg_const [simp]:
893   assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
894 proof (rule le_anti_sym)
895   show "deg R (monom P a 0) <= 0" by (rule deg_aboveI) (simp_all add: R)
896 next
897   show "0 <= deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
898 qed
900 lemma (in UP_cring) deg_zero [simp]:
901   "deg R \<zero>\<^sub>2 = 0"
902 proof (rule le_anti_sym)
903   show "deg R \<zero>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
904 next
905   show "0 <= deg R \<zero>\<^sub>2" by (rule deg_belowI) simp_all
906 qed
908 lemma (in UP_cring) deg_one [simp]:
909   "deg R \<one>\<^sub>2 = 0"
910 proof (rule le_anti_sym)
911   show "deg R \<one>\<^sub>2 <= 0" by (rule deg_aboveI) simp_all
912 next
913   show "0 <= deg R \<one>\<^sub>2" by (rule deg_belowI) simp_all
914 qed
916 lemma (in UP_cring) deg_uminus [simp]:
917   assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^sub>2 p) = deg R p"
918 proof (rule le_anti_sym)
919   show "deg R (\<ominus>\<^sub>2 p) <= deg R p" by (simp add: deg_aboveI deg_aboveD R)
920 next
921   show "deg R p <= deg R (\<ominus>\<^sub>2 p)"
922     by (simp add: deg_belowI lcoeff_nonzero_deg
923       inj_on_iff [OF a_inv_inj, of _ "\<zero>", simplified] R)
924 qed
926 lemma (in UP_domain) deg_smult_ring:
927   "[| a \<in> carrier R; p \<in> carrier P |] ==>
928   deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
929   by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
931 lemma (in UP_domain) deg_smult [simp]:
932   assumes R: "a \<in> carrier R" "p \<in> carrier P"
933   shows "deg R (a \<odot>\<^sub>2 p) = (if a = \<zero> then 0 else deg R p)"
934 proof (rule le_anti_sym)
935   show "deg R (a \<odot>\<^sub>2 p) <= (if a = \<zero> then 0 else deg R p)"
936     by (rule deg_smult_ring)
937 next
938   show "(if a = \<zero> then 0 else deg R p) <= deg R (a \<odot>\<^sub>2 p)"
939   proof (cases "a = \<zero>")
940   qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
941 qed
943 lemma (in UP_cring) deg_mult_cring:
944   assumes R: "p \<in> carrier P" "q \<in> carrier P"
945   shows "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q"
946 proof (rule deg_aboveI)
947   fix m
948   assume boundm: "deg R p + deg R q < m"
949   {
950     fix k i
951     assume boundk: "deg R p + deg R q < k"
952     then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
953     proof (cases "deg R p < i")
954       case True then show ?thesis by (simp add: deg_aboveD R)
955     next
956       case False with boundk have "deg R q < k - i" by arith
957       then show ?thesis by (simp add: deg_aboveD R)
958     qed
959   }
960   with boundm R show "coeff P (p \<otimes>\<^sub>2 q) m = \<zero>" by simp
961 qed (simp add: R)
963 ML_setup {*
964 Context.>> (fn thy => (simpset_ref_of thy :=
965   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
967 lemma (in UP_domain) deg_mult [simp]:
968   "[| p ~= \<zero>\<^sub>2; q ~= \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==>
969   deg R (p \<otimes>\<^sub>2 q) = deg R p + deg R q"
970 proof (rule le_anti_sym)
971   assume "p \<in> carrier P" " q \<in> carrier P"
972   show "deg R (p \<otimes>\<^sub>2 q) <= deg R p + deg R q" by (rule deg_mult_cring)
973 next
974   let ?s = "(%i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
975   assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p ~= \<zero>\<^sub>2" "q ~= \<zero>\<^sub>2"
976   have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
977   show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
978   proof (rule deg_belowI, simp add: R)
979     have "finsum R ?s {.. deg R p + deg R q}
980       = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
981       by (simp only: ivl_disj_un_one)
982     also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
983       by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
984         deg_aboveD less_add_diff R Pi_def)
985     also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
986       by (simp only: ivl_disj_un_singleton)
987     also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
988       by (simp cong: finsum_cong add: finsum_Un_disjoint
989 	ivl_disj_int_singleton deg_aboveD R Pi_def)
990     finally have "finsum R ?s {.. deg R p + deg R q}
991       = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
992     with nz show "finsum R ?s {.. deg R p + deg R q} ~= \<zero>"
993       by (simp add: integral_iff lcoeff_nonzero R)
994     qed (simp add: R)
995   qed
997 lemma (in UP_cring) coeff_finsum:
998   assumes fin: "finite A"
999   shows "p \<in> A -> carrier P ==>
1000     coeff P (finsum P p A) k == finsum R (%i. coeff P (p i) k) A"
1001   using fin by induct (auto simp: Pi_def)
1003 ML_setup {*
1004 Context.>> (fn thy => (simpset_ref_of thy :=
1005   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
1007 lemma (in UP_cring) up_repr:
1008   assumes R: "p \<in> carrier P"
1009   shows "finsum P (%i. monom P (coeff P p i) i) {..deg R p} = p"
1010 proof (rule up_eqI)
1011   let ?s = "(%i. monom P (coeff P p i) i)"
1012   fix k
1013   from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
1014     by simp
1015   show "coeff P (finsum P ?s {..deg R p}) k = coeff P p k"
1016   proof (cases "k <= deg R p")
1017     case True
1018     hence "coeff P (finsum P ?s {..deg R p}) k =
1019           coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
1020       by (simp only: ivl_disj_un_one)
1021     also from True
1022     have "... = coeff P (finsum P ?s {..k}) k"
1023       by (simp cong: finsum_cong add: finsum_Un_disjoint
1024 	ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
1025     also
1026     have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
1027       by (simp only: ivl_disj_un_singleton)
1028     also have "... = coeff P p k"
1029       by (simp cong: finsum_cong add: setsum_Un_disjoint
1030 	ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
1031     finally show ?thesis .
1032   next
1033     case False
1034     hence "coeff P (finsum P ?s {..deg R p}) k =
1035           coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
1036       by (simp only: ivl_disj_un_singleton)
1037     also from False have "... = coeff P p k"
1038       by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
1039         coeff_finsum deg_aboveD R Pi_def)
1040     finally show ?thesis .
1041   qed
1042 qed (simp_all add: R Pi_def)
1044 lemma (in UP_cring) up_repr_le:
1045   "[| deg R p <= n; p \<in> carrier P |] ==>
1046   finsum P (%i. monom P (coeff P p i) i) {..n} = p"
1047 proof -
1048   let ?s = "(%i. monom P (coeff P p i) i)"
1049   assume R: "p \<in> carrier P" and "deg R p <= n"
1050   then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
1051     by (simp only: ivl_disj_un_one)
1052   also have "... = finsum P ?s {..deg R p}"
1053     by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
1054       deg_aboveD R Pi_def)
1055   also have "... = p" by (rule up_repr)
1056   finally show ?thesis .
1057 qed
1059 ML_setup {*
1060 Context.>> (fn thy => (simpset_ref_of thy :=
1061   simpset_of thy setsubgoaler asm_simp_tac; thy)) *}
1063 subsection {* Polynomial over an Integral Domain are an Integral Domain *}
1065 lemma domainI:
1066   assumes cring: "cring R"
1067     and one_not_zero: "one R ~= zero R"
1068     and integral: "!!a b. [| mult R a b = zero R; a \<in> carrier R;
1069       b \<in> carrier R |] ==> a = zero R | b = zero R"
1070   shows "domain R"
1071   by (auto intro!: domain.intro domain_axioms.intro cring.axioms prems
1072     del: disjCI)
1074 lemma (in UP_domain) UP_one_not_zero:
1075   "\<one>\<^sub>2 ~= \<zero>\<^sub>2"
1076 proof
1077   assume "\<one>\<^sub>2 = \<zero>\<^sub>2"
1078   hence "coeff P \<one>\<^sub>2 0 = (coeff P \<zero>\<^sub>2 0)" by simp
1079   hence "\<one> = \<zero>" by simp
1080   with one_not_zero show "False" by contradiction
1081 qed
1083 lemma (in UP_domain) UP_integral:
1084   "[| p \<otimes>\<^sub>2 q = \<zero>\<^sub>2; p \<in> carrier P; q \<in> carrier P |] ==> p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
1085 proof -
1086   fix p q
1087   assume pq: "p \<otimes>\<^sub>2 q = \<zero>\<^sub>2" and R: "p \<in> carrier P" "q \<in> carrier P"
1088   show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2"
1089   proof (rule classical)
1090     assume c: "~ (p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2)"
1091     with R have "deg R p + deg R q = deg R (p \<otimes>\<^sub>2 q)" by simp
1092     also from pq have "... = 0" by simp
1093     finally have "deg R p + deg R q = 0" .
1094     then have f1: "deg R p = 0 & deg R q = 0" by simp
1095     from f1 R have "p = finsum P (%i. (monom P (coeff P p i) i)) {..0}"
1096       by (simp only: up_repr_le)
1097     also from R have "... = monom P (coeff P p 0) 0" by simp
1098     finally have p: "p = monom P (coeff P p 0) 0" .
1099     from f1 R have "q = finsum P (%i. (monom P (coeff P q i) i)) {..0}"
1100       by (simp only: up_repr_le)
1101     also from R have "... = monom P (coeff P q 0) 0" by simp
1102     finally have q: "q = monom P (coeff P q 0) 0" .
1103     from R have "coeff P p 0 \<otimes> coeff P q 0 = coeff P (p \<otimes>\<^sub>2 q) 0" by simp
1104     also from pq have "... = \<zero>" by simp
1105     finally have "coeff P p 0 \<otimes> coeff P q 0 = \<zero>" .
1106     with R have "coeff P p 0 = \<zero> | coeff P q 0 = \<zero>"
1107       by (simp add: R.integral_iff)
1108     with p q show "p = \<zero>\<^sub>2 | q = \<zero>\<^sub>2" by fastsimp
1109   qed
1110 qed
1112 theorem (in UP_domain) UP_domain:
1113   "domain P"
1114   by (auto intro!: domainI UP_cring UP_one_not_zero UP_integral del: disjCI)
1116 text {*
1117   Instantiation of results from @{term domain}.
1118 *}
1120 lemmas (in UP_domain) UP_zero_not_one [simp] =
1121   domain.zero_not_one [OF UP_domain]
1123 lemmas (in UP_domain) UP_integral_iff =
1124   domain.integral_iff [OF UP_domain]
1126 lemmas (in UP_domain) UP_m_lcancel =
1127   domain.m_lcancel [OF UP_domain]
1129 lemmas (in UP_domain) UP_m_rcancel =
1130   domain.m_rcancel [OF UP_domain]
1132 lemma (in UP_domain) smult_integral:
1133   "[| a \<odot>\<^sub>2 p = \<zero>\<^sub>2; a \<in> carrier R; p \<in> carrier P |] ==> a = \<zero> | p = \<zero>\<^sub>2"
1134   by (simp add: monom_mult_is_smult [THEN sym] UP_integral_iff
1135     inj_on_iff [OF monom_inj, of _ "\<zero>", simplified])
1137 subsection {* Evaluation Homomorphism *}
1139 ML_setup {*
1140 Context.>> (fn thy => (simpset_ref_of thy :=
1141   simpset_of thy setsubgoaler asm_full_simp_tac; thy)) *}
1143 (* alternative congruence rule (more efficient)
1144 lemma (in abelian_monoid) finsum_cong2:
1145   "[| !!i. i \<in> A ==> f i \<in> carrier G = True; A = B;
1146   !!i. i \<in> B ==> f i = g i |] ==> finsum G f A = finsum G g B"
1147   sorry
1148 *)
1150 theorem (in cring) diagonal_sum:
1151   "[| f \<in> {..n + m::nat} -> carrier R; g \<in> {..n + m} -> carrier R |] ==>
1152   finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..n + m} =
1153   finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
1154 proof -
1155   assume Rf: "f \<in> {..n + m} -> carrier R" and Rg: "g \<in> {..n + m} -> carrier R"
1156   {
1157     fix j
1158     have "j <= n + m ==>
1159       finsum R (%k. finsum R (%i. f i \<otimes> g (k - i)) {..k}) {..j} =
1160       finsum R (%k. finsum R (%i. f k \<otimes> g i) {..j - k}) {..j}"
1161     proof (induct j)
1162       case 0 from Rf Rg show ?case by (simp add: Pi_def)
1163     next
1164       case (Suc j)
1165       (* The following could be simplified if there was a reasoner for
1166 	total orders integrated with simip. *)
1167       have R6: "!!i k. [| k <= j; i <= Suc j - k |] ==> g i \<in> carrier R"
1168 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1169       have R8: "!!i k. [| k <= Suc j; i <= k |] ==> g (k - i) \<in> carrier R"
1170 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1171       have R9: "!!i k. [| k <= Suc j |] ==> f k \<in> carrier R"
1172 	using Suc by (auto intro!: funcset_mem [OF Rf])
1173       have R10: "!!i k. [| k <= Suc j; i <= Suc j - k |] ==> g i \<in> carrier R"
1174 	using Suc by (auto intro!: funcset_mem [OF Rg]) arith
1175       have R11: "g 0 \<in> carrier R"
1176 	using Suc by (auto intro!: funcset_mem [OF Rg])
1177       from Suc show ?case
1178 	by (simp cong: finsum_cong add: Suc_diff_le a_ac
1179 	  Pi_def R6 R8 R9 R10 R11)
1180     qed
1181   }
1182   then show ?thesis by fast
1183 qed
1185 lemma (in abelian_monoid) boundD_carrier:
1186   "[| bound \<zero> n f; n < m |] ==> f m \<in> carrier G"
1187   by auto
1189 theorem (in cring) cauchy_product:
1190   assumes bf: "bound \<zero> n f" and bg: "bound \<zero> m g"
1191     and Rf: "f \<in> {..n} -> carrier R" and Rg: "g \<in> {..m} -> carrier R"
1192   shows "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
1193     finsum R f {..n} \<otimes> finsum R g {..m}"
1194 (* State revese direction? *)
1195 proof -
1196   have f: "!!x. f x \<in> carrier R"
1197   proof -
1198     fix x
1199     show "f x \<in> carrier R"
1200       using Rf bf boundD_carrier by (cases "x <= n") (auto simp: Pi_def)
1201   qed
1202   have g: "!!x. g x \<in> carrier R"
1203   proof -
1204     fix x
1205     show "g x \<in> carrier R"
1206       using Rg bg boundD_carrier by (cases "x <= m") (auto simp: Pi_def)
1207   qed
1208   from f g have "finsum R (%k. finsum R (%i. f i \<otimes> g (k-i)) {..k}) {..n + m} =
1209     finsum R (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n + m}"
1210     by (simp add: diagonal_sum Pi_def)
1211   also have "... = finsum R
1212       (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) ({..n} Un {)n..n + m})"
1213     by (simp only: ivl_disj_un_one)
1214   also from f g have "... = finsum R
1215       (%k. finsum R (%i. f k \<otimes> g i) {..n + m - k}) {..n}"
1216     by (simp cong: finsum_cong
1217       add: boundD [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1218   also from f g have "... = finsum R
1219       (%k. finsum R (%i. f k \<otimes> g i) ({..m} Un {)m..n + m - k})) {..n}"
1220     by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
1221   also from f g have "... = finsum R
1222       (%k. finsum R (%i. f k \<otimes> g i) {..m}) {..n}"
1223     by (simp cong: finsum_cong
1224       add: boundD [OF bg] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1225   also from f g have "... = finsum R f {..n} \<otimes> finsum R g {..m}"
1226     by (simp add: finsum_ldistr diagonal_sum Pi_def,
1227       simp cong: finsum_cong add: finsum_rdistr Pi_def)
1228   finally show ?thesis .
1229 qed
1231 lemma (in UP_cring) const_ring_hom:
1232   "(%a. monom P a 0) \<in> ring_hom R P"
1233   by (auto intro!: ring_hom_memI intro: up_eqI simp: monom_mult_is_smult)
1235 constdefs
1236   eval :: "[('a, 'm) ring_scheme, ('b, 'n) ring_scheme,
1237           'a => 'b, 'b, nat => 'a] => 'b"
1238   "eval R S phi s == (\<lambda>p \<in> carrier (UP R).
1239     finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p})"
1240 (*
1241   "eval R S phi s p == if p \<in> carrier (UP R)
1242   then finsum S (%i. mult S (phi (coeff (UP R) p i)) (pow S s i)) {..deg R p}
1243   else arbitrary"
1244 *)
1246 locale ring_hom_UP_cring = ring_hom_cring R S + UP_cring R
1248 lemma (in ring_hom_UP_cring) eval_on_carrier:
1249   "p \<in> carrier P ==>
1250     eval R S phi s p =
1251     finsum S (%i. mult S (phi (coeff P p i)) (pow S s i)) {..deg R p}"
1252   by (unfold eval_def, fold P_def) simp
1254 lemma (in ring_hom_UP_cring) eval_extensional:
1255   "eval R S phi s \<in> extensional (carrier P)"
1256   by (unfold eval_def, fold P_def) simp
1258 theorem (in ring_hom_UP_cring) eval_ring_hom:
1259   "s \<in> carrier S ==> eval R S h s \<in> ring_hom P S"
1260 proof (rule ring_hom_memI)
1261   fix p
1262   assume RS: "p \<in> carrier P" "s \<in> carrier S"
1263   then show "eval R S h s p \<in> carrier S"
1264     by (simp only: eval_on_carrier) (simp add: Pi_def)
1265 next
1266   fix p q
1267   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
1268   then show "eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
1269   proof (simp only: eval_on_carrier UP_mult_closed)
1270     from RS have
1271       "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
1272       finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1273         ({..deg R (p \<otimes>\<^sub>3 q)} Un {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q})"
1274       by (simp cong: finsum_cong
1275 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1276 	del: coeff_mult)
1277     also from RS have "... =
1278       finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p + deg R q}"
1279       by (simp only: ivl_disj_un_one deg_mult_cring)
1280     also from RS have "... =
1281       finsum S (%i.
1282         finsum S (%k.
1283         (h (coeff P p k) \<otimes>\<^sub>2 h (coeff P q (i-k))) \<otimes>\<^sub>2 (s (^)\<^sub>2 k \<otimes>\<^sub>2 s (^)\<^sub>2 (i-k)))
1284       {..i}) {..deg R p + deg R q}"
1285       by (simp cong: finsum_cong add: nat_pow_mult Pi_def
1286 	S.m_ac S.finsum_rdistr)
1287     also from RS have "... =
1288       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
1289       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
1290       by (simp add: S.cauchy_product [THEN sym] boundI deg_aboveD S.m_ac
1291 	Pi_def)
1292     finally show
1293       "finsum S (%i. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<otimes>\<^sub>3 q)} =
1294       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<otimes>\<^sub>2
1295       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}" .
1296   qed
1297 next
1298   fix p q
1299   assume RS: "p \<in> carrier P" "q \<in> carrier P" "s \<in> carrier S"
1300   then show "eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
1301   proof (simp only: eval_on_carrier UP_a_closed)
1302     from RS have
1303       "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
1304       finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1305         ({..deg R (p \<oplus>\<^sub>3 q)} Un {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)})"
1306       by (simp cong: finsum_cong
1307 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1309     also from RS have "... =
1310       finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1311         {..max (deg R p) (deg R q)}"
1312       by (simp add: ivl_disj_un_one)
1313     also from RS have "... =
1314       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)} \<oplus>\<^sub>2
1315       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..max (deg R p) (deg R q)}"
1316       by (simp cong: finsum_cong
1317 	add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1318     also have "... =
1319       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1320         ({..deg R p} Un {)deg R p..max (deg R p) (deg R q)}) \<oplus>\<^sub>2
1321       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1322         ({..deg R q} Un {)deg R q..max (deg R p) (deg R q)})"
1323       by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
1324     also from RS have "... =
1325       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
1326       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
1327       by (simp cong: finsum_cong
1328 	add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1329     finally show
1330       "finsum S (%i. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R (p \<oplus>\<^sub>3 q)} =
1331       finsum S (%i. h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R p} \<oplus>\<^sub>2
1332       finsum S (%i. h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..deg R q}"
1333       .
1334   qed
1335 next
1336   assume S: "s \<in> carrier S"
1337   then show "eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
1338     by (simp only: eval_on_carrier UP_one_closed) simp
1339 qed
1341 text {* Instantiation of ring homomorphism lemmas. *}
1343 lemma (in ring_hom_UP_cring) ring_hom_cring_P_S:
1344   "s \<in> carrier S ==> ring_hom_cring P S (eval R S h s)"
1345   by (fast intro!: ring_hom_cring.intro UP_cring cring.axioms prems
1346   intro: ring_hom_cring_axioms.intro eval_ring_hom)
1348 lemma (in ring_hom_UP_cring) UP_hom_closed [intro, simp]:
1349   "[| s \<in> carrier S; p \<in> carrier P |] ==> eval R S h s p \<in> carrier S"
1350   by (rule ring_hom_cring.hom_closed [OF ring_hom_cring_P_S])
1352 lemma (in ring_hom_UP_cring) UP_hom_mult [simp]:
1353   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
1354   eval R S h s (p \<otimes>\<^sub>3 q) = eval R S h s p \<otimes>\<^sub>2 eval R S h s q"
1355   by (rule ring_hom_cring.hom_mult [OF ring_hom_cring_P_S])
1357 lemma (in ring_hom_UP_cring) UP_hom_add [simp]:
1358   "[| s \<in> carrier S; p \<in> carrier P; q \<in> carrier P |] ==>
1359   eval R S h s (p \<oplus>\<^sub>3 q) = eval R S h s p \<oplus>\<^sub>2 eval R S h s q"
1360   by (rule ring_hom_cring.hom_add [OF ring_hom_cring_P_S])
1362 lemma (in ring_hom_UP_cring) UP_hom_one [simp]:
1363   "s \<in> carrier S ==> eval R S h s \<one>\<^sub>3 = \<one>\<^sub>2"
1364   by (rule ring_hom_cring.hom_one [OF ring_hom_cring_P_S])
1366 lemma (in ring_hom_UP_cring) UP_hom_zero [simp]:
1367   "s \<in> carrier S ==> eval R S h s \<zero>\<^sub>3 = \<zero>\<^sub>2"
1368   by (rule ring_hom_cring.hom_zero [OF ring_hom_cring_P_S])
1370 lemma (in ring_hom_UP_cring) UP_hom_a_inv [simp]:
1371   "[| s \<in> carrier S; p \<in> carrier P |] ==>
1372   (eval R S h s) (\<ominus>\<^sub>3 p) = \<ominus>\<^sub>2 (eval R S h s) p"
1373   by (rule ring_hom_cring.hom_a_inv [OF ring_hom_cring_P_S])
1375 lemma (in ring_hom_UP_cring) UP_hom_finsum [simp]:
1376   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
1377   (eval R S h s) (finsum P f A) = finsum S (eval R S h s o f) A"
1378   by (rule ring_hom_cring.hom_finsum [OF ring_hom_cring_P_S])
1380 lemma (in ring_hom_UP_cring) UP_hom_finprod [simp]:
1381   "[| s \<in> carrier S; finite A; f \<in> A -> carrier P |] ==>
1382   (eval R S h s) (finprod P f A) = finprod S (eval R S h s o f) A"
1383   by (rule ring_hom_cring.hom_finprod [OF ring_hom_cring_P_S])
1385 text {* Further properties of the evaluation homomorphism. *}
1387 (* The following lemma could be proved in UP\_cring with the additional
1388    assumption that h is closed. *)
1390 lemma (in ring_hom_UP_cring) eval_const:
1391   "[| s \<in> carrier S; r \<in> carrier R |] ==> eval R S h s (monom P r 0) = h r"
1392   by (simp only: eval_on_carrier monom_closed) simp
1394 text {* The following proof is complicated by the fact that in arbitrary
1395   rings one might have @{term "one R = zero R"}. *}
1397 (* TODO: simplify by cases "one R = zero R" *)
1399 lemma (in ring_hom_UP_cring) eval_monom1:
1400   "s \<in> carrier S ==> eval R S h s (monom P \<one> 1) = s"
1401 proof (simp only: eval_on_carrier monom_closed R.one_closed)
1402   assume S: "s \<in> carrier S"
1403   then have "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1404       {..deg R (monom P \<one> 1)} =
1405     finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1406       ({..deg R (monom P \<one> 1)} Un {)deg R (monom P \<one> 1)..1})"
1407     by (simp cong: finsum_cong del: coeff_monom
1408       add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1409   also have "... =
1410     finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) {..1}"
1411     by (simp only: ivl_disj_un_one deg_monom_le R.one_closed)
1412   also have "... = s"
1413   proof (cases "s = \<zero>\<^sub>2")
1414     case True then show ?thesis by (simp add: Pi_def)
1415   next
1416     case False with S show ?thesis by (simp add: Pi_def)
1417   qed
1418   finally show "finsum S (\<lambda>i. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)
1419       {..deg R (monom P \<one> 1)} = s" .
1420 qed
1422 lemma (in UP_cring) monom_pow:
1423   assumes R: "a \<in> carrier R"
1424   shows "(monom P a n) (^)\<^sub>2 m = monom P (a (^) m) (n * m)"
1425 proof (induct m)
1426   case 0 from R show ?case by simp
1427 next
1428   case Suc with R show ?case
1429     by (simp del: monom_mult add: monom_mult [THEN sym] add_commute)
1430 qed
1432 lemma (in ring_hom_cring) hom_pow [simp]:
1433   "x \<in> carrier R ==> h (x (^) n) = h x (^)\<^sub>2 (n::nat)"
1434   by (induct n) simp_all
1436 lemma (in ring_hom_UP_cring) UP_hom_pow [simp]:
1437   "[| s \<in> carrier S; p \<in> carrier P |] ==>
1438   (eval R S h s) (p (^)\<^sub>3 n) = eval R S h s p (^)\<^sub>2 (n::nat)"
1439   by (rule ring_hom_cring.hom_pow [OF ring_hom_cring_P_S])
1441 lemma (in ring_hom_UP_cring) eval_monom:
1442   "[| s \<in> carrier S; r \<in> carrier R |] ==>
1443   eval R S h s (monom P r n) = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
1444 proof -
1445   assume RS: "s \<in> carrier S" "r \<in> carrier R"
1446   then have "eval R S h s (monom P r n) =
1447     eval R S h s (monom P r 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 n)"
1448     by (simp del: monom_mult UP_hom_mult UP_hom_pow
1449       add: monom_mult [THEN sym] monom_pow)
1450   also from RS eval_monom1 have "... = h r \<otimes>\<^sub>2 s (^)\<^sub>2 n"
1451     by (simp add: eval_const)
1452   finally show ?thesis .
1453 qed
1455 lemma (in ring_hom_UP_cring) eval_smult:
1456   "[| s \<in> carrier S; r \<in> carrier R; p \<in> carrier P |] ==>
1457   eval R S h s (r \<odot>\<^sub>3 p) = h r \<otimes>\<^sub>2 eval R S h s p"
1458   by (simp add: monom_mult_is_smult [THEN sym] eval_const)
1460 lemma ring_hom_cringI:
1461   assumes "cring R"
1462     and "cring S"
1463     and "h \<in> ring_hom R S"
1464   shows "ring_hom_cring R S h"
1465   by (fast intro: ring_hom_cring.intro ring_hom_cring_axioms.intro
1466     cring.axioms prems)
1468 lemma (in ring_hom_UP_cring) UP_hom_unique:
1469   assumes Phi: "Phi \<in> ring_hom P S" "Phi (monom P \<one> (Suc 0)) = s"
1470       "!!r. r \<in> carrier R ==> Phi (monom P r 0) = h r"
1471     and Psi: "Psi \<in> ring_hom P S" "Psi (monom P \<one> (Suc 0)) = s"
1472       "!!r. r \<in> carrier R ==> Psi (monom P r 0) = h r"
1473     and RS: "s \<in> carrier S" "p \<in> carrier P"
1474   shows "Phi p = Psi p"
1475 proof -
1476   have Phi_hom: "ring_hom_cring P S Phi"
1477     by (auto intro: ring_hom_cringI UP_cring S.cring Phi)
1478   have Psi_hom: "ring_hom_cring P S Psi"
1479     by (auto intro: ring_hom_cringI UP_cring S.cring Psi)
1480 thm monom_mult
1481   have "Phi p = Phi (finsum P
1482     (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
1483     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
1484   also have "... = Psi (finsum P
1485     (%i. monom P (coeff P p i) 0 \<otimes>\<^sub>3 (monom P \<one> 1) (^)\<^sub>3 i) {..deg R p})"
1486     by (simp add: ring_hom_cring.hom_finsum [OF Phi_hom]
1487       ring_hom_cring.hom_mult [OF Phi_hom]
1488       ring_hom_cring.hom_pow [OF Phi_hom] Phi
1489       ring_hom_cring.hom_finsum [OF Psi_hom]
1490       ring_hom_cring.hom_mult [OF Psi_hom]
1491       ring_hom_cring.hom_pow [OF Psi_hom] Psi RS Pi_def comp_def)
1492   also have "... = Psi p"
1493     by (simp add: up_repr RS monom_mult [THEN sym] monom_pow del: monom_mult)
1494   finally show ?thesis .
1495 qed
1498 theorem (in ring_hom_UP_cring) UP_universal_property:
1499   "s \<in> carrier S ==>
1500   EX! Phi. Phi \<in> ring_hom P S \<inter> extensional (carrier P) &
1501     Phi (monom P \<one> 1) = s &
1502     (ALL r : carrier R. Phi (monom P r 0) = h r)"
1503   using eval_monom1
1504   apply (auto intro: eval_ring_hom eval_const eval_extensional)
1505   apply (rule extensionalityI)
1506   apply (auto intro: UP_hom_unique)
1507   done
1509 subsection {* Sample application of evaluation homomorphism *}
1511 lemma ring_hom_UP_cringI:
1512   assumes "cring R"
1513     and "cring S"
1514     and "h \<in> ring_hom R S"
1515   shows "ring_hom_UP_cring R S h"
1516   by (fast intro: ring_hom_UP_cring.intro ring_hom_cring_axioms.intro
1517     cring.axioms prems)
1519 lemma INTEG_id:
1520   "ring_hom_UP_cring INTEG INTEG id"
1521   by (fast intro: ring_hom_UP_cringI cring_INTEG id_ring_hom)
1523 text {*
1524   An instantiation mechanism would now import all theorems and lemmas
1525   valid in the context of homomorphisms between @{term INTEG} and @{term
1526   "UP INTEG"}.  *}
1528 lemma INTEG_closed [intro, simp]:
1529   "z \<in> carrier INTEG"
1530   by (unfold INTEG_def) simp
1532 lemma INTEG_mult [simp]:
1533   "mult INTEG z w = z * w"
1534   by (unfold INTEG_def) simp
1536 lemma INTEG_pow [simp]:
1537   "pow INTEG z n = z ^ n"
1538   by (induct n) (simp_all add: INTEG_def nat_pow_def)
1540 lemma "eval INTEG INTEG id 10 (monom (UP INTEG) 5 2) = 500"
1541   by (simp add: ring_hom_UP_cring.eval_monom [OF INTEG_id])
1543 -- {* Calculates @{term "x = 500"} *}
1546 end