author huffman Tue, 26 May 2009 07:39:52 -0700 changeset 31257 547bf9819d6c parent 31256 cf75908fd3c3 child 31258 43a418a41317
clean up some rsum proofs
 src/HOL/Integration.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integration.thy	Tue May 26 13:40:50 2009 +0200
+++ b/src/HOL/Integration.thy	Tue May 26 07:39:52 2009 -0700
@@ -66,6 +66,20 @@
apply force
done

+lemma rsum_zero [simp]: "rsum (D,p) (\<lambda>x. 0) = 0"
+unfolding rsum_def by simp
+
+lemma rsum_left_distrib: "rsum (D,p) f * c = rsum (D,p) (\<lambda>x. f x * c)"
+unfolding rsum_def
+by (simp add: setsum_left_distrib setsum_right_distrib algebra_simps)
+
+lemma rsum_right_distrib: "c * rsum (D,p) f = rsum (D,p) (\<lambda>x. c * f x)"
+unfolding rsum_def
+by (simp add: setsum_left_distrib setsum_right_distrib algebra_simps)
+
+lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"
+
lemma psize_unique:
assumes 1: "\<forall>n < N. D(n) < D(Suc n)"
assumes 2: "\<forall>n \<ge> N. D(n) = D(N)"
@@ -365,16 +379,15 @@
"[| a \<le> b; Integral(a,b) f k |] ==> Integral(a,b) (%x. c * f x) (c * k)"
dest: Integral_unique [OF order_refl Integral_zero])
-apply (auto simp add: rsum_def Integral_def setsum_right_distrib[symmetric] mult_assoc)
-apply (rule_tac a2 = c in abs_ge_zero [THEN order_le_imp_less_or_eq, THEN disjE])
- prefer 2 apply force
-apply (drule_tac x = "e/abs c" in spec, auto)
-apply (rule exI, auto)
-apply (drule spec)+
-apply auto
-apply (rule_tac z1 = "inverse (abs c)" in real_mult_less_iff1 [THEN iffD1])
-apply (auto simp add: abs_mult divide_inverse [symmetric] right_diff_distrib [symmetric])
+apply (auto simp add: Integral_def setsum_right_distrib[symmetric] mult_assoc)
+apply (case_tac "c = 0", force)
+apply (drule_tac x = "e/abs c" in spec)
+apply clarify
+apply (rule_tac x="g" in exI, clarify)
+apply (drule_tac x="D" in spec, drule_tac x="p" in spec)
+apply (simp add: pos_less_divide_eq abs_mult [symmetric]
+                 algebra_simps rsum_right_distrib)
done

text{*Fundamental theorem of calculus (Part I)*}
@@ -759,9 +772,6 @@
apply arith
done

-lemma rsum_add: "rsum (D, p) (%x. f x + g x) =  rsum (D, p) f + rsum(D, p) g"