# HG changeset patch
# User nipkow
# Date 1108994650 -3600
# Node ID 333a8824456991b447db46ee075ecffb4872d5b7
# Parent  d8edf54cc28c76408b1f206d8add326dede62b7a
comprehensive cleanup, replacing sumr by setsum

diff -r d8edf54cc28c -r 333a88244569 src/HOL/Complex/CSeries.thy
--- a/src/HOL/Complex/CSeries.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Complex/CSeries.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -63,7 +63,7 @@
 apply (simp add: add_ac)
 done
 
-lemma sumc_cmod: "cmod(sumc m n f) \<le> sumr m n (%i. cmod(f i))"
+lemma sumc_cmod: "cmod(sumc m n f) \<le> (\<Sum>i=m..<n. cmod(f i))"
 apply (induct "n")
 apply (auto intro: complex_mod_triangle_ineq [THEN order_trans])
 done
@@ -147,11 +147,11 @@
 qed_spec_mp "sumc_ge_zero2";
 ***)
 
-lemma sumr_cmod_ge_zero [iff]: "0 \<le> sumr m n (%n. cmod (f n))"
-by (induct "n", auto simp add: add_increasing) 
+lemma sumr_cmod_ge_zero [iff]: "0 \<le> (\<Sum>n=m..<n::nat. cmod (f n))"
+by (induct "n", auto simp add: add_increasing)
 
 lemma rabs_sumc_cmod_cancel [simp]:
-     "abs (sumr m n (%n. cmod (f n))) = (sumr m n (%n. cmod (f n)))"
+     "abs (\<Sum>n=m..<n::nat. cmod (f n)) = (\<Sum>n=m..<n. cmod (f n))"
 by (simp add: abs_if linorder_not_less)
 
 lemma sumc_one_lb_complexpow_zero [simp]: "sumc 1 n (%n. f(n) * 0 ^ n) = 0"
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -327,7 +327,7 @@
    apply assumption
   apply simp
  apply(fastsimp simp add:inj_on_def)
-apply (simp add:setsum_constant_nat)
+apply (simp add:setsum_constant)
 done
 
 ML
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Finite_Set.thy
--- a/src/HOL/Finite_Set.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Finite_Set.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -1064,17 +1064,6 @@
     by (simp add: setsum_def)
 qed
 
-lemma setsum_mono2_nat:
-  assumes fin: "finite B" and sub: "A \<subseteq> B"
-shows "setsum f A \<le> (setsum f B :: nat)"
-proof -
-  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
-  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
-    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
-  also have "A \<union> (B-A) = B" using sub by blast
-  finally show ?thesis .
-qed
-
 lemma setsum_negf:
  "setsum (%x. - (f x)::'a::ab_group_add) A = - setsum f A"
 proof (cases "finite A")
@@ -1118,6 +1107,30 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
+lemma setsum_mono2:
+fixes f :: "'a \<Rightarrow> 'b :: {pordered_ab_semigroup_add_imp_le,comm_monoid_add}"
+assumes fin: "finite B" and sub: "A \<subseteq> B" and nn: "\<And>b. b \<in> B-A \<Longrightarrow> 0 \<le> f b"
+shows "setsum f A \<le> setsum f B"
+proof -
+  have "setsum f A \<le> setsum f A + setsum f (B-A)"
+    by(simp add: add_increasing2[OF setsum_nonneg] nn Ball_def)
+  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
+    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
+  also have "A \<union> (B-A) = B" using sub by blast
+  finally show ?thesis .
+qed
+(*
+lemma setsum_mono2_nat:
+  assumes fin: "finite B" and sub: "A \<subseteq> B"
+shows "setsum f A \<le> (setsum f B :: nat)"
+proof -
+  have "setsum f A \<le> setsum f A + setsum f (B-A)" by arith
+  also have "\<dots> = setsum f (A \<union> (B-A))" using fin finite_subset[OF sub fin]
+    by (simp add:setsum_Un_disjoint del:Un_Diff_cancel)
+  also have "A \<union> (B-A) = B" using sub by blast
+  finally show ?thesis .
+qed
+*)
 lemma setsum_mult: 
   fixes f :: "'a => ('b::semiring_0_cancel)"
   shows "r * setsum f A = setsum (%n. r * f n) A"
@@ -1164,6 +1177,26 @@
   case False thus ?thesis by (simp add: setsum_def)
 qed
 
+lemma abs_setsum_abs[simp]: 
+  fixes f :: "'a => ('b::lordered_ab_group_abs)"
+  shows "abs (\<Sum>a\<in>A. abs(f a)) = (\<Sum>a\<in>A. abs(f a))"
+proof (cases "finite A")
+  case True
+  thus ?thesis
+  proof (induct)
+    case empty thus ?case by simp
+  next
+    case (insert a A)
+    hence "\<bar>\<Sum>a\<in>insert a A. \<bar>f a\<bar>\<bar> = \<bar>\<bar>f a\<bar> + (\<Sum>a\<in>A. \<bar>f a\<bar>)\<bar>" by simp
+    also have "\<dots> = \<bar>\<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>\<bar>"  using insert by simp
+    also have "\<dots> = \<bar>f a\<bar> + \<bar>\<Sum>a\<in>A. \<bar>f a\<bar>\<bar>" by simp
+    also have "\<dots> = (\<Sum>a\<in>insert a A. \<bar>f a\<bar>)" using insert by simp
+    finally show ?case .
+  qed
+next
+  case False thus ?thesis by (simp add: setsum_def)
+qed
+
 
 subsection {* Generalized product over a set *}
 
@@ -1430,7 +1463,7 @@
   by (simp add: card_insert_if)
 
 lemma card_mono: "\<lbrakk> finite B; A \<subseteq> B \<rbrakk> \<Longrightarrow> card A \<le> card B"
-by (simp add: card_def setsum_mono2_nat)
+by (simp add: card_def setsum_mono2)
 
 lemma card_seteq: "finite B ==> (!!A. A <= B ==> card B <= card A ==> A = B)"
   apply (induct set: Finites, simp, clarify)
@@ -1497,13 +1530,13 @@
 done
 
 
-lemma setsum_constant_nat: "(\<Sum>x\<in>A. y) = (card A) * y"
-  -- {* Generalized to any @{text comm_semiring_1_cancel} in
-        @{text IntDef} as @{text setsum_constant}. *}
-apply (cases "finite A") 
-apply (erule finite_induct, auto)
+lemma setsum_constant [simp]: "(\<Sum>x \<in> A. y) = of_nat(card A) * y"
+apply (cases "finite A")
+apply (erule finite_induct)
+apply (auto simp add: ring_distrib add_ac)
 done
 
+
 lemma setprod_constant: "finite A ==> (\<Prod>x: A. (y::'a::recpower)) = y^(card A)"
   apply (erule finite_induct)
   apply (auto simp add: power_Suc)
@@ -1512,15 +1545,18 @@
 
 subsubsection {* Cardinality of unions *}
 
+lemma of_nat_id[simp]: "(of_nat n :: nat) = n"
+by(induct n, auto)
+
 lemma card_UN_disjoint:
     "finite I ==> (ALL i:I. finite (A i)) ==>
         (ALL i:I. ALL j:I. i \<noteq> j --> A i Int A j = {}) ==>
       card (UNION I A) = (\<Sum>i\<in>I. card(A i))"
-  apply (simp add: card_def)
+  apply (simp add: card_def del: setsum_constant)
   apply (subgoal_tac
            "setsum (%i. card (A i)) I = setsum (%i. (setsum (%x. 1) (A i))) I")
-  apply (simp add: setsum_UN_disjoint)
-  apply (simp add: setsum_constant_nat cong: setsum_cong)
+  apply (simp add: setsum_UN_disjoint del: setsum_constant)
+  apply (simp cong: setsum_cong)
   done
 
 lemma card_Union_disjoint:
@@ -1546,7 +1582,7 @@
   done
 
 lemma card_image: "inj_on f A ==> card (f ` A) = card A"
-by(simp add:card_def setsum_reindex o_def)
+by(simp add:card_def setsum_reindex o_def del:setsum_constant)
 
 lemma endo_inj_surj: "finite A ==> f ` A \<subseteq> A ==> inj_on f A ==> f ` A = A"
   by (simp add: card_seteq card_image)
@@ -1587,18 +1623,17 @@
 lemma card_SigmaI [simp]:
   "\<lbrakk> finite A; ALL a:A. finite (B a) \<rbrakk>
   \<Longrightarrow> card (SIGMA x: A. B x) = (\<Sum>a\<in>A. card (B a))"
-by(simp add:card_def setsum_Sigma)
+by(simp add:card_def setsum_Sigma del:setsum_constant)
 
 lemma card_cartesian_product: "card (A <*> B) = card(A) * card(B)"
 apply (cases "finite A") 
 apply (cases "finite B") 
-  apply (simp add: setsum_constant_nat) 
 apply (auto simp add: card_eq_0_iff
-            dest: finite_cartesian_productD1 finite_cartesian_productD2) 
+            dest: finite_cartesian_productD1 finite_cartesian_productD2)
 done
 
 lemma card_cartesian_product_singleton:  "card({x} <*> A) = card(A)"
-by (simp add: card_cartesian_product) 
+by (simp add: card_cartesian_product)
 
 
 
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HSeries.thy
--- a/src/HOL/Hyperreal/HSeries.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/HSeries.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -15,10 +15,10 @@
   sumhr :: "(hypnat * hypnat * (nat=>real)) => hypreal"
    "sumhr p == 
       (%(M,N,f). Abs_hypreal(\<Union>X \<in> Rep_hypnat(M). \<Union>Y \<in> Rep_hypnat(N).  
-                             hyprel ``{%n::nat. sumr (X n) (Y n) f})) p"
+                             hyprel ``{%n::nat. setsum f {X n..<Y n}})) p"
 
   NSsums  :: "[nat=>real,real] => bool"     (infixr "NSsums" 80)
-   "f NSsums s  == (%n. sumr 0 n f) ----NS> s"
+   "f NSsums s  == (%n. setsum f {0..<n}) ----NS> s"
 
   NSsummable :: "(nat=>real) => bool"
    "NSsummable f == (\<exists>s. f NSsums s)"
@@ -30,9 +30,9 @@
 lemma sumhr: 
      "sumhr(Abs_hypnat(hypnatrel``{%n. M n}),  
             Abs_hypnat(hypnatrel``{%n. N n}), f) =  
-      Abs_hypreal(hyprel `` {%n. sumr (M n) (N n) f})"
+      Abs_hypreal(hyprel `` {%n. setsum f {M n..<N n}})"
 apply (simp add: sumhr_def)
-apply (rule arg_cong [where f = Abs_hypreal]) 
+apply (rule arg_cong [where f = Abs_hypreal])
 apply (auto, ultra)
 done
 
@@ -84,7 +84,7 @@
 lemma sumhr_split_add: "n < p ==> sumhr(0,n,f) + sumhr(n,p,f) = sumhr(0,p,f)"
 apply (cases n, cases p)
 apply (auto elim!: FreeUltrafilterNat_subset simp 
-            add: hypnat_zero_def sumhr hypreal_add hypnat_less sumr_split_add)
+            add: hypnat_zero_def sumhr hypreal_add hypnat_less setsum_add_nat_ivl)
 done
 
 lemma sumhr_split_diff: "n<p ==> sumhr(0,p,f) - sumhr(0,n,f) = sumhr(n,p,f)"
@@ -124,7 +124,7 @@
 lemma sumhr_shift_bounds:
      "sumhr(m+hypnat_of_nat k,n+hypnat_of_nat k,f) = sumhr(m,n,%i. f(i + k))"
 apply (cases m, cases n)
-apply (simp add: sumhr hypnat_add sumr_shift_bounds hypnat_of_nat_eq)
+apply (simp add: sumhr hypnat_add setsum_shift_bounds_nat_ivl hypnat_of_nat_eq)
 done
 
 
@@ -147,15 +147,20 @@
          add: sumhr hypnat_add nat_mult_2 [symmetric] hypreal_zero_def 
               hypnat_zero_def hypnat_omega_def)
 
+(* FIXME move *)
+lemma setsum_ivl_cong:
+ "i = m \<Longrightarrow> j = n \<Longrightarrow> (!!x. m <= x \<Longrightarrow> x < n \<Longrightarrow> f x = g x) \<Longrightarrow>
+ setsum f {i..<j} = setsum g {m..<n}"
+by(rule setsum_cong, simp_all)
+
 lemma sumhr_interval_const:
      "(\<forall>n. m \<le> Suc n --> f n = r) & m \<le> na  
       ==> sumhr(hypnat_of_nat m,hypnat_of_nat na,f) =  
           (hypreal_of_nat (na - m) * hypreal_of_real r)"
-by (auto dest!: sumr_interval_const 
-         simp add: hypreal_of_real_def sumhr hypreal_of_nat_eq 
-                   hypnat_of_nat_eq hypreal_of_real_def hypreal_mult)
+by(simp add: sumhr hypreal_of_nat_eq hypnat_of_nat_eq hypreal_of_real_def
+             real_of_nat_def hypreal_mult cong: setsum_ivl_cong)
 
-lemma starfunNat_sumr: "( *fNat* (%n. sumr 0 n f)) N = sumhr(0,N,f)"
+lemma starfunNat_sumr: "( *fNat* (%n. setsum f {0..<n})) N = sumhr(0,N,f)"
 apply (cases N)
 apply (simp add: hypnat_zero_def starfunNat sumhr)
 done
