# HG changeset patch
# User hoelzl
# Date 1300109864 -3600
# Node ID dbfc073c310d232150e2e14fccd4f69b2836a0bd
# Parent  3fdbc7d5b5259b0dd03716a7668572783d85e3dc
introduce setsum on extreal

diff -r 3fdbc7d5b525 -r dbfc073c310d src/HOL/Library/Extended_Reals.thy
--- a/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:42 2011 +0100
+++ b/src/HOL/Library/Extended_Reals.thy	Mon Mar 14 14:37:44 2011 +0100
@@ -3076,4 +3076,51 @@
   "[| (a::extreal) <= x; c <= x |] ==> max a c <= x"
   by (metis sup_extreal_def sup_least)
 
+subsection {* Sums *}
+
+lemma setsum_extreal[simp]:
+  "(\<Sum>x\<in>A. extreal (f x)) = extreal (\<Sum>x\<in>A. f x)"
+proof cases
+  assume "finite A" then show ?thesis by induct auto
+qed simp
+
+lemma setsum_Pinfty: "(\<Sum>x\<in>P. f x) = \<infinity> \<longleftrightarrow> (finite P \<and> (\<exists>i\<in>P. f i = \<infinity>))"
+proof safe
+  assume *: "setsum f P = \<infinity>"
+  show "finite P"
+  proof (rule ccontr) assume "infinite P" with * show False by auto qed
+  show "\<exists>i\<in>P. f i = \<infinity>"
+  proof (rule ccontr)
+    assume "\<not> ?thesis" then have "\<And>i. i \<in> P \<Longrightarrow> f i \<noteq> \<infinity>" by auto
+    from `finite P` this have "setsum f P \<noteq> \<infinity>"
+      by induct auto
+    with * show False by auto
+  qed
+next
+  fix i assume "finite P" "i \<in> P" "f i = \<infinity>"
+  thus "setsum f P = \<infinity>"
+  proof induct
+    case (insert x A)
+    show ?case using insert by (cases "x = i") auto
+  qed simp
+qed
+
+lemma setsum_of_pextreal:
+  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 -
+  have "\<forall>x\<in>S. \<exists>r. f x = extreal r"
+  proof
+    fix x assume "x \<in> S"
+    from assms[OF this] show "\<exists>r. f x = extreal r" by (cases "f x") auto
+  qed
+  from bchoice[OF this] guess r ..
+  then show ?thesis by simp
+qed
+
+lemma setsum_0:
+  fixes f :: "'a \<Rightarrow> pextreal" assumes "finite A"
+  shows "(\<Sum>x\<in>A. f x) = 0 \<longleftrightarrow> (\<forall>i\<in>A. f i = 0)"
+  using assms by induct auto
+
 end