# HG changeset patch
# User hoelzl
# Date 1300816385 -3600
# Node ID 6db76c88907a2737cc04b117def32b955ed4a9e2
# Parent  2b98b4c2e2f1f7da0d4bd5dde0993e7ecc367f06
generalized Caratheodory from algebra to ring_of_sets

diff -r 2b98b4c2e2f1 -r 6db76c88907a src/HOL/Probability/Caratheodory.thy
--- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
+++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 18:53:05 2011 +0100
@@ -148,7 +148,7 @@
 
 lemma (in algebra) lambda_system_empty:
   "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
-  by (auto simp add: positive_def lambda_system_eq algebra_def)
+  by (auto simp add: positive_def lambda_system_eq)
 
 lemma lambda_system_sets:
   "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
@@ -456,7 +456,7 @@
     by (simp add: measure_space_def)
 qed
 
-lemma (in algebra) additive_increasing:
+lemma (in ring_of_sets) additive_increasing:
   assumes posf: "positive M f" and addf: "additive M f"
   shows "increasing M f"
 proof (auto simp add: increasing_def)
@@ -472,7 +472,7 @@
   finally show "f x \<le> f y" by simp
 qed
 
-lemma (in algebra) countably_additive_additive:
+lemma (in ring_of_sets) countably_additive_additive:
   assumes posf: "positive M f" and ca: "countably_additive M f"
   shows "additive M f"
 proof (auto simp add: additive_def)
@@ -506,7 +506,7 @@
              simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
 qed
 
-lemma (in algebra) inf_measure_agrees:
+lemma (in ring_of_sets) inf_measure_agrees:
   assumes posf: "positive M f" and ca: "countably_additive M f"
       and s: "s \<in> sets M"
   shows "Inf (measure_set M f s) = f s"
@@ -575,7 +575,7 @@
               inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
 qed (rule inf_measure_pos[OF posf])
 
-lemma (in algebra) inf_measure_positive:
+lemma (in ring_of_sets) inf_measure_positive:
   assumes p: "positive M f" and "{} \<in> sets M"
   shows "positive M (\<lambda>x. Inf (measure_set M f x))"
 proof (unfold positive_def, intro conjI ballI)
@@ -583,7 +583,7 @@
   fix A assume "A \<in> sets M"
 qed (rule inf_measure_pos[OF p])
 
-lemma (in algebra) inf_measure_increasing:
+lemma (in ring_of_sets) inf_measure_increasing:
   assumes posf: "positive M f"
   shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr>
                     (\<lambda>x. Inf (measure_set M f x))"
@@ -593,7 +593,7 @@
 apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
 done
 
-lemma (in algebra) inf_measure_le:
+lemma (in ring_of_sets) inf_measure_le:
   assumes posf: "positive M f" and inc: "increasing M f"
       and x: "x \<in> {r . \<exists>A. range A \<subseteq> sets M \<and> s \<subseteq> (\<Union>i. A i) \<and> (\<Sum>i. f (A i)) = r}"
   shows "Inf (measure_set M f s) \<le> x"
@@ -620,73 +620,63 @@
     by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
 qed
 
-lemma (in algebra) inf_measure_close:
+lemma (in ring_of_sets) inf_measure_close:
   fixes e :: extreal
-  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
+  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
   shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
                (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
-proof (cases "Inf (measure_set M f s) = \<infinity>")
-  case False
-  then have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
+proof -
+  from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
     using inf_measure_pos[OF posf, of s] by auto
   obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
     using Inf_extreal_close[OF fin e] by auto
   thus ?thesis
     by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
-next
-  case True
-  have "measure_set M f s \<noteq> {}"
-    by (metis emptyE ss inf_measure_nonempty [of _ f, OF posf top _ empty_sets])
-  then obtain l where "l \<in> measure_set M f s" by auto
-  moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
-  ultimately show ?thesis
-    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
 qed
 
-lemma (in algebra) inf_measure_countably_subadditive:
+lemma (in ring_of_sets) inf_measure_countably_subadditive:
   assumes posf: "positive M f" and inc: "increasing M f"
   shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
                   (\<lambda>x. Inf (measure_set M f x))"
-  unfolding countably_subadditive_def o_def
-proof (safe, simp, rule extreal_le_epsilon, safe)
-  fix A :: "nat \<Rightarrow> 'a set" and e :: extreal
-  let "?outer n" = "Inf (measure_set M f (A n))"
+proof (simp add: countably_subadditive_def, safe)
+  fix A :: "nat \<Rightarrow> 'a set"
+  let "?outer B" = "Inf (measure_set M f B)"
   assume A: "range A \<subseteq> Pow (space M)"
      and disj: "disjoint_family A"
      and sb: "(\<Union>i. A i) \<subseteq> space M"
-     and e: "0 < e"
-  hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
-                   A n \<subseteq> (\<Union>i. BB n i) \<and>
-                   (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
-    apply (safe intro!: choice inf_measure_close [of f, OF posf])
-    using e sb by (cases e) (auto simp add: not_le mult_pos_pos one_extreal_def)
-  then obtain BB
-    where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
+
+  { fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
+    hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
+        A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
+      apply (safe intro!: choice inf_measure_close [of f, OF posf])
+      using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def)
+    then obtain BB
+      where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
       and disjBB: "\<And>n. disjoint_family (BB n)"
       and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
-      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
-    by auto blast
-  have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> suminf ?outer + e"
+      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
+      by auto blast
+    have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
     proof -
       have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
         using suminf_half_series_extreal e
         by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal)
       have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
       then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
-      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer n + e*(1/2) ^ Suc n)"
+      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
         by (rule suminf_le_pos[OF BBle])
-      also have "... = suminf ?outer + e"
+      also have "... = (\<Sum>n. ?outer (A n)) + e"
         using sum_eq_1 inf_measure_pos[OF posf] e
         by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff)
       finally show ?thesis .
     qed
-  def C \<equiv> "(split BB) o prod_decode"
-  have C: "!!n. C n \<in> sets M"
-    apply (rule_tac p="prod_decode n" in PairE)
-    apply (simp add: C_def)
-    apply (metis BB subsetD rangeI)
-    done
-  have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
+    def C \<equiv> "(split BB) o prod_decode"
+    have C: "!!n. C n \<in> sets M"
+      apply (rule_tac p="prod_decode n" in PairE)
+      apply (simp add: C_def)
+      apply (metis BB subsetD rangeI)
+      done
+    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
     proof (auto simp add: C_def)
       fix x i
       assume x: "x \<in> A i"
@@ -695,23 +685,39 @@
       thus "\<exists>i. x \<in> split BB (prod_decode i)"
         by (metis prod_encode_inverse prod.cases)
     qed
-  have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
-    by (rule ext)  (auto simp add: C_def)
-  moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
-    using BB posf[unfolded positive_def]
-    by (force intro!: suminf_extreal_2dimen simp: o_def)
-  ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
-  have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
-    apply (rule inf_measure_le [OF posf(1) inc], auto)
-    apply (rule_tac x="C" in exI)
-    apply (auto simp add: C sbC Csums)
-    done
-  also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
-    by blast
-  finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ?outer + e" .
+    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
+      by (rule ext)  (auto simp add: C_def)
+    moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
+      using BB posf[unfolded positive_def]
+      by (force intro!: suminf_extreal_2dimen simp: o_def)
+    ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
+    have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
+      apply (rule inf_measure_le [OF posf(1) inc], auto)
+      apply (rule_tac x="C" in exI)
+      apply (auto simp add: C sbC Csums)
+      done
+    also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
+      by blast
+    finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
+  note for_finite_Inf = this
+
+  show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
+  proof cases
+    assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
+    with for_finite_Inf show ?thesis
+      by (intro extreal_le_epsilon) auto
+  next
+    assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
+    then have "\<exists>i. ?outer (A i) = \<infinity>"
+      by auto
+    then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
+      using suminf_PInfty[OF inf_measure_pos, OF posf]
+      by metis
+    then show ?thesis by simp
+  qed
 qed
 
-lemma (in algebra) inf_measure_outer:
+lemma (in ring_of_sets) inf_measure_outer:
   "\<lbrakk> positive M f ; increasing M f \<rbrakk>
    \<Longrightarrow> outer_measure_space \<lparr> space = space M, sets = Pow (space M) \<rparr>
                           (\<lambda>x. Inf (measure_set M f x))"
@@ -719,12 +725,10 @@
   by (simp add: outer_measure_space_def inf_measure_empty
                 inf_measure_increasing inf_measure_countably_subadditive positive_def)
 
-(*MOVE UP*)
-
-lemma (in algebra) algebra_subset_lambda_system:
+lemma (in ring_of_sets) algebra_subset_lambda_system:
   assumes posf: "positive M f" and inc: "increasing M f"
       and add: "additive M f"
-  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
+  shows "sets M \<subseteq> lambda_system \<lparr> space = space M, sets = Pow (space M) \<rparr>
                                 (\<lambda>x. Inf (measure_set M f x))"
 proof (auto dest: sets_into_space
             simp add: algebra.lambda_system_eq [OF algebra_Pow])
@@ -735,50 +739,42 @@
     by blast
   have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
         \<le> Inf (measure_set M f s)"
-    proof (rule extreal_le_epsilon, intro allI impI)
-      fix e :: extreal
-      assume e: "0 < e"
-      from inf_measure_close [of f, OF posf e s]
-      obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
-                 and sUN: "s \<subseteq> (\<Union>i. A i)"
-                 and l: "(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
-        by auto
-      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
-                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
-        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
-      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
-        by (subst additiveD [OF add, symmetric])
-           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
-      { fix u
-        assume u: "u \<in> sets M"
-        have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
-          by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
-        have 2: "Inf (measure_set M f (s \<inter> u)) \<le> (\<Sum>i. f (A i \<inter> u))"
-          proof (rule complete_lattice_class.Inf_lower)
-            show "(\<Sum>i. f (A i \<inter> u)) \<in> measure_set M f (s \<inter> u)"
-              apply (simp add: measure_set_def)
-              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
-              apply (auto simp add: disjoint_family_subset [OF disj] o_def)
-              apply (blast intro: u range_subsetD [OF A])
-              apply (blast dest: subsetD [OF sUN])
-              done
-          qed
-      } note lesum = this
-      have [simp]: "\<And>i. A i \<inter> (space M - x) = A i - x" using A sets_into_space by auto
-      have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> (\<Sum>i. f (A i \<inter> x))"
-        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
-                   \<le> (\<Sum>i. f (A i \<inter> (space M - x)))"
-        by (metis Diff lesum top x)+
-      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
-           \<le> (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))"
-        by (simp add: add_mono x)
-      also have "... \<le> (\<Sum>i. f (A i))" using posf[unfolded positive_def] A x
-        by (subst suminf_add_extreal[symmetric]) auto
-      also have "... \<le> Inf (measure_set M f s) + e"
-        by (rule l)
-      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
-        \<le> Inf (measure_set M f s) + e" .
+  proof cases
+    assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
+  next
+    assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
+    then have "measure_set M f s \<noteq> {}"
+      by (auto simp: top_extreal_def)
+    show ?thesis
+    proof (rule complete_lattice_class.Inf_greatest)
+      fix r assume "r \<in> measure_set M f s"
+      then obtain A where A: "disjoint_family A" "range A \<subseteq> sets M" "s \<subseteq> (\<Union>i. A i)"
+        and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
+      have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
+        unfolding measure_set_def
+      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
+        from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
+          by (rule disjoint_family_on_bisimulation) auto
+      qed (insert x A, auto)
+      moreover
+      have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
+        unfolding measure_set_def
+      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
+        from A(1) show "disjoint_family (\<lambda>i. A i - x)"
+          by (rule disjoint_family_on_bisimulation) auto
+      qed (insert x A, auto)
+      ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
+          (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
+      also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
+        using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def)
+      also have "\<dots> = (\<Sum>i. f (A i))"
+        using A x
+        by (subst add[THEN additiveD, symmetric])
+           (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
+      finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
+        using r by simp
     qed
+  qed
   moreover
   have "Inf (measure_set M f s)
        \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
@@ -805,7 +801,7 @@
                 countably_additive_def)
      blast
 
-theorem (in algebra) caratheodory:
+theorem (in ring_of_sets) caratheodory:
   assumes posf: "positive M f" and ca: "countably_additive M f"
   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>"
diff -r 2b98b4c2e2f1 -r 6db76c88907a src/HOL/Probability/Measure.thy
--- a/src/HOL/Probability/Measure.thy	Tue Mar 22 16:44:57 2011 +0100
+++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 18:53:05 2011 +0100
@@ -107,10 +107,7 @@
 qed
 
 lemma (in measure_space) additive: "additive M \<mu>"
-proof (rule algebra.countably_additive_additive [OF _ _ ca])
-  show "algebra M" by default
-  show "positive M \<mu>" by (simp add: positive_def)
-qed
+  using ca by (auto intro!: countably_additive_additive simp: positive_def)
 
 lemma (in measure_space) measure_additive:
      "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}