src/HOL/Probability/Caratheodory.thy
changeset 42065 2b98b4c2e2f1
parent 41981 cdf7693bbe08
child 42066 6db76c88907a
     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 19:04:32 2011 +0100
     1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Tue Mar 22 16:44:57 2011 +0100
     1.3 @@ -217,7 +217,7 @@
     1.4  
     1.5  lemma (in algebra) lambda_system_algebra:
     1.6    "positive M f \<Longrightarrow> algebra (M\<lparr>sets := lambda_system M f\<rparr>)"
     1.7 -  apply (auto simp add: algebra_def)
     1.8 +  apply (auto simp add: algebra_iff_Un)
     1.9    apply (metis lambda_system_sets set_mp sets_into_space)
    1.10    apply (metis lambda_system_empty)
    1.11    apply (metis lambda_system_Compl)
    1.12 @@ -332,9 +332,10 @@
    1.13      by (force simp add: disjoint_family_on_def neq_iff)
    1.14    have 3: "A n \<in> lambda_system M f" using A
    1.15      by blast
    1.16 +  interpret l: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
    1.17 +    using f by (rule lambda_system_algebra)
    1.18    have 4: "UNION {0..<n} A \<in> lambda_system M f"
    1.19 -    using A algebra.UNION_in_sets [OF local.lambda_system_algebra, of f, OF f]
    1.20 -    by simp
    1.21 +    using A l.UNION_in_sets by simp
    1.22    from Suc.hyps show ?case
    1.23      by (simp add: atLeastLessThanSuc lambda_system_strong_additive [OF a 2 3 4])
    1.24  qed
    1.25 @@ -352,8 +353,8 @@
    1.26      by (metis countably_subadditive_subadditive csa pos)
    1.27    have A': "range A \<subseteq> sets (M(|sets := lambda_system M f|))" using A
    1.28      by simp
    1.29 -  have alg_ls: "algebra (M(|sets := lambda_system M f|))"
    1.30 -    by (rule lambda_system_algebra) (rule pos)
    1.31 +  interpret ls: algebra "M\<lparr>sets := lambda_system M f\<rparr>"
    1.32 +    using pos by (rule lambda_system_algebra)
    1.33    have A'': "range A \<subseteq> sets M"
    1.34       by (metis A image_subset_iff lambda_system_sets)
    1.35  
    1.36 @@ -366,7 +367,7 @@
    1.37      have *: "\<And>i. 0 \<le> f (A i)" using pos A'' unfolding positive_def by auto
    1.38      have dis: "\<And>N. disjoint_family_on A {..<N}" by (intro disjoint_family_on_mono[OF _ disj]) auto
    1.39      show "(\<Sum>i. f (A i)) \<le> f (\<Union>i. A i)"
    1.40 -      using algebra.additive_sum [OF alg_ls lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
    1.41 +      using ls.additive_sum [OF lambda_system_positive[OF pos] lambda_system_additive _ A' dis]
    1.42        using A''
    1.43        by (intro suminf_bound[OF _ *]) (auto intro!: increasingD[OF inc] allI countable_UN)
    1.44    qed
    1.45 @@ -401,8 +402,7 @@
    1.46              have le_fa: "f (UNION {0..<n} A \<inter> a) \<le> f a" using A''
    1.47                by (blast intro: increasingD [OF inc] A'' UNION_in_sets)
    1.48              have ls: "(\<Union>i\<in>{0..<n}. A i) \<in> lambda_system M f"
    1.49 -              using algebra.UNION_in_sets [OF lambda_system_algebra [of f, OF pos]]
    1.50 -              by (simp add: A)
    1.51 +              using ls.UNION_in_sets by (simp add: A)
    1.52              hence eq_fa: "f a = f (a \<inter> (\<Union>i\<in>{0..<n}. A i)) + f (a - (\<Union>i\<in>{0..<n}. A i))"
    1.53                by (simp add: lambda_system_eq UNION_in)
    1.54              have "f (a - (\<Union>i. A i)) \<le> f (a - (\<Union>i\<in>{0..<n}. A i))"
    1.55 @@ -441,8 +441,8 @@
    1.56      by (metis oms outer_measure_space_def)
    1.57    have alg: "algebra ?M"
    1.58      using lambda_system_algebra [of f, OF pos]
    1.59 -    by (simp add: algebra_def)
    1.60 -  then moreover
    1.61 +    by (simp add: algebra_iff_Un)
    1.62 +  then
    1.63    have "sigma_algebra ?M"
    1.64      using lambda_system_caratheodory [OF oms]
    1.65      by (simp add: sigma_algebra_disjoint_iff)
    1.66 @@ -453,7 +453,7 @@
    1.67                    countably_additive_def o_def)
    1.68    ultimately
    1.69    show ?thesis
    1.70 -    by intro_locales (auto simp add: sigma_algebra_def)
    1.71 +    by (simp add: measure_space_def)
    1.72  qed
    1.73  
    1.74  lemma (in algebra) additive_increasing: