diff -r a0cf3a19ee36 -r 3ce1cb7a24f0 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:42 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Fri Feb 18 11:48:53 2005 +0100
@@ -11,13 +11,15 @@
 imports SEQ Lim
 begin
 
+declare atLeastLessThan_empty[simp];
+
 syntax sumr :: "[nat,nat,(nat=>real)] => real"
 translations
   "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
 
 constdefs
    sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
-   "f sums s  == (%n. sumr 0 n f) ----> s"
+   "f sums s  == (%n. setsum f {0..<n}) ----> s"
 
    summable :: "(nat=>real) => bool"
    "summable f == (\<exists>s. f sums s)"
@@ -27,9 +29,10 @@
 
 
 lemma sumr_Suc [simp]:
-     "sumr m (Suc n) f = (if n < m then 0 else sumr m n f + f(n))"
-by (simp add: atLeastLessThanSuc)
+  "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
+by (simp add: atLeastLessThanSuc add_commute)
 
+(*
 lemma sumr_add: "sumr m n f + sumr m n g = sumr m n (%n. f n + g n)"
 by (simp add: setsum_addf)
 
@@ -42,13 +45,22 @@
 apply (rename_tac k) 
 apply (subgoal_tac "n=k", auto) 
 done
+*)
+
+lemma sumr_split_add: "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+  setsum f {m..<n} + setsum f {n..<p} = setsum f {m..<p::nat}"
+by (simp add:setsum_Un_disjoint[symmetric] ivl_disj_int ivl_disj_un)
 
 lemma sumr_split_add_minus:
      "n < p ==> sumr 0 p f + - sumr 0 n f = sumr n p (f::nat=>real)"
-apply (drule_tac f1 = f in sumr_split_add [symmetric])
+using sumr_split_add [of 0 n p f,symmetric]
 apply (simp add: add_ac)
 done
 
+lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
+by (simp add: diff_minus setsum_addf real_of_nat_def)
+
+(*
 lemma sumr_rabs: "abs(sumr m n  (f::nat=>real)) \<le> sumr m n (%i. abs(f i))"
 by (simp add: setsum_abs)
 
@@ -60,14 +72,12 @@
      "(\<forall>r. m \<le> r & r < n --> f r = g r) ==> sumr m n f = sumr m n g"
 by (auto intro: setsum_cong) 
 
-lemma sumr_diff_mult_const: "sumr 0 n f - (real n*r) = sumr 0 n (%i. f i - r)"
-by (simp add: diff_minus setsum_addf real_of_nat_def)
-
 lemma sumr_less_bounds_zero [simp]: "n < m ==> sumr m n f = 0"
 by (simp add: atLeastLessThan_empty)
 
 lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
 by (simp add: Finite_Set.setsum_negf)
+*)
 
 lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
 by (induct "n", auto)
@@ -114,6 +124,7 @@
 apply (drule_tac x = n in spec, arith)
 done
 
+(* FIXME generalize *)
 lemma rabs_sumr_rabs_cancel [simp]:
      "abs (sumr m n (%k. abs (f k))) = (sumr m n (%k. abs (f k)))"
 by (induct "n", simp_all add: add_increasing)
@@ -132,10 +143,10 @@
 apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
-
+(*
 lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
-by (simp add: diff_minus sumr_add [symmetric] sumr_minus)
-
+by (simp add: diff_minus setsum_addf setsum_negf)
+*)
 lemma sumr_subst [rule_format (no_asm)]:
      "(\<forall>p. m \<le> p & p < m+n --> (f p = g p)) --> sumr m n f = sumr m n g"
 by (induct "n", auto)
@@ -213,14 +224,14 @@
 done
 
 lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
-by (auto simp add: sums_def sumr_mult [symmetric]
+by (auto simp add: sums_def setsum_mult [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
 
 lemma sums_divide: "x sums x' ==> (%n. x(n)/c) sums (x'/c)"
 by (simp add: real_divide_def sums_mult mult_commute [of _ "inverse c"])
 
 lemma sums_diff: "[| x sums x0; y sums y0 |] ==> (%n. x n - y n) sums (x0-y0)"
-by (auto simp add: sums_def sumr_diff [symmetric] intro: LIMSEQ_diff)
+by (auto simp add: sums_def setsum_subtractf intro: LIMSEQ_diff)
 
 lemma suminf_mult: "summable f ==> suminf f * c = suminf(%n. f n * c)"
 by (auto intro!: sums_unique sums_mult summable_sums simp add: mult_commute)
@@ -234,7 +245,7 @@
 by (auto intro!: sums_diff sums_unique summable_sums)
 
 lemma sums_minus: "x sums x0 ==> (%n. - x n) sums - x0"
-by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: sumr_minus)
+by (auto simp add: sums_def intro!: LIMSEQ_minus simp add: setsum_negf)
 
 lemma sums_group:
      "[|summable f; 0 < k |] ==> (%n. sumr (n*k) (n*k + k) f) sums (suminf f)"
@@ -356,7 +367,7 @@
 apply (drule_tac x = m in spec)
 apply (auto, rotate_tac 2, drule_tac x = n in spec)
 apply (rule_tac y = "sumr m n (%k. abs (f k))" in order_le_less_trans)
-apply (rule sumr_rabs)
+apply (rule setsum_abs)
 apply (rule_tac y = "sumr m n g" in order_le_less_trans)
 apply (auto intro: sumr_le2 simp add: abs_interval_iff)
 done
@@ -387,18 +398,18 @@
 
 text{*Absolute convergence imples normal convergence*}
 lemma summable_rabs_cancel: "summable (%n. abs (f n)) ==> summable f"
-apply (auto simp add: sumr_rabs summable_Cauchy)
+apply (auto simp add: summable_Cauchy)
 apply (drule spec, auto)
 apply (rule_tac x = N in exI, auto)
 apply (drule spec, auto)
 apply (rule_tac y = "sumr m n (%n. abs (f n))" in order_le_less_trans)
-apply (auto intro: sumr_rabs)
+apply (auto)
 done
 
 text{*Absolute convergence of series*}
 lemma summable_rabs:
      "summable (%n. abs (f n)) ==> abs(suminf f) \<le> suminf (%n. abs(f n))"
-by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf sumr_rabs)
+by (auto intro: LIMSEQ_le LIMSEQ_imp_rabs summable_rabs_cancel summable_sumr_LIMSEQ_suminf)
 
 
 subsection{* The Ratio Test*}
@@ -465,19 +476,13 @@
 val summable_def = thm"summable_def";
 val suminf_def = thm"suminf_def";
 
-val sumr_add = thm "sumr_add";
-val sumr_mult = thm "sumr_mult";
 val sumr_split_add = thm "sumr_split_add";
-val sumr_rabs = thm "sumr_rabs";
-val sumr_fun_eq = thm "sumr_fun_eq";
-val sumr_diff_mult_const = thm "sumr_diff_mult_const";
 val sumr_minus_one_realpow_zero = thm "sumr_minus_one_realpow_zero";
 val sumr_le2 = thm "sumr_le2";
 val rabs_sumr_rabs_cancel = thm "rabs_sumr_rabs_cancel";
 val sumr_zero = thm "sumr_zero";
 val Suc_le_imp_diff_ge2 = thm "Suc_le_imp_diff_ge2";
 val sumr_one_lb_realpow_zero = thm "sumr_one_lb_realpow_zero";
-val sumr_diff = thm "sumr_diff";
 val sumr_subst = thm "sumr_subst";
 val sumr_bound = thm "sumr_bound";
 val sumr_bound2 = thm "sumr_bound2";