--- a/src/HOL/Algebra/poly/UnivPoly2.thy Thu Jul 15 08:38:37 2004 +0200
+++ b/src/HOL/Algebra/poly/UnivPoly2.thy Thu Jul 15 13:11:34 2004 +0200
@@ -643,12 +643,12 @@
show "deg p + deg q <= deg (p * q)"
proof (rule deg_belowI, simp)
have "setsum ?s {.. deg p + deg q}
- = setsum ?s ({.. deg p(} Un {deg p .. deg p + deg q})"
+ = setsum ?s ({..< deg p} Un {deg p .. deg p + deg q})"
by (simp only: ivl_disj_un_one)
also have "... = setsum ?s {deg p .. deg p + deg q}"
by (simp add: setsum_Un_disjoint ivl_disj_int_one
setsum_0 deg_aboveD less_add_diff)
- also have "... = setsum ?s ({deg p} Un {)deg p .. deg p + deg q})"
+ also have "... = setsum ?s ({deg p} Un {deg p <.. deg p + deg q})"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff p (deg p) * coeff q (deg q)"
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
@@ -686,14 +686,14 @@
proof (cases "k <= deg p")
case True
hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..k} Un {)k..deg p})) k"
+ coeff (setsum ?s ({..k} Un {k<..deg p})) k"
by (simp only: ivl_disj_un_one)
also from True
have "... = coeff (setsum ?s {..k}) k"
by (simp add: setsum_Un_disjoint ivl_disj_int_one order_less_imp_not_eq2
setsum_0 coeff_natsum )
also
- have "... = coeff (setsum ?s ({..k(} Un {k})) k"
+ have "... = coeff (setsum ?s ({..<k} Un {k})) k"
by (simp only: ivl_disj_un_singleton)
also have "... = coeff p k"
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
@@ -702,7 +702,7 @@
next
case False
hence "coeff (setsum ?s {..deg p}) k =
- coeff (setsum ?s ({..deg p(} Un {deg p})) k"
+ coeff (setsum ?s ({..<deg p} Un {deg p})) k"
by (simp only: ivl_disj_un_singleton)
also from False have "... = coeff p k"
by (simp add: setsum_Un_disjoint ivl_disj_int_singleton
@@ -716,7 +716,7 @@
proof -
let ?s = "(%i. monom (coeff p i) i)"
assume "deg p <= n"
- then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {)deg p..n})"
+ then have "setsum ?s {..n} = setsum ?s ({..deg p} Un {deg p<..n})"
by (simp only: ivl_disj_un_one)
also have "... = setsum ?s {..deg p}"
by (simp add: setsum_Un_disjoint ivl_disj_int_one