--- a/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 14 14:37:47 2011 +0100
+++ b/src/HOL/Multivariate_Analysis/Extended_Real_Limits.thy Mon Mar 14 14:37:49 2011 +0100
@@ -1028,7 +1028,7 @@
qed simp
qed
-lemma setsum_of_pextreal:
+lemma setsum_real_of_extreal:
assumes "\<And>x. x \<in> S \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
shows "(\<Sum>x\<in>S. real (f x)) = real (setsum f S)"
proof -
@@ -1062,17 +1062,6 @@
by induct (auto simp: extreal_right_distrib setsum_nonneg)
qed simp
-lemma setsum_real_of_extreal:
- assumes "\<And>x. x \<in> A \<Longrightarrow> \<bar>f x\<bar> \<noteq> \<infinity>"
- shows "real (\<Sum>x\<in>A. f x) = (\<Sum>x\<in>A. real (f x))"
-proof cases
- assume "finite A" from this assms show ?thesis
- proof induct
- case (insert a A) then show ?case
- by (simp add: real_of_extreal_add setsum_Inf)
- qed simp
-qed simp
-
lemma sums_extreal_positive:
fixes f :: "nat \<Rightarrow> extreal" assumes "\<And>i. 0 \<le> f i" shows "f sums (SUP n. \<Sum>i<n. f i)"
proof -