generalized Caratheodory from algebra to ring_of_sets
authorhoelzl
Tue Mar 22 18:53:05 2011 +0100 (2011-03-22)
changeset 420666db76c88907a
parent 42065 2b98b4c2e2f1
child 42067 66c8281349ec
generalized Caratheodory from algebra to ring_of_sets
src/HOL/Probability/Caratheodory.thy
src/HOL/Probability/Measure.thy
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 18:53:05 2011 +0100
     1.3 @@ -148,7 +148,7 @@
     1.4  
     1.5  lemma (in algebra) lambda_system_empty:
     1.6    "positive M f \<Longrightarrow> {} \<in> lambda_system M f"
     1.7 -  by (auto simp add: positive_def lambda_system_eq algebra_def)
     1.8 +  by (auto simp add: positive_def lambda_system_eq)
     1.9  
    1.10  lemma lambda_system_sets:
    1.11    "x \<in> lambda_system M f \<Longrightarrow> x \<in> sets M"
    1.12 @@ -456,7 +456,7 @@
    1.13      by (simp add: measure_space_def)
    1.14  qed
    1.15  
    1.16 -lemma (in algebra) additive_increasing:
    1.17 +lemma (in ring_of_sets) additive_increasing:
    1.18    assumes posf: "positive M f" and addf: "additive M f"
    1.19    shows "increasing M f"
    1.20  proof (auto simp add: increasing_def)
    1.21 @@ -472,7 +472,7 @@
    1.22    finally show "f x \<le> f y" by simp
    1.23  qed
    1.24  
    1.25 -lemma (in algebra) countably_additive_additive:
    1.26 +lemma (in ring_of_sets) countably_additive_additive:
    1.27    assumes posf: "positive M f" and ca: "countably_additive M f"
    1.28    shows "additive M f"
    1.29  proof (auto simp add: additive_def)
    1.30 @@ -506,7 +506,7 @@
    1.31               simp: measure_set_def disjoint_family_on_def split_if_mem2 comp_def)
    1.32  qed
    1.33  
    1.34 -lemma (in algebra) inf_measure_agrees:
    1.35 +lemma (in ring_of_sets) inf_measure_agrees:
    1.36    assumes posf: "positive M f" and ca: "countably_additive M f"
    1.37        and s: "s \<in> sets M"
    1.38    shows "Inf (measure_set M f s) = f s"
    1.39 @@ -575,7 +575,7 @@
    1.40                inf_measure_nonempty[OF posf] subset_refl posf[unfolded positive_def])
    1.41  qed (rule inf_measure_pos[OF posf])
    1.42  
    1.43 -lemma (in algebra) inf_measure_positive:
    1.44 +lemma (in ring_of_sets) inf_measure_positive:
    1.45    assumes p: "positive M f" and "{} \<in> sets M"
    1.46    shows "positive M (\<lambda>x. Inf (measure_set M f x))"
    1.47  proof (unfold positive_def, intro conjI ballI)
    1.48 @@ -583,7 +583,7 @@
    1.49    fix A assume "A \<in> sets M"
    1.50  qed (rule inf_measure_pos[OF p])
    1.51  
    1.52 -lemma (in algebra) inf_measure_increasing:
    1.53 +lemma (in ring_of_sets) inf_measure_increasing:
    1.54    assumes posf: "positive M f"
    1.55    shows "increasing \<lparr> space = space M, sets = Pow (space M) \<rparr>
    1.56                      (\<lambda>x. Inf (measure_set M f x))"
    1.57 @@ -593,7 +593,7 @@
    1.58  apply (clarsimp simp add: measure_set_def, rule_tac x=A in exI, blast)
    1.59  done
    1.60  
    1.61 -lemma (in algebra) inf_measure_le:
    1.62 +lemma (in ring_of_sets) inf_measure_le:
    1.63    assumes posf: "positive M f" and inc: "increasing M f"
    1.64        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}"
    1.65    shows "Inf (measure_set M f s) \<le> x"
    1.66 @@ -620,73 +620,63 @@
    1.67      by (blast intro: y order_trans [OF _ ley] posf complete_lattice_class.Inf_lower)
    1.68  qed
    1.69  
    1.70 -lemma (in algebra) inf_measure_close:
    1.71 +lemma (in ring_of_sets) inf_measure_close:
    1.72    fixes e :: extreal
    1.73 -  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)"
    1.74 +  assumes posf: "positive M f" and e: "0 < e" and ss: "s \<subseteq> (space M)" and "Inf (measure_set M f s) \<noteq> \<infinity>"
    1.75    shows "\<exists>A. range A \<subseteq> sets M \<and> disjoint_family A \<and> s \<subseteq> (\<Union>i. A i) \<and>
    1.76                 (\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
    1.77 -proof (cases "Inf (measure_set M f s) = \<infinity>")
    1.78 -  case False
    1.79 -  then have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
    1.80 +proof -
    1.81 +  from `Inf (measure_set M f s) \<noteq> \<infinity>` have fin: "\<bar>Inf (measure_set M f s)\<bar> \<noteq> \<infinity>"
    1.82      using inf_measure_pos[OF posf, of s] by auto
    1.83    obtain l where "l \<in> measure_set M f s" "l \<le> Inf (measure_set M f s) + e"
    1.84      using Inf_extreal_close[OF fin e] by auto
    1.85    thus ?thesis
    1.86      by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
    1.87 -next
    1.88 -  case True
    1.89 -  have "measure_set M f s \<noteq> {}"
    1.90 -    by (metis emptyE ss inf_measure_nonempty [of _ f, OF posf top _ empty_sets])
    1.91 -  then obtain l where "l \<in> measure_set M f s" by auto
    1.92 -  moreover from True have "l \<le> Inf (measure_set M f s) + e" by simp
    1.93 -  ultimately show ?thesis
    1.94 -    by (auto intro!: exI[of _ l] simp: measure_set_def comp_def)
    1.95  qed
    1.96  
    1.97 -lemma (in algebra) inf_measure_countably_subadditive:
    1.98 +lemma (in ring_of_sets) inf_measure_countably_subadditive:
    1.99    assumes posf: "positive M f" and inc: "increasing M f"
   1.100    shows "countably_subadditive (| space = space M, sets = Pow (space M) |)
   1.101                    (\<lambda>x. Inf (measure_set M f x))"
   1.102 -  unfolding countably_subadditive_def o_def
   1.103 -proof (safe, simp, rule extreal_le_epsilon, safe)
   1.104 -  fix A :: "nat \<Rightarrow> 'a set" and e :: extreal
   1.105 -  let "?outer n" = "Inf (measure_set M f (A n))"
   1.106 +proof (simp add: countably_subadditive_def, safe)
   1.107 +  fix A :: "nat \<Rightarrow> 'a set"
   1.108 +  let "?outer B" = "Inf (measure_set M f B)"
   1.109    assume A: "range A \<subseteq> Pow (space M)"
   1.110       and disj: "disjoint_family A"
   1.111       and sb: "(\<Union>i. A i) \<subseteq> space M"
   1.112 -     and e: "0 < e"
   1.113 -  hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   1.114 -                   A n \<subseteq> (\<Union>i. BB n i) \<and>
   1.115 -                   (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
   1.116 -    apply (safe intro!: choice inf_measure_close [of f, OF posf])
   1.117 -    using e sb by (cases e) (auto simp add: not_le mult_pos_pos one_extreal_def)
   1.118 -  then obtain BB
   1.119 -    where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
   1.120 +
   1.121 +  { fix e :: extreal assume e: "0 < e" and "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
   1.122 +    hence "\<exists>BB. \<forall>n. range (BB n) \<subseteq> sets M \<and> disjoint_family (BB n) \<and>
   1.123 +        A n \<subseteq> (\<Union>i. BB n i) \<and> (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
   1.124 +      apply (safe intro!: choice inf_measure_close [of f, OF posf])
   1.125 +      using e sb by (auto simp: extreal_zero_less_0_iff one_extreal_def)
   1.126 +    then obtain BB
   1.127 +      where BB: "\<And>n. (range (BB n) \<subseteq> sets M)"
   1.128        and disjBB: "\<And>n. disjoint_family (BB n)"
   1.129        and sbBB: "\<And>n. A n \<subseteq> (\<Union>i. BB n i)"
   1.130 -      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer n + e * (1/2)^(Suc n)"
   1.131 -    by auto blast
   1.132 -  have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> suminf ?outer + e"
   1.133 +      and BBle: "\<And>n. (\<Sum>i. f (BB n i)) \<le> ?outer (A n) + e * (1/2)^(Suc n)"
   1.134 +      by auto blast
   1.135 +    have sll: "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n)) + e"
   1.136      proof -
   1.137        have sum_eq_1: "(\<Sum>n. e*(1/2) ^ Suc n) = e"
   1.138          using suminf_half_series_extreal e
   1.139          by (simp add: extreal_zero_le_0_iff zero_le_divide_extreal suminf_cmult_extreal)
   1.140        have "\<And>n i. 0 \<le> f (BB n i)" using posf[unfolded positive_def] BB by auto
   1.141        then have "\<And>n. 0 \<le> (\<Sum>i. f (BB n i))" by (rule suminf_0_le)
   1.142 -      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer n + e*(1/2) ^ Suc n)"
   1.143 +      then have "(\<Sum>n. \<Sum>i. (f (BB n i))) \<le> (\<Sum>n. ?outer (A n) + e*(1/2) ^ Suc n)"
   1.144          by (rule suminf_le_pos[OF BBle])
   1.145 -      also have "... = suminf ?outer + e"
   1.146 +      also have "... = (\<Sum>n. ?outer (A n)) + e"
   1.147          using sum_eq_1 inf_measure_pos[OF posf] e
   1.148          by (subst suminf_add_extreal) (auto simp add: extreal_zero_le_0_iff)
   1.149        finally show ?thesis .
   1.150      qed
   1.151 -  def C \<equiv> "(split BB) o prod_decode"
   1.152 -  have C: "!!n. C n \<in> sets M"
   1.153 -    apply (rule_tac p="prod_decode n" in PairE)
   1.154 -    apply (simp add: C_def)
   1.155 -    apply (metis BB subsetD rangeI)
   1.156 -    done
   1.157 -  have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   1.158 +    def C \<equiv> "(split BB) o prod_decode"
   1.159 +    have C: "!!n. C n \<in> sets M"
   1.160 +      apply (rule_tac p="prod_decode n" in PairE)
   1.161 +      apply (simp add: C_def)
   1.162 +      apply (metis BB subsetD rangeI)
   1.163 +      done
   1.164 +    have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   1.165      proof (auto simp add: C_def)
   1.166        fix x i
   1.167        assume x: "x \<in> A i"
   1.168 @@ -695,23 +685,39 @@
   1.169        thus "\<exists>i. x \<in> split BB (prod_decode i)"
   1.170          by (metis prod_encode_inverse prod.cases)
   1.171      qed
   1.172 -  have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   1.173 -    by (rule ext)  (auto simp add: C_def)
   1.174 -  moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
   1.175 -    using BB posf[unfolded positive_def]
   1.176 -    by (force intro!: suminf_extreal_2dimen simp: o_def)
   1.177 -  ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
   1.178 -  have "Inf (measure_set M f (\<Union>i. A i)) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
   1.179 -    apply (rule inf_measure_le [OF posf(1) inc], auto)
   1.180 -    apply (rule_tac x="C" in exI)
   1.181 -    apply (auto simp add: C sbC Csums)
   1.182 -    done
   1.183 -  also have "... \<le> (\<Sum>n. Inf (measure_set M f (A n))) + e" using sll
   1.184 -    by blast
   1.185 -  finally show "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ?outer + e" .
   1.186 +    have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> prod_decode"
   1.187 +      by (rule ext)  (auto simp add: C_def)
   1.188 +    moreover have "suminf ... = (\<Sum>n. \<Sum>i. f (BB n i))" using BBle
   1.189 +      using BB posf[unfolded positive_def]
   1.190 +      by (force intro!: suminf_extreal_2dimen simp: o_def)
   1.191 +    ultimately have Csums: "(\<Sum>i. f (C i)) = (\<Sum>n. \<Sum>i. f (BB n i))" by (simp add: o_def)
   1.192 +    have "?outer (\<Union>i. A i) \<le> (\<Sum>n. \<Sum>i. f (BB n i))"
   1.193 +      apply (rule inf_measure_le [OF posf(1) inc], auto)
   1.194 +      apply (rule_tac x="C" in exI)
   1.195 +      apply (auto simp add: C sbC Csums)
   1.196 +      done
   1.197 +    also have "... \<le> (\<Sum>n. ?outer (A n)) + e" using sll
   1.198 +      by blast
   1.199 +    finally have "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n)) + e" . }
   1.200 +  note for_finite_Inf = this
   1.201 +
   1.202 +  show "?outer (\<Union>i. A i) \<le> (\<Sum>n. ?outer (A n))"
   1.203 +  proof cases
   1.204 +    assume "\<forall>i. ?outer (A i) \<noteq> \<infinity>"
   1.205 +    with for_finite_Inf show ?thesis
   1.206 +      by (intro extreal_le_epsilon) auto
   1.207 +  next
   1.208 +    assume "\<not> (\<forall>i. ?outer (A i) \<noteq> \<infinity>)"
   1.209 +    then have "\<exists>i. ?outer (A i) = \<infinity>"
   1.210 +      by auto
   1.211 +    then have "(\<Sum>n. ?outer (A n)) = \<infinity>"
   1.212 +      using suminf_PInfty[OF inf_measure_pos, OF posf]
   1.213 +      by metis
   1.214 +    then show ?thesis by simp
   1.215 +  qed
   1.216  qed
   1.217  
   1.218 -lemma (in algebra) inf_measure_outer:
   1.219 +lemma (in ring_of_sets) inf_measure_outer:
   1.220    "\<lbrakk> positive M f ; increasing M f \<rbrakk>
   1.221     \<Longrightarrow> outer_measure_space \<lparr> space = space M, sets = Pow (space M) \<rparr>
   1.222                            (\<lambda>x. Inf (measure_set M f x))"
   1.223 @@ -719,12 +725,10 @@
   1.224    by (simp add: outer_measure_space_def inf_measure_empty
   1.225                  inf_measure_increasing inf_measure_countably_subadditive positive_def)
   1.226  
   1.227 -(*MOVE UP*)
   1.228 -
   1.229 -lemma (in algebra) algebra_subset_lambda_system:
   1.230 +lemma (in ring_of_sets) algebra_subset_lambda_system:
   1.231    assumes posf: "positive M f" and inc: "increasing M f"
   1.232        and add: "additive M f"
   1.233 -  shows "sets M \<subseteq> lambda_system (| space = space M, sets = Pow (space M) |)
   1.234 +  shows "sets M \<subseteq> lambda_system \<lparr> space = space M, sets = Pow (space M) \<rparr>
   1.235                                  (\<lambda>x. Inf (measure_set M f x))"
   1.236  proof (auto dest: sets_into_space
   1.237              simp add: algebra.lambda_system_eq [OF algebra_Pow])
   1.238 @@ -735,50 +739,42 @@
   1.239      by blast
   1.240    have "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.241          \<le> Inf (measure_set M f s)"
   1.242 -    proof (rule extreal_le_epsilon, intro allI impI)
   1.243 -      fix e :: extreal
   1.244 -      assume e: "0 < e"
   1.245 -      from inf_measure_close [of f, OF posf e s]
   1.246 -      obtain A where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   1.247 -                 and sUN: "s \<subseteq> (\<Union>i. A i)"
   1.248 -                 and l: "(\<Sum>i. f (A i)) \<le> Inf (measure_set M f s) + e"
   1.249 -        by auto
   1.250 -      have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   1.251 -                      (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   1.252 -        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   1.253 -      have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   1.254 -        by (subst additiveD [OF add, symmetric])
   1.255 -           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   1.256 -      { fix u
   1.257 -        assume u: "u \<in> sets M"
   1.258 -        have [simp]: "\<And>n. f (A n \<inter> u) \<le> f (A n)"
   1.259 -          by (simp add: increasingD [OF inc] u Int range_subsetD [OF A])
   1.260 -        have 2: "Inf (measure_set M f (s \<inter> u)) \<le> (\<Sum>i. f (A i \<inter> u))"
   1.261 -          proof (rule complete_lattice_class.Inf_lower)
   1.262 -            show "(\<Sum>i. f (A i \<inter> u)) \<in> measure_set M f (s \<inter> u)"
   1.263 -              apply (simp add: measure_set_def)
   1.264 -              apply (rule_tac x="(\<lambda>z. z \<inter> u) o A" in exI)
   1.265 -              apply (auto simp add: disjoint_family_subset [OF disj] o_def)
   1.266 -              apply (blast intro: u range_subsetD [OF A])
   1.267 -              apply (blast dest: subsetD [OF sUN])
   1.268 -              done
   1.269 -          qed
   1.270 -      } note lesum = this
   1.271 -      have [simp]: "\<And>i. A i \<inter> (space M - x) = A i - x" using A sets_into_space by auto
   1.272 -      have inf1: "Inf (measure_set M f (s\<inter>x)) \<le> (\<Sum>i. f (A i \<inter> x))"
   1.273 -        and inf2: "Inf (measure_set M f (s \<inter> (space M - x)))
   1.274 -                   \<le> (\<Sum>i. f (A i \<inter> (space M - x)))"
   1.275 -        by (metis Diff lesum top x)+
   1.276 -      hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.277 -           \<le> (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))"
   1.278 -        by (simp add: add_mono x)
   1.279 -      also have "... \<le> (\<Sum>i. f (A i))" using posf[unfolded positive_def] A x
   1.280 -        by (subst suminf_add_extreal[symmetric]) auto
   1.281 -      also have "... \<le> Inf (measure_set M f s) + e"
   1.282 -        by (rule l)
   1.283 -      finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.284 -        \<le> Inf (measure_set M f s) + e" .
   1.285 +  proof cases
   1.286 +    assume "Inf (measure_set M f s) = \<infinity>" then show ?thesis by simp
   1.287 +  next
   1.288 +    assume fin: "Inf (measure_set M f s) \<noteq> \<infinity>"
   1.289 +    then have "measure_set M f s \<noteq> {}"
   1.290 +      by (auto simp: top_extreal_def)
   1.291 +    show ?thesis
   1.292 +    proof (rule complete_lattice_class.Inf_greatest)
   1.293 +      fix r assume "r \<in> measure_set M f s"
   1.294 +      then obtain A where A: "disjoint_family A" "range A \<subseteq> sets M" "s \<subseteq> (\<Union>i. A i)"
   1.295 +        and r: "r = (\<Sum>i. f (A i))" unfolding measure_set_def by auto
   1.296 +      have "Inf (measure_set M f (s \<inter> x)) \<le> (\<Sum>i. f (A i \<inter> x))"
   1.297 +        unfolding measure_set_def
   1.298 +      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i \<inter> x"])
   1.299 +        from A(1) show "disjoint_family (\<lambda>i. A i \<inter> x)"
   1.300 +          by (rule disjoint_family_on_bisimulation) auto
   1.301 +      qed (insert x A, auto)
   1.302 +      moreover
   1.303 +      have "Inf (measure_set M f (s - x)) \<le> (\<Sum>i. f (A i - x))"
   1.304 +        unfolding measure_set_def
   1.305 +      proof (safe intro!: complete_lattice_class.Inf_lower exI[of _ "\<lambda>i. A i - x"])
   1.306 +        from A(1) show "disjoint_family (\<lambda>i. A i - x)"
   1.307 +          by (rule disjoint_family_on_bisimulation) auto
   1.308 +      qed (insert x A, auto)
   1.309 +      ultimately have "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le>
   1.310 +          (\<Sum>i. f (A i \<inter> x)) + (\<Sum>i. f (A i - x))" by (rule add_mono)
   1.311 +      also have "\<dots> = (\<Sum>i. f (A i \<inter> x) + f (A i - x))"
   1.312 +        using A(2) x posf by (subst suminf_add_extreal) (auto simp: positive_def)
   1.313 +      also have "\<dots> = (\<Sum>i. f (A i))"
   1.314 +        using A x
   1.315 +        by (subst add[THEN additiveD, symmetric])
   1.316 +           (auto intro!: arg_cong[where f=suminf] arg_cong[where f=f])
   1.317 +      finally show "Inf (measure_set M f (s \<inter> x)) + Inf (measure_set M f (s - x)) \<le> r"
   1.318 +        using r by simp
   1.319      qed
   1.320 +  qed
   1.321    moreover
   1.322    have "Inf (measure_set M f s)
   1.323         \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))"
   1.324 @@ -805,7 +801,7 @@
   1.325                  countably_additive_def)
   1.326       blast
   1.327  
   1.328 -theorem (in algebra) caratheodory:
   1.329 +theorem (in ring_of_sets) caratheodory:
   1.330    assumes posf: "positive M f" and ca: "countably_additive M f"
   1.331    shows "\<exists>\<mu> :: 'a set \<Rightarrow> extreal. (\<forall>s \<in> sets M. \<mu> s = f s) \<and>
   1.332              measure_space \<lparr> space = space M, sets = sets (sigma M), measure = \<mu> \<rparr>"
     2.1 --- a/src/HOL/Probability/Measure.thy	Tue Mar 22 16:44:57 2011 +0100
     2.2 +++ b/src/HOL/Probability/Measure.thy	Tue Mar 22 18:53:05 2011 +0100
     2.3 @@ -107,10 +107,7 @@
     2.4  qed
     2.5  
     2.6  lemma (in measure_space) additive: "additive M \<mu>"
     2.7 -proof (rule algebra.countably_additive_additive [OF _ _ ca])
     2.8 -  show "algebra M" by default
     2.9 -  show "positive M \<mu>" by (simp add: positive_def)
    2.10 -qed
    2.11 +  using ca by (auto intro!: countably_additive_additive simp: positive_def)
    2.12  
    2.13  lemma (in measure_space) measure_additive:
    2.14       "a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<inter> b = {}