@@ -192,7 +197,8 @@
 lemma NSsums_unique: "f NSsums s ==> (s = NSsuminf f)"
 by (simp add: suminf_NSsuminf_iff [symmetric] sums_NSsums_iff sums_unique)
 
-lemma NSseries_zero: "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (sumr 0 n f)"
+lemma NSseries_zero:
+  "\<forall>m. n \<le> Suc m --> f(m) = 0 ==> f NSsums (setsum f {0..<n})"
 by (simp add: sums_NSsums_iff [symmetric] series_zero)
 
 lemma NSsummable_NSCauchy:
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HTranscendental.thy
--- a/src/HOL/Hyperreal/HTranscendental.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/HTranscendental.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -56,7 +56,6 @@
 lemma hypreal_sqrt_pow2_iff: "(( *f* sqrt)(x) ^ 2 = x) = (0 \<le> x)"
 apply (cases x)
 apply (auto simp add: hypreal_le hypreal_zero_num starfun hrealpow 
-                      real_sqrt_pow2_iff 
             simp del: hpowr_Suc realpow_Suc)
 done
 
@@ -586,7 +585,7 @@
 apply (frule STAR_sin_Infinitesimal_divide
                [OF Infinitesimal_pi_divide_HNatInfinite 
                    pi_divide_HNatInfinite_not_zero])
-apply (auto simp add: inverse_mult_distrib)
+apply (auto)
 apply (rule approx_SReal_mult_cancel [of "inverse (hypreal_of_real pi)"])
 apply (auto intro: SReal_inverse simp add: divide_inverse mult_ac)
 done
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HyperDef.thy
--- a/src/HOL/Hyperreal/HyperDef.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/HyperDef.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -167,7 +167,7 @@
      "X\<notin> FreeUltrafilterNat ==> -X \<in> FreeUltrafilterNat"
 apply (cut_tac FreeUltrafilterNat_mem [THEN FreeUltrafilter_iff [THEN iffD1]])
 apply (safe, drule_tac x = X in bspec)
-apply (auto simp add: UNIV_diff_Compl)
+apply (auto)
 done
 
 lemma FreeUltrafilterNat_Compl_iff1:
@@ -183,12 +183,9 @@
 apply (simp add: FreeUltrafilterNat_Compl_iff2 [symmetric])
 done
 
-lemma FreeUltrafilterNat_UNIV [simp]: "(UNIV::nat set) \<in> FreeUltrafilterNat"
+lemma FreeUltrafilterNat_UNIV [iff]: "UNIV \<in> FreeUltrafilterNat"
 by (rule FreeUltrafilterNat_mem [THEN FreeUltrafilter_Ultrafilter, THEN Ultrafilter_Filter, THEN mem_FiltersetD4])
 
-lemma FreeUltrafilterNat_Nat_set [simp]: "UNIV \<in> FreeUltrafilterNat"
-by auto
-
 lemma FreeUltrafilterNat_Nat_set_refl [intro]:
      "{n. P(n) = P(n)} \<in> FreeUltrafilterNat"
 by simp
@@ -200,7 +197,7 @@
 by (rule ccontr, simp)
 
 lemma FreeUltrafilterNat_all: "\<forall>n. P(n) ==> {n. P(n)} \<in> FreeUltrafilterNat"
-by (auto intro: FreeUltrafilterNat_Nat_set)
+by (auto)
 
 
 text{*Define and use Ultrafilter tactics*}
@@ -335,8 +332,7 @@
 
 lemma hypreal_minus: 
    "- (Abs_hypreal(hyprel``{%n. X n})) = Abs_hypreal(hyprel `` {%n. -(X n)})"
-by (simp add: hypreal_minus_def Abs_hypreal_inject 
-              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
+by (simp add: hypreal_minus_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
               UN_equiv_class [OF equiv_hyprel hypreal_minus_congruent])
 
 lemma hypreal_diff:
@@ -348,7 +344,7 @@
 by (cases z, simp add: hypreal_zero_def hypreal_minus hypreal_add)
 
 lemma hypreal_add_minus_left: "-z + z = (0::hypreal)"
-by (simp add: hypreal_add_commute hypreal_add_minus)
+by (simp add: hypreal_add_commute)
 
 
 subsection{*Hyperreal Multiplication*}
@@ -390,8 +386,7 @@
 lemma hypreal_inverse: 
       "inverse (Abs_hypreal(hyprel``{%n. X n})) =  
        Abs_hypreal(hyprel `` {%n. if X n = 0 then 0 else inverse(X n)})"
-by (simp add: hypreal_inverse_def Abs_hypreal_inject 
-              hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
+by (simp add: hypreal_inverse_def hyprel_in_hypreal [THEN Abs_hypreal_inverse] 
               UN_equiv_class [OF equiv_hyprel hypreal_inverse_congruent])
 
 lemma hypreal_mult_inverse: 
@@ -466,7 +461,7 @@
   by intro_classes (rule hypreal_le_linear)
 
 lemma hypreal_not_refl2: "!!(x::hypreal). x < y ==> x \<noteq> y"
-by (auto simp add: order_less_irrefl)
+by (auto)
 
 lemma hypreal_add_left_mono: "x \<le> y ==> z + x \<le> z + (y::hypreal)"
 apply (cases x, cases y, cases z)
@@ -702,7 +697,6 @@
 val FreeUltrafilterNat_Compl_iff1 = thm "FreeUltrafilterNat_Compl_iff1";
 val FreeUltrafilterNat_Compl_iff2 = thm "FreeUltrafilterNat_Compl_iff2";
 val FreeUltrafilterNat_UNIV = thm "FreeUltrafilterNat_UNIV";
-val FreeUltrafilterNat_Nat_set = thm "FreeUltrafilterNat_Nat_set";
 val FreeUltrafilterNat_Nat_set_refl = thm "FreeUltrafilterNat_Nat_set_refl";
 val FreeUltrafilterNat_P = thm "FreeUltrafilterNat_P";
 val FreeUltrafilterNat_Ex_P = thm "FreeUltrafilterNat_Ex_P";
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/HyperPow.thy
--- a/src/HOL/Hyperreal/HyperPow.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/HyperPow.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -71,7 +71,7 @@
 
 lemma hrabs_hrealpow_two [simp]:
      "abs(x ^ Suc (Suc 0)) = (x::hypreal) ^ Suc (Suc 0)"
-by (simp add: abs_mult)
+by (simp)
 
 lemma two_hrealpow_ge_one [simp]: "(1::hypreal) \<le> 2 ^ n"
 by (insert power_increasing [of 0 n "2::hypreal"], simp)
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Integration.thy
--- a/src/HOL/Hyperreal/Integration.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Integration.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -40,7 +40,7 @@
   --{*Riemann sum*}
 
   rsum :: "[((nat=>real)*(nat=>real)),real=>real] => real"
-  "rsum == %(D,p) f. sumr 0 (psize(D)) (%n. f(p n) * (D(Suc n) - D(n)))"
+  "rsum == %(D,p) f. \<Sum>n=0..<psize(D). f(p n) * (D(Suc n) - D(n))"
 
   --{*Gauge integrability (definite)*}
 
@@ -331,7 +331,7 @@
 done
 
 lemma sumr_partition_eq_diff_bounds [simp]:
-     "sumr 0 m (%n. D (Suc n) - D n) = D(m) - D 0"
+     "(\<Sum>n=0..<m. D (Suc n) - D n::real) = D(m) - D 0"
 by (induct "m", auto)
 
 lemma Integral_eq_diff_bounds: "a \<le> b ==> Integral(a,b) (%x. 1) (b - a)"
@@ -453,7 +453,7 @@
 apply (auto simp add: zero_less_divide_iff)
 apply (rule exI)
 apply (auto simp add: tpart_def rsum_def)
-apply (subgoal_tac "sumr 0 (psize D) (%n. f(D(Suc n)) - f(D n)) = f b - f a")
+apply (subgoal_tac "(\<Sum>n=0..<psize D. f(D(Suc n)) - f(D n)) = f b - f a")
  prefer 2
  apply (cut_tac D = "%n. f (D n)" and m = "psize D"
         in sumr_partition_eq_diff_bounds)
@@ -461,10 +461,10 @@
 apply (drule sym, simp)
 apply (simp (no_asm) add: setsum_subtractf[symmetric])
 apply (rule setsum_abs [THEN order_trans])
-apply (subgoal_tac "ea = sumr 0 (psize D) (%n. (ea / (b - a)) * (D (Suc n) - (D n)))")
+apply (subgoal_tac "ea = (\<Sum>n=0..<psize D. (ea / (b - a)) * (D (Suc n) - (D n)))")
 apply (simp add: abs_minus_commute)
 apply (rule_tac t = ea in ssubst, assumption)
-apply (rule sumr_le2)
+apply (rule setsum_mono)
 apply (rule_tac [2] setsum_mult [THEN subst])
 apply (auto simp add: partition_rhs partition_lhs partition_lb partition_ub
           fine_def)
@@ -812,7 +812,7 @@
          tpart(a,b) (D,p)
       |] ==> rsum(D,p) f \<le> rsum(D,p) g"
 apply (simp add: rsum_def)
-apply (auto intro!: sumr_le2 dest: tpart_partition [THEN partition_lt_gen2]
+apply (auto intro!: setsum_mono dest: tpart_partition [THEN partition_lt_gen2]
                dest!: lemma_Integral_le)
 done
 
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Lim.thy
--- a/src/HOL/Hyperreal/Lim.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Lim.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -771,7 +771,7 @@
 apply (drule_tac c = "u - hypreal_of_real x" and b = "hypreal_of_real D" in approx_mult1)
 apply (drule_tac [!] hypreal_not_eq_minus_iff [THEN iffD1])
 apply (subgoal_tac [2] "( *f* (%z. z-x)) u \<noteq> (0::hypreal) ")
-apply (auto simp add: times_divide_eq_left diff_minus
+apply (auto simp add: diff_minus
 	       approx_minus_iff [THEN iffD1, THEN mem_infmal_iff [THEN iffD2]]
 		     Infinitesimal_subset_HFinite [THEN subsetD])
 done
@@ -787,7 +787,7 @@
 apply (drule_tac x = h in bspec)
 apply (drule_tac [2] c = h in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-            simp add: times_divide_eq_left diff_minus)
+            simp add: diff_minus)
 done
 
 lemma NSDERIVD3:
@@ -799,7 +799,7 @@
 apply (rule ccontr, drule_tac x = h in bspec)
 apply (drule_tac [2] c = h in approx_mult1)
 apply (auto intro: Infinitesimal_subset_HFinite [THEN subsetD]
-            simp add: mult_assoc times_divide_eq_left diff_minus)
+            simp add: mult_assoc diff_minus)
 done
 
 text{*Now equivalence between NSDERIV and DERIV*}
@@ -821,7 +821,7 @@
 apply (drule_tac x3=D in
            HFinite_hypreal_of_real [THEN [2] Infinitesimal_HFinite_mult,
              THEN mem_infmal_iff [THEN iffD1]])
-apply (auto simp add: times_divide_eq_right mult_commute
+apply (auto simp add: mult_commute
             intro: approx_trans approx_minus_iff [THEN iffD2])
 done
 
@@ -872,7 +872,7 @@
 apply (frule_tac c1 = z in hypreal_mult_right_cancel [THEN iffD2], assumption)
 apply (erule_tac V = "(x + y) / z = hypreal_of_real D + yb" in thin_rl)
 apply (auto intro!: Infinitesimal_HFinite_mult2 HFinite_add
-            simp add: times_divide_eq_left mult_assoc mem_infmal_iff [symmetric])
+            simp add: mult_assoc mem_infmal_iff [symmetric])
 apply (erule Infinitesimal_subset_HFinite [THEN subsetD])
 done
 
@@ -983,7 +983,7 @@
         in hypreal_mult_right_cancel [THEN iffD2])
 apply (erule_tac [2] V = "(( *f* f) (hypreal_of_real (x) + h) + - hypreal_of_real (f x)) / h = hypreal_of_real (D) + y" in thin_rl)
 apply assumption
-apply (simp add: times_divide_eq_left times_divide_eq_right [symmetric])
+apply (simp add: times_divide_eq_right [symmetric])
 apply (auto simp add: left_distrib)
 done
 
@@ -1188,7 +1188,7 @@
   show "\<exists>g. (\<forall>z. f z - f x = g z * (z-x)) \<and> isCont g x \<and> g x = l"
   proof (intro exI conjI)
     let ?g = "(%z. if z = x then l else (f z - f x) / (z-x))"
-    show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp add: times_divide_eq)
+    show "\<forall>z. f z - f x = ?g z * (z-x)" by (simp)
     show "isCont ?g x" using der
       by (simp add: isCont_iff DERIV_iff diff_minus
                cong: LIM_equal [rule_format])
@@ -1327,13 +1327,13 @@
    \<forall>n. snd(Bolzano_bisect P a b (Suc n)) \<le> snd (Bolzano_bisect P a b n)"
 apply (rule allI)
 apply (induct_tac "n")
-apply (auto simp add: Bolzano_bisect_le Let_def split_def times_divide_eq)
+apply (auto simp add: Bolzano_bisect_le Let_def split_def)
 done
 
 lemma eq_divide_2_times_iff: "((x::real) = y / (2 * z)) = (2 * x = y/z)" 
-apply (auto simp add: times_divide_eq) 
+apply (auto)
 apply (drule_tac f = "%u. (1/2) *u" in arg_cong)
