src/HOL/Algebra/UnivPoly.thy
 changeset 32456 341c83339aeb parent 32436 10cd49e0c067 child 32960 69916a850301
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Sat Aug 29 14:31:39 2009 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Mon Aug 31 14:09:42 2009 +0200
1.3 @@ -592,15 +592,14 @@
1.4          proof (cases "n = k")
1.5            case True
1.6            then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
1.7 -            by (simp cong: R.finsum_cong add: ivl_disj_int_singleton Pi_def)
1.8 +            by (simp cong: R.finsum_cong add: Pi_def)
1.9            also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
1.10              by (simp only: ivl_disj_un_singleton)
1.11            finally show ?thesis .
1.12          next
1.13            case False with n_le_k have n_less_k: "n < k" by arith
1.14            with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
1.15 -            by (simp add: R.finsum_Un_disjoint f1 f2
1.16 -              ivl_disj_int_singleton Pi_def del: Un_insert_right)
1.17 +            by (simp add: R.finsum_Un_disjoint f1 f2 Pi_def del: Un_insert_right)
1.18            also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
1.19              by (simp only: ivl_disj_un_singleton)
1.20            also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
1.21 @@ -939,8 +938,7 @@
1.22      also have "...= (\<Oplus>i \<in> {deg R p} \<union> {deg R p <.. deg R p + deg R q}. ?s i)"
1.23        by (simp only: ivl_disj_un_singleton)
1.24      also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
1.25 -      by (simp cong: R.finsum_cong
1.26 -	add: ivl_disj_int_singleton deg_aboveD R Pi_def)
1.27 +      by (simp cong: R.finsum_cong add: deg_aboveD R Pi_def)
1.28      finally have "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i)
1.29        = coeff P p (deg R p) \<otimes> coeff P q (deg R q)" .
1.30      with nz show "(\<Oplus>i \<in> {.. deg R p + deg R q}. ?s i) ~= \<zero>"
1.31 @@ -983,8 +981,7 @@
1.32      have "... = coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<k} \<union> {k}. ?s i) k"
1.33        by (simp only: ivl_disj_un_singleton)
1.34      also have "... = coeff P p k"
1.35 -      by (simp cong: R.finsum_cong
1.36 -	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R RR Pi_def)
1.37 +      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R RR Pi_def)
1.38      finally show ?thesis .
1.39    next
1.40      case False
1.41 @@ -992,8 +989,7 @@
1.42            coeff P (\<Oplus>\<^bsub>P\<^esub> i \<in> {..<deg R p} \<union> {deg R p}. ?s i) k"
1.43        by (simp only: ivl_disj_un_singleton)
1.44      also from False have "... = coeff P p k"
1.45 -      by (simp cong: R.finsum_cong
1.46 -	add: ivl_disj_int_singleton coeff_finsum deg_aboveD R Pi_def)
1.47 +      by (simp cong: R.finsum_cong add: coeff_finsum deg_aboveD R Pi_def)
1.48      finally show ?thesis .
1.49    qed
1.50  qed (simp_all add: R Pi_def)
```