src/HOL/Algebra/UnivPoly.thy
 changeset 15045 d59f7e2e18d3 parent 14963 d584e32f7d46 child 15076 4b3d280ef06a
```     1.1 --- a/src/HOL/Algebra/UnivPoly.thy	Thu Jul 15 08:38:37 2004 +0200
1.2 +++ b/src/HOL/Algebra/UnivPoly.thy	Thu Jul 15 13:11:34 2004 +0200
1.3 @@ -646,13 +646,13 @@
1.4          "!!i. [| n < i; i <= n + m |] ==> n + m - i < m" by arith
1.5        from True have "coeff P (monom P \<one> (Suc n)) k = \<one>" by simp
1.6        also from True
1.7 -      have "... = (\<Oplus>i \<in> {..n(} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
1.8 +      have "... = (\<Oplus>i \<in> {..<n} \<union> {n}. coeff P (monom P \<one> n) i \<otimes>
1.9          coeff P (monom P \<one> 1) (k - i))"
1.10          by (simp cong: finsum_cong add: finsum_Un_disjoint Pi_def)
1.11        also have "... = (\<Oplus>i \<in>  {..n}. coeff P (monom P \<one> n) i \<otimes>
1.12          coeff P (monom P \<one> 1) (k - i))"
1.13          by (simp only: ivl_disj_un_singleton)
1.14 -      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. coeff P (monom P \<one> n) i \<otimes>
1.15 +      also from True have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. coeff P (monom P \<one> n) i \<otimes>
1.16          coeff P (monom P \<one> 1) (k - i))"
1.17          by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
1.18            order_less_imp_not_eq Pi_def)
1.19 @@ -668,10 +668,10 @@
1.20      from neq have "coeff P (monom P \<one> (Suc n)) k = \<zero>" by simp
1.21      also have "... = (\<Oplus>i \<in> {..k}. ?s i)"
1.22      proof -
1.23 -      have f1: "(\<Oplus>i \<in> {..n(}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
1.24 +      have f1: "(\<Oplus>i \<in> {..<n}. ?s i) = \<zero>" by (simp cong: finsum_cong add: Pi_def)
1.25        from neq have f2: "(\<Oplus>i \<in> {n}. ?s i) = \<zero>"
1.26          by (simp cong: finsum_cong add: Pi_def) arith
1.27 -      have f3: "n < k ==> (\<Oplus>i \<in> {)n..k}. ?s i) = \<zero>"
1.28 +      have f3: "n < k ==> (\<Oplus>i \<in> {n<..k}. ?s i) = \<zero>"
1.29          by (simp cong: finsum_cong add: order_less_imp_not_eq Pi_def)
1.30        show ?thesis
1.31        proof (cases "k < n")
1.32 @@ -681,7 +681,7 @@
1.33          show ?thesis
1.34          proof (cases "n = k")
1.35            case True
1.36 -          then have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
1.37 +          then have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
1.38              by (simp cong: finsum_cong add: finsum_Un_disjoint
1.39                ivl_disj_int_singleton Pi_def)
1.40            also from True have "... = (\<Oplus>i \<in> {..k}. ?s i)"
1.41 @@ -689,12 +689,12 @@
1.42            finally show ?thesis .
1.43          next
1.44            case False with n_le_k have n_less_k: "n < k" by arith
1.45 -          with neq have "\<zero> = (\<Oplus>i \<in> {..n(} \<union> {n}. ?s i)"
1.46 +          with neq have "\<zero> = (\<Oplus>i \<in> {..<n} \<union> {n}. ?s i)"
1.47              by (simp add: finsum_Un_disjoint f1 f2
1.48                ivl_disj_int_singleton Pi_def del: Un_insert_right)
1.49            also have "... = (\<Oplus>i \<in> {..n}. ?s i)"
1.50              by (simp only: ivl_disj_un_singleton)
1.51 -          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {)n..k}. ?s i)"
1.52 +          also from n_less_k neq have "... = (\<Oplus>i \<in> {..n} \<union> {n<..k}. ?s i)"
1.53              by (simp add: finsum_Un_disjoint f3 ivl_disj_int_one Pi_def)
1.54            also from n_less_k have "... = (\<Oplus>i \<in> {..k}. ?s i)"
1.55              by (simp only: ivl_disj_un_one)
1.56 @@ -976,12 +976,12 @@
1.57    show "deg R p + deg R q <= deg R (p \<otimes>\<^sub>2 q)"
1.58    proof (rule deg_belowI, simp add: R)
1.59      have "finsum R ?s {.. deg R p + deg R q}
1.60 -      = finsum R ?s ({.. deg R p(} Un {deg R p .. deg R p + deg R q})"
1.61 +      = finsum R ?s ({..< deg R p} Un {deg R p .. deg R p + deg R q})"
1.62        by (simp only: ivl_disj_un_one)
1.63      also have "... = finsum R ?s {deg R p .. deg R p + deg R q}"
1.64        by (simp cong: finsum_cong add: finsum_Un_disjoint ivl_disj_int_one
1.66 -    also have "...= finsum R ?s ({deg R p} Un {)deg R p .. deg R p + deg R q})"
1.67 +    also have "...= finsum R ?s ({deg R p} Un {deg R p <.. deg R p + deg R q})"
1.68        by (simp only: ivl_disj_un_singleton)
1.69      also have "... = coeff P p (deg R p) \<otimes> coeff P q (deg R q)"
1.70        by (simp cong: finsum_cong add: finsum_Un_disjoint
1.71 @@ -1015,14 +1015,14 @@
1.72    proof (cases "k <= deg R p")
1.73      case True
1.74      hence "coeff P (finsum P ?s {..deg R p}) k =
1.75 -          coeff P (finsum P ?s ({..k} Un {)k..deg R p})) k"
1.76 +          coeff P (finsum P ?s ({..k} Un {k<..deg R p})) k"
1.77        by (simp only: ivl_disj_un_one)
1.78      also from True
1.79      have "... = coeff P (finsum P ?s {..k}) k"
1.80        by (simp cong: finsum_cong add: finsum_Un_disjoint
1.81          ivl_disj_int_one order_less_imp_not_eq2 coeff_finsum R RR Pi_def)
1.82      also
1.83 -    have "... = coeff P (finsum P ?s ({..k(} Un {k})) k"
1.84 +    have "... = coeff P (finsum P ?s ({..<k} Un {k})) k"
1.85        by (simp only: ivl_disj_un_singleton)
1.86      also have "... = coeff P p k"
1.87        by (simp cong: finsum_cong add: setsum_Un_disjoint
1.88 @@ -1031,7 +1031,7 @@
1.89    next
1.90      case False
1.91      hence "coeff P (finsum P ?s {..deg R p}) k =
1.92 -          coeff P (finsum P ?s ({..deg R p(} Un {deg R p})) k"
1.93 +          coeff P (finsum P ?s ({..<deg R p} Un {deg R p})) k"
1.94        by (simp only: ivl_disj_un_singleton)
1.95      also from False have "... = coeff P p k"
1.96        by (simp cong: finsum_cong add: setsum_Un_disjoint ivl_disj_int_singleton
1.97 @@ -1046,7 +1046,7 @@
1.98  proof -
1.99    let ?s = "(%i. monom P (coeff P p i) i)"
1.100    assume R: "p \<in> carrier P" and "deg R p <= n"
1.101 -  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {)deg R p..n})"
1.102 +  then have "finsum P ?s {..n} = finsum P ?s ({..deg R p} Un {deg R p<..n})"
1.103      by (simp only: ivl_disj_un_one)
1.104    also have "... = finsum P ?s {..deg R p}"
1.105      by (simp cong: UP_finsum_cong add: UP_finsum_Un_disjoint ivl_disj_int_one
1.106 @@ -1206,12 +1206,12 @@
1.107    from f g have "(\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..k}. f i \<otimes> g (k - i)) =
1.108        (\<Oplus>k \<in> {..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1.109      by (simp add: diagonal_sum Pi_def)
1.110 -  also have "... = (\<Oplus>k \<in> {..n} \<union> {)n..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1.111 +  also have "... = (\<Oplus>k \<in> {..n} \<union> {n<..n + m}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1.112      by (simp only: ivl_disj_un_one)
1.113    also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..n + m - k}. f k \<otimes> g i)"
1.114      by (simp cong: finsum_cong
1.115        add: bound.bound [OF bf] finsum_Un_disjoint ivl_disj_int_one Pi_def)
1.116 -  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {)m..n + m - k}. f k \<otimes> g i)"
1.117 +  also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m} \<union> {m<..n + m - k}. f k \<otimes> g i)"
1.119    also from f g have "... = (\<Oplus>k \<in> {..n}. \<Oplus>i \<in> {..m}. f k \<otimes> g i)"
1.120      by (simp cong: finsum_cong
1.121 @@ -1262,7 +1262,7 @@
1.122    proof (simp only: eval_on_carrier UP_mult_closed)
1.123      from RS have
1.124        "(\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)}. h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
1.125 -      (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {)deg R (p \<otimes>\<^sub>3 q)..deg R p + deg R q}.
1.126 +      (\<Oplus>\<^sub>2 i \<in> {..deg R (p \<otimes>\<^sub>3 q)} \<union> {deg R (p \<otimes>\<^sub>3 q)<..deg R p + deg R q}.
1.127          h (coeff P (p \<otimes>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
1.128        by (simp cong: finsum_cong
1.129          add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1.130 @@ -1292,7 +1292,7 @@
1.131    proof (simp only: eval_on_carrier UP_a_closed)
1.132      from RS have
1.133        "(\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)}. h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
1.134 -      (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {)deg R (p \<oplus>\<^sub>3 q)..max (deg R p) (deg R q)}.
1.135 +      (\<Oplus>\<^sub>2i \<in> {..deg R (p \<oplus>\<^sub>3 q)} \<union> {deg R (p \<oplus>\<^sub>3 q)<..max (deg R p) (deg R q)}.
1.136          h (coeff P (p \<oplus>\<^sub>3 q) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
1.137        by (simp cong: finsum_cong
1.138          add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def
1.139 @@ -1306,9 +1306,9 @@
1.140        by (simp cong: finsum_cong
1.141          add: l_distr deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
1.142      also have "... =
1.143 -        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {)deg R p..max (deg R p) (deg R q)}.
1.144 +        (\<Oplus>\<^sub>2 i \<in> {..deg R p} \<union> {deg R p<..max (deg R p) (deg R q)}.
1.145            h (coeff P p i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) \<oplus>\<^sub>2
1.146 -        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {)deg R q..max (deg R p) (deg R q)}.
1.147 +        (\<Oplus>\<^sub>2 i \<in> {..deg R q} \<union> {deg R q<..max (deg R p) (deg R q)}.
1.148            h (coeff P q i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
1.149        by (simp only: ivl_disj_un_one le_maxI1 le_maxI2)
1.150      also from RS have "... =
1.151 @@ -1392,7 +1392,7 @@
1.152    assume S: "s \<in> carrier S"
1.153    then have
1.154      "(\<Oplus>\<^sub>2 i \<in> {..deg R (monom P \<one> 1)}. h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i) =
1.155 -    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {)deg R (monom P \<one> 1)..1}.
1.156 +    (\<Oplus>\<^sub>2i\<in>{..deg R (monom P \<one> 1)} \<union> {deg R (monom P \<one> 1)<..1}.
1.157        h (coeff P (monom P \<one> 1) i) \<otimes>\<^sub>2 s (^)\<^sub>2 i)"
1.158      by (simp cong: finsum_cong del: coeff_monom
1.159        add: deg_aboveD finsum_Un_disjoint ivl_disj_int_one Pi_def)
```