-apply (simp add: times_divide_eq) 
+apply (simp)
 done
 
 lemma Bolzano_bisect_diff:
@@ -1798,7 +1798,7 @@
   hence ba: "b-a \<noteq> 0" by arith
   show ?thesis
     by (rule real_mult_left_cancel [OF ba, THEN iffD1],
-        simp add: times_divide_eq right_diff_distrib, 
+        simp add: right_diff_distrib, 
         simp add: left_diff_distrib)
 qed
 
@@ -1834,8 +1834,7 @@
   proof (intro exI conjI)
     show "a < z" .
     show "z < b" .
-    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" 
-      by (simp add: times_divide_eq)
+    show "f b - f a = (b - a) * ((f b - f a)/(b-a))" by (simp)
     show "DERIV f z :> ((f b - f a)/(b-a))"  using derF by simp
   qed
 qed
@@ -1885,14 +1884,14 @@
 lemma DERIV_const_ratio_const2:
      "[|a \<noteq> b; \<forall>x. DERIV f x :> k |] ==> (f(b) - f(a))/(b-a) = k"
 apply (rule_tac c1 = "b-a" in real_mult_right_cancel [THEN iffD1])
-apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc times_divide_eq)
+apply (auto dest!: DERIV_const_ratio_const simp add: mult_assoc)
 done
 
 lemma real_average_minus_first [simp]: "((a + b) /2 - a) = (b-a)/(2::real)"
-by (simp add: times_divide_eq) 
+by (simp) 
 
 lemma real_average_minus_second [simp]: "((b + a)/2 - a) = (b-a)/(2::real)"
