diff -r a25e51e2d64d -r b16d99a72dc9 src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Thu Mar 04 19:50:45 2010 +0100
+++ b/src/HOL/Probability/Measure.thy	Thu Mar 04 21:52:26 2010 +0100
@@ -104,7 +104,7 @@
   have ra: "range (binaryset A B) \<subseteq> sets M"
    by (simp add: range_binaryset_eq empty A B) 
  have di:  "disjoint_family (binaryset A B)" using disj
-   by (simp add: disjoint_family_def binaryset_def Int_commute) 
+   by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
  from closed_cdi_Disj [OF cdi ra di]
  show ?thesis
    by (simp add: UN_binaryset_eq) 
@@ -118,7 +118,7 @@
   have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)"
     by (simp add: range_binaryset_eq  A B empty_sets smallest_ccdi_sets.Basic)
   have di:  "disjoint_family (binaryset A B)" using disj
-    by (simp add: disjoint_family_def binaryset_def Int_commute) 
+    by (simp add: disjoint_family_on_def binaryset_def Int_commute) 
   from Disj [OF ra di]
   show ?thesis
     by (simp add: UN_binaryset_eq) 
@@ -164,7 +164,7 @@
   have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj
     by blast
   moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj
-    by (auto simp add: disjoint_family_def) 
+    by (auto simp add: disjoint_family_on_def) 
   ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M"
     by (rule smallest_ccdi_sets.Disj) 
   show ?case
@@ -208,7 +208,7 @@
   have "range (\<lambda>i. A i \<inter> b) \<in> Pow(smallest_ccdi_sets M)" using Disj
     by blast
   moreover have "disjoint_family (\<lambda>i. A i \<inter> b)" using Disj
-    by (auto simp add: disjoint_family_def) 
+    by (auto simp add: disjoint_family_on_def) 
   ultimately have 2: "(\<Union>i. (\<lambda>i. A i \<inter> b) i) \<in> smallest_ccdi_sets M"
     by (rule smallest_ccdi_sets.Disj) 
   show ?case
@@ -355,7 +355,7 @@
   hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n"
     by (metis add_commute le_add_diff_inverse nat_less_le)
   thus ?thesis
-    by (auto simp add: disjoint_family_def)
+    by (auto simp add: disjoint_family_on_def)
       (metis insert_absorb insert_subset le_SucE le_antisym not_leE) 
 qed
 
@@ -642,7 +642,7 @@
                   show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1"
                     using f12 rA2 by (auto simp add: measurable_def)
                   show "disjoint_family (\<lambda>i. f -` A i \<inter> space m1)" using dA
-                    by (auto simp add: disjoint_family_def) 
+                    by (auto simp add: disjoint_family_on_def) 
                   show "(\<Union>i. f -` A i \<inter> space m1) \<in> sets m1"
                     proof (rule sigma_algebra.countable_UN [OF sa1])
                       show "range (\<lambda>i. f -` A i \<inter> space m1) \<subseteq> sets m1" using f12 rA2
@@ -820,7 +820,98 @@
   thus ?thesis
     by (metis subset_refl s)
 qed
-  
+
+lemma (in measure_space) measure_finitely_additive':
+  assumes "f \<in> ({0 :: nat ..< n} \<rightarrow> sets M)"
+  assumes "\<And> a b. \<lbrakk>a < n ; b < n ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
+  assumes "s = \<Union> (f ` {0 ..< n})"
+  shows "(\<Sum> i \<in> {0 ..< n}. (measure M \<circ> f) i) = measure M s"
+proof -
+  def f' == "\<lambda> i. (if i < n then f i else {})"
+  have rf: "range f' \<subseteq> sets M" unfolding f'_def 
+    using assms empty_sets by auto
+  have df: "disjoint_family f'" unfolding f'_def disjoint_family_on_def 
+    using assms by simp
+  have "\<Union> range f' = (\<Union> i \<in> {0 ..< n}. f i)" 
+    unfolding f'_def by auto
+  then have "measure M s = measure M (\<Union> range f')" 
+    using assms by simp
+  then have part1: "(\<lambda> i. measure M (f' i)) sums measure M s" 
+    using df rf ca[unfolded countably_additive_def, rule_format, of f']
+    by auto
+
+  have "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f' i))" 
+    using series_zero[of "n" "\<lambda> i. measure M (f' i)", rule_format] 
+    unfolding f'_def by simp
+  also have "\<dots> = (\<Sum> i \<in> {0 ..< n}. measure M (f i))" 
+    unfolding f'_def by auto
+  finally have part2: "(\<lambda> i. measure M (f' i)) sums (\<Sum> i \<in> {0 ..< n}. measure M (f i))" by simp
+  show ?thesis 
+    using sums_unique[OF part1] 
+          sums_unique[OF part2] by auto
+qed
+
+
+lemma (in measure_space) measure_finitely_additive:
+  assumes "finite r"
+  assumes "r \<subseteq> sets M"
+  assumes d: "\<And> a b. \<lbrakk>a \<in> r ; b \<in> r ; a \<noteq> b\<rbrakk> \<Longrightarrow> a \<inter> b = {}"
+  shows "(\<Sum> i \<in> r. measure M i) = measure M (\<Union> r)"
+using assms
+proof -
+  (* counting the elements in r is enough *)
+  let ?R = "{0 ..< card r}"
+  obtain f where f: "f ` ?R = r" "inj_on f ?R"
+    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite r`]
+    by auto
+  hence f_into_sets: "f \<in> ?R \<rightarrow> sets M" using assms by auto
+  have disj: "\<And> a b. \<lbrakk>a \<in> ?R ; b \<in> ?R ; a \<noteq> b\<rbrakk> \<Longrightarrow> f a \<inter> f b = {}"
+  proof -
+    fix a b assume asm: "a \<in> ?R" "b \<in> ?R" "a \<noteq> b"
+    hence neq: "f a \<noteq> f b" using f[unfolded inj_on_def, rule_format] by blast
+    from asm have "f a \<in> r" "f b \<in> r" using f by auto
+    thus "f a \<inter> f b = {}" using d[of "f a" "f b"] f using neq by auto
+  qed
+  have "(\<Union> r) = (\<Union> i \<in> ?R. f i)"
+    using f by auto
+  hence "measure M (\<Union> r)= measure M (\<Union> i \<in> ?R. f i)" by simp
+  also have "\<dots> = (\<Sum> i \<in> ?R. measure M (f i))"
+    using measure_finitely_additive'[OF f_into_sets disj] by simp
+  also have "\<dots> = (\<Sum> a \<in> r. measure M a)" 
+    using f[rule_format] setsum_reindex[of f ?R "\<lambda> a. measure M a"] by auto
+  finally show ?thesis by simp
+qed
+
+lemma (in measure_space) measure_finitely_additive'':
+  assumes "finite s"
+  assumes "\<And> i. i \<in> s \<Longrightarrow> a i \<in> sets M"
+  assumes d: "disjoint_family_on a s"
+  shows "(\<Sum> i \<in> s. measure M (a i)) = measure M (\<Union> i \<in> s. a i)"
+using assms
+proof -
+  (* counting the elements in s is enough *)
+  let ?R = "{0 ..< card s}"
+  obtain f where f: "f ` ?R = s" "inj_on f ?R"
+    using ex_bij_betw_nat_finite[unfolded bij_betw_def, OF `finite s`]
+    by auto
+  hence f_into_sets: "a \<circ> f \<in> ?R \<rightarrow> sets M" using assms unfolding o_def by auto
+  have disj: "\<And> i j. \<lbrakk>i \<in> ?R ; j \<in> ?R ; i \<noteq> j\<rbrakk> \<Longrightarrow> (a \<circ> f) i \<inter> (a \<circ> f) j = {}"
+  proof -
+    fix i j assume asm: "i \<in> ?R" "j \<in> ?R" "i \<noteq> j"
+    hence neq: "f i \<noteq> f j" using f[unfolded inj_on_def, rule_format] by blast
+    from asm have "f i \<in> s" "f j \<in> s" using f by auto
+    thus "(a \<circ> f) i \<inter> (a \<circ> f) j = {}"
+      using d f neq unfolding disjoint_family_on_def by auto
+  qed
+  have "(\<Union> i \<in> s. a i) = (\<Union> i \<in> f ` ?R. a i)" using f by auto
+  hence "(\<Union> i \<in> s. a i) = (\<Union> i \<in> ?R. a (f i))" by auto
+  hence "measure M (\<Union> i \<in> s. a i) = (\<Sum> i \<in> ?R. measure M (a (f i)))"
+    using measure_finitely_additive'[OF f_into_sets disj] by simp
+  also have "\<dots> = (\<Sum> i \<in> s. measure M (a i))"
+    using f[rule_format] setsum_reindex[of f ?R "\<lambda> i. measure M (a i)"] by auto
+  finally show ?thesis by simp
+qed
+
 lemma (in sigma_algebra) sigma_algebra_extend:
      "sigma_algebra \<lparr>space = space M, sets = sets M, measure_space.measure = f\<rparr>"
    by unfold_locales (auto intro!: space_closed)
@@ -845,7 +936,7 @@
       hence "finite (A ` I)"
         by (metis finite_UnionD finite_subset fin) 
       moreover have "inj_on A I" using disj
-        by (auto simp add: I_def disjoint_family_def inj_on_def) 
+        by (auto simp add: I_def disjoint_family_on_def inj_on_def) 
       ultimately have finI: "finite I"
         by (metis finite_imageD)
       hence "\<exists>N. \<forall>m\<ge>N. A m = {}"
@@ -873,7 +964,7 @@
           have "f (A n \<union> (\<Union> x<n. A x)) = f (A n) + f (\<Union> i<n. A i)"
             proof (rule Caratheodory.additiveD [OF addf])
               show "A n \<inter> (\<Union> x<n. A x) = {}" using disj
-                by (auto simp add: disjoint_family_def nat_less_le) blast
+                by (auto simp add: disjoint_family_on_def nat_less_le) blast
               show "A n \<in> sets M" using A 
                 by (force simp add: Mf_def) 
               show "(\<Union>i<n. A i) \<in> sets M"
@@ -906,5 +997,4 @@
       \<Longrightarrow> measure_space M"
   by (rule measure_down [OF sigma_algebra.finite_additivity_sufficient], auto) 
 
-end
-
+end
\ No newline at end of file