-
Notifications
You must be signed in to change notification settings - Fork 0
/
UnivPoly.thy
1843 lines (1586 loc) · 77.2 KB
/
UnivPoly.thy
1
2
3
4
5
6
7
8
9
10
11
12
13
14
15
16
17
18
19
20
21
22
23
24
25
26
27
28
29
30
31
32
33
34
35
36
37
38
39
40
41
42
43
44
45
46
47
48
49
50
51
52
53
54
55
56
57
58
59
60
61
62
63
64
65
66
67
68
69
70
71
72
73
74
75
76
77
78
79
80
81
82
83
84
85
86
87
88
89
90
91
92
93
94
95
96
97
98
99
100
101
102
103
104
105
106
107
108
109
110
111
112
113
114
115
116
117
118
119
120
121
122
123
124
125
126
127
128
129
130
131
132
133
134
135
136
137
138
139
140
141
142
143
144
145
146
147
148
149
150
151
152
153
154
155
156
157
158
159
160
161
162
163
164
165
166
167
168
169
170
171
172
173
174
175
176
177
178
179
180
181
182
183
184
185
186
187
188
189
190
191
192
193
194
195
196
197
198
199
200
201
202
203
204
205
206
207
208
209
210
211
212
213
214
215
216
217
218
219
220
221
222
223
224
225
226
227
228
229
230
231
232
233
234
235
236
237
238
239
240
241
242
243
244
245
246
247
248
249
250
251
252
253
254
255
256
257
258
259
260
261
262
263
264
265
266
267
268
269
270
271
272
273
274
275
276
277
278
279
280
281
282
283
284
285
286
287
288
289
290
291
292
293
294
295
296
297
298
299
300
301
302
303
304
305
306
307
308
309
310
311
312
313
314
315
316
317
318
319
320
321
322
323
324
325
326
327
328
329
330
331
332
333
334
335
336
337
338
339
340
341
342
343
344
345
346
347
348
349
350
351
352
353
354
355
356
357
358
359
360
361
362
363
364
365
366
367
368
369
370
371
372
373
374
375
376
377
378
379
380
381
382
383
384
385
386
387
388
389
390
391
392
393
394
395
396
397
398
399
400
401
402
403
404
405
406
407
408
409
410
411
412
413
414
415
416
417
418
419
420
421
422
423
424
425
426
427
428
429
430
431
432
433
434
435
436
437
438
439
440
441
442
443
444
445
446
447
448
449
450
451
452
453
454
455
456
457
458
459
460
461
462
463
464
465
466
467
468
469
470
471
472
473
474
475
476
477
478
479
480
481
482
483
484
485
486
487
488
489
490
491
492
493
494
495
496
497
498
499
500
501
502
503
504
505
506
507
508
509
510
511
512
513
514
515
516
517
518
519
520
521
522
523
524
525
526
527
528
529
530
531
532
533
534
535
536
537
538
539
540
541
542
543
544
545
546
547
548
549
550
551
552
553
554
555
556
557
558
559
560
561
562
563
564
565
566
567
568
569
570
571
572
573
574
575
576
577
578
579
580
581
582
583
584
585
586
587
588
589
590
591
592
593
594
595
596
597
598
599
600
601
602
603
604
605
606
607
608
609
610
611
612
613
614
615
616
617
618
619
620
621
622
623
624
625
626
627
628
629
630
631
632
633
634
635
636
637
638
639
640
641
642
643
644
645
646
647
648
649
650
651
652
653
654
655
656
657
658
659
660
661
662
663
664
665
666
667
668
669
670
671
672
673
674
675
676
677
678
679
680
681
682
683
684
685
686
687
688
689
690
691
692
693
694
695
696
697
698
699
700
701
702
703
704
705
706
707
708
709
710
711
712
713
714
715
716
717
718
719
720
721
722
723
724
725
726
727
728
729
730
731
732
733
734
735
736
737
738
739
740
741
742
743
744
745
746
747
748
749
750
751
752
753
754
755
756
757
758
759
760
761
762
763
764
765
766
767
768
769
770
771
772
773
774
775
776
777
778
779
780
781
782
783
784
785
786
787
788
789
790
791
792
793
794
795
796
797
798
799
800
801
802
803
804
805
806
807
808
809
810
811
812
813
814
815
816
817
818
819
820
821
822
823
824
825
826
827
828
829
830
831
832
833
834
835
836
837
838
839
840
841
842
843
844
845
846
847
848
849
850
851
852
853
854
855
856
857
858
859
860
861
862
863
864
865
866
867
868
869
870
871
872
873
874
875
876
877
878
879
880
881
882
883
884
885
886
887
888
889
890
891
892
893
894
895
896
897
898
899
900
901
902
903
904
905
906
907
908
909
910
911
912
913
914
915
916
917
918
919
920
921
922
923
924
925
926
927
928
929
930
931
932
933
934
935
936
937
938
939
940
941
942
943
944
945
946
947
948
949
950
951
952
953
954
955
956
957
958
959
960
961
962
963
964
965
966
967
968
969
970
971
972
973
974
975
976
977
978
979
980
981
982
983
984
985
986
987
988
989
990
991
992
993
994
995
996
997
998
999
1000
(* Title: HOL/Algebra/UnivPoly.thy
Author: Clemens Ballarin, started 9 December 1996
Copyright: Clemens Ballarin
Contributions, in particular on long division, by Jesus Aransay.
*)
theory UnivPoly
imports Module RingHom
begin
section \<open>Univariate Polynomials\<close>
text \<open>
Polynomials are formalised as modules with additional operations for
extracting coefficients from polynomials and for obtaining monomials
from coefficients and exponents (record \<open>up_ring\<close>). The
carrier set is a set of bounded functions from Nat to the
coefficient domain. Bounded means that these functions return zero
above a certain bound (the degree). There is a chapter on the
formalisation of polynomials in the PhD thesis @{cite "Ballarin:1999"},
which was implemented with axiomatic type classes. This was later
ported to Locales.
\<close>
subsection \<open>The Constructor for Univariate Polynomials\<close>
text \<open>
Functions with finite support.
\<close>
locale bound =
fixes z :: 'a
and n :: nat
and f :: "nat => 'a"
assumes bound: "!!m. n < m \<Longrightarrow> f m = z"
declare bound.intro [intro!]
and bound.bound [dest]
lemma bound_below:
assumes bound: "bound z m f" and nonzero: "f n \<noteq> z" shows "n \<le> m"
proof (rule classical)
assume "\<not> ?thesis"
then have "m < n" by arith
with bound have "f n = z" ..
with nonzero show ?thesis by contradiction
qed
record ('a, 'p) up_ring = "('a, 'p) module" +
monom :: "['a, nat] => 'p"
coeff :: "['p, nat] => 'a"
definition
up :: "('a, 'm) ring_scheme => (nat => 'a) set"
where "up R = {f. f \<in> UNIV \<rightarrow> carrier R \<and> (\<exists>n. bound \<zero>\<^bsub>R\<^esub> n f)}"
definition UP :: "('a, 'm) ring_scheme => ('a, nat => 'a) up_ring"
where "UP R = \<lparr>
carrier = up R,
mult = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>n. \<Oplus>\<^bsub>R\<^esub>i \<in> {..n}. p i \<otimes>\<^bsub>R\<^esub> q (n-i)),
one = (\<lambda>i. if i=0 then \<one>\<^bsub>R\<^esub> else \<zero>\<^bsub>R\<^esub>),
zero = (\<lambda>i. \<zero>\<^bsub>R\<^esub>),
add = (\<lambda>p\<in>up R. \<lambda>q\<in>up R. \<lambda>i. p i \<oplus>\<^bsub>R\<^esub> q i),
smult = (\<lambda>a\<in>carrier R. \<lambda>p\<in>up R. \<lambda>i. a \<otimes>\<^bsub>R\<^esub> p i),
monom = (\<lambda>a\<in>carrier R. \<lambda>n i. if i=n then a else \<zero>\<^bsub>R\<^esub>),
coeff = (\<lambda>p\<in>up R. \<lambda>n. p n)\<rparr>"
text \<open>
Properties of the set of polynomials @{term up}.
\<close>
lemma mem_upI [intro]:
"[| \<And>n. f n \<in> carrier R; \<exists>n. bound (zero R) n f |] ==> f \<in> up R"
by (simp add: up_def Pi_def)
lemma mem_upD [dest]:
"f \<in> up R ==> f n \<in> carrier R"
by (simp add: up_def Pi_def)
context ring
begin
lemma bound_upD [dest]: "f \<in> up R \<Longrightarrow> \<exists>n. bound \<zero> n f" by (simp add: up_def)
lemma up_one_closed: "(\<lambda>n. if n = 0 then \<one> else \<zero>) \<in> up R" using up_def by force
lemma up_smult_closed: "[| a \<in> carrier R; p \<in> up R |] ==> (\<lambda>i. a \<otimes> p i) \<in> up R" by force
lemma up_add_closed:
"[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<oplus> q i) \<in> up R"
proof
fix n
assume "p \<in> up R" and "q \<in> up R"
then show "p n \<oplus> q n \<in> carrier R"
by auto
next
assume UP: "p \<in> up R" "q \<in> up R"
show "\<exists>n. bound \<zero> n (\<lambda>i. p i \<oplus> q i)"
proof -
from UP obtain n where boundn: "bound \<zero> n p" by fast
from UP obtain m where boundm: "bound \<zero> m q" by fast
have "bound \<zero> (max n m) (\<lambda>i. p i \<oplus> q i)"
proof
fix i
assume "max n m < i"
with boundn and boundm and UP show "p i \<oplus> q i = \<zero>" by fastforce
qed
then show ?thesis ..
qed
qed
lemma up_a_inv_closed:
"p \<in> up R ==> (\<lambda>i. \<ominus> (p i)) \<in> up R"
proof
assume R: "p \<in> up R"
then obtain n where "bound \<zero> n p" by auto
then have "bound \<zero> n (\<lambda>i. \<ominus> p i)"
by (simp add: bound_def minus_equality)
then show "\<exists>n. bound \<zero> n (\<lambda>i. \<ominus> p i)" by auto
qed auto
lemma up_minus_closed:
"[| p \<in> up R; q \<in> up R |] ==> (\<lambda>i. p i \<ominus> q i) \<in> up R"
unfolding a_minus_def
using mem_upD [of p R] mem_upD [of q R] up_add_closed up_a_inv_closed by auto
lemma up_mult_closed:
"[| p \<in> up R; q \<in> up R |] ==>
(\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> up R"
proof
fix n
assume "p \<in> up R" "q \<in> up R"
then show "(\<Oplus>i \<in> {..n}. p i \<otimes> q (n-i)) \<in> carrier R"
by (simp add: mem_upD funcsetI)
next
assume UP: "p \<in> up R" "q \<in> up R"
show "\<exists>n. bound \<zero> n (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n-i))"
proof -
from UP obtain n where boundn: "bound \<zero> n p" by fast
from UP obtain m where boundm: "bound \<zero> m q" by fast
have "bound \<zero> (n + m) (\<lambda>n. \<Oplus>i \<in> {..n}. p i \<otimes> q (n - i))"
proof
fix k assume bound: "n + m < k"
{
fix i
have "p i \<otimes> q (k-i) = \<zero>"
proof (cases "n < i")
case True
with boundn have "p i = \<zero>" by auto
moreover from UP have "q (k-i) \<in> carrier R" by auto
ultimately show ?thesis by simp
next
case False
with bound have "m < k-i" by arith
with boundm have "q (k-i) = \<zero>" by auto
moreover from UP have "p i \<in> carrier R" by auto
ultimately show ?thesis by simp
qed
}
then show "(\<Oplus>i \<in> {..k}. p i \<otimes> q (k-i)) = \<zero>"
by (simp add: Pi_def)
qed
then show ?thesis by fast
qed
qed
end
subsection \<open>Effect of Operations on Coefficients\<close>
locale UP =
fixes R (structure) and P (structure)
defines P_def: "P == UP R"
locale UP_ring = UP + R?: ring R
locale UP_cring = UP + R?: cring R
sublocale UP_cring < UP_ring
by intro_locales [1] (rule P_def)
locale UP_domain = UP + R?: "domain" R
sublocale UP_domain < UP_cring
by intro_locales [1] (rule P_def)
context UP
begin
text \<open>Temporarily declare @{thm P_def} as simp rule.\<close>
declare P_def [simp]
lemma up_eqI:
assumes prem: "!!n. coeff P p n = coeff P q n" and R: "p \<in> carrier P" "q \<in> carrier P"
shows "p = q"
proof
fix x
from prem and R show "p x = q x" by (simp add: UP_def)
qed
lemma coeff_closed [simp]:
"p \<in> carrier P ==> coeff P p n \<in> carrier R" by (auto simp add: UP_def)
end
context UP_ring
begin
(* Theorems generalised from commutative rings to rings by Jesus Aransay. *)
lemma coeff_monom [simp]:
"a \<in> carrier R ==> coeff P (monom P a m) n = (if m=n then a else \<zero>)"
proof -
assume R: "a \<in> carrier R"
then have "(\<lambda>n. if n = m then a else \<zero>) \<in> up R"
using up_def by force
with R show ?thesis by (simp add: UP_def)
qed
lemma coeff_zero [simp]: "coeff P \<zero>\<^bsub>P\<^esub> n = \<zero>" by (auto simp add: UP_def)
lemma coeff_one [simp]: "coeff P \<one>\<^bsub>P\<^esub> n = (if n=0 then \<one> else \<zero>)"
using up_one_closed by (simp add: UP_def)
lemma coeff_smult [simp]:
"[| a \<in> carrier R; p \<in> carrier P |] ==> coeff P (a \<odot>\<^bsub>P\<^esub> p) n = a \<otimes> coeff P p n"
by (simp add: UP_def up_smult_closed)
lemma coeff_add [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<oplus>\<^bsub>P\<^esub> q) n = coeff P p n \<oplus> coeff P q n"
by (simp add: UP_def up_add_closed)
lemma coeff_mult [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = (\<Oplus>i \<in> {..n}. coeff P p i \<otimes> coeff P q (n-i))"
by (simp add: UP_def up_mult_closed)
end
subsection \<open>Polynomials Form a Ring.\<close>
context UP_ring
begin
text \<open>Operations are closed over @{term P}.\<close>
lemma UP_mult_closed [simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> p \<otimes>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_mult_closed)
lemma UP_one_closed [simp]:
"\<one>\<^bsub>P\<^esub> \<in> carrier P" by (simp add: UP_def up_one_closed)
lemma UP_zero_closed [intro, simp]:
"\<zero>\<^bsub>P\<^esub> \<in> carrier P" by (auto simp add: UP_def)
lemma UP_a_closed [intro, simp]:
"[| p \<in> carrier P; q \<in> carrier P |] ==> p \<oplus>\<^bsub>P\<^esub> q \<in> carrier P" by (simp add: UP_def up_add_closed)
lemma monom_closed [simp]:
"a \<in> carrier R ==> monom P a n \<in> carrier P" by (auto simp add: UP_def up_def Pi_def)
lemma UP_smult_closed [simp]:
"[| a \<in> carrier R; p \<in> carrier P |] ==> a \<odot>\<^bsub>P\<^esub> p \<in> carrier P" by (simp add: UP_def up_smult_closed)
end
declare (in UP) P_def [simp del]
text \<open>Algebraic ring properties\<close>
context UP_ring
begin
lemma UP_a_assoc:
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
shows "(p \<oplus>\<^bsub>P\<^esub> q) \<oplus>\<^bsub>P\<^esub> r = p \<oplus>\<^bsub>P\<^esub> (q \<oplus>\<^bsub>P\<^esub> r)" by (rule up_eqI, simp add: a_assoc R, simp_all add: R)
lemma UP_l_zero [simp]:
assumes R: "p \<in> carrier P"
shows "\<zero>\<^bsub>P\<^esub> \<oplus>\<^bsub>P\<^esub> p = p" by (rule up_eqI, simp_all add: R)
lemma UP_l_neg_ex:
assumes R: "p \<in> carrier P"
shows "\<exists>q \<in> carrier P. q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
proof -
let ?q = "\<lambda>i. \<ominus> (p i)"
from R have closed: "?q \<in> carrier P"
by (simp add: UP_def P_def up_a_inv_closed)
from R have coeff: "!!n. coeff P ?q n = \<ominus> (coeff P p n)"
by (simp add: UP_def P_def up_a_inv_closed)
show ?thesis
proof
show "?q \<oplus>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
by (auto intro!: up_eqI simp add: R closed coeff R.l_neg)
qed (rule closed)
qed
lemma UP_a_comm:
assumes R: "p \<in> carrier P" "q \<in> carrier P"
shows "p \<oplus>\<^bsub>P\<^esub> q = q \<oplus>\<^bsub>P\<^esub> p" by (rule up_eqI, simp add: a_comm R, simp_all add: R)
lemma UP_m_assoc:
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
shows "(p \<otimes>\<^bsub>P\<^esub> q) \<otimes>\<^bsub>P\<^esub> r = p \<otimes>\<^bsub>P\<^esub> (q \<otimes>\<^bsub>P\<^esub> r)"
proof (rule up_eqI)
fix n
{
fix k and a b c :: "nat=>'a"
assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
"c \<in> UNIV \<rightarrow> carrier R"
then have "k <= n ==>
(\<Oplus>j \<in> {..k}. (\<Oplus>i \<in> {..j}. a i \<otimes> b (j-i)) \<otimes> c (n-j)) =
(\<Oplus>j \<in> {..k}. a j \<otimes> (\<Oplus>i \<in> {..k-j}. b i \<otimes> c (n-j-i)))"
(is "_ \<Longrightarrow> ?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def m_assoc)
next
case (Suc k)
then have "k <= n" by arith
from this R have "?eq k" by (rule Suc)
with R show ?case
by (simp cong: finsum_cong
add: Suc_diff_le Pi_def l_distr r_distr m_assoc)
(simp cong: finsum_cong add: Pi_def a_ac finsum_ldistr m_assoc)
qed
}
with R show "coeff P ((p \<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"
by (simp add: Pi_def)
qed (simp_all add: R)
lemma UP_r_one [simp]:
assumes R: "p \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub> = p"
proof (rule up_eqI)
fix n
show "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) n = coeff P p n"
proof (cases n)
case 0
{
with R show ?thesis by simp
}
next
case Suc
{
(*JE: in the locale UP_cring the proof was solved only with "by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)", but I did not get it to work here*)
fix nn assume Succ: "n = Suc nn"
have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = coeff P p (Suc nn)"
proof -
have "coeff P (p \<otimes>\<^bsub>P\<^esub> \<one>\<^bsub>P\<^esub>) (Suc nn) = (\<Oplus>i\<in>{..Suc nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" using R by simp
also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>) \<oplus> (\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))"
using finsum_Suc [of "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "nn"] unfolding Pi_def using R by simp
also have "\<dots> = coeff P p (Suc nn) \<otimes> (if Suc nn \<le> Suc nn then \<one> else \<zero>)"
proof -
have "(\<Oplus>i\<in>{..nn}. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>)) = (\<Oplus>i\<in>{..nn}. \<zero>)"
using finsum_cong [of "{..nn}" "{..nn}" "(\<lambda>i::nat. coeff P p i \<otimes> (if Suc nn \<le> i then \<one> else \<zero>))" "(\<lambda>i::nat. \<zero>)"] using R
unfolding Pi_def by simp
also have "\<dots> = \<zero>" by simp
finally show ?thesis using r_zero R by simp
qed
also have "\<dots> = coeff P p (Suc nn)" using R by simp
finally show ?thesis by simp
qed
then show ?thesis using Succ by simp
}
qed
qed (simp_all add: R)
lemma UP_l_one [simp]:
assumes R: "p \<in> carrier P"
shows "\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p = p"
proof (rule up_eqI)
fix n
show "coeff P (\<one>\<^bsub>P\<^esub> \<otimes>\<^bsub>P\<^esub> p) n = coeff P p n"
proof (cases n)
case 0 with R show ?thesis by simp
next
case Suc with R show ?thesis
by (simp del: finsum_Suc add: finsum_Suc2 Pi_def)
qed
qed (simp_all add: R)
lemma UP_l_distr:
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
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)"
by (rule up_eqI) (simp add: l_distr R Pi_def, simp_all add: R)
lemma UP_r_distr:
assumes R: "p \<in> carrier P" "q \<in> carrier P" "r \<in> carrier P"
shows "r \<otimes>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = (r \<otimes>\<^bsub>P\<^esub> p) \<oplus>\<^bsub>P\<^esub> (r \<otimes>\<^bsub>P\<^esub> q)"
by (rule up_eqI) (simp add: r_distr R Pi_def, simp_all add: R)
theorem UP_ring: "ring P"
by (auto intro!: ringI abelian_groupI monoidI UP_a_assoc)
(auto intro: UP_a_comm UP_l_neg_ex UP_m_assoc UP_l_distr UP_r_distr)
end
subsection \<open>Polynomials Form a Commutative Ring.\<close>
context UP_cring
begin
lemma UP_m_comm:
assumes R1: "p \<in> carrier P" and R2: "q \<in> carrier P" shows "p \<otimes>\<^bsub>P\<^esub> q = q \<otimes>\<^bsub>P\<^esub> p"
proof (rule up_eqI)
fix n
{
fix k and a b :: "nat=>'a"
assume R: "a \<in> UNIV \<rightarrow> carrier R" "b \<in> UNIV \<rightarrow> carrier R"
then have "k <= n ==>
(\<Oplus>i \<in> {..k}. a i \<otimes> b (n-i)) = (\<Oplus>i \<in> {..k}. a (k-i) \<otimes> b (i+n-k))"
(is "_ \<Longrightarrow> ?eq k")
proof (induct k)
case 0 then show ?case by (simp add: Pi_def)
next
case (Suc k) then show ?case
by (subst (2) finsum_Suc2) (simp add: Pi_def a_comm)+
qed
}
note l = this
from R1 R2 show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) n = coeff P (q \<otimes>\<^bsub>P\<^esub> p) n"
unfolding coeff_mult [OF R1 R2, of n]
unfolding coeff_mult [OF R2 R1, of n]
using l [of "(\<lambda>i. coeff P p i)" "(\<lambda>i. coeff P q i)" "n"] by (simp add: Pi_def m_comm)
qed (simp_all add: R1 R2)
subsection \<open>Polynomials over a commutative ring for a commutative ring\<close>
theorem UP_cring:
"cring P" using UP_ring unfolding cring_def by (auto intro!: comm_monoidI UP_m_assoc UP_m_comm)
end
context UP_ring
begin
lemma UP_a_inv_closed [intro, simp]:
"p \<in> carrier P ==> \<ominus>\<^bsub>P\<^esub> p \<in> carrier P"
by (rule abelian_group.a_inv_closed [OF ring.is_abelian_group [OF UP_ring]])
lemma coeff_a_inv [simp]:
assumes R: "p \<in> carrier P"
shows "coeff P (\<ominus>\<^bsub>P\<^esub> p) n = \<ominus> (coeff P p n)"
proof -
from R coeff_closed UP_a_inv_closed have
"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)"
by algebra
also from R have "... = \<ominus> (coeff P p n)"
by (simp del: coeff_add add: coeff_add [THEN sym]
abelian_group.r_neg [OF ring.is_abelian_group [OF UP_ring]])
finally show ?thesis .
qed
end
sublocale UP_ring < P?: ring P using UP_ring .
sublocale UP_cring < P?: cring P using UP_cring .
subsection \<open>Polynomials Form an Algebra\<close>
context UP_ring
begin
lemma UP_smult_l_distr:
"[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
(a \<oplus> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> b \<odot>\<^bsub>P\<^esub> p"
by (rule up_eqI) (simp_all add: R.l_distr)
lemma UP_smult_r_distr:
"[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
a \<odot>\<^bsub>P\<^esub> (p \<oplus>\<^bsub>P\<^esub> q) = a \<odot>\<^bsub>P\<^esub> p \<oplus>\<^bsub>P\<^esub> a \<odot>\<^bsub>P\<^esub> q"
by (rule up_eqI) (simp_all add: R.r_distr)
lemma UP_smult_assoc1:
"[| a \<in> carrier R; b \<in> carrier R; p \<in> carrier P |] ==>
(a \<otimes> b) \<odot>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> (b \<odot>\<^bsub>P\<^esub> p)"
by (rule up_eqI) (simp_all add: R.m_assoc)
lemma UP_smult_zero [simp]:
"p \<in> carrier P ==> \<zero> \<odot>\<^bsub>P\<^esub> p = \<zero>\<^bsub>P\<^esub>"
by (rule up_eqI) simp_all
lemma UP_smult_one [simp]:
"p \<in> carrier P ==> \<one> \<odot>\<^bsub>P\<^esub> p = p"
by (rule up_eqI) simp_all
lemma UP_smult_assoc2:
"[| a \<in> carrier R; p \<in> carrier P; q \<in> carrier P |] ==>
(a \<odot>\<^bsub>P\<^esub> p) \<otimes>\<^bsub>P\<^esub> q = a \<odot>\<^bsub>P\<^esub> (p \<otimes>\<^bsub>P\<^esub> q)"
by (rule up_eqI) (simp_all add: R.finsum_rdistr R.m_assoc Pi_def)
end
text \<open>
Interpretation of lemmas from @{term algebra}.
\<close>
lemma (in cring) cring:
"cring R" ..
lemma (in UP_cring) UP_algebra:
"algebra R P" by (auto intro!: algebraI R.cring UP_cring UP_smult_l_distr UP_smult_r_distr
UP_smult_assoc1 UP_smult_assoc2)
sublocale UP_cring < algebra R P using UP_algebra .
subsection \<open>Further Lemmas Involving Monomials\<close>
context UP_ring
begin
lemma monom_zero [simp]:
"monom P \<zero> n = \<zero>\<^bsub>P\<^esub>" by (simp add: UP_def P_def)
lemma monom_mult_is_smult:
assumes R: "a \<in> carrier R" "p \<in> carrier P"
shows "monom P a 0 \<otimes>\<^bsub>P\<^esub> p = a \<odot>\<^bsub>P\<^esub> p"
proof (rule up_eqI)
fix n
show "coeff P (monom P a 0 \<otimes>\<^bsub>P\<^esub> p) n = coeff P (a \<odot>\<^bsub>P\<^esub> p) n"
proof (cases n)
case 0 with R show ?thesis by simp
next
case Suc with R show ?thesis
using R.finsum_Suc2 by (simp del: R.finsum_Suc add: Pi_def)
qed
qed (simp_all add: R)
lemma monom_one [simp]:
"monom P \<one> 0 = \<one>\<^bsub>P\<^esub>"
by (rule up_eqI) simp_all
lemma monom_add [simp]:
"[| a \<in> carrier R; b \<in> carrier R |] ==>
monom P (a \<oplus> b) n = monom P a n \<oplus>\<^bsub>P\<^esub> monom P b n"
by (rule up_eqI) simp_all
lemma monom_one_Suc:
"monom P \<one> (Suc n) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
proof (rule up_eqI)
fix k
show "coeff P (monom P \<one> (Suc n)) k = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
proof (cases "k = Suc n")
case True show ?thesis
proof -
fix m
from True have less_add_diff:
"!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
also from True
have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp cong: R.finsum_cong add: Pi_def)
also have "... = (\<Oplus>i \<in> {..n}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp only: ivl_disj_un_singleton)
also from True
have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
coeff P (monom P \<one> 1) (k - i))"
by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
order_less_imp_not_eq Pi_def)
also from True have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k"
by (simp add: ivl_disj_un_one)
finally show ?thesis .
qed
next
case False
note neq = False
let ?s =
"\<lambda>i. (if n = i then \<one> else \<zero>) \<otimes> (if Suc 0 = k - i then \<one> else \<zero>)"
from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
proof -
have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: Pi_def)
from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: Pi_def) arith
have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
by (simp cong: R.finsum_cong add: order_less_imp_not_eq Pi_def)
show ?thesis
proof (cases "k < n")
case True then show ?thesis by (simp cong: R.finsum_cong add: Pi_def)
next
case False then have n_le_k: "n <= k" by arith
show ?thesis
proof (cases "n = k")
case True
then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
by (simp cong: R.finsum_cong add: Pi_def)
also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
by (simp only: ivl_disj_un_singleton)
finally show ?thesis .
next
case False with n_le_k have n_less_k: "n < k" by arith
with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
by (simp only: ivl_disj_un_singleton)
also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
by (simp add: R.finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
by (simp only: ivl_disj_un_one)
finally show ?thesis .
qed
qed
qed
also have "... = coeff P (monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> 1) k" by simp
finally show ?thesis .
qed
qed (simp_all)
lemma monom_one_Suc2:
"monom P \<one> (Suc n) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
proof (induct n)
case 0 show ?case by simp
next
case Suc
{
fix k:: nat
assume hypo: "monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
then show "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k)"
proof -
have lhs: "monom P \<one> (Suc (Suc k)) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
unfolding monom_one_Suc [of "Suc k"] unfolding hypo ..
note cl = monom_closed [OF R.one_closed, of 1]
note clk = monom_closed [OF R.one_closed, of k]
have rhs: "monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> (Suc k) = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1"
unfolding monom_one_Suc [of k] unfolding sym [OF m_assoc [OF cl clk cl]] ..
from lhs rhs show ?thesis by simp
qed
}
qed
text\<open>The following corollary follows from lemmas @{thm "monom_one_Suc"}
and @{thm "monom_one_Suc2"}, and is trivial in @{term UP_cring}\<close>
corollary monom_one_comm: shows "monom P \<one> k \<otimes>\<^bsub>P\<^esub> monom P \<one> 1 = monom P \<one> 1 \<otimes>\<^bsub>P\<^esub> monom P \<one> k"
unfolding monom_one_Suc [symmetric] monom_one_Suc2 [symmetric] ..
lemma monom_mult_smult:
"[| a \<in> carrier R; b \<in> carrier R |] ==> monom P (a \<otimes> b) n = a \<odot>\<^bsub>P\<^esub> monom P b n"
by (rule up_eqI) simp_all
lemma monom_one_mult:
"monom P \<one> (n + m) = monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m"
proof (induct n)
case 0 show ?case by simp
next
case Suc then show ?case
unfolding add_Suc unfolding monom_one_Suc unfolding Suc.hyps
using m_assoc monom_one_comm [of m] by simp
qed
lemma monom_one_mult_comm: "monom P \<one> n \<otimes>\<^bsub>P\<^esub> monom P \<one> m = monom P \<one> m \<otimes>\<^bsub>P\<^esub> monom P \<one> n"
unfolding monom_one_mult [symmetric] by (rule up_eqI) simp_all
lemma monom_mult [simp]:
assumes a_in_R: "a \<in> carrier R" and b_in_R: "b \<in> carrier R"
shows "monom P (a \<otimes> b) (n + m) = monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m"
proof (rule up_eqI)
fix k
show "coeff P (monom P (a \<otimes> b) (n + m)) k = coeff P (monom P a n \<otimes>\<^bsub>P\<^esub> monom P b m) k"
proof (cases "n + m = k")
case True
{
show ?thesis
unfolding True [symmetric]
coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of "n + m"]
coeff_monom [OF a_in_R, of n] coeff_monom [OF b_in_R, of m]
using R.finsum_cong [of "{.. n + m}" "{.. n + m}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = n + m - i then b else \<zero>))"
"(\<lambda>i. if n = i then a \<otimes> b else \<zero>)"]
a_in_R b_in_R
unfolding simp_implies_def
using R.finsum_singleton [of n "{.. n + m}" "(\<lambda>i. a \<otimes> b)"]
unfolding Pi_def by auto
}
next
case False
{
show ?thesis
unfolding coeff_monom [OF R.m_closed [OF a_in_R b_in_R], of "n + m" k] apply (simp add: False)
unfolding coeff_mult [OF monom_closed [OF a_in_R, of n] monom_closed [OF b_in_R, of m], of k]
unfolding coeff_monom [OF a_in_R, of n] unfolding coeff_monom [OF b_in_R, of m] using False
using R.finsum_cong [of "{..k}" "{..k}" "(\<lambda>i. (if n = i then a else \<zero>) \<otimes> (if m = k - i then b else \<zero>))" "(\<lambda>i. \<zero>)"]
unfolding Pi_def simp_implies_def using a_in_R b_in_R by force
}
qed
qed (simp_all add: a_in_R b_in_R)
lemma monom_a_inv [simp]:
"a \<in> carrier R ==> monom P (\<ominus> a) n = \<ominus>\<^bsub>P\<^esub> monom P a n"
by (rule up_eqI) auto
lemma monom_inj:
"inj_on (\<lambda>a. monom P a n) (carrier R)"
proof (rule inj_onI)
fix x y
assume R: "x \<in> carrier R" "y \<in> carrier R" and eq: "monom P x n = monom P y n"
then have "coeff P (monom P x n) n = coeff P (monom P y n) n" by simp
with R show "x = y" by simp
qed
end
subsection \<open>The Degree Function\<close>
definition
deg :: "[('a, 'm) ring_scheme, nat => 'a] => nat"
where "deg R p = (LEAST n. bound \<zero>\<^bsub>R\<^esub> n (coeff (UP R) p))"
context UP_ring
begin
lemma deg_aboveI:
"[| (!!m. n < m ==> coeff P p m = \<zero>); p \<in> carrier P |] ==> deg R p <= n"
by (unfold deg_def P_def) (fast intro: Least_le)
(*
lemma coeff_bound_ex: "EX n. bound n (coeff p)"
proof -
have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
then show ?thesis ..
qed
lemma bound_coeff_obtain:
assumes prem: "(!!n. bound n (coeff p) ==> P)" shows "P"
proof -
have "(\<lambda>n. coeff p n) : UP" by (simp add: coeff_def Rep_UP)
then obtain n where "bound n (coeff p)" by (unfold UP_def) fast
with prem show P .
qed
*)
lemma deg_aboveD:
assumes "deg R p < m" and "p \<in> carrier P"
shows "coeff P p m = \<zero>"
proof -
from \<open>p \<in> carrier P\<close> obtain n where "bound \<zero> n (coeff P p)"
by (auto simp add: UP_def P_def)
then have "bound \<zero> (deg R p) (coeff P p)"
by (auto simp: deg_def P_def dest: LeastI)
from this and \<open>deg R p < m\<close> show ?thesis ..
qed
lemma deg_belowI:
assumes non_zero: "n \<noteq> 0 \<Longrightarrow> coeff P p n \<noteq> \<zero>"
and R: "p \<in> carrier P"
shows "n \<le> deg R p"
\<comment> \<open>Logically, this is a slightly stronger version of
@{thm [source] deg_aboveD}\<close>
proof (cases "n=0")
case True then show ?thesis by simp
next
case False then have "coeff P p n \<noteq> \<zero>" by (rule non_zero)
then have "\<not> deg R p < n" by (fast dest: deg_aboveD intro: R)
then show ?thesis by arith
qed
lemma lcoeff_nonzero_deg:
assumes deg: "deg R p \<noteq> 0" and R: "p \<in> carrier P"
shows "coeff P p (deg R p) \<noteq> \<zero>"
proof -
from R obtain m where "deg R p \<le> m" and m_coeff: "coeff P p m \<noteq> \<zero>"
proof -
have minus: "\<And>(n::nat) m. n \<noteq> 0 \<Longrightarrow> (n - Suc 0 < m) = (n \<le> m)"
by arith
from deg have "deg R p - 1 < (LEAST n. bound \<zero> n (coeff P p))"
by (unfold deg_def P_def) simp
then have "\<not> bound \<zero> (deg R p - 1) (coeff P p)" by (rule not_less_Least)
then have "\<exists>m. deg R p - 1 < m \<and> coeff P p m \<noteq> \<zero>"
by (unfold bound_def) fast
then have "\<exists>m. deg R p \<le> m \<and> coeff P p m \<noteq> \<zero>" by (simp add: deg minus)
then show ?thesis by (auto intro: that)
qed
with deg_belowI R have "deg R p = m" by fastforce
with m_coeff show ?thesis by simp
qed
lemma lcoeff_nonzero_nonzero:
assumes deg: "deg R p = 0" and nonzero: "p \<noteq> \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
shows "coeff P p 0 \<noteq> \<zero>"
proof -
have "\<exists>m. coeff P p m \<noteq> \<zero>"
proof (rule classical)
assume "\<not> ?thesis"
with R have "p = \<zero>\<^bsub>P\<^esub>" by (auto intro: up_eqI)
with nonzero show ?thesis by contradiction
qed
then obtain m where coeff: "coeff P p m \<noteq> \<zero>" ..
from this and R have "m \<le> deg R p" by (rule deg_belowI)
then have "m = 0" by (simp add: deg)
with coeff show ?thesis by simp
qed
lemma lcoeff_nonzero:
assumes neq: "p \<noteq> \<zero>\<^bsub>P\<^esub>" and R: "p \<in> carrier P"
shows "coeff P p (deg R p) \<noteq> \<zero>"
proof (cases "deg R p = 0")
case True with neq R show ?thesis by (simp add: lcoeff_nonzero_nonzero)
next
case False with neq R show ?thesis by (simp add: lcoeff_nonzero_deg)
qed
lemma deg_eqI:
"[| \<And>m. n < m \<Longrightarrow> coeff P p m = \<zero>;
\<And>n. n \<noteq> 0 \<Longrightarrow> coeff P p n \<noteq> \<zero>; p \<in> carrier P |] ==> deg R p = n"
by (fast intro: le_antisym deg_aboveI deg_belowI)
text \<open>Degree and polynomial operations\<close>
lemma deg_add [simp]:
"p \<in> carrier P \<Longrightarrow> q \<in> carrier P \<Longrightarrow>
deg R (p \<oplus>\<^bsub>P\<^esub> q) \<le> max (deg R p) (deg R q)"
by(rule deg_aboveI)(simp_all add: deg_aboveD)
lemma deg_monom_le:
"a \<in> carrier R \<Longrightarrow> deg R (monom P a n) \<le> n"
by (intro deg_aboveI) simp_all
lemma deg_monom [simp]:
"[| a \<noteq> \<zero>; a \<in> carrier R |] ==> deg R (monom P a n) = n"
by (fastforce intro: le_antisym deg_aboveI deg_belowI)
lemma deg_const [simp]:
assumes R: "a \<in> carrier R" shows "deg R (monom P a 0) = 0"
proof (rule le_antisym)
show "deg R (monom P a 0) \<le> 0" by (rule deg_aboveI) (simp_all add: R)
next
show "0 \<le> deg R (monom P a 0)" by (rule deg_belowI) (simp_all add: R)
qed
lemma deg_zero [simp]:
"deg R \<zero>\<^bsub>P\<^esub> = 0"
proof (rule le_antisym)
show "deg R \<zero>\<^bsub>P\<^esub> \<le> 0" by (rule deg_aboveI) simp_all
next
show "0 \<le> deg R \<zero>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
qed
lemma deg_one [simp]:
"deg R \<one>\<^bsub>P\<^esub> = 0"
proof (rule le_antisym)
show "deg R \<one>\<^bsub>P\<^esub> \<le> 0" by (rule deg_aboveI) simp_all
next
show "0 \<le> deg R \<one>\<^bsub>P\<^esub>" by (rule deg_belowI) simp_all
qed
lemma deg_uminus [simp]:
assumes R: "p \<in> carrier P" shows "deg R (\<ominus>\<^bsub>P\<^esub> p) = deg R p"
proof (rule le_antisym)
show "deg R (\<ominus>\<^bsub>P\<^esub> p) \<le> deg R p" by (simp add: deg_aboveI deg_aboveD R)
next
show "deg R p \<le> deg R (\<ominus>\<^bsub>P\<^esub> p)"
by (simp add: deg_belowI lcoeff_nonzero_deg
inj_on_eq_iff [OF R.a_inv_inj, of _ "\<zero>", simplified] R)
qed
text\<open>The following lemma is later \emph{overwritten} by the most
specific one for domains, \<open>deg_smult\<close>.\<close>
lemma deg_smult_ring [simp]:
"[| a \<in> carrier R; p \<in> carrier P |] ==>
deg R (a \<odot>\<^bsub>P\<^esub> p) \<le> (if a = \<zero> then 0 else deg R p)"
by (cases "a = \<zero>") (simp add: deg_aboveI deg_aboveD)+
end
context UP_domain
begin
lemma deg_smult [simp]:
assumes R: "a \<in> carrier R" "p \<in> carrier P"
shows "deg R (a \<odot>\<^bsub>P\<^esub> p) = (if a = \<zero> then 0 else deg R p)"
proof (rule le_antisym)
show "deg R (a \<odot>\<^bsub>P\<^esub> p) \<le> (if a = \<zero> then 0 else deg R p)"
using R by (rule deg_smult_ring)
next
show "(if a = \<zero> then 0 else deg R p) \<le> deg R (a \<odot>\<^bsub>P\<^esub> p)"
proof (cases "a = \<zero>")
qed (simp, simp add: deg_belowI lcoeff_nonzero_deg integral_iff R)
qed
end
context UP_ring
begin
lemma deg_mult_ring:
assumes R: "p \<in> carrier P" "q \<in> carrier P"
shows "deg R (p \<otimes>\<^bsub>P\<^esub> q) \<le> deg R p + deg R q"
proof (rule deg_aboveI)
fix m
assume boundm: "deg R p + deg R q < m"
{
fix k i
assume boundk: "deg R p + deg R q < k"
then have "coeff P p i \<otimes> coeff P q (k - i) = \<zero>"
proof (cases "deg R p < i")
case True then show ?thesis by (simp add: deg_aboveD R)
next
case False with boundk have "deg R q < k - i" by arith
then show ?thesis by (simp add: deg_aboveD R)
qed
}
with boundm R show "coeff P (p \<otimes>\<^bsub>P\<^esub> q) m = \<zero>" by simp
qed (simp add: R)
end
context UP_domain
begin
lemma deg_mult [simp]:
"[| p \<noteq> \<zero>\<^bsub>P\<^esub>; q \<noteq> \<zero>\<^bsub>P\<^esub>; p \<in> carrier P; q \<in> carrier P |] ==>
deg R (p \<otimes>\<^bsub>P\<^esub> q) = deg R p + deg R q"
proof (rule le_antisym)
assume "p \<in> carrier P" " q \<in> carrier P"
then show "deg R (p \<otimes>\<^bsub>P\<^esub> q) \<le> deg R p + deg R q" by (rule deg_mult_ring)
next
let ?s = "(\<lambda>i. coeff P p i \<otimes> coeff P q (deg R p + deg R q - i))"
assume R: "p \<in> carrier P" "q \<in> carrier P" and nz: "p \<noteq> \<zero>\<^bsub>P\<^esub>" "q \<noteq> \<zero>\<^bsub>P\<^esub>"
have less_add_diff: "!!(k::nat) n m. k < n ==> m < n + m - k" by arith
show "deg R p + deg R q \<le> deg R (p \<otimes>\<^bsub>P\<^esub> q)"
proof (rule deg_belowI, simp add: R)
have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
= (\<Oplus>i \<in> {..< deg R p} \<union> {deg R p .. deg R p + deg R q}. ?s i)"
by (simp only: ivl_disj_un_one)
also have "... = (\<Oplus>i \<in> {deg R p .. deg R p + deg R q}. ?s i)"
by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint ivl_disj_int_one
deg_aboveD less_add_diff R Pi_def)
also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
= coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) \<noteq> \<zero>"
by (simp add: integral_iff lcoeff_nonzero R)
qed (simp add: R)
qed
end
text\<open>The following lemmas also can be lifted to @{term UP_ring}.\<close>
context UP_ring
begin
lemma coeff_finsum:
assumes fin: "finite A"
shows "p \<in> A \<rightarrow> carrier P ==>
coeff P (finsum P p A) k = (\<Oplus>i \<in> A. coeff P (p i) k)"
using fin by induct (auto simp: Pi_def)
lemma up_repr:
assumes R: "p \<in> carrier P"
shows "(\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. monom P (coeff P p i) i) = p"
proof (rule up_eqI)
let ?s = "(\<lambda>i. monom P (coeff P p i) i)"
fix k
from R have RR: "!!i. (if i = k then coeff P p i else \<zero>) \<in> carrier R"
by simp
show "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k = coeff P p k"
proof (cases "k \<le> deg R p")
case True
hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k} \<union> {k<..deg R p}. ?s i) k"
by (simp only: ivl_disj_un_one)
also from True
have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..k}. ?s i) k"
by (simp cong: R.finsum_cong add: R.finsum_Un_disjoint
ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
also
have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff P p k"
by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
finally show ?thesis .
next
case False
hence "coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..deg R p}. ?s i) k =
coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff P p k"
by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
finally show ?thesis .
qed
qed (simp_all add: R Pi_def)
lemma up_repr_le:
"[| deg R p <= n; p \<in> carrier P |] ==>