-by (simp add: times_divide_eq) 
+by (simp) 
 
 text{*Gallileo's "trick": average velocity = av. of end velocities*}
 
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/MacLaurin.thy
--- a/src/HOL/Hyperreal/MacLaurin.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/MacLaurin.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -9,25 +9,32 @@
 imports Log
 begin
 
-lemma sumr_offset: "sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
+(* FIXME generalize? *)
+lemma sumr_offset:
+ "(\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
 by (induct "n", auto)
 
-lemma sumr_offset2: "\<forall>f. sumr 0 n (%m. f (m+k)) = sumr 0 (n+k) f - sumr 0 k f"
+lemma sumr_offset2:
+ "\<forall>f. (\<Sum>m=0..<n::nat. f(m+k)::real) = setsum f {0..<n+k} - setsum f {0..<k}"
 by (induct "n", auto)
 
-lemma sumr_offset3: "sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
+lemma sumr_offset3:
+  "setsum f {0::nat..<n+k} = (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
 by (simp  add: sumr_offset)
 
-lemma sumr_offset4: "\<forall>n f. sumr 0 (n+k) f = sumr 0 n (%m. f (m+k)) + sumr 0 k f"
+lemma sumr_offset4:
+ "\<forall>n f. setsum f {0::nat..<n+k} =
+        (\<Sum>m=0..<n. f (m+k)::real) + setsum f {0..<k}"
 by (simp add: sumr_offset)
 
+(*
 lemma sumr_from_1_from_0: "0 < n ==>
-      sumr (Suc 0) (Suc n) (%n. (if even(n) then 0 else
-             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n) =
-      sumr 0 (Suc n) (%n. (if even(n) then 0 else
-             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n)"
+      (\<Sum>n=Suc 0 ..< Suc n. if even(n) then 0 else
+             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n =
+      (\<Sum>n=0..<Suc n. if even(n) then 0 else
+             ((- 1) ^ ((n - (Suc 0)) div 2))/(real (fact n))) * a ^ n"
 by (rule_tac n1 = 1 in sumr_split_add [THEN subst], auto)
-
+*)
 
 subsection{*Maclaurin's Theorem with Lagrange Form of Remainder*}
 
@@ -36,12 +43,12 @@
 
 lemma Maclaurin_lemma:
     "0 < h ==>
-     \<exists>B. f h = sumr 0 n (%m. (j m / real (fact m)) * (h^m)) +
+     \<exists>B. f h = (\<Sum>m=0..<n. (j m / real (fact m)) * (h^m)) +
                (B * ((h^n) / real(fact n)))"
-apply (rule_tac x = "(f h - sumr 0 n (%m. (j m / real (fact m)) * h^m)) *
+apply (rule_tac x = "(f h - (\<Sum>m=0..<n. (j m / real (fact m)) * h^m)) *
                  real(fact n) / (h^n)"
        in exI)
-apply (simp add: times_divide_eq) 
+apply (simp) 
 done
 
 lemma eq_diff_eq': "(x = y - z) = (y = x + (z::real))"
@@ -92,9 +99,9 @@
   prefer 3 apply (simp add: fact_diff_Suc)
  prefer 2 apply simp
 apply (frule_tac m = m in less_add_one, clarify)
-apply (simp del: sumr_Suc)
+apply (simp del: setsum_Suc)
 apply (insert sumr_offset4 [of 1])
-apply (simp del: sumr_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_Suc fact_Suc realpow_Suc)
 apply (rule lemma_DERIV_subst)
 apply (rule DERIV_add)
 apply (rule_tac [2] DERIV_const)
@@ -106,7 +113,7 @@
 apply (best intro: DERIV_chain2 intro!: DERIV_intros)
 apply (subst fact_Suc)
 apply (subst real_of_nat_mult)
-apply (simp add: inverse_mult_distrib mult_ac)
+apply (simp add: mult_ac)
 done
 
 
@@ -137,7 +144,7 @@
     ==> \<exists>t. 0 < t &
               t < h &
               f h =
-              sumr 0 n (%m. (diff m 0 / real (fact m)) * h ^ m) +
+              setsum (%m. (diff m 0 / real (fact m)) * h ^ m) {0..<n} +
               (diff n t / real (fact n)) * h ^ n"
 apply (case_tac "n = 0", force)
 apply (drule not0_implies_Suc)
@@ -145,15 +152,15 @@
 apply (frule_tac f=f and n=n and j="%m. diff m 0" in Maclaurin_lemma)
 apply (erule exE)
 apply (subgoal_tac "\<exists>g.
-     g = (%t. f t - (sumr 0 n (%m. (diff m 0 / real(fact m)) * t^m) + (B * (t^n / real(fact n)))))")
+     g = (%t. f t - (setsum (%m. (diff m 0 / real(fact m)) * t^m) {0..<n} + (B * (t^n / real(fact n)))))")
  prefer 2 apply blast
 apply (erule exE)
 apply (subgoal_tac "g 0 = 0 & g h =0")
  prefer 2
- apply (simp del: sumr_Suc)
+ apply (simp del: setsum_Suc)
  apply (cut_tac n = m and k = 1 in sumr_offset2)
- apply (simp add: eq_diff_eq' del: sumr_Suc)
-apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (sumr 0 (n - m) (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
+ apply (simp add: eq_diff_eq' del: setsum_Suc)
+apply (subgoal_tac "\<exists>difg. difg = (%m t. diff m t - (setsum (%p. (diff (m + p) 0 / real (fact p)) * (t ^ p)) {0..<n-m} + (B * ((t ^ (n - m)) / real (fact (n - m))))))")
  prefer 2 apply blast
 apply (erule exE)
 apply (subgoal_tac "difg 0 = g")
@@ -165,15 +172,15 @@
   apply (simp (no_asm_simp))
  apply (erule exE)
  apply (rule_tac x = t in exI)
- apply (simp add: times_divide_eq del: realpow_Suc fact_Suc)
+ apply (simp del: realpow_Suc fact_Suc)
 apply (subgoal_tac "\<forall>m. m < n --> difg m 0 = 0")
  prefer 2
  apply clarify
  apply simp
  apply (frule_tac m = ma in less_add_one, clarify)
- apply (simp del: sumr_Suc)
+ apply (simp del: setsum_Suc)
 apply (insert sumr_offset4 [of 1])
-apply (simp del: sumr_Suc fact_Suc realpow_Suc)
+apply (simp del: setsum_Suc fact_Suc realpow_Suc)
 apply (subgoal_tac "\<forall>m. m < n --> (\<exists>t. 0 < t & t < h & DERIV (difg m) t :> 0) ")
 apply (rule allI, rule impI)
 apply (drule_tac x = ma and P="%m. m<n --> (\<exists>t. ?QQ m t)" in spec)
@@ -181,11 +188,11 @@
 apply (erule exE)
 apply (rule_tac x = t in exI)
 (* do some tidying up *)
-apply (erule_tac [!] V= "difg = (%m t. diff m t - (sumr 0 (n - m) (%p. diff (m + p) 0 / real (fact p) * t ^ p) + B * (t ^ (n - m) / real (fact (n - m)))))"
+apply (erule_tac [!] V= "difg = (%m t. diff m t - (setsum (%p. diff (m + p) 0 / real (fact p) * t ^ p) {0..<n-m} + B * (t ^ (n - m) / real (fact (n - m)))))"
        in thin_rl)
-apply (erule_tac [!] V="g = (%t. f t - (sumr 0 n (%m. diff m 0 / real (fact m) * t ^ m) + B * (t ^ n / real (fact n))))"
+apply (erule_tac [!] V="g = (%t. f t - (setsum (%m. diff m 0 / real (fact m) * t ^ m) {0..<n} + B * (t ^ n / real (fact n))))"
        in thin_rl)
-apply (erule_tac [!] V="f h = sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) + B * (h ^ n / real (fact n))"
+apply (erule_tac [!] V="f h = setsum (%m. diff m 0 / real (fact m) * h ^ m) {0..<n} + B * (h ^ n / real (fact n))"
        in thin_rl)
 (* back to business *)
 apply (simp (no_asm_simp))
@@ -215,7 +222,7 @@
     --> (\<exists>t. 0 < t &
               t < h &
               f h =
-              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n)"
 by (blast intro: Maclaurin)
 
@@ -227,7 +234,7 @@
     ==> \<exists>t. 0 < t &
               t \<le> h &
               f h =
-              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n"
 apply (case_tac "n", auto)
 apply (drule Maclaurin, auto)
@@ -240,7 +247,7 @@
     --> (\<exists>t. 0 < t &
               t \<le> h &
               f h =
-              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n)"
 by (blast intro: Maclaurin2)
 
@@ -250,12 +257,12 @@
     ==> \<exists>t. h < t &
               t < 0 &
               f h =
-              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n"
 apply (cut_tac f = "%x. f (-x)"
         and diff = "%n x. ((- 1) ^ n) * diff n (-x)"
         and h = "-h" and n = n in Maclaurin_objl)
-apply (simp add: times_divide_eq) 
+apply (simp)
 apply safe
 apply (subst minus_mult_right)
 apply (rule DERIV_cmult)
@@ -278,7 +285,7 @@
     --> (\<exists>t. h < t &
               t < 0 &
               f h =
-              sumr 0 n (%m. diff m 0 / real (fact m) * h ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * h ^ m) +
               diff n t / real (fact n) * h ^ n)"
 by (blast intro: Maclaurin_minus)
 
@@ -299,12 +306,12 @@
        \<forall>m t. m < n & abs t \<le> abs x --> DERIV (diff m) t :> diff (Suc m) t |]
     ==> \<exists>t. abs t \<le> abs x &
               f x =
-              sumr 0 n (%m. diff m 0 / real (fact m) * x ^ m) +
+              (\<Sum>m=0..<n. diff m 0 / real (fact m) * x ^ m) +
               diff n t / real (fact n) * x ^ n"
 apply (case_tac "n = 0", force)
 apply (case_tac "x = 0")
 apply (rule_tac x = 0 in exI)
-apply (force simp add: Maclaurin_bi_le_lemma times_divide_eq)
+apply (force simp add: Maclaurin_bi_le_lemma)
 apply (cut_tac x = x and y = 0 in linorder_less_linear, auto)
 txt{*Case 1, where @{term "x < 0"}*}
 apply (cut_tac f = "diff 0" and diff = diff and h = x and n = n in Maclaurin_minus_objl, safe)
@@ -323,7 +330,7 @@
          \<forall>m x. DERIV (diff m) x :> diff(Suc m) x;
         x ~= 0; 0 < n
       |] ==> \<exists>t. 0 < abs t & abs t < abs x &
-               f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                      (diff n t / real (fact n)) * x ^ n"
 apply (rule_tac x = x and y = 0 in linorder_cases)
 prefer 2 apply blast
@@ -337,21 +344,21 @@
       (\<forall>m x. DERIV (diff m) x :> diff(Suc m) x) &
       x ~= 0 & 0 < n
       --> (\<exists>t. 0 < abs t & abs t < abs x &
-               f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+               f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                      (diff n t / real (fact n)) * x ^ n)"
 by (blast intro: Maclaurin_all_lt)
 
 lemma Maclaurin_zero [rule_format]:
      "x = (0::real)
       ==> 0 < n -->
-          sumr 0 n (%m. (diff m (0::real) / real (fact m)) * x ^ m) =
+          (\<Sum>m=0..<n. (diff m (0::real) / real (fact m)) * x ^ m) =
           diff 0 0"
 by (induct n, auto)
 
 lemma Maclaurin_all_le: "[| diff 0 = f;
         \<forall>m x. DERIV (diff m) x :> diff (Suc m) x
       |] ==> \<exists>t. abs t \<le> abs x &
-              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                     (diff n t / real (fact n)) * x ^ n"
 apply (insert linorder_le_less_linear [of n 0])
 apply (erule disjE, force)
@@ -366,7 +373,7 @@
 lemma Maclaurin_all_le_objl: "diff 0 = f &
       (\<forall>m x. DERIV (diff m) x :> diff (Suc m) x)
       --> (\<exists>t. abs t \<le> abs x &
-              f x = sumr 0 n (%m. (diff m 0 / real (fact m)) * x ^ m) +
+              f x = (\<Sum>m=0..<n. (diff m 0 / real (fact m)) * x ^ m) +
                     (diff n t / real (fact n)) * x ^ n)"
 by (blast intro: Maclaurin_all_le)
 
@@ -376,14 +383,14 @@
 lemma Maclaurin_exp_lt: "[| x ~= 0; 0 < n |]
       ==> (\<exists>t. 0 < abs t &
                 abs t < abs x &
-                exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
+                exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
                         (exp t / real (fact n)) * x ^ n)"
 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_lt_objl, auto)
 
 
 lemma Maclaurin_exp_le:
      "\<exists>t. abs t \<le> abs x &
-            exp x = sumr 0 n (%m. (x ^ m) / real (fact m)) +
+            exp x = (\<Sum>m=0..<n. (x ^ m) / real (fact m)) +
                        (exp t / real (fact n)) * x ^ n"
 by (cut_tac diff = "%n. exp" and f = exp and x = x and n = n in Maclaurin_all_le_objl, auto)
 
@@ -421,29 +428,29 @@
 lemma Maclaurin_sin_expansion2:
      "\<exists>t. abs t \<le> abs x &
        sin x =
-       (sumr 0 n (%m. (if even m then 0
+       (\<Sum>m=0..<n. (if even m then 0
                        else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
+                       x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and x = x
         and diff = "%n x. sin (x + 1/2*real n * pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (case_tac "n", clarify, simp, simp)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 lemma Maclaurin_sin_expansion:
      "\<exists>t. sin x =
-       (sumr 0 n (%m. (if even m then 0
+       (\<Sum>m=0..<n. (if even m then 0
                        else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
+                       x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (insert Maclaurin_sin_expansion2 [of x n]) 
 apply (blast intro: elim:); 
@@ -455,63 +462,60 @@
      "[| 0 < n; 0 < x |] ==>
        \<exists>t. 0 < t & t < x &
        sin x =
-       (sumr 0 n (%m. (if even m then 0
+       (\<Sum>m=0..<n. (if even m then 0
                        else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
+                       x ^ m)
       + ((sin(t + 1/2 * real(n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 lemma Maclaurin_sin_expansion4:
      "0 < x ==>
        \<exists>t. 0 < t & t \<le> x &
        sin x =
-       (sumr 0 n (%m. (if even m then 0
+       (\<Sum>m=0..<n. (if even m then 0
                        else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
-                       x ^ m))
+                       x ^ m)
       + ((sin(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = sin and n = n and h = x and diff = "%n x. sin (x + 1/2*real (n) *pi)" in Maclaurin2_objl)
 apply safe
 apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
-apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex times_divide_eq)
+apply (auto simp add: sin_zero_iff odd_Suc_mult_two_ex)
 done
 
 
 subsection{*Maclaurin Expansion for Cosine Function*}
 
 lemma sumr_cos_zero_one [simp]:
-     "sumr 0 (Suc n)
-         (%m. (if even m
-               then (- 1) ^ (m div 2)/(real  (fact m))
-               else 0) *
-              0 ^ m) = 1"
+ "(\<Sum>m=0..<(Suc n).
+     (if even m then (- 1) ^ (m div 2)/(real  (fact m)) else 0) * 0 ^ m) = 1"
 by (induct "n", auto)
 
 lemma Maclaurin_cos_expansion:
      "\<exists>t. abs t \<le> abs x &
        cos x =
-       (sumr 0 n (%m. (if even m
+       (\<Sum>m=0..<n. (if even m
                        then (- 1) ^ (m div 2)/(real (fact m))
                        else 0) *
-                       x ^ m))
+                       x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and x = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_all_lt_objl)
 apply safe
 apply (simp (no_asm))
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (case_tac "n", simp)
-apply (simp del: sumr_Suc)
+apply (simp del: setsum_Suc)
 apply (rule ccontr, simp)
 apply (drule_tac x = x in spec, simp)
 apply (erule ssubst)
@@ -524,15 +528,15 @@
      "[| 0 < x; 0 < n |] ==>
        \<exists>t. 0 < t & t < x &
        cos x =
-       (sumr 0 n (%m. (if even m
+       (\<Sum>m=0..<n. (if even m
                        then (- 1) ^ (m div 2)/(real (fact m))
                        else 0) *
-                       x ^ m))
+                       x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_objl)
 apply safe
 apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -543,15 +547,15 @@
      "[| x < 0; 0 < n |] ==>
        \<exists>t. x < t & t < 0 &
        cos x =
-       (sumr 0 n (%m. (if even m
+       (\<Sum>m=0..<n. (if even m
                        then (- 1) ^ (m div 2)/(real (fact m))
                        else 0) *
-                       x ^ m))
+                       x ^ m)
       + ((cos(t + 1/2 * real (n) *pi) / real (fact n)) * x ^ n)"
 apply (cut_tac f = cos and n = n and h = x and diff = "%n x. cos (x + 1/2*real (n) *pi)" in Maclaurin_minus_objl)
 apply safe
 apply simp
-apply (simp (no_asm) add: times_divide_eq)
+apply (simp (no_asm))
 apply (erule ssubst)
 apply (rule_tac x = t in exI, simp)
 apply (rule setsum_cong[OF refl])
@@ -567,7 +571,7 @@
 by auto
 
 lemma Maclaurin_sin_bound:
-  "abs(sin x - sumr 0 n (%m. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
+  "abs(sin x - (\<Sum>m=0..<n. (if even m then 0 else ((- 1) ^ ((m - (Suc 0)) div 2)) / real (fact m)) *
   x ^ m))  \<le> inverse(real (fact n)) * \<bar>x\<bar> ^ n"
 proof -
   have "!! x (y::real). x \<le> 1 \<Longrightarrow> 0 \<le> y \<Longrightarrow> x * y \<le> 1 * y"
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/NSA.thy
--- a/src/HOL/Hyperreal/NSA.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/NSA.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -61,7 +61,7 @@
 lemma SReal_mult: "[| (x::hypreal) \<in> Reals; y \<in> Reals |] ==> x * y \<in> Reals"
 apply (simp add: SReal_def, safe)
 apply (rule_tac x = "r * ra" in exI)
-apply (simp (no_asm) add: hypreal_of_real_mult)
+apply (simp (no_asm))
 done
 
 lemma SReal_inverse: "(x::hypreal) \<in> Reals ==> inverse x \<in> Reals"
@@ -301,7 +301,7 @@
 apply (auto simp add: Infinitesimal_def)
 apply (rule hypreal_sum_of_halves [THEN subst])
 apply (drule half_gt_zero)
-apply (blast intro: hrabs_add_less hrabs_add_less SReal_divide_number_of)
+apply (blast intro: hrabs_add_less SReal_divide_number_of)
 done
 
 lemma Infinitesimal_minus_iff [simp]: "(-x:Infinitesimal) = (x:Infinitesimal)"
@@ -325,7 +325,7 @@
 apply (drule_tac x = "r/t" in bspec)
 apply (blast intro: SReal_divide)
 apply (cut_tac a = "abs x" and b = "r/t" and c = "abs y" in mult_strict_mono)
-apply (auto simp add: times_divide_eq_left zero_less_divide_iff)
+apply (auto simp add: zero_less_divide_iff)
 done
 
 lemma Infinitesimal_HFinite_mult2:
@@ -693,13 +693,13 @@
 lemma Infinitesimal_add_approx: "[| y \<in> Infinitesimal; x + y = z |] ==> x @= z"
 apply (rule bex_Infinitesimal_iff [THEN iffD1])
 apply (drule Infinitesimal_minus_iff [THEN iffD2])
-apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric])
+apply (auto simp add: hypreal_add_assoc [symmetric])
 done
 
 lemma Infinitesimal_add_approx_self: "y \<in> Infinitesimal ==> x @= x + y"
 apply (rule bex_Infinitesimal_iff [THEN iffD1])
 apply (drule Infinitesimal_minus_iff [THEN iffD2])
-apply (auto simp add: minus_add_distrib hypreal_add_assoc [symmetric])
+apply (auto simp add: hypreal_add_assoc [symmetric])
 done
 
 lemma Infinitesimal_add_approx_self2: "y \<in> Infinitesimal ==> x @= y + x"
@@ -723,7 +723,7 @@
 
 lemma approx_add_left_cancel: "d + b  @= d + c ==> b @= c"
 apply (drule approx_minus_iff [THEN iffD1])
-apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] add_ac)
 done
 
 lemma approx_add_right_cancel: "b + d @= c + d ==> b @= c"
@@ -733,7 +733,7 @@
 
 lemma approx_add_mono1: "b @= c ==> d + b @= d + c"
 apply (rule approx_minus_iff [THEN iffD2])
-apply (simp add: minus_add_distrib approx_minus_iff [symmetric] add_ac)
+apply (simp add: approx_minus_iff [symmetric] add_ac)
 done
 
 lemma approx_add_mono2: "b @= c ==> b + a @= c + a"
@@ -805,7 +805,7 @@
 done
 
 
-subsection{* Zero is the Only Infinitesimal that is Also a Real*}
+subsection{* Zero is the Only Infinitesimal that is also a Real*}
 
 lemma Infinitesimal_less_SReal:
      "[| x \<in> Reals; y \<in> Infinitesimal; 0 < x |] ==> y < x"
@@ -1077,7 +1077,7 @@
          isLub Reals {s. s \<in> Reals & s < x} t;
          r \<in> Reals; 0 < r |]
       ==> -(x + -t) \<noteq> r"
-apply (auto simp add: minus_add_distrib)
+apply (auto)
 apply (frule isLubD1a)
 apply (drule SReal_add_cancel, assumption)
 apply (drule_tac x = "-x" in SReal_minus, simp)
@@ -1141,7 +1141,7 @@
 lemma not_HFinite_HInfinite: "x\<notin> HFinite ==> x \<in> HInfinite"
 apply (simp add: HInfinite_def HFinite_def, auto)
 apply (drule_tac x = "r + 1" in bspec)
-apply (auto simp add: SReal_add)
+apply (auto)
 done
 
 lemma HInfinite_HFinite_disj: "x \<in> HInfinite | x \<in> HFinite"
@@ -1432,7 +1432,7 @@
       ==> hypreal_of_real x + u < hypreal_of_real y"
 apply (simp add: Infinitesimal_def)
 apply (drule_tac x = "hypreal_of_real y + -hypreal_of_real x" in bspec, simp)  
-apply (auto simp add: add_commute abs_less_iff SReal_add SReal_minus)
+apply (auto simp add: add_commute abs_less_iff SReal_minus)
 apply (simp add: compare_rls) 
 done
 
@@ -1646,7 +1646,7 @@
     by (simp add: ex ey) 
   also have "... = st ((ex + ey) + (st x + st y))" by (simp add: add_ac)
   also have "... = st x + st y" 
-    by (simp add: prems st_SReal SReal_add Infinitesimal_add 
+    by (simp add: prems st_SReal Infinitesimal_add 
                   st_Infinitesimal_add_SReal2) 
   finally show ?thesis .
 qed
@@ -1870,7 +1870,7 @@
 apply (drule_tac Y = "{n. X n = Xa n}" in FreeUltrafilterNat_Int, simp) 
 apply (drule lemma_Int_HI [THEN [2] FreeUltrafilterNat_subset])
 apply (drule_tac Y = "{n. abs (X n) < u}" in FreeUltrafilterNat_Int)
-apply (auto simp add: lemma_Int_HIa FreeUltrafilterNat_empty)
+apply (auto simp add: lemma_Int_HIa)
 done
 
 lemma HInfinite_FreeUltrafilterNat_iff:
@@ -1923,7 +1923,7 @@
 
 lemma of_nat_in_Reals [simp]: "(of_nat n::hypreal) \<in> \<real>"
 apply (induct n)
-apply (simp_all add: SReal_add)
+apply (simp_all)
 done 
  
 lemma lemma_Infinitesimal2:
@@ -2075,7 +2075,7 @@
 
 lemma real_of_nat_inverse_eq_iff:
      "(u = inverse (real(Suc n))) = (real(Suc n) = inverse u)"
-by (auto simp add: inverse_inverse_eq real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
+by (auto simp add: real_of_nat_Suc_gt_zero real_not_refl2 [THEN not_sym])
 
 lemma lemma_finite_omega_set2: "finite {n::nat. u = inverse(real(Suc n))}"
 apply (simp (no_asm_simp) add: real_of_nat_inverse_eq_iff)
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Poly.thy
--- a/src/HOL/Hyperreal/Poly.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Poly.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -1026,7 +1026,7 @@
 apply (induct "p", auto)
 apply (rule_tac j = "abs a + abs (x * poly p x)" in real_le_trans)
 apply (rule abs_triangle_ineq)
-apply (auto intro!: mult_mono simp add: abs_mult, arith)
+apply (auto intro!: mult_mono, arith)
 done
 
 ML
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/SEQ.thy
--- a/src/HOL/Hyperreal/SEQ.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/SEQ.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -169,7 +169,7 @@
 apply (drule FreeUltrafilterNat_all)
 apply (erule_tac V = "{n. \<bar>Y n\<bar> < r} : FreeUltrafilterNat" in thin_rl)
 apply (drule FreeUltrafilterNat_Int, assumption)
-apply (simp add: lemmaLIM2 FreeUltrafilterNat_empty)
+apply (simp add: lemmaLIM2)
 done
 
 lemma NSLIMSEQ_LIMSEQ: "X ----NS> L ==> X ----> L"
@@ -207,7 +207,7 @@
 lemma NSLIMSEQ_mult:
       "[| X ----NS> a; Y ----NS> b |] ==> (%n. X n * Y n) ----NS> a * b"
 by (auto intro!: approx_mult_HFinite 
-        simp add: NSLIMSEQ_def hypreal_of_real_mult starfunNat_mult [symmetric])
+        simp add: NSLIMSEQ_def starfunNat_mult [symmetric])
 
 lemma LIMSEQ_mult: "[| X ----> a; Y ----> b |] ==> (%n. X n * Y n) ----> a * b"
 by (simp add: LIMSEQ_NSLIMSEQ_iff NSLIMSEQ_mult)
@@ -707,7 +707,7 @@
 apply (drule_tac M = M in lemmaCauchy1)
 apply (rule_tac x1 = xa in lemmaCauchy2 [THEN [2] FreeUltrafilterNat_subset])
 apply (rule FreeUltrafilterNat_Int)
-apply (auto intro: FreeUltrafilterNat_Int FreeUltrafilterNat_Nat_set)
+apply (auto intro: FreeUltrafilterNat_Int)
 done
 
 subsubsection{*Nonstandard Implies Standard*}
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Series.thy
--- a/src/HOL/Hyperreal/Series.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Series.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -3,6 +3,7 @@
     Copyright   : 1998  University of Cambridge
 
 Converted to Isar and polished by lcp
+Converted to setsum and polished yet more by TNN
 *) 
 
 header{*Finite Summation and Infinite Series*}
@@ -11,11 +12,9 @@
 imports SEQ Lim
 begin
 
+(* FIXME why not globally? *)
 declare atLeastLessThan_empty[simp];
-
-syntax sumr :: "[nat,nat,(nat=>real)] => real"
-translations
-  "sumr m n f" => "setsum (f::nat=>real) (atLeastLessThan m n)"
+declare atLeastLessThan_iff[iff]
 
 constdefs
    sums  :: "[nat=>real,real] => bool"     (infixr "sums" 80)
@@ -25,10 +24,9 @@
    "summable f == (\<exists>s. f sums s)"
 
    suminf   :: "(nat=>real) => real"
-   "suminf f == (@s. f sums s)"
+   "suminf f == SOME s. f sums s"
 
-
-lemma sumr_Suc [simp]:
+lemma setsum_Suc[simp]:
   "setsum f {m..<Suc n} = (if n < m then 0 else setsum f {m..<n} + f(n))"
 by (simp add: atLeastLessThanSuc add_commute)
 
@@ -45,7 +43,6 @@
 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}"
@@ -58,8 +55,10 @@
 using sumr_split_add [of m 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)"
+lemma sumr_diff_mult_const:
+ "setsum f {0..<n} - (real n*r) = setsum (%i. f i - r) {0..<n::nat}"
 by (simp add: diff_minus setsum_addf real_of_nat_def)
 
 (*
@@ -79,32 +78,54 @@
 
 lemma sumr_minus: "sumr m n (%i. - f i) = - sumr m n f"
 by (simp add: Finite_Set.setsum_negf)
+
+lemma sumr_shift_bounds:
+  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto)
 *)
 
-lemma sumr_shift_bounds: "sumr (m+k) (n+k) f = sumr m n (%i. f(i + k))"
+(* Generalize from real to some algebraic structure? *)
+lemma sumr_minus_one_realpow_zero [simp]:
+  "setsum (%i. (-1) ^ Suc i) {0..<2*n} = (0::real)"
 by (induct "n", auto)
 
-lemma sumr_minus_one_realpow_zero [simp]: "sumr 0 (2*n) (%i. (-1) ^ Suc i) = 0"
-by (induct "n", auto)
-
-lemma sumr_interval_const:
-     "\<lbrakk>\<forall>n. m \<le> Suc n --> f n = r; m \<le> k\<rbrakk> \<Longrightarrow> sumr m k f = (real(k-m) * r)"
-apply (induct "k", auto) 
+(*
+lemma sumr_interval_const2:
+     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
+      ==> sumr m k f = (real (k - m) * r)"
+apply (induct "k", auto)
 apply (drule_tac x = k in spec)
 apply (auto dest!: le_imp_less_or_eq)
 apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
 done
+*)
+(* FIXME split in tow steps
+lemma setsum_nat_set_real_const:
+  "(\<And>n. n\<in>A \<Longrightarrow> f n = r) \<Longrightarrow> setsum f A = real(card A) * r" (is "PROP ?P")
+proof (cases "finite A")
+  case True
+  thus "PROP ?P"
+  proof induct
+    case empty thus ?case by simp
+  next
+    case insert thus ?case by(simp add: left_distrib real_of_nat_Suc)
+  qed
+next
+  case False thus "PROP ?P" by (simp add: setsum_def)
+qed
+ *)
 
-lemma sumr_interval_const2:
-     "[|\<forall>n\<ge>m. f n = r; m \<le> k|]
-      ==> sumr m k f = (real (k - m) * r)"
-apply (induct "k", auto) 
-apply (drule_tac x = k in spec)
-apply (auto dest!: le_imp_less_or_eq)
-apply (simp add: left_distrib real_of_nat_Suc split: nat_diff_split)
+(*
+lemma sumr_le:
+     "[|\<forall>n\<ge>m. 0 \<le> (f n::real); m < k|] ==> setsum f {0..<m} \<le> setsum f {0..<k::nat}"
+apply (induct "k")
+apply (auto simp add: less_Suc_eq_le)
+apply (drule_tac x = k in spec, safe)
+apply (drule le_imp_less_or_eq, safe)
+apply (arith)
+apply (drule_tac a = "sumr 0 m f" in order_refl [THEN add_mono], auto)
 done
 
-
 lemma sumr_le:
      "[|\<forall>n\<ge>m. 0 \<le> f n; m < k|] ==> sumr 0 m f \<le> sumr 0 k f"
 apply (induct "k")
@@ -120,13 +141,16 @@
 apply (induct "n")
 apply (auto intro: add_mono simp add: le_def)
 done
+*)
 
+(*
 lemma sumr_ge_zero: "(\<forall>n\<ge>m. 0 \<le> f n) --> 0 \<le> sumr m n f"
 apply (induct "n", auto)
 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)
@@ -134,14 +158,19 @@
 lemma sumr_zero [rule_format]:
      "\<forall>n \<ge> N. f n = 0 ==> N \<le> m --> sumr m n f = 0"
 by (induct "n", auto)
+*)
 
 lemma Suc_le_imp_diff_ge2:
-     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> sumr m n f = 0"
-apply (rule sumr_zero) 
+     "[|\<forall>n \<ge> N. f (Suc n) = 0; Suc N \<le> m|] ==> setsum f {m..<n} = 0"
+apply (rule setsum_0')
 apply (case_tac "n", auto)
+apply(erule_tac x = "a - 1" in allE)
+apply (simp split:nat_diff_split)
 done
 
-lemma sumr_one_lb_realpow_zero [simp]: "sumr (Suc 0) n (%n. f(n) * 0 ^ n) = 0"
+(* FIXME this is an awful lemma! *)
+lemma sumr_one_lb_realpow_zero [simp]:
+  "(\<Sum>n=Suc 0..<n. f(n) * (0::real) ^ n) = 0"
 apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
@@ -149,30 +178,46 @@
 lemma sumr_diff: "sumr m n f - sumr m n g = sumr m n (%n. f n - g n)"
 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)
+*)
 
+lemma setsum_bounded:
+  assumes le: "\<And>i. i\<in>A \<Longrightarrow> f i \<le> (K::'a::{comm_semiring_1_cancel, pordered_ab_semigroup_add})"
+  shows "setsum f A \<le> of_nat(card A) * K"
+proof (cases "finite A")
+  case True
+  thus ?thesis using le setsum_mono[where K=A and g = "%x. K"] by simp
+next
+  case False thus ?thesis by (simp add: setsum_def)
+qed
+(*
 lemma sumr_bound [rule_format (no_asm)]:
      "(\<forall>p. m \<le> p & p < m + n --> (f(p) \<le> K))  
-      --> (sumr m (m + n) f \<le> (real n * K))"
+      --> setsum f {m..<m+n::nat} \<le> (real n * K)"
 apply (induct "n")
 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc)
 done
-
+*)
+(* FIXME should be generalized
 lemma sumr_bound2 [rule_format (no_asm)]:
      "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
-      --> (sumr 0 n f \<le> (real n * K))"
+      --> setsum f {0..<n::nat} \<le> (real n * K)"
 apply (induct "n")
 apply (auto intro: add_mono simp add: left_distrib real_of_nat_Suc add_commute)
 done
-
+ *)
+(* FIXME a bit specialized for [simp]! *)
 lemma sumr_group [simp]:
-     "sumr 0 n (%m. sumr (m * k) (m*k + k) f) = sumr 0 (n * k) f"
-apply (subgoal_tac "k = 0 | 0 < k", auto)
+     "(\<Sum>m=0..<n::nat. setsum f {m * k ..< m*k + k}) = setsum f {0 ..< n * k}"
+apply (subgoal_tac "k = 0 | 0 < k", auto simp:setsum_0')
 apply (induct "n")
-apply (simp_all add: sumr_split_add add_commute)
+apply (simp_all add: setsum_add_nat_ivl add_commute)
 done
+(* FIXME setsum_0[simp] *)
+
 
 subsection{* Infinite Sums, by the Properties of Limits*}
 
@@ -188,7 +233,7 @@
 done
 
 lemma summable_sumr_LIMSEQ_suminf: 
-     "summable f ==> (%n. sumr 0 n f) ----> (suminf f)"
+     "summable f ==> (%n. setsum f {0..<n}) ----> (suminf f)"
 apply (simp add: summable_def suminf_def sums_def)
 apply (blast intro: someI2)
 done
@@ -216,14 +261,31 @@
 next one was called series_zero2
 **********************)
 
+lemma ivl_subset[simp]:
+ "({i..<j} \<subseteq> {m..<n}) = (j \<le> i | m \<le> i & j \<le> (n::'a::linorder))"
+apply(auto simp:linorder_not_le)
+apply(rule ccontr)
+apply(frule subsetCE[where c = n])
+apply(auto simp:linorder_not_le)
+done
+
+lemma ivl_diff[simp]:
+ "i \<le> n \<Longrightarrow> {i..<m} - {i..<n} = {n..<(m::'a::linorder)}"
+by(auto)
+
+
+(* FIXME the last step should work w/o Ball_def, ideally just with
+   setsum_0 and setsum_cong. Currently the simplifier does not simplify
+   the premise x:{i..<j} that ball_cong (or a modified version of setsum_0')
+   generates. FIX simplifier??? *)
 lemma series_zero: 
-     "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (sumr 0 n f)"
+     "(\<forall>m. n \<le> m --> f(m) = 0) ==> f sums (setsum f {0..<n})"
 apply (simp add: sums_def LIMSEQ_def diff_minus[symmetric], safe)
 apply (rule_tac x = n in exI)
-apply (clarsimp simp:sumr_split_add_minus)
-apply (drule sumr_interval_const2, auto)
+apply (clarsimp simp add:setsum_diff[symmetric] setsum_0' Ball_def)
 done
 
+
 lemma sums_mult: "x sums x0 ==> (%n. c * x(n)) sums (c * x0)"
 by (auto simp add: sums_def setsum_mult [symmetric]
          intro!: LIMSEQ_mult intro: LIMSEQ_const)
@@ -249,7 +311,7 @@
 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)"
+     "[|summable f; 0 < k |] ==> (%n. setsum f {n*k..<n*k+k}) sums (suminf f)"
 apply (drule summable_sums)
 apply (auto simp add: sums_def LIMSEQ_def)
 apply (drule_tac x = r in spec, safe)
@@ -260,18 +322,18 @@
 done
 
 lemma sumr_pos_lt_pair_lemma:
-     "[|\<forall>d. - f (n + (d + d)) < f (Suc (n + (d + d)))|]
-      ==> sumr 0 (n + Suc (Suc 0)) f \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f"
+  "[|\<forall>d. - f (n + (d + d)) < (f (Suc (n + (d + d))) :: real) |]
+   ==> setsum f {0..<n+Suc(Suc 0)} \<le> setsum f {0..<Suc(Suc 0) * Suc no + n}"
 apply (induct "no", auto)
 apply (drule_tac x = "Suc no" in spec)
-apply (simp add: add_ac) 
+apply (simp add: add_ac)
 done
 
 
 lemma sumr_pos_lt_pair:
      "[|summable f; 
         \<forall>d. 0 < (f(n + (Suc(Suc 0) * d))) + f(n + ((Suc(Suc 0) * d) + 1))|]  
-      ==> sumr 0 n f < suminf f"
+      ==> setsum f {0..<n} < suminf f"
 apply (drule summable_sums)
 apply (auto simp add: sums_def LIMSEQ_def)
 apply (drule_tac x = "f (n) + f (n + 1)" in spec)
@@ -282,18 +344,19 @@
 apply (drule_tac x = 0 in spec, simp)
 apply (rotate_tac 1, drule_tac x = "Suc (Suc 0) * (Suc no) + n" in spec)
 apply (safe, simp)
-apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
-apply (rule_tac [2] y = "sumr 0 (n+ Suc (Suc 0)) f" in order_trans)
+apply (subgoal_tac "suminf f + (f (n) + f (n + 1)) \<le>
+ setsum f {0 ..< Suc (Suc 0) * (Suc no) + n}")
+apply (rule_tac [2] y = "setsum f {0..<n+ Suc (Suc 0)}" in order_trans)
 prefer 3 apply assumption
-apply (rule_tac [2] y = "sumr 0 n f + (f (n) + f (n + 1))" in order_trans)
+apply (rule_tac [2] y = "setsum f {0..<n} + (f (n) + f (n + 1))" in order_trans)
 apply simp_all 
-apply (subgoal_tac "suminf f \<le> sumr 0 (Suc (Suc 0) * (Suc no) + n) f")
+apply (subgoal_tac "suminf f \<le> setsum f {0..< Suc (Suc 0) * (Suc no) + n}")
 apply (rule_tac [2] y = "suminf f + (f (n) + f (n + 1))" in order_trans)
-prefer 3 apply simp 
+prefer 3 apply simp
 apply (drule_tac [2] x = 0 in spec)
  prefer 2 apply simp 
-apply (subgoal_tac "0 \<le> sumr 0 (Suc (Suc 0) * Suc no + n) f + - suminf f")
-apply (simp add: abs_if) 
+apply (subgoal_tac "0 \<le> setsum f {0 ..< Suc (Suc 0) * Suc no + n} + - suminf f")
+apply (simp add: abs_if)
 apply (auto simp add: linorder_not_less [symmetric])
 done
 
@@ -301,29 +364,30 @@
 great as any partial sum.*}
 
 lemma series_pos_le: 
-     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> sumr 0 n f \<le> suminf f"
+     "[| summable f; \<forall>m \<ge> n. 0 \<le> f(m) |] ==> setsum f {0..<n} \<le> suminf f"
 apply (drule summable_sums)
 apply (simp add: sums_def)
-apply (cut_tac k = "sumr 0 n f" in LIMSEQ_const)
-apply (erule LIMSEQ_le, blast) 
-apply (rule_tac x = n in exI, clarify) 
-apply (drule le_imp_less_or_eq)
-apply (auto intro: sumr_le)
+apply (cut_tac k = "setsum f {0..<n}" in LIMSEQ_const)
+apply (erule LIMSEQ_le, blast)
+apply (rule_tac x = n in exI, clarify)
+apply (rule setsum_mono2)
+apply auto
 done
 
 lemma series_pos_less:
-     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> sumr 0 n f < suminf f"
-apply (rule_tac y = "sumr 0 (Suc n) f" in order_less_le_trans)
+     "[| summable f; \<forall>m \<ge> n. 0 < f(m) |] ==> setsum f {0..<n} < suminf f"
+apply (rule_tac y = "setsum f {0..<Suc n}" in order_less_le_trans)
 apply (rule_tac [2] series_pos_le, auto)
 apply (drule_tac x = m in spec, auto)
 done
 
 text{*Sum of a geometric progression.*}
 
-lemma sumr_geometric: "x ~= 1 ==> sumr 0 n (%n. x ^ n) = (x ^ n - 1) / (x - 1)"
+lemma sumr_geometric:
+ "x ~= 1 ==> (\<Sum>i=0..<n. x ^ i) = (x ^ n - 1) / (x - 1::real)"
 apply (induct "n", auto)
 apply (rule_tac c1 = "x - 1" in real_mult_right_cancel [THEN iffD1])
-apply (auto simp add: mult_assoc left_distrib  times_divide_eq)
+apply (auto simp add: mult_assoc left_distrib)
 apply (simp add: right_distrib diff_minus mult_commute)
 done
 
@@ -339,25 +403,27 @@
 
 text{*Cauchy-type criterion for convergence of series (c.f. Harrison)*}
 
-lemma summable_convergent_sumr_iff: "summable f = convergent (%n. sumr 0 n f)"
+lemma summable_convergent_sumr_iff:
+ "summable f = convergent (%n. setsum f {0..<n})"
 by (simp add: summable_def sums_def convergent_def)
 
 lemma summable_Cauchy:
      "summable f =  
-      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(sumr m n f) < e)"
+      (\<forall>e > 0. \<exists>N. \<forall>m \<ge> N. \<forall>n. abs(setsum f {m..<n}) < e)"
 apply (auto simp add: summable_convergent_sumr_iff Cauchy_convergent_iff [symmetric] Cauchy_def diff_minus[symmetric])
-apply (drule_tac [!] spec, auto) 
+apply (drule_tac [!] spec, auto)
 apply (rule_tac x = M in exI)
 apply (rule_tac [2] x = N in exI, auto)
 apply (cut_tac [!] m = m and n = n in less_linear, auto)
 apply (frule le_less_trans [THEN less_imp_le], assumption)
 apply (drule_tac x = n in spec, simp)
 apply (drule_tac x = m in spec)
-apply(simp add: sumr_split_add_minus)
+apply(simp add: setsum_diff[symmetric])
 apply(subst abs_minus_commute)
-apply(simp add: sumr_split_add_minus)
-apply (simp add: sumr_split_add_minus)
+apply(simp add: setsum_diff[symmetric])
+apply(simp add: setsum_diff[symmetric])
 done
+(* FIXME move ivl_ lemmas out of this theory *)
 
 text{*Comparison test*}
 
@@ -369,10 +435,10 @@
 apply (rotate_tac 2)
 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_tac y = "\<Sum>k=m..<n. abs(f k)" in order_le_less_trans)
 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)
+apply (rule_tac y = "setsum g {m..<n}" in order_le_less_trans)
+apply (auto intro: setsum_mono simp add: abs_interval_iff)
 done
 
 lemma summable_rabs_comparison_test:
@@ -389,7 +455,7 @@
 apply (drule summable_sums)+
 apply (auto intro!: LIMSEQ_le simp add: sums_def)
 apply (rule exI)
-apply (auto intro!: sumr_le2)
+apply (auto intro!: setsum_mono)
 done
 
 lemma summable_le2:
@@ -405,7 +471,7 @@
 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 (rule_tac y = "\<Sum>n=m..<n. abs(f n)" in order_le_less_trans)
 apply (auto)
 done
 
@@ -452,7 +518,7 @@
 apply (rule_tac x = N in exI, safe)
 apply (drule le_Suc_ex_iff [THEN iffD1])
 apply (auto simp add: power_add realpow_not_zero)
-apply (induct_tac "na", auto simp add: times_divide_eq)
+apply (induct_tac "na", auto)
 apply (rule_tac y = "c*abs (f (N + n))" in order_trans)
 apply (auto intro: mult_right_mono simp add: summable_def)
 apply (simp add: mult_ac)
@@ -467,28 +533,20 @@
 
 lemma DERIV_sumr [rule_format (no_asm)]:
      "(\<forall>r. m \<le> r & r < (m + n) --> DERIV (%x. f r x) x :> (f' r x))  
-      --> DERIV (%x. sumr m n (%n. f n x)) x :> sumr m n (%r. f' r x)"
+      --> DERIV (%x. \<Sum>n=m..<n::nat. f n x) x :> (\<Sum>r=m..<n. f' r x)"
 apply (induct "n")
 apply (auto intro: DERIV_add)
 done
 
 ML
 {*
-val sumr_Suc = thm"sumr_Suc";
 val sums_def = thm"sums_def";
 val summable_def = thm"summable_def";
 val suminf_def = thm"suminf_def";
 
-val sumr_split_add = thm "sumr_split_add";
 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_subst = thm "sumr_subst";
-val sumr_bound = thm "sumr_bound";
-val sumr_bound2 = thm "sumr_bound2";
 val sumr_group = thm "sumr_group";
 val sums_summable = thm "sums_summable";
 val summable_sums = thm "summable_sums";
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Hyperreal/Transcendental.thy
--- a/src/HOL/Hyperreal/Transcendental.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Hyperreal/Transcendental.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -75,7 +75,7 @@
 apply (rule_tac x = u and y = x in linorder_cases)
 apply (drule_tac n1 = n and x = u in zero_less_Suc [THEN [3] realpow_less])
 apply (drule_tac [4] n1 = n and x = x in zero_less_Suc [THEN [3] realpow_less])
-apply (auto simp add: order_less_irrefl)
+apply (auto)
 done
 
 lemma real_root_pos2: "0 \<le> x ==> root(Suc n) (x ^ (Suc n)) = x"
@@ -100,7 +100,7 @@
 apply (rule_tac x = u and y = 1 in linorder_cases)
 apply (drule_tac n = n in realpow_Suc_less_one)
 apply (drule_tac [4] n = n in power_gt1_lemma)
-apply (auto simp add: order_less_irrefl)
+apply (auto)
 done
 
 
@@ -117,7 +117,7 @@
 lemma real_sqrt_one [simp]: "sqrt 1 = 1"
 by (simp add: sqrt_def)
 
-lemma real_sqrt_pow2_iff [simp]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
+lemma real_sqrt_pow2_iff [iff]: "((sqrt x)\<twosuperior> = x) = (0 \<le> x)"
 apply (simp add: sqrt_def)
 apply (rule iffI) 
  apply (cut_tac r = "root 2 x" in realpow_two_le)
@@ -130,7 +130,7 @@
 by (rule realpow_two_le_add_order [THEN real_sqrt_pow2_iff [THEN iffD2]])
 
 lemma real_sqrt_pow2 [simp]: "0 \<le> x ==> (sqrt x)\<twosuperior> = x"
-by (simp add: real_sqrt_pow2_iff)
+by (simp)
 
 lemma real_sqrt_abs_abs [simp]: "sqrt\<bar>x\<bar> ^ 2 = \<bar>x\<bar>"
 by (rule real_sqrt_pow2_iff [THEN iffD2], arith)
@@ -209,13 +209,13 @@
 
 lemma real_sqrt_sum_squares_mult_squared_eq [simp]:
      "sqrt ((x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)) ^ 2 = (x\<twosuperior> + y\<twosuperior>) * (xa\<twosuperior> + ya\<twosuperior>)"
-by (auto simp add: real_sqrt_pow2_iff zero_le_mult_iff simp del: realpow_Suc)
+by (auto simp add: zero_le_mult_iff simp del: realpow_Suc)
 
 lemma real_sqrt_abs [simp]: "sqrt(x\<twosuperior>) = \<bar>x\<bar>"
 apply (rule abs_realpow_two [THEN subst])
 apply (rule real_sqrt_abs_abs [THEN subst])
 apply (subst real_pow_sqrt_eq_sqrt_pow)
-apply (auto simp add: numeral_2_eq_2 abs_mult)
+apply (auto simp add: numeral_2_eq_2)
 done
 
 lemma real_sqrt_abs2 [simp]: "sqrt(x*x) = \<bar>x\<bar>"
@@ -229,7 +229,7 @@
 
 lemma real_sqrt_not_eq_zero: "0 < x ==> sqrt x \<noteq> 0"
 apply (frule real_sqrt_pow2_gt_zero)
-apply (auto simp add: numeral_2_eq_2 order_less_irrefl)
+apply (auto simp add: numeral_2_eq_2)
 done
 
 lemma real_inv_sqrt_pow2: "0 < x ==> inverse (sqrt(x)) ^ 2 = inverse x"
@@ -269,21 +269,20 @@
 apply (cut_tac x = r in reals_Archimedean3, auto)
 apply (drule_tac x = "\<bar>x\<bar>" in spec, safe)
 apply (rule_tac N = n and c = r in ratio_test)
-apply (auto simp add: abs_mult mult_assoc [symmetric] simp del: fact_Suc)
+apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
 apply (rule mult_right_mono)
 apply (rule_tac b1 = "\<bar>x\<bar>" in mult_commute [THEN ssubst])
 apply (subst fact_Suc)
 apply (subst real_of_nat_mult)
-apply (auto simp add: abs_mult inverse_mult_distrib)
+apply (auto)
 apply (auto simp add: mult_assoc [symmetric] positive_imp_inverse_positive)
 apply (rule order_less_imp_le)
 apply (rule_tac z1 = "real (Suc na)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc abs_inverse)
+apply (auto simp add: real_not_refl2 [THEN not_sym] mult_assoc)
 apply (erule order_less_trans)
 apply (auto simp add: mult_less_cancel_left mult_ac)
 done
 
-
 lemma summable_sin: 
      "summable (%n.  
            (if even n then 0  
@@ -321,10 +320,8 @@
 by (induct "n", auto)
 
 lemma lemma_STAR_cos2 [simp]:
-     "sumr 1 n (%n. if even n  
-                    then (- 1) ^ (n div 2)/(real (fact n)) *  
-                          0 ^ n  
-                    else 0) = 0"
+  "(\<Sum>n=1..<n. if even n then (- 1) ^ (n div 2)/(real (fact n)) *  0 ^ n 
+                         else 0) = 0"
 apply (induct "n")
 apply (case_tac [2] "n", auto)
 done
@@ -364,34 +361,33 @@
 subsection{*Properties of Power Series*}
 
 lemma lemma_realpow_diff_sumr:
-     "sumr 0 (Suc n) (%p. (x ^ p) * y ^ ((Suc n) - p)) =  
-      y * sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p)))"
-apply (auto simp add: setsum_mult simp del: sumr_Suc)
-apply (rule sumr_subst)
-apply (intro strip)
+     "(\<Sum>p=0..<Suc n. (x ^ p) * y ^ ((Suc n) - p)) =  
+      y * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))::real)"
+apply (auto simp add: setsum_mult simp del: setsum_Suc)
+apply (rule setsum_cong[OF refl])
 apply (subst lemma_realpow_diff)
 apply (auto simp add: mult_ac)
 done
 
 lemma lemma_realpow_diff_sumr2:
      "x ^ (Suc n) - y ^ (Suc n) =  
-      (x - y) * sumr 0 (Suc n) (%p. (x ^ p) * (y ^(n - p)))"
+      (x - y) * (\<Sum>p=0..<Suc n. (x ^ p) * (y ^(n - p))::real)"
 apply (induct "n", simp)
-apply (auto simp del: sumr_Suc)
-apply (subst sumr_Suc)
+apply (auto simp del: setsum_Suc)
+apply (subst setsum_Suc)
 apply (drule sym)
-apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: sumr_Suc)
+apply (auto simp add: lemma_realpow_diff_sumr right_distrib diff_minus mult_ac simp del: setsum_Suc)
 done
 
 lemma lemma_realpow_rev_sumr:
-     "sumr 0 (Suc n) (%p. (x ^ p) * (y ^ (n - p))) =  
-      sumr 0 (Suc n) (%p. (x ^ (n - p)) * (y ^ p))"
+     "(\<Sum>p=0..<Suc n. (x ^ p) * (y ^ (n - p))) =  
+      (\<Sum>p=0..<Suc n. (x ^ (n - p)) * (y ^ p)::real)"
 apply (case_tac "x = y")
-apply (auto simp add: mult_commute power_add [symmetric] simp del: sumr_Suc)
+apply (auto simp add: mult_commute power_add [symmetric] simp del: setsum_Suc)
 apply (rule_tac c1 = "x - y" in real_mult_left_cancel [THEN iffD1])
 apply (rule_tac [2] minus_minus [THEN subst], simp)
 apply (subst minus_mult_left)
-apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: sumr_Suc)
+apply (simp add: lemma_realpow_diff_sumr2 [symmetric] del: setsum_Suc)
 done
 
 text{*Power series has a `circle` of convergence, i.e. if it sums for @{term
@@ -412,7 +408,7 @@
 apply (auto simp add: mult_assoc power_abs)
  prefer 2
  apply (drule_tac x = 0 in spec, force)
-apply (auto simp add: abs_mult power_abs mult_ac)
+apply (auto simp add: power_abs mult_ac)
 apply (rule_tac a2 = "z ^ n" 
        in abs_ge_zero [THEN real_le_imp_less_or_eq, THEN disjE])
 apply (auto intro!: mult_right_mono simp add: mult_assoc [symmetric] power_abs summable_def power_0_left)
@@ -423,8 +419,7 @@
 apply (subgoal_tac "x \<noteq> 0")
 apply (subgoal_tac [3] "x \<noteq> 0")
 apply (auto simp del: abs_inverse abs_mult simp add: abs_inverse [symmetric] realpow_not_zero abs_mult [symmetric] power_inverse power_mult_distrib [symmetric])
-apply (auto intro!: geometric_sums 
-            simp add: power_abs inverse_eq_divide times_divide_eq)
+apply (auto intro!: geometric_sums  simp add: power_abs inverse_eq_divide)
 done
 
 lemma powser_inside:
@@ -443,16 +438,16 @@
 
 text{*Show that we can shift the terms down one*}
 lemma lemma_diffs:
-     "sumr 0 n (%n. (diffs c)(n) * (x ^ n)) =  
-      sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) +  
+     "(\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) =  
+      (\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) +  
       (real n * c(n) * x ^ (n - Suc 0))"
 apply (induct "n")
 apply (auto simp add: mult_assoc add_assoc [symmetric] diffs_def)
 done
 
 lemma lemma_diffs2:
-     "sumr 0 n (%n. real n * c(n) * (x ^ (n - Suc 0))) =  
-      sumr 0 n (%n. (diffs c)(n) * (x ^ n)) -  
+     "(\<Sum>n=0..<n. real n * c(n) * (x ^ (n - Suc 0))) =  
+      (\<Sum>n=0..<n. (diffs c)(n) * (x ^ n)) -  
       (real n * c(n) * x ^ (n - Suc 0))"
 by (auto simp add: lemma_diffs)
 
@@ -474,10 +469,9 @@
 subsection{*Term-by-Term Differentiability of Power Series*}
 
 lemma lemma_termdiff1:
-     "sumr 0 m (%p. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
-        sumr 0 m (%p. (z ^ p) *  
-        (((z + h) ^ (m - p)) - (z ^ (m - p))))"
-apply (rule sumr_subst)
+  "(\<Sum>p=0..<m. (((z + h) ^ (m - p)) * (z ^ p)) - (z ^ m)) =  
+   (\<Sum>p=0..<m. (z ^ p) * (((z + h) ^ (m - p)) - (z ^ (m - p)))::real)"
+apply (rule setsum_cong[OF refl])
 apply (auto simp add: right_distrib diff_minus power_add [symmetric] mult_ac)
 done
 
@@ -489,54 +483,59 @@
 
 
 lemma lemma_termdiff2:
-     " h \<noteq> 0 ==>  
-        (((z + h) ^ n) - (z ^ n)) * inverse h -  
-            real n * (z ^ (n - Suc 0)) =  
-         h * sumr 0 (n - Suc 0) (%p. (z ^ p) *  
-               sumr 0 ((n - Suc 0) - p)  
-                 (%q. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"
+  "h \<noteq> 0 ==>
+   (((z + h) ^ n) - (z ^ n)) * inverse h - real n * (z ^ (n - Suc 0)) =
+   h * (\<Sum>p=0..< n - Suc 0. (z ^ p) *
+       (\<Sum>q=0..< (n - Suc 0) - p. ((z + h) ^ q) * (z ^ (((n - 2) - p) - q))))"
 apply (rule real_mult_left_cancel [THEN iffD1], simp (no_asm_simp))
 apply (simp add: right_diff_distrib mult_ac)
 apply (simp add: mult_assoc [symmetric])
 apply (case_tac "n")
 apply (auto simp add: lemma_realpow_diff_sumr2 
                       right_diff_distrib [symmetric] mult_assoc
-            simp del: realpow_Suc sumr_Suc)
-apply (auto simp add: lemma_realpow_rev_sumr simp del: sumr_Suc)
+            simp del: realpow_Suc setsum_Suc)
+apply (auto simp add: lemma_realpow_rev_sumr simp del: setsum_Suc)
 apply (auto simp add: real_of_nat_Suc sumr_diff_mult_const left_distrib 
                 sumdiff lemma_termdiff1 setsum_mult)
-apply (auto intro!: sumr_subst simp add: diff_minus real_add_assoc)
-apply (simp add: diff_minus [symmetric] less_iff_Suc_add) 
+apply (auto intro!: setsum_cong[OF refl] simp add: diff_minus real_add_assoc)
+apply (simp add: diff_minus [symmetric] less_iff_Suc_add)
 apply (auto simp add: setsum_mult lemma_realpow_diff_sumr2 mult_ac simp
-                 del: sumr_Suc realpow_Suc)
+                 del: setsum_Suc realpow_Suc)
 done
 
+(* FIXME move *)
+lemma sumr_bound2 [rule_format (no_asm)]:
+     "(\<forall>p. 0 \<le> p & p < n --> (f(p) \<le> K))  
+      --> setsum f {0..<n::nat} \<le> (real n * K)"
+using setsum_bounded[where A = "{0..<n}"]
+by (auto simp:real_of_nat_def)
+
 lemma lemma_termdiff3:
      "[| h \<noteq> 0; \<bar>z\<bar> \<le> K; \<bar>z + h\<bar> \<le> K |]  
       ==> abs (((z + h) ^ n - z ^ n) * inverse h - real n * z ^ (n - Suc 0))  
           \<le> real n * real (n - Suc 0) * K ^ (n - 2) * \<bar>h\<bar>"
 apply (subst lemma_termdiff2, assumption)
-apply (simp add: abs_mult mult_commute) 
+apply (simp add: mult_commute) 
 apply (simp add: mult_commute [of _ "K ^ (n - 2)"]) 
 apply (rule setsum_abs [THEN real_le_trans])
 apply (simp add: mult_assoc [symmetric])
 apply (simp add: mult_commute [of _ "real (n - Suc 0)"])
-apply (auto intro!: sumr_bound2 simp add: abs_mult)
+apply (auto intro!: sumr_bound2)
 apply (case_tac "n", auto)
 apply (drule less_add_one)
 (*CLAIM_SIMP " (a * b * c = a * (c * (b::real))" mult_ac]*)
 apply clarify 
 apply (subgoal_tac "K ^ p * K ^ d * real (Suc (Suc (p + d))) =
                     K ^ p * (real (Suc (Suc (p + d))) * K ^ d)") 
-apply (simp (no_asm_simp) add: power_add del: sumr_Suc)
-apply (auto intro!: mult_mono simp del: sumr_Suc)
-apply (auto intro!: power_mono simp add: power_abs simp del: sumr_Suc)
+apply (simp (no_asm_simp) add: power_add del: setsum_Suc)
+apply (auto intro!: mult_mono simp del: setsum_Suc)
+apply (auto intro!: power_mono simp add: power_abs simp del: setsum_Suc)
 apply (rule_tac j = "real (Suc d) * (K ^ d)" in real_le_trans)
 apply (subgoal_tac [2] "0 \<le> K")
 apply (drule_tac [2] n = d in zero_le_power)
-apply (auto simp del: sumr_Suc)
+apply (auto simp del: setsum_Suc)
 apply (rule setsum_abs [THEN real_le_trans])
-apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: abs_mult power_add)
+apply (rule sumr_bound2, auto dest!: less_add_one intro!: mult_mono simp add: power_add)
 apply (auto intro!: power_mono zero_le_power simp add: power_abs, arith+)
 done
 
@@ -910,7 +909,7 @@
   hence "exp x * inverse (exp x) < exp y * inverse (exp x)"
     by (auto simp add: exp_add exp_minus)
   thus ?thesis
-    by (simp add: divide_inverse [symmetric] pos_less_divide_eq times_divide_eq
+    by (simp add: divide_inverse [symmetric] pos_less_divide_eq
              del: divide_self_if)
 qed
 
@@ -1067,7 +1066,8 @@
 by (auto intro!: sums_unique [symmetric] LIMSEQ_const 
          simp add: sin_def sums_def simp del: power_0_left)
 
-lemma lemma_series_zero2: "(\<forall>m. n \<le> m --> f m = 0) --> f sums sumr 0 n f"
+lemma lemma_series_zero2:
+ "(\<forall>m. n \<le> m --> f m = 0) --> f sums setsum f {0..<n}"
 by (auto intro: series_zero)
 
 lemma cos_zero [simp]: "cos 0 = 1"
@@ -1237,7 +1237,6 @@
                     DERIV_add  DERIV_diff  DERIV_mult  DERIV_minus 
                     DERIV_inverse_fun DERIV_quotient DERIV_fun_pow 
                     DERIV_fun_exp DERIV_fun_sin DERIV_fun_cos 
-                    DERIV_Id DERIV_const DERIV_cos
 
 (* lemma *)
 lemma lemma_DERIV_sin_cos_add:
@@ -1361,9 +1360,8 @@
 apply (case_tac "m=0")
 apply (simp (no_asm_simp))
 apply (subgoal_tac "6 * (x * (x * x) / real (Suc (Suc (Suc (Suc (Suc (Suc 0))))))) < 6 * x") 
-apply (simp only: mult_less_cancel_left, simp add: times_divide_eq)  
-apply (simp (no_asm_simp) add: times_divide_eq 
-               numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
+apply (simp only: mult_less_cancel_left, simp)  
+apply (simp (no_asm_simp) add: numeral_2_eq_2 [symmetric] mult_assoc [symmetric])
 apply (subgoal_tac "x*x < 2*3", simp) 
 apply (rule mult_strict_mono)
 apply (auto simp add: real_0_less_add_iff real_of_nat_Suc simp del: fact_Suc)
@@ -1375,7 +1373,7 @@
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
 apply (subst real_of_nat_mult)
-apply (simp (no_asm) add: divide_inverse inverse_mult_distrib del: fact_Suc)
+apply (simp (no_asm) add: divide_inverse del: fact_Suc)
 apply (auto simp add: mult_assoc [symmetric] simp del: fact_Suc)
 apply (rule_tac c="real (Suc (Suc (4*m)))" in mult_less_imp_less_right) 
 apply (auto simp add: mult_assoc simp del: fact_Suc)
@@ -1422,12 +1420,12 @@
 apply (cut_tac x = 2 in cos_paired)
 apply (drule sums_minus)
 apply (rule neg_less_iff_less [THEN iffD1]) 
-apply (frule sums_unique, auto simp add: times_divide_eq)
-apply (rule_tac y = "sumr 0 (Suc (Suc (Suc 0))) 
-                      (%n. - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n)))" 
+apply (frule sums_unique, auto)
+apply (rule_tac y =
+ "\<Sum>n=0..< Suc(Suc(Suc 0)). - ((- 1) ^ n / (real(fact (2*n))) * 2 ^ (2*n))"
        in order_less_trans)
 apply (simp (no_asm) add: fact_num_eq_if realpow_num_eq_if del: fact_Suc realpow_Suc)
-apply (simp (no_asm) add: mult_assoc times_divide_eq del: sumr_Suc)
+apply (simp (no_asm) add: mult_assoc del: setsum_Suc)
 apply (rule sumr_pos_lt_pair)
 apply (erule sums_summable, safe)
 apply (simp (no_asm) add: divide_inverse real_0_less_add_iff mult_assoc [symmetric] 
@@ -1520,10 +1518,10 @@
 done
 
 lemma cos_pi [simp]: "cos pi = -1"
-by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp add: times_divide_eq)
+by (cut_tac x = "pi/2" and y = "pi/2" in cos_add, simp)
 
 lemma sin_pi [simp]: "sin pi = 0"
-by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp add: times_divide_eq)
+by (cut_tac x = "pi/2" and y = "pi/2" in sin_add, simp)
 
 lemma sin_cos_eq: "sin x = cos (pi/2 - x)"
 by (simp add: diff_minus cos_add)
@@ -1706,7 +1704,7 @@
 apply (cut_tac x="-x" in cos_zero_lemma, simp, simp) 
 apply (force simp add: minus_equation_iff [of x]) 
 apply (auto simp only: odd_Suc_mult_two_ex real_of_nat_Suc left_distrib) 
-apply (auto simp add: cos_add times_divide_eq)
+apply (auto simp add: cos_add)
 done
 
 (* ditto: but to a lesser extent *)
@@ -1719,7 +1717,7 @@
 apply (drule sin_zero_lemma, assumption+)
 apply (cut_tac x="-x" in sin_zero_lemma, simp, simp, safe)
 apply (force simp add: minus_equation_iff [of x]) 
-apply (auto simp add: even_mult_two_ex times_divide_eq)
+apply (auto simp add: even_mult_two_ex)
 done
 
 
@@ -1757,7 +1755,7 @@
 apply (simp add: tan_def)
 apply (rule_tac c1 = "cos x * cos y" in real_mult_right_cancel [THEN subst])
 apply (auto simp add: mult_assoc left_distrib)
-apply (simp add: sin_add times_divide_eq)
+apply (simp add: sin_add)
 done
 
 lemma tan_add:
@@ -2068,7 +2066,7 @@
 by (rule DERIV_exp [THEN DERIV_isCont])
 
 lemma sin_zero_abs_cos_one: "sin x = 0 ==> \<bar>cos x\<bar> = 1"
-by (auto simp add: sin_zero_iff even_mult_two_ex times_divide_eq)
+by (auto simp add: sin_zero_iff even_mult_two_ex)
 
 lemma exp_eq_one_iff [simp]: "(exp x = 1) = (x = 0)"
 apply auto
@@ -2185,7 +2183,7 @@
 lemma real_divide_square_eq [simp]: "(((r::real) * a) / (r * r)) = a / r"
 apply (simp add: divide_inverse)
 apply (case_tac "r=0")
-apply (auto simp add: inverse_mult_distrib mult_ac)
+apply (auto simp add: mult_ac)
 done
 
 
@@ -2456,7 +2454,7 @@
 apply (rule order_less_le_trans [of _ "7/5"], simp) 
 apply (rule_tac n = 1 in realpow_increasing)
   prefer 3 apply (simp add: numeral_2_eq_2 [symmetric] del: realpow_Suc)
-apply (simp_all add: numeral_2_eq_2 times_divide_eq)
+apply (simp_all add: numeral_2_eq_2)
 done
 
 lemma lemma_real_divide_sqrt_less: "0 < u ==> u / sqrt 2 < u"
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Integ/IntDef.thy
--- a/src/HOL/Integ/IntDef.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Integ/IntDef.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -559,80 +559,6 @@
 by (simp add: linorder_not_less neg_def)
 
 
-subsection{*Embedding of the Naturals into any @{text
-comm_semiring_1_cancel}: @{term of_nat}*}
-
-consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
-
-primrec
-  of_nat_0:   "of_nat 0 = 0"
-  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
-
-lemma of_nat_1 [simp]: "of_nat 1 = 1"
-by simp
-
-lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
-apply (induct m)
-apply (simp_all add: add_ac)
-done
-
-lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
-apply (induct m)
-apply (simp_all add: mult_ac add_ac right_distrib)
-done
-
-lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
-apply (induct m, simp_all)
-apply (erule order_trans)
-apply (rule less_add_one [THEN order_less_imp_le])
-done
-
-lemma less_imp_of_nat_less:
-     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
-apply (induct m n rule: diff_induct, simp_all)
-apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
-done
-
-lemma of_nat_less_imp_less:
-     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
-apply (induct m n rule: diff_induct, simp_all)
-apply (insert zero_le_imp_of_nat)
-apply (force simp add: linorder_not_less [symmetric])
-done
-
-lemma of_nat_less_iff [simp]:
-     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
-by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
-
-text{*Special cases where either operand is zero*}
-declare of_nat_less_iff [of 0, simplified, simp]
-declare of_nat_less_iff [of _ 0, simplified, simp]
-
-lemma of_nat_le_iff [simp]:
-     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
-by (simp add: linorder_not_less [symmetric])
-
-text{*Special cases where either operand is zero*}
-declare of_nat_le_iff [of 0, simplified, simp]
-declare of_nat_le_iff [of _ 0, simplified, simp]
-
-text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
-to exclude the possibility of a finite field, which indeed wraps back to
-zero.*}
-lemma of_nat_eq_iff [simp]:
-     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
-by (simp add: order_eq_iff)
-
-text{*Special cases where either operand is zero*}
-declare of_nat_eq_iff [of 0, simplified, simp]
-declare of_nat_eq_iff [of _ 0, simplified, simp]
-
-lemma of_nat_diff [simp]:
-     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
-by (simp del: of_nat_add
-	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
-
-
 subsection{*The Set of Natural Numbers*}
 
 constdefs
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Nat.thy
--- a/src/HOL/Nat.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Nat.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -1022,4 +1022,5 @@
   apply (fastsimp dest: mult_less_mono2)
   done
 
+
 end
diff -r d8edf54cc28c -r 333a88244569 src/HOL/NatArith.thy
--- a/src/HOL/NatArith.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/NatArith.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -162,5 +162,78 @@
 val diff_Suc_diff_eq2 = thm "diff_Suc_diff_eq2";
 *}
 
+subsection{*Embedding of the Naturals into any @{text
+comm_semiring_1_cancel}: @{term of_nat}*}
+
+consts of_nat :: "nat => 'a::comm_semiring_1_cancel"
+
+primrec
+  of_nat_0:   "of_nat 0 = 0"
+  of_nat_Suc: "of_nat (Suc m) = of_nat m + 1"
+
+lemma of_nat_1 [simp]: "of_nat 1 = 1"
+by simp
+
+lemma of_nat_add [simp]: "of_nat (m+n) = of_nat m + of_nat n"
+apply (induct m)
+apply (simp_all add: add_ac)
+done
+
+lemma of_nat_mult [simp]: "of_nat (m*n) = of_nat m * of_nat n"
+apply (induct m)
+apply (simp_all add: mult_ac add_ac right_distrib)
+done
+
+lemma zero_le_imp_of_nat: "0 \<le> (of_nat m::'a::ordered_semidom)"
+apply (induct m, simp_all)
+apply (erule order_trans)
+apply (rule less_add_one [THEN order_less_imp_le])
+done
+
+lemma less_imp_of_nat_less:
+     "m < n ==> of_nat m < (of_nat n::'a::ordered_semidom)"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert add_le_less_mono [OF zero_le_imp_of_nat zero_less_one], force)
+done
+
+lemma of_nat_less_imp_less:
+     "of_nat m < (of_nat n::'a::ordered_semidom) ==> m < n"
+apply (induct m n rule: diff_induct, simp_all)
+apply (insert zero_le_imp_of_nat)
+apply (force simp add: linorder_not_less [symmetric])
+done
+
+lemma of_nat_less_iff [simp]:
+     "(of_nat m < (of_nat n::'a::ordered_semidom)) = (m<n)"
+by (blast intro: of_nat_less_imp_less less_imp_of_nat_less)
+
+text{*Special cases where either operand is zero*}
+declare of_nat_less_iff [of 0, simplified, simp]
+declare of_nat_less_iff [of _ 0, simplified, simp]
+
+lemma of_nat_le_iff [simp]:
+     "(of_nat m \<le> (of_nat n::'a::ordered_semidom)) = (m \<le> n)"
+by (simp add: linorder_not_less [symmetric])
+
+text{*Special cases where either operand is zero*}
+declare of_nat_le_iff [of 0, simplified, simp]
+declare of_nat_le_iff [of _ 0, simplified, simp]
+
+text{*The ordering on the @{text comm_semiring_1_cancel} is necessary
+to exclude the possibility of a finite field, which indeed wraps back to
+zero.*}
+lemma of_nat_eq_iff [simp]:
+     "(of_nat m = (of_nat n::'a::ordered_semidom)) = (m = n)"
+by (simp add: order_eq_iff)
+
+text{*Special cases where either operand is zero*}
+declare of_nat_eq_iff [of 0, simplified, simp]
+declare of_nat_eq_iff [of _ 0, simplified, simp]
+
+lemma of_nat_diff [simp]:
+     "n \<le> m ==> of_nat (m - n) = of_nat m - (of_nat n :: 'a::comm_ring_1)"
+by (simp del: of_nat_add
+	 add: compare_rls of_nat_add [symmetric] split add: nat_diff_split)
+
 
 end
diff -r d8edf54cc28c -r 333a88244569 src/HOL/OrderedGroup.thy
--- a/src/HOL/OrderedGroup.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/OrderedGroup.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -319,6 +319,11 @@
   shows  "[|0\<le>a; b\<le>c|] ==> b \<le> a + c"
 by (insert add_mono [of 0 a b c], simp)
 
+lemma add_increasing2:
+  fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
+  shows  "[|0\<le>c; b\<le>a|] ==> b \<le> a + c"
+by (simp add:add_increasing add_commute[of a])
+
 lemma add_strict_increasing:
   fixes c :: "'a::{pordered_ab_semigroup_add_imp_le, comm_monoid_add}"
   shows "[|0<a; b\<le>c|] ==> b < a + c"
@@ -806,7 +811,7 @@
 lemma abs_le_iff: "(abs a \<le> b) = (a \<le> b & -a \<le> (b::'a::lordered_ab_group_abs))"
 by (blast intro: abs_leI dest: abs_le_D1 abs_le_D2)
 
-lemma abs_triangle_ineq: "abs (a+b) \<le> abs a + abs (b::'a::lordered_ab_group_abs)"
+lemma abs_triangle_ineq: "abs(a+b) \<le> abs a + abs(b::'a::lordered_ab_group_abs)"
 proof -
   have g:"abs a + abs b = join (a+b) (join (-a-b) (join (-a+b) (a + (-b))))" (is "_=join ?m ?n")
     apply (simp add: abs_lattice add_meet_join_distribs join_aci)
@@ -829,6 +834,17 @@
   finally show ?thesis .
 qed
 
+lemma abs_add_abs[simp]:
+fixes a:: "'a::{lordered_ab_group_abs}"
+shows "abs(abs a + abs b) = abs a + abs b" (is "?L = ?R")
+proof (rule order_antisym)
+  show "?L \<ge> ?R" by(rule abs_ge_self)
+next
+  have "?L \<le> \<bar>\<bar>a\<bar>\<bar> + \<bar>\<bar>b\<bar>\<bar>" by(rule abs_triangle_ineq)
+  also have "\<dots> = ?R" by simp
+  finally show "?L \<le> ?R" .
+qed
+
 text {* Needed for abelian cancellation simprocs: *}
 
 lemma add_cancel_21: "((x::'a::ab_group_add) + (y + z) = y + u) = (x + z = u)"
diff -r d8edf54cc28c -r 333a88244569 src/HOL/Real/RComplete.thy
--- a/src/HOL/Real/RComplete.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/Real/RComplete.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -389,7 +389,7 @@
 lemma floor_eq3: "[| real n < x; x < real (Suc n) |] ==> nat(floor x) = n"
 apply (rule inj_int [THEN injD])
 apply (simp add: real_of_nat_Suc)
-apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "of_nat n"])
+apply (simp add: real_of_nat_Suc floor_eq floor_eq [where n = "int n"])
 done
 
 lemma floor_eq4: "[| real n \<le> x; x < real (Suc n) |] ==> nat(floor x) = n"
@@ -532,7 +532,3 @@
 
 
 end
-
-
-
-
diff -r d8edf54cc28c -r 333a88244569 src/HOL/SetInterval.thy
--- a/src/HOL/SetInterval.thy	Sat Feb 19 18:44:34 2005 +0100
+++ b/src/HOL/SetInterval.thy	Mon Feb 21 15:04:10 2005 +0100
@@ -589,6 +589,22 @@
 lemma Summation_Suc[simp]: "(\<Sum>i < Suc n. b i) = b n + (\<Sum>i < n. b i)"
 by (simp add:lessThan_Suc)
 
+lemma setsum_add_nat_ivl: "\<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 setsum_diff_nat_ivl:
+fixes f :: "nat \<Rightarrow> 'a::ab_group_add"
+shows "\<lbrakk> m \<le> n; n \<le> p \<rbrakk> \<Longrightarrow>
+  setsum f {m..<p} - setsum f {m..<n} = setsum f {n..<p}"
+using setsum_add_nat_ivl [of m n p f,symmetric]
+apply (simp add: add_ac)
+done
+
+lemma setsum_shift_bounds_nat_ivl:
+  "setsum f {m+k..<n+k} = setsum (%i. f(i + k)){m..<n::nat}"
+by (induct "n", auto simp:atLeastLessThanSuc)
+
 
 ML
 {*