1.1 --- a/src/HOL/Integration.thy	Tue May 26 13:40:50 2009 +0200
     1.2 +++ b/src/HOL/Integration.thy	Tue May 26 07:39:52 2009 -0700
     1.3 @@ -66,6 +66,20 @@
     1.4  apply force
     1.5  done
     1.6  
     1.7 +lemma rsum_zero [simp]: "rsum (D,p) (\<lambda>x. 0) = 0"
     1.8 +unfolding rsum_def by simp
     1.9 +
    1.10 +lemma rsum_left_distrib: "rsum (D,p) f * c = rsum (D,p) (\<lambda>x. f x * c)"
    1.11 +unfolding rsum_def
    1.12 +by (simp add: setsum_left_distrib setsum_right_distrib algebra_simps)
    1.13 +
    1.14 +lemma rsum_right_distrib: "c * rsum (D,p) f = rsum (D,p) (\<lambda>x. c * f x)"
    1.15 +unfolding rsum_def
    1.16 +by (simp add: setsum_left_distrib setsum_right_distrib algebra_simps)
    1.17 +
    1.18 +lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
    1.19 +by (simp add: rsum_def setsum_addf left_distrib)
    1.20 +
    1.21  lemma psize_unique:
    1.22    assumes 1: "\<forall>n < N. D(n) < D(Suc n)"
    1.23    assumes 2: "\<forall>n \<ge> N. D(n) = D(N)"
    1.24 @@ -365,16 +379,15 @@
    1.25       "[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
    1.26  apply (auto simp add: order_le_less 
    1.27              dest: Integral_unique [OF order_refl Integral_zero])
    1.28 -apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
    1.29 -apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE])
    1.30 - prefer 2 apply force
    1.31 -apply (drule_tac x = "e/abs c" in spec, auto)
    1.32 -apply (simp add: zero_less_mult_iff divide_inverse)
    1.33 -apply (rule exI, auto)
    1.34 -apply (drule spec)+
    1.35 -apply auto
    1.36 -apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
    1.37 -apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric])
    1.38 +apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
    1.39 +apply (case_tac "c = 0", force)
    1.40 +apply (drule_tac x = "e/abs c" in spec)
    1.41 +apply (simp add: divide_pos_pos)
    1.42 +apply clarify
    1.43 +apply (rule_tac x="g" in exI, clarify)
    1.44 +apply (drule_tac x="D" in spec, drule_tac x="p" in spec)
    1.45 +apply (simp add: pos_less_divide_eq abs_mult [symmetric]
    1.46 +                 algebra_simps rsum_right_distrib)
    1.47  done
    1.48  
    1.49  text{*Fundamental theorem of calculus (Part I)*}
    1.50 @@ -759,9 +772,6 @@
    1.51  apply arith
    1.52  done
    1.53  
    1.54 -lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
    1.55 -by (simp add: rsum_def setsum_addf left_distrib)
    1.56 -
    1.57  text{* Bartle/Sherbert: Theorem 10.1.5 p. 278 *}
    1.58  lemma Integral_add_fun:
    1.59      "[| a \<le> b; Integral(a,b) f k1; Integral(a,b) g k2 |]