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)