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.65          deg_aboveD less_add_diff R Pi_def)
    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.118      by (simp cong: finsum_cong add: ivl_disj_un_one le_add_diff Pi_def)
   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)