diff -r 15218eb98fd7 -r 8448713d48b7 src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Mon Mar 28 23:49:53 2011 +0200
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 29 14:27:31 2011 +0200
@@ -258,7 +258,21 @@
     by (simp add: Un)
 qed
 
-lemma (in algebra) countably_subadditive_subadditive:
+lemma (in ring_of_sets) disjointed_additive:
+  assumes f: "positive M f" "additive M f" and A: "range A \<subseteq> sets M" "incseq A"
+  shows "(\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
+proof (induct n)
+  case (Suc n)
+  then have "(\<Sum>i\<le>Suc n. f (disjointed A i)) = f (A n) + f (disjointed A (Suc n))"
+    by simp
+  also have "\<dots> = f (A n \<union> disjointed A (Suc n))"
+    using A by (subst f(2)[THEN additiveD]) (auto simp: disjointed_incseq)
+  also have "A n \<union> disjointed A (Suc n) = A (Suc n)"
+    using `incseq A` by (auto dest: incseq_SucD simp: disjointed_incseq)
+  finally show ?case .
+qed simp
+
+lemma (in ring_of_sets) countably_subadditive_subadditive:
   assumes f: "positive M f" and cs: "countably_subadditive M f"
   shows  "subadditive M f"
 proof (auto simp add: subadditive_def)
@@ -277,7 +291,7 @@
     by (auto simp add: Un o_def suminf_binaryset_eq positive_def)
 qed
 
-lemma (in algebra) additive_sum:
+lemma (in ring_of_sets) additive_sum:
   fixes A:: "nat \<Rightarrow> 'a set"
   assumes f: "positive M f" and ad: "additive M f" and "finite S"
       and A: "range A \<subseteq> sets M"
@@ -785,17 +799,17 @@
   moreover
   have "Inf (measure_set M f s)
        \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
-    proof -
+  proof -
     have "Inf (measure_set M f s) = Inf (measure_set M f ((s\<inter>x) \<union> (s-x)))"
       by (metis Un_Diff_Int Un_commute)
     also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
       apply (rule subadditiveD)
-      apply (rule algebra.countably_subadditive_subadditive[OF algebra_Pow])
+      apply (rule ring_of_sets.countably_subadditive_subadditive [OF ring_of_sets_Pow])
       apply (simp add: positive_def inf_measure_empty[OF posf] inf_measure_pos[OF posf])
       apply (rule inf_measure_countably_subadditive)
       using s by (auto intro!: posf inc)
     finally show ?thesis .
-    qed
+  qed
   ultimately
   show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
         = Inf (measure_set M f s)"
@@ -837,4 +851,183 @@
     by (intro exI[of _ ?infm]) auto
 qed
 
+subsubsection {*Alternative instances of caratheodory*}
+
+lemma sums_def2:
+  "f sums x \<longleftrightarrow> (\<lambda>n. (\<Sum>i\<le>n. f i)) ----> x"
+  unfolding sums_def
+  apply (subst LIMSEQ_Suc_iff[symmetric])
+  unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost ..
+
+lemma (in ring_of_sets) countably_additive_iff_continuous_from_below:
+  assumes f: "positive M f" "additive M f"
+  shows "countably_additive M f \<longleftrightarrow>
+    (\<forall>A. range A \<subseteq> sets M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i))"
+  unfolding countably_additive_def
+proof safe
+  assume count_sum: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> UNION UNIV A \<in> sets M \<longrightarrow> (\<Sum>i. f (A i)) = f (UNION UNIV A)"
+  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
+  then have dA: "range (disjointed A) \<subseteq> sets M" by (auto simp: range_disjointed_sets)
+  with count_sum[THEN spec, of "disjointed A"] A(3)
+  have f_UN: "(\<Sum>i. f (disjointed A i)) = f (\<Union>i. A i)"
+    by (auto simp: UN_disjointed_eq disjoint_family_disjointed)
+  moreover have "(\<lambda>n. (\<Sum>i=0..<n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+    using f(1)[unfolded positive_def] dA
+    by (auto intro!: summable_sumr_LIMSEQ_suminf summable_extreal_pos)
+  from LIMSEQ_Suc[OF this]
+  have "(\<lambda>n. (\<Sum>i\<le>n. f (disjointed A i))) ----> (\<Sum>i. f (disjointed A i))"
+    unfolding atLeastLessThanSuc_atLeastAtMost atLeast0AtMost .
+  moreover have "\<And>n. (\<Sum>i\<le>n. f (disjointed A i)) = f (A n)"
+    using disjointed_additive[OF f A(1,2)] .
+  ultimately show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)" by simp
+next
+  assume cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> incseq A \<longrightarrow> (\<Union>i. A i) \<in> sets M \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "disjoint_family A" "(\<Union>i. A i) \<in> sets M"
+  have *: "(\<Union>n. (\<Union>i\<le>n. A i)) = (\<Union>i. A i)" by auto
+  have "(\<lambda>n. f (\<Union>i\<le>n. A i)) ----> f (\<Union>i. A i)"
+  proof (unfold *[symmetric], intro cont[rule_format])
+    show "range (\<lambda>i. \<Union> i\<le>i. A i) \<subseteq> sets M" "(\<Union>i. \<Union> i\<le>i. A i) \<in> sets M"
+      using A * by auto
+  qed (force intro!: incseq_SucI)
+  moreover have "\<And>n. f (\<Union>i\<le>n. A i) = (\<Sum>i\<le>n. f (A i))"
+    using A
+    by (intro additive_sum[OF f, of _ A, symmetric])
+       (auto intro: disjoint_family_on_mono[where B=UNIV])
+  ultimately
+  have "(\<lambda>i. f (A i)) sums f (\<Union>i. A i)"
+    unfolding sums_def2 by simp
+  from sums_unique[OF this]
+  show "(\<Sum>i. f (A i)) = f (\<Union>i. A i)" by simp
+qed
+
+lemma uminus_extreal_add_uminus_uminus:
+  fixes a b :: extreal shows "a \<noteq> \<infinity> \<Longrightarrow> b \<noteq> \<infinity> \<Longrightarrow> - (- a + - b) = a + b"
+  by (cases rule: extreal2_cases[of a b]) auto
+
+lemma INFI_extreal_add:
+  assumes "decseq f" "decseq g" and fin: "\<And>i. f i \<noteq> \<infinity>" "\<And>i. g i \<noteq> \<infinity>"
+  shows "(INF i. f i + g i) = INFI UNIV f + INFI UNIV g"
+proof -
+  have INF_less: "(INF i. f i) < \<infinity>" "(INF i. g i) < \<infinity>"
+    using assms unfolding INF_less_iff by auto
+  { fix i from fin[of i] have "- ((- f i) + (- g i)) = f i + g i"
+      by (rule uminus_extreal_add_uminus_uminus) }
+  then have "(INF i. f i + g i) = (INF i. - ((- f i) + (- g i)))"
+    by simp
+  also have "\<dots> = INFI UNIV f + INFI UNIV g"
+    unfolding extreal_INFI_uminus
+    using assms INF_less
+    by (subst SUPR_extreal_add)
+       (auto simp: extreal_SUPR_uminus intro!: uminus_extreal_add_uminus_uminus)
+  finally show ?thesis .
+qed
+
+lemma (in ring_of_sets) continuous_from_above_iff_empty_continuous:
+  assumes f: "positive M f" "additive M f"
+  shows "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))
+     \<longleftrightarrow> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0)"
+proof safe
+  assume cont: "(\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) \<in> sets M \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> f (\<Inter>i. A i))"
+  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "decseq A" "(\<Inter>i. A i) = {}" "\<forall>i. f (A i) \<noteq> \<infinity>"
+  with cont[THEN spec, of A] show "(\<lambda>i. f (A i)) ----> 0"
+    using `positive M f`[unfolded positive_def] by auto
+next
+  assume cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<forall>i. f (A i) \<noteq> \<infinity>) \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+  fix A :: "nat \<Rightarrow> 'a set" assume A: "range A \<subseteq> sets M" "decseq A" "(\<Inter>i. A i) \<in> sets M" "\<forall>i. f (A i) \<noteq> \<infinity>"
+
+  have f_mono: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<subseteq> b \<Longrightarrow> f a \<le> f b"
+    using additive_increasing[OF f] unfolding increasing_def by simp
+
+  have decseq_fA: "decseq (\<lambda>i. f (A i))"
+    using A by (auto simp: decseq_def intro!: f_mono)
+  have decseq: "decseq (\<lambda>i. A i - (\<Inter>i. A i))"
+    using A by (auto simp: decseq_def)
+  then have decseq_f: "decseq (\<lambda>i. f (A i - (\<Inter>i. A i)))"
+    using A unfolding decseq_def by (auto intro!: f_mono Diff)
+  have "f (\<Inter>x. A x) \<le> f (A 0)"
+    using A by (auto intro!: f_mono)
+  then have f_Int_fin: "f (\<Inter>x. A x) \<noteq> \<infinity>"
+    using A by auto
+  { fix i
+    have "f (A i - (\<Inter>i. A i)) \<le> f (A i)" using A by (auto intro!: f_mono)
+    then have "f (A i - (\<Inter>i. A i)) \<noteq> \<infinity>"
+      using A by auto }
+  note f_fin = this
+  have "(\<lambda>i. f (A i - (\<Inter>i. A i))) ----> 0"
+  proof (intro cont[rule_format, OF _ decseq _ f_fin])
+    show "range (\<lambda>i. A i - (\<Inter>i. A i)) \<subseteq> sets M" "(\<Inter>i. A i - (\<Inter>i. A i)) = {}"
+      using A by auto
+  qed
+  from INF_Lim_extreal[OF decseq_f this]
+  have "(INF n. f (A n - (\<Inter>i. A i))) = 0" .
+  moreover have "(INF n. f (\<Inter>i. A i)) = f (\<Inter>i. A i)"
+    by auto
+  ultimately have "(INF n. f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i)) = 0 + f (\<Inter>i. A i)"
+    using A(4) f_fin f_Int_fin
+    by (subst INFI_extreal_add) (auto simp: decseq_f)
+  moreover {
+    fix n
+    have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f ((A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i))"
+      using A by (subst f(2)[THEN additiveD]) auto
+    also have "(A n - (\<Inter>i. A i)) \<union> (\<Inter>i. A i) = A n"
+      by auto
+    finally have "f (A n - (\<Inter>i. A i)) + f (\<Inter>i. A i) = f (A n)" . }
+  ultimately have "(INF n. f (A n)) = f (\<Inter>i. A i)"
+    by simp
+  with LIMSEQ_extreal_INFI[OF decseq_fA]
+  show "(\<lambda>i. f (A i)) ----> f (\<Inter>i. A i)" by simp
+qed
+
+lemma positiveD1: "positive M f \<Longrightarrow> f {} = 0" by (auto simp: positive_def)
+lemma positiveD2: "positive M f \<Longrightarrow> A \<in> sets M \<Longrightarrow> 0 \<le> f A" by (auto simp: positive_def)
+
+lemma (in ring_of_sets) empty_continuous_imp_continuous_from_below:
+  assumes f: "positive M f" "additive M f" "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
+  assumes cont: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> decseq A \<longrightarrow> (\<Inter>i. A i) = {} \<longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+  assumes A: "range A \<subseteq> sets M" "incseq A" "(\<Union>i. A i) \<in> sets M"
+  shows "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+proof -
+  have "\<forall>A\<in>sets M. \<exists>x. f A = extreal x"
+  proof
+    fix A assume "A \<in> sets M" with f show "\<exists>x. f A = extreal x"
+      unfolding positive_def by (cases "f A") auto
+  qed
+  from bchoice[OF this] guess f' .. note f' = this[rule_format]
+  from A have "(\<lambda>i. f ((\<Union>i. A i) - A i)) ----> 0"
+    by (intro cont[rule_format]) (auto simp: decseq_def incseq_def)
+  moreover
+  { fix i
+    have "f ((\<Union>i. A i) - A i) + f (A i) = f ((\<Union>i. A i) - A i \<union> A i)"
+      using A by (intro f(2)[THEN additiveD, symmetric]) auto
+    also have "(\<Union>i. A i) - A i \<union> A i = (\<Union>i. A i)"
+      by auto
+    finally have "f' (\<Union>i. A i) - f' (A i) = f' ((\<Union>i. A i) - A i)"
+      using A by (subst (asm) (1 2 3) f') auto
+    then have "f ((\<Union>i. A i) - A i) = extreal (f' (\<Union>i. A i) - f' (A i))"
+      using A f' by auto }
+  ultimately have "(\<lambda>i. f' (\<Union>i. A i) - f' (A i)) ----> 0"
+    by (simp add: zero_extreal_def)
+  then have "(\<lambda>i. f' (A i)) ----> f' (\<Union>i. A i)"
+    by (rule LIMSEQ_diff_approach_zero2[OF LIMSEQ_const])
+  then show "(\<lambda>i. f (A i)) ----> f (\<Union>i. A i)"
+    using A by (subst (1 2) f') auto
+qed
+
+lemma (in ring_of_sets) empty_continuous_imp_countably_additive:
+  assumes f: "positive M f" "additive M f" and fin: "\<forall>A\<in>sets M. f A \<noteq> \<infinity>"
+  assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+  shows "countably_additive M f"
+  using countably_additive_iff_continuous_from_below[OF f]
+  using empty_continuous_imp_continuous_from_below[OF f fin] cont
+  by blast
+
+lemma (in ring_of_sets) caratheodory_empty_continuous:
+  assumes f: "positive M f" "additive M f" and fin: "\<And>A. A \<in> sets M \<Longrightarrow> f A \<noteq> \<infinity>"
+  assumes cont: "\<And>A. range A \<subseteq> sets M \<Longrightarrow> decseq A \<Longrightarrow> (\<Inter>i. A i) = {} \<Longrightarrow> (\<lambda>i. f (A i)) ----> 0"
+  shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
+            measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
+proof (intro caratheodory empty_continuous_imp_countably_additive f)
+  show "\<forall>A\<in>sets M. f A \<noteq> \<infinity>" using fin by auto
+qed (rule cont)
+
 end