461 by (induct n, simp add: monom_0, simp add: monom_Suc) |
461 by (induct n, simp add: monom_0, simp add: monom_Suc) |
462 |
462 |
463 |
463 |
464 subsection {* Multiplication of polynomials *} |
464 subsection {* Multiplication of polynomials *} |
465 |
465 |
466 lemma Poly_mult_lemma: |
466 text {* TODO: move to SetInterval.thy *} |
467 fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0" and m n :: nat |
|
468 assumes "\<forall>i>m. f i = 0" |
|
469 assumes "\<forall>j>n. g j = 0" |
|
470 shows "\<forall>k>m+n. (\<Sum>i\<le>k. f i * g (k-i)) = 0" |
|
471 proof (clarify) |
|
472 fix k :: nat |
|
473 assume "m + n < k" |
|
474 show "(\<Sum>i\<le>k. f i * g (k - i)) = 0" |
|
475 proof (rule setsum_0' [rule_format]) |
|
476 fix i :: nat |
|
477 assume "i \<in> {..k}" hence "i \<le> k" by simp |
|
478 with `m + n < k` have "m < i \<or> n < k - i" by arith |
|
479 thus "f i * g (k - i) = 0" |
|
480 using prems by auto |
|
481 qed |
|
482 qed |
|
483 |
|
484 lemma Poly_mult: |
|
485 fixes f g :: "nat \<Rightarrow> 'a::comm_semiring_0" |
|
486 shows "\<lbrakk>f \<in> Poly; g \<in> Poly\<rbrakk> \<Longrightarrow> (\<lambda>n. \<Sum>i\<le>n. f i * g (n-i)) \<in> Poly" |
|
487 unfolding Poly_def |
|
488 by (safe, rule exI, rule Poly_mult_lemma) |
|
489 |
|
490 lemma poly_mult_assoc_lemma: |
|
491 fixes k :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" |
|
492 shows "(\<Sum>j\<le>k. \<Sum>i\<le>j. f i (j - i) (n - j)) = |
|
493 (\<Sum>j\<le>k. \<Sum>i\<le>k - j. f j i (n - j - i))" |
|
494 proof (induct k) |
|
495 case 0 show ?case by simp |
|
496 next |
|
497 case (Suc k) thus ?case |
|
498 by (simp add: Suc_diff_le setsum_addf add_assoc |
|
499 cong: strong_setsum_cong) |
|
500 qed |
|
501 |
|
502 lemma poly_mult_commute_lemma: |
|
503 fixes n :: nat and f :: "nat \<Rightarrow> nat \<Rightarrow> 'a::comm_monoid_add" |
|
504 shows "(\<Sum>i\<le>n. f i (n - i)) = (\<Sum>i\<le>n. f (n - i) i)" |
|
505 proof (rule setsum_reindex_cong) |
|
506 show "inj_on (\<lambda>i. n - i) {..n}" |
|
507 by (rule inj_onI) simp |
|
508 show "{..n} = (\<lambda>i. n - i) ` {..n}" |
|
509 by (auto, rule_tac x="n - x" in image_eqI, simp_all) |
|
510 next |
|
511 fix i assume "i \<in> {..n}" |
|
512 hence "n - (n - i) = i" by simp |
|
513 thus "f (n - i) i = f (n - i) (n - (n - i))" by simp |
|
514 qed |
|
515 |
|
516 text {* TODO: move to appropriate theory *} |
|
517 lemma setsum_atMost_Suc_shift: |
467 lemma setsum_atMost_Suc_shift: |
518 fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" |
468 fixes f :: "nat \<Rightarrow> 'a::comm_monoid_add" |
519 shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
469 shows "(\<Sum>i\<le>Suc n. f i) = f 0 + (\<Sum>i\<le>n. f (Suc i))" |
520 proof (induct n) |
470 proof (induct n) |
521 case 0 show ?case by simp |
471 case 0 show ?case by simp |
536 instantiation poly :: (comm_semiring_0) comm_semiring_0 |
486 instantiation poly :: (comm_semiring_0) comm_semiring_0 |
537 begin |
487 begin |
538 |
488 |
539 definition |
489 definition |
540 times_poly_def: |
490 times_poly_def: |
541 "p * q = Abs_poly (\<lambda>n. \<Sum>i\<le>n. coeff p i * coeff q (n-i))" |
491 "p * q = poly_rec 0 (\<lambda>a p pq. smult a q + pCons 0 pq) p" |
542 |
492 |
543 lemma coeff_mult: |
493 lemma mult_poly_0_left: "(0::'a poly) * q = 0" |
544 "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))" |
494 unfolding times_poly_def by (simp add: poly_rec_0) |
545 unfolding times_poly_def |
495 |
546 by (simp add: Abs_poly_inverse coeff Poly_mult) |
496 lemma mult_pCons_left [simp]: |
|
497 "pCons a p * q = smult a q + pCons 0 (p * q)" |
|
498 unfolding times_poly_def by (simp add: poly_rec_pCons) |
|
499 |
|
500 lemma mult_poly_0_right: "p * (0::'a poly) = 0" |
|
501 by (induct p, simp add: mult_poly_0_left, simp) |
|
502 |
|
503 lemma mult_pCons_right [simp]: |
|
504 "p * pCons a q = smult a p + pCons 0 (p * q)" |
|
505 by (induct p, simp add: mult_poly_0_left, simp add: ring_simps) |
|
506 |
|
507 lemmas mult_poly_0 = mult_poly_0_left mult_poly_0_right |
|
508 |
|
509 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" |
|
510 by (induct p, simp add: mult_poly_0, simp add: smult_add_right) |
|
511 |
|
512 lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" |
|
513 by (induct q, simp add: mult_poly_0, simp add: smult_add_right) |
|
514 |
|
515 lemma mult_poly_add_left: |
|
516 fixes p q r :: "'a poly" |
|
517 shows "(p + q) * r = p * r + q * r" |
|
518 by (induct r, simp add: mult_poly_0, |
|
519 simp add: smult_distribs group_simps) |
547 |
520 |
548 instance proof |
521 instance proof |
549 fix p q r :: "'a poly" |
522 fix p q r :: "'a poly" |
550 show 0: "0 * p = 0" |
523 show 0: "0 * p = 0" |
551 by (simp add: expand_poly_eq coeff_mult) |
524 by (rule mult_poly_0_left) |
552 show "p * 0 = 0" |
525 show "p * 0 = 0" |
553 by (simp add: expand_poly_eq coeff_mult) |
526 by (rule mult_poly_0_right) |
554 show "(p + q) * r = p * r + q * r" |
527 show "(p + q) * r = p * r + q * r" |
555 by (simp add: expand_poly_eq coeff_mult left_distrib setsum_addf) |
528 by (rule mult_poly_add_left) |
556 show "(p * q) * r = p * (q * r)" |
529 show "(p * q) * r = p * (q * r)" |
557 proof (rule poly_ext) |
530 by (induct p, simp add: mult_poly_0, simp add: mult_poly_add_left) |
558 fix n :: nat |
|
559 have "(\<Sum>j\<le>n. \<Sum>i\<le>j. coeff p i * coeff q (j - i) * coeff r (n - j)) = |
|
560 (\<Sum>j\<le>n. \<Sum>i\<le>n - j. coeff p j * coeff q i * coeff r (n - j - i))" |
|
561 by (rule poly_mult_assoc_lemma) |
|
562 thus "coeff ((p * q) * r) n = coeff (p * (q * r)) n" |
|
563 by (simp add: coeff_mult setsum_right_distrib |
|
564 setsum_left_distrib mult_assoc) |
|
565 qed |
|
566 show "p * q = q * p" |
531 show "p * q = q * p" |
567 proof (rule poly_ext) |
532 by (induct p, simp add: mult_poly_0, simp) |
568 fix n :: nat |
|
569 have "(\<Sum>i\<le>n. coeff p i * coeff q (n - i)) = |
|
570 (\<Sum>i\<le>n. coeff p (n - i) * coeff q i)" |
|
571 by (rule poly_mult_commute_lemma) |
|
572 thus "coeff (p * q) n = coeff (q * p) n" |
|
573 by (simp add: coeff_mult mult_commute) |
|
574 qed |
|
575 qed |
533 qed |
576 |
534 |
577 end |
535 end |
578 |
536 |
|
537 lemma coeff_mult: |
|
538 "coeff (p * q) n = (\<Sum>i\<le>n. coeff p i * coeff q (n-i))" |
|
539 proof (induct p arbitrary: n) |
|
540 case 0 show ?case by simp |
|
541 next |
|
542 case (pCons a p n) thus ?case |
|
543 by (cases n, simp, simp add: setsum_atMost_Suc_shift |
|
544 del: setsum_atMost_Suc) |
|
545 qed |
|
546 |
579 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q" |
547 lemma degree_mult_le: "degree (p * q) \<le> degree p + degree q" |
580 apply (rule degree_le, simp add: coeff_mult) |
548 apply (rule degree_le) |
581 apply (rule Poly_mult_lemma) |
549 apply (induct p) |
582 apply (simp_all add: coeff_eq_0) |
550 apply simp |
|
551 apply (simp add: coeff_eq_0 coeff_pCons split: nat.split) |
583 done |
552 done |
584 |
|
585 lemma mult_pCons_left [simp]: |
|
586 "pCons a p * q = smult a q + pCons 0 (p * q)" |
|
587 apply (rule poly_ext) |
|
588 apply (case_tac n) |
|
589 apply (simp add: coeff_mult) |
|
590 apply (simp add: coeff_mult setsum_atMost_Suc_shift |
|
591 del: setsum_atMost_Suc) |
|
592 done |
|
593 |
|
594 lemma mult_pCons_right [simp]: |
|
595 "p * pCons a q = smult a p + pCons 0 (p * q)" |
|
596 using mult_pCons_left [of a q p] by (simp add: mult_commute) |
|
597 |
|
598 lemma mult_smult_left [simp]: "smult a p * q = smult a (p * q)" |
|
599 by (induct p, simp, simp add: smult_add_right) |
|
600 |
|
601 lemma mult_smult_right [simp]: "p * smult a q = smult a (p * q)" |
|
602 by (induct q, simp, simp add: smult_add_right) |
|
603 |
553 |
604 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)" |
554 lemma mult_monom: "monom a m * monom b n = monom (a * b) (m + n)" |
605 by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc) |
555 by (induct m, simp add: monom_0 smult_monom, simp add: monom_Suc) |
606 |
556 |
607 |
557 |