src/HOL/Probability/Caratheodory.thy
changeset 33536 fd28b7399f2b
parent 33271 7be66dee1a5a
child 35582 b16d99a72dc9
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 16:06:08 2009 +0000
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Mon Nov 09 19:42:33 2009 +0100
     1.3 @@ -2,7 +2,6 @@
     1.4  
     1.5  theory Caratheodory
     1.6    imports Sigma_Algebra SupInf SeriesPlus
     1.7 -
     1.8  begin
     1.9  
    1.10  text{*From the Hurd/Coble measure theory development, translated by Lawrence Paulson.*}
    1.11 @@ -136,7 +135,7 @@
    1.12      proof 
    1.13        fix n
    1.14        show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
    1.15 -	by (induct n)  (auto simp add: binaryset_def f) 
    1.16 +        by (induct n)  (auto simp add: binaryset_def f) 
    1.17      qed
    1.18    moreover
    1.19    have "... ----> f A + f B" by (rule LIMSEQ_const) 
    1.20 @@ -198,30 +197,30 @@
    1.21    proof -
    1.22      from xl yl show ?thesis
    1.23        proof (auto simp add: positive_def lambda_system_eq Int)
    1.24 -	fix u
    1.25 -	assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
    1.26 +        fix u
    1.27 +        assume x: "x \<in> sets M" and y: "y \<in> sets M" and u: "u \<in> sets M"
    1.28             and fx: "\<forall>z\<in>sets M. f (z \<inter> x) + f (z - x) = f z"
    1.29             and fy: "\<forall>z\<in>sets M. f (z \<inter> y) + f (z - y) = f z"
    1.30 -	have "u - x \<inter> y \<in> sets M"
    1.31 -	  by (metis Diff Diff_Int Un u x y)
    1.32 -	moreover
    1.33 -	have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
    1.34 -	moreover
    1.35 -	have "u - x \<inter> y - y = u - y" by blast
    1.36 -	ultimately
    1.37 -	have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
    1.38 -	  by force
    1.39 -	have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
    1.40 +        have "u - x \<inter> y \<in> sets M"
    1.41 +          by (metis Diff Diff_Int Un u x y)
    1.42 +        moreover
    1.43 +        have "(u - (x \<inter> y)) \<inter> y = u \<inter> y - x" by blast
    1.44 +        moreover
    1.45 +        have "u - x \<inter> y - y = u - y" by blast
    1.46 +        ultimately
    1.47 +        have ey: "f (u - x \<inter> y) = f (u \<inter> y - x) + f (u - y)" using fy
    1.48 +          by force
    1.49 +        have "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) 
    1.50                = (f (u \<inter> (x \<inter> y)) + f (u \<inter> y - x)) + f (u - y)"
    1.51 -	  by (simp add: ey) 
    1.52 -	also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
    1.53 -	  by (simp add: Int_ac) 
    1.54 -	also have "... = f (u \<inter> y) + f (u - y)"
    1.55 -	  using fx [THEN bspec, of "u \<inter> y"] Int y u
    1.56 -	  by force
    1.57 -	also have "... = f u"
    1.58 -	  by (metis fy u) 
    1.59 -	finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
    1.60 +          by (simp add: ey) 
    1.61 +        also have "... =  (f ((u \<inter> y) \<inter> x) + f (u \<inter> y - x)) + f (u - y)"
    1.62 +          by (simp add: Int_ac) 
    1.63 +        also have "... = f (u \<inter> y) + f (u - y)"
    1.64 +          using fx [THEN bspec, of "u \<inter> y"] Int y u
    1.65 +          by force
    1.66 +        also have "... = f u"
    1.67 +          by (metis fy u) 
    1.68 +        finally show "f (u \<inter> (x \<inter> y)) + f (u - x \<inter> y) = f u" .
    1.69        qed
    1.70    qed
    1.71  
    1.72 @@ -478,11 +477,11 @@
    1.73    have U_eq: "f (\<Union>i. A i) = suminf (f o A)" 
    1.74      proof (rule antisym)
    1.75        show "f (\<Union>i. A i) \<le> suminf (f \<circ> A)"
    1.76 -	by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
    1.77 +        by (rule countably_subadditiveD [OF csa A'' disj U_in sumfA]) 
    1.78        show "suminf (f \<circ> A) \<le> f (\<Union>i. A i)"
    1.79 -	by (rule suminf_le [OF sumfA]) 
    1.80 +        by (rule suminf_le [OF sumfA]) 
    1.81             (metis algebra.additive_sum [OF alg_ls] pos disj UN_Un Un_UNIV_right
    1.82 -	          lambda_system_positive lambda_system_additive 
    1.83 +                  lambda_system_positive lambda_system_additive 
    1.84                    subset_Un_eq increasingD [OF inc] A' A'' UNION_in_sets U_in) 
    1.85      qed
    1.86    {
    1.87 @@ -491,58 +490,58 @@
    1.88      have "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) = f a"
    1.89      proof -
    1.90        have summ: "summable (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)" using pos A'' 
    1.91 -	apply -
    1.92 -	apply (rule summable_comparison_test [OF _ sumfA]) 
    1.93 -	apply (rule_tac x="0" in exI) 
    1.94 -	apply (simp add: positive_def) 
    1.95 -	apply (auto simp add: )
    1.96 -	apply (subst abs_of_nonneg)
    1.97 -	apply (metis A'' Int UNIV_I a image_subset_iff)
    1.98 -	apply (blast intro:  increasingD [OF inc] a)   
    1.99 -	done
   1.100 +        apply -
   1.101 +        apply (rule summable_comparison_test [OF _ sumfA]) 
   1.102 +        apply (rule_tac x="0" in exI) 
   1.103 +        apply (simp add: positive_def) 
   1.104 +        apply (auto simp add: )
   1.105 +        apply (subst abs_of_nonneg)
   1.106 +        apply (metis A'' Int UNIV_I a image_subset_iff)
   1.107 +        apply (blast intro:  increasingD [OF inc] a)   
   1.108 +        done
   1.109        show ?thesis
   1.110        proof (rule antisym)
   1.111 -	have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
   1.112 -	  by blast
   1.113 -	moreover 
   1.114 -	have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   1.115 -	  by (auto simp add: disjoint_family_def) 
   1.116 -	moreover 
   1.117 -	have "a \<inter> (\<Union>i. A i) \<in> sets M"
   1.118 -	  by (metis Int U_in a)
   1.119 -	ultimately 
   1.120 -	have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
   1.121 -	  using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
   1.122 -	  by (simp add: o_def) 
   1.123 -	moreover 
   1.124 -	have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
   1.125 -	  proof (rule suminf_le [OF summ])
   1.126 -	    fix n
   1.127 -	    have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   1.128 -	      by (metis A'' UNION_in_sets) 
   1.129 -	    have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   1.130 -	      by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
   1.131 -	    have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
   1.132 -	      using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
   1.133 -	      by (simp add: A) 
   1.134 -	    hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
   1.135 -	      by (simp add: lambda_system_eq UNION_in Diff_Compl a)
   1.136 -	    have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.137 -	      by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
   1.138 +        have "range (\<lambda>i. a \<inter> A i) \<subseteq> sets M" using A''
   1.139 +          by blast
   1.140 +        moreover 
   1.141 +        have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
   1.142 +          by (auto simp add: disjoint_family_def) 
   1.143 +        moreover 
   1.144 +        have "a \<inter> (\<Union>i. A i) \<in> sets M"
   1.145 +          by (metis Int U_in a)
   1.146 +        ultimately 
   1.147 +        have "f (a \<inter> (\<Union>i. A i)) \<le> suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)"
   1.148 +          using countably_subadditiveD [OF csa, of "(\<lambda>i. a \<inter> A i)"] summ
   1.149 +          by (simp add: o_def) 
   1.150 +        moreover 
   1.151 +        have "suminf (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A)  \<le> f a - f (a - (\<Union>i. A i))"
   1.152 +          proof (rule suminf_le [OF summ])
   1.153 +            fix n
   1.154 +            have UNION_in: "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
   1.155 +              by (metis A'' UNION_in_sets) 
   1.156 +            have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
   1.157 +              by (blast intro: increasingD [OF inc] A'' Int UNION_in_sets a) 
   1.158 +            have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
   1.159 +              using algebra.UNION_in_sets [OF lambda_system_algebra [OF pos]]
   1.160 +              by (simp add: A) 
   1.161 +            hence eq_fa: "f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i)) = f a"
   1.162 +              by (simp add: lambda_system_eq UNION_in Diff_Compl a)
   1.163 +            have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
   1.164 +              by (blast intro: increasingD [OF inc] Diff UNION_eq_Union_image 
   1.165                                 UNION_in U_in a) 
   1.166 -	    thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
   1.167 -	      using eq_fa
   1.168 -	      by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
   1.169 +            thus "setsum (f \<circ> (\<lambda>i. a \<inter> i) \<circ> A) {0..<n} \<le> f a - f (a - (\<Union>i. A i))"
   1.170 +              using eq_fa
   1.171 +              by (simp add: suminf_le [OF summ] lambda_system_strong_sum pos 
   1.172                              a A disj)
   1.173 -	  qed
   1.174 -	ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
   1.175 -	  by arith
   1.176 +          qed
   1.177 +        ultimately show "f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i)) \<le> f a" 
   1.178 +          by arith
   1.179        next
   1.180 -	have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
   1.181 -	  by (blast intro:  increasingD [OF inc] a U_in)
   1.182 -	also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   1.183 -	  by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
   1.184 -	finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   1.185 +        have "f a \<le> f (a \<inter> (\<Union>i. A i) \<union> (a - (\<Union>i. A i)))" 
   1.186 +          by (blast intro:  increasingD [OF inc] a U_in)
   1.187 +        also have "... \<le>  f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))"
   1.188 +          by (blast intro: subadditiveD [OF sa] Int Diff U_in) 
   1.189 +        finally show "f a \<le> f (a \<inter> (\<Union>i. A i)) + f (a - (\<Union>i. A i))" .
   1.190          qed
   1.191       qed
   1.192    }
   1.193 @@ -654,20 +653,20 @@
   1.194    have sums: "(\<lambda>i. f (A i \<inter> s)) sums f (\<Union>i. A i \<inter> s)"
   1.195      proof (rule countably_additiveD [OF ca]) 
   1.196        show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
   1.197 -	by blast
   1.198 +        by blast
   1.199        show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
   1.200 -	by (auto simp add: disjoint_family_def)
   1.201 +        by (auto simp add: disjoint_family_def)
   1.202        show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
   1.203 -	by (metis UN_extend_simps(4) s seq)
   1.204 +        by (metis UN_extend_simps(4) s seq)
   1.205      qed
   1.206    hence "f s = suminf (\<lambda>i. f (A i \<inter> s))"
   1.207      by (metis Int_commute UN_simps(4) seq sums_iff) 
   1.208    also have "... \<le> suminf (f \<circ> A)" 
   1.209      proof (rule summable_le [OF _ _ sm]) 
   1.210        show "\<forall>n. f (A n \<inter> s) \<le> (f \<circ> A) n" using A s
   1.211 -	by (force intro: increasingD [OF inc]) 
   1.212 +        by (force intro: increasingD [OF inc]) 
   1.213        show "summable (\<lambda>i. f (A i \<inter> s))" using sums
   1.214 -	by (simp add: sums_iff) 
   1.215 +        by (simp add: sums_iff) 
   1.216      qed
   1.217    also have "... = z" by (rule si) 
   1.218    finally show "f s \<le> z" .
   1.219 @@ -722,9 +721,9 @@
   1.220      proof (auto)
   1.221        fix n
   1.222        have "\<bar>f (disjointed A n)\<bar> = f (disjointed A n)" using posf dA
   1.223 -	by (auto simp add: positive_def image_subset_iff)
   1.224 +        by (auto simp add: positive_def image_subset_iff)
   1.225        also have "... \<le> f (A n)" 
   1.226 -	by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   1.227 +        by (metis increasingD [OF inc] UNIV_I dA image_subset_iff disjointed_subset A)
   1.228        finally show "\<bar>f (disjointed A n)\<bar> \<le> f (A n)" .
   1.229      qed
   1.230    from Series.summable_le2 [OF this sm]
   1.231 @@ -787,32 +786,32 @@
   1.232          and ll: "!!n. ll n \<le> Inf (measure_set M f (A n)) + e * (1/2)^(Suc n)"
   1.233        by auto blast
   1.234      have llpos: "!!n. 0 \<le> ll n"
   1.235 -	by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
   1.236 +        by (metis BBsums sums_iff o_apply posf positive_imp_pos suminf_ge_zero 
   1.237                range_subsetD BB) 
   1.238      have sll: "summable ll &
   1.239                 suminf ll \<le> suminf (\<lambda>n. Inf (measure_set M f (A n))) + e"
   1.240        proof -
   1.241 -	have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
   1.242 -	  by (rule sums_mult [OF power_half_series]) 
   1.243 -	hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
   1.244 -	  and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
   1.245 -	  by (auto simp add: sums_iff) 
   1.246 -	have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
   1.247 +        have "(\<lambda>n. e * (1/2)^(Suc n)) sums (e*1)"
   1.248 +          by (rule sums_mult [OF power_half_series]) 
   1.249 +        hence sum0: "summable (\<lambda>n. e * (1 / 2) ^ Suc n)"
   1.250 +          and eqe:  "(\<Sum>n. e * (1 / 2) ^ n / 2) = e"
   1.251 +          by (auto simp add: sums_iff) 
   1.252 +        have 0: "suminf (\<lambda>n. Inf (measure_set M f (A n))) +
   1.253                   suminf (\<lambda>n. e * (1/2)^(Suc n)) =
   1.254                   suminf (\<lambda>n. Inf (measure_set M f (A n)) + e * (1/2)^(Suc n))"
   1.255 -	  by (rule suminf_add [OF sum1 sum0]) 
   1.256 -	have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
   1.257 -	  by (metis ll llpos abs_of_nonneg)
   1.258 -	have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
   1.259 -	  by (rule summable_add [OF sum1 sum0]) 
   1.260 -	have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
   1.261 -	  using Series.summable_le2 [OF 1 2] by auto
   1.262 -	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
   1.263 +          by (rule suminf_add [OF sum1 sum0]) 
   1.264 +        have 1: "\<forall>n. \<bar>ll n\<bar> \<le> Inf (measure_set M f (A n)) + e * (1/2) ^ Suc n"
   1.265 +          by (metis ll llpos abs_of_nonneg)
   1.266 +        have 2: "summable (\<lambda>n. Inf (measure_set M f (A n)) + e*(1/2)^(Suc n))"
   1.267 +          by (rule summable_add [OF sum1 sum0]) 
   1.268 +        have "suminf ll \<le> (\<Sum>n. Inf (measure_set M f (A n)) + e*(1/2) ^ Suc n)"
   1.269 +          using Series.summable_le2 [OF 1 2] by auto
   1.270 +        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + 
   1.271                           (\<Sum>n. e * (1 / 2) ^ Suc n)"
   1.272 -	  by (metis 0) 
   1.273 -	also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
   1.274 -	  by (simp add: eqe) 
   1.275 -	finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
   1.276 +          by (metis 0) 
   1.277 +        also have "... = (\<Sum>n. Inf (measure_set M f (A n))) + e"
   1.278 +          by (simp add: eqe) 
   1.279 +        finally show ?thesis using  Series.summable_le2 [OF 1 2] by auto
   1.280        qed
   1.281      def C \<equiv> "(split BB) o nat_to_nat2"
   1.282      have C: "!!n. C n \<in> sets M"
   1.283 @@ -822,24 +821,24 @@
   1.284        done
   1.285      have sbC: "(\<Union>i. A i) \<subseteq> (\<Union>i. C i)"
   1.286        proof (auto simp add: C_def)
   1.287 -	fix x i
   1.288 -	assume x: "x \<in> A i"
   1.289 -	with sbBB [of i] obtain j where "x \<in> BB i j"
   1.290 -	  by blast	  
   1.291 -	thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
   1.292 -	  by (metis nat_to_nat2_surj internal_split_def prod.cases 
   1.293 +        fix x i
   1.294 +        assume x: "x \<in> A i"
   1.295 +        with sbBB [of i] obtain j where "x \<in> BB i j"
   1.296 +          by blast        
   1.297 +        thus "\<exists>i. x \<in> split BB (nat_to_nat2 i)"
   1.298 +          by (metis nat_to_nat2_surj internal_split_def prod.cases 
   1.299                  prod_case_split surj_f_inv_f)
   1.300        qed 
   1.301      have "(f \<circ> C) = (f \<circ> (\<lambda>(x, y). BB x y)) \<circ> nat_to_nat2"
   1.302        by (rule ext)  (auto simp add: C_def) 
   1.303      also have "... sums suminf ll" 
   1.304        proof (rule suminf_2dimen)
   1.305 -	show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
   1.306 -	  by (force simp add: positive_def)
   1.307 -	show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
   1.308 -	  by (force simp add: o_def)
   1.309 -	show "summable ll" using sll
   1.310 -	  by auto
   1.311 +        show "\<And>m n. 0 \<le> (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)" using posf BB 
   1.312 +          by (force simp add: positive_def)
   1.313 +        show "\<And>m. (\<lambda>n. (f \<circ> (\<lambda>(x, y). BB x y)) (m, n)) sums ll m"using BBsums BB
   1.314 +          by (force simp add: o_def)
   1.315 +        show "summable ll" using sll
   1.316 +          by auto
   1.317        qed
   1.318      finally have Csums: "(f \<circ> C) sums suminf ll" .
   1.319      have "Inf (measure_set M f (\<Union>i. A i)) \<le> suminf ll"
   1.320 @@ -882,24 +881,24 @@
   1.321        from inf_measure_close [OF posf e s]
   1.322        obtain A l where A: "range A \<subseteq> sets M" and disj: "disjoint_family A"
   1.323                     and sUN: "s \<subseteq> (\<Union>i. A i)" and fsums: "(f \<circ> A) sums l"
   1.324 -	           and l: "l \<le> Inf (measure_set M f s) + e"
   1.325 -	by auto
   1.326 +                   and l: "l \<le> Inf (measure_set M f s) + e"
   1.327 +        by auto
   1.328        have [simp]: "!!x. x \<in> sets M \<Longrightarrow>
   1.329                        (f o (\<lambda>z. z \<inter> (space M - x)) o A) = (f o (\<lambda>z. z - x) o A)"
   1.330 -	by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   1.331 +        by (rule ext, simp, metis A Int_Diff Int_space_eq2 range_subsetD)
   1.332        have  [simp]: "!!n. f (A n \<inter> x) + f (A n - x) = f (A n)"
   1.333 -	by (subst additiveD [OF add, symmetric])
   1.334 - 	   (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   1.335 +        by (subst additiveD [OF add, symmetric])
   1.336 +           (auto simp add: x range_subsetD [OF A] Int_Diff_Un Int_Diff_disjoint)
   1.337        have fsumb: "summable (f \<circ> A)"
   1.338 -	by (metis fsums sums_iff) 
   1.339 +        by (metis fsums sums_iff) 
   1.340        { fix u
   1.341 -	assume u: "u \<in> sets M"
   1.342 -	have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
   1.343 -	  by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
   1.344 +        assume u: "u \<in> sets M"
   1.345 +        have [simp]: "\<And>n. \<bar>f (A n \<inter> u)\<bar> \<le> f (A n)"
   1.346 +          by (simp add: positive_imp_pos [OF posf]  increasingD [OF inc] 
   1.347                          u Int  range_subsetD [OF A]) 
   1.348 -	have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
   1.349 +        have 1: "summable (f o (\<lambda>z. z\<inter>u) o A)" 
   1.350            by (rule summable_comparison_test [OF _ fsumb]) simp
   1.351 -	have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
   1.352 +        have 2: "Inf (measure_set M f (s\<inter>u)) \<le> suminf (f o (\<lambda>z. z\<inter>u) o A)"
   1.353            proof (rule Inf_lower) 
   1.354              show "suminf (f \<circ> (\<lambda>z. z \<inter> u) \<circ> A) \<in> measure_set M f (s \<inter> u)"
   1.355                apply (simp add: measure_set_def) 
   1.356 @@ -920,14 +919,14 @@
   1.357          and sum2: "summable (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   1.358          and inf2: "Inf (measure_set M f (s \<inter> (space M - x))) 
   1.359                     \<le> suminf (f o (\<lambda>z. z \<inter> (space M - x)) o A)"
   1.360 -	by (metis Diff lesum top x)+
   1.361 +        by (metis Diff lesum top x)+
   1.362        hence "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.363             \<le> suminf (f o (\<lambda>s. s\<inter>x) o A) + suminf (f o (\<lambda>s. s-x) o A)"
   1.364 -	by (simp add: x)
   1.365 +        by (simp add: x)
   1.366        also have "... \<le> suminf (f o A)" using suminf_add [OF sum1 sum2] 
   1.367 -	by (simp add: x) (simp add: o_def) 
   1.368 +        by (simp add: x) (simp add: o_def) 
   1.369        also have "... \<le> Inf (measure_set M f s) + e"
   1.370 -	by (metis fsums l sums_unique) 
   1.371 +        by (metis fsums l sums_unique) 
   1.372        finally show "Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))
   1.373          \<le> Inf (measure_set M f s) + e" .
   1.374      qed
   1.375 @@ -940,7 +939,7 @@
   1.376      also have "... \<le> Inf (measure_set M f (s\<inter>x)) + Inf (measure_set M f (s-x))" 
   1.377        apply (rule subadditiveD) 
   1.378        apply (iprover intro: algebra.countably_subadditive_subadditive algebra_Pow 
   1.379 -	       inf_measure_positive inf_measure_countably_subadditive posf inc)
   1.380 +               inf_measure_positive inf_measure_countably_subadditive posf inc)
   1.381        apply (auto simp add: subsetD [OF s])  
   1.382        done
   1.383      finally show ?thesis .