src/HOL/Probability/Caratheodory.thy
 changeset 35582 b16d99a72dc9 parent 33536 fd28b7399f2b child 35704 5007843dae33
```     1.1 --- a/src/HOL/Probability/Caratheodory.thy	Thu Mar 04 19:50:45 2010 +0100
1.2 +++ b/src/HOL/Probability/Caratheodory.thy	Thu Mar 04 21:52:26 2010 +0100
1.3 @@ -15,8 +15,11 @@
1.4    measure:: "'a set \<Rightarrow> real"
1.5
1.6  definition
1.7 -  disjoint_family  where
1.8 -  "disjoint_family A \<longleftrightarrow> (\<forall>m n. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
1.9 +  disjoint_family_on  where
1.10 +  "disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})"
1.11 +
1.12 +abbreviation
1.13 +  "disjoint_family A \<equiv> disjoint_family_on A UNIV"
1.14
1.15  definition
1.16    positive  where
1.17 @@ -99,9 +102,9 @@
1.19
1.21 -  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
1.22 +  "countably_additive M f \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A
1.23     \<Longrightarrow> (\<Union>i. A i) \<in> sets M \<Longrightarrow> (\<lambda>n. f (A n))  sums  f (\<Union>i. A i)"
1.26
1.27  lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A - B) = {}"
1.28    by blast
1.29 @@ -111,7 +114,7 @@
1.30
1.31  lemma disjoint_family_subset:
1.32       "disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B"
1.33 -  by (force simp add: disjoint_family_def)
1.34 +  by (force simp add: disjoint_family_on_def)
1.35
1.36  subsection {* A Two-Element Series *}
1.37
1.38 @@ -119,28 +122,28 @@
1.39    where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)"
1.40
1.41  lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}"
1.42 -  apply (simp add: binaryset_def)
1.43 -  apply (rule set_ext)
1.44 -  apply (auto simp add: image_iff)
1.45 +  apply (simp add: binaryset_def)
1.46 +  apply (rule set_ext)
1.47 +  apply (auto simp add: image_iff)
1.48    done
1.49
1.50  lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B"
1.51 -  by (simp add: UNION_eq_Union_image range_binaryset_eq)
1.52 +  by (simp add: UNION_eq_Union_image range_binaryset_eq)
1.53
1.54 -lemma LIMSEQ_binaryset:
1.55 +lemma LIMSEQ_binaryset:
1.56    assumes f: "f {} = 0"
1.57    shows  "(\<lambda>n. \<Sum>i = 0..<n. f (binaryset A B i)) ----> f A + f B"
1.58  proof -
1.59    have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) = (\<lambda>n. f A + f B)"
1.60 -    proof
1.61 +    proof
1.62        fix n
1.63        show "(\<Sum>i\<Colon>nat = 0\<Colon>nat..<Suc (Suc n). f (binaryset A B i)) = f A + f B"
1.64 -        by (induct n)  (auto simp add: binaryset_def f)
1.65 +        by (induct n)  (auto simp add: binaryset_def f)
1.66      qed
1.67    moreover
1.68 -  have "... ----> f A + f B" by (rule LIMSEQ_const)
1.69 +  have "... ----> f A + f B" by (rule LIMSEQ_const)
1.70    ultimately
1.71 -  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
1.72 +  have "(\<lambda>n. \<Sum>i = 0..< Suc (Suc n). f (binaryset A B i)) ----> f A + f B"
1.73      by metis
1.74    hence "(\<lambda>n. \<Sum>i = 0..< n+2. f (binaryset A B i)) ----> f A + f B"
1.75      by simp
1.76 @@ -285,23 +288,23 @@
1.78    assumes f: "positive M f" and cs: "countably_subadditive M f"
1.82    fix x y
1.83    assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
1.84    hence "disjoint_family (binaryset x y)"
1.85 -    by (auto simp add: disjoint_family_def binaryset_def)
1.86 -  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.87 -         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.88 +    by (auto simp add: disjoint_family_on_def binaryset_def)
1.89 +  hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.90 +         (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.91           summable (f o (binaryset x y)) \<longrightarrow>
1.92           f (\<Union>i. binaryset x y i) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.94 -  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.96 +  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow>
1.97           summable (f o (binaryset x y)) \<longrightarrow>
1.98           f (x \<union> y) \<le> suminf (\<lambda>n. f (binaryset x y n))"
1.99      by (simp add: range_binaryset_eq UN_binaryset_eq)
1.100    thus "f (x \<union> y) \<le>  f x + f y" using f x y binaryset_sums
1.101 -    by (auto simp add: Un sums_iff positive_def o_def)
1.102 -qed
1.103 +    by (auto simp add: Un sums_iff positive_def o_def)
1.104 +qed
1.105
1.106
1.107  definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set "
1.108 @@ -312,19 +315,19 @@
1.109    case 0 show ?case by simp
1.110  next
1.111    case (Suc n)
1.112 -  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
1.113 +  thus ?case by (simp add: atLeastLessThanSuc disjointed_def)
1.114  qed
1.115
1.116  lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)"
1.117 -  apply (rule UN_finite2_eq [where k=0])
1.118 -  apply (simp add: finite_UN_disjointed_eq)
1.119 +  apply (rule UN_finite2_eq [where k=0])
1.120 +  apply (simp add: finite_UN_disjointed_eq)
1.121    done
1.122
1.123  lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}"
1.124    by (auto simp add: disjointed_def)
1.125
1.126  lemma disjoint_family_disjointed: "disjoint_family (disjointed A)"
1.127 -  by (simp add: disjoint_family_def)
1.128 +  by (simp add: disjoint_family_on_def)
1.129       (metis neq_iff Int_commute less_disjoint_disjointed)
1.130
1.131  lemma disjointed_subset: "disjointed A n \<subseteq> A n"
1.132 @@ -383,7 +386,7 @@
1.133  next
1.134    case (Suc n)
1.135    have "A n \<inter> (\<Union>i\<in>{0..<n}. A i) = {}" using disj
1.136 -    by (auto simp add: disjoint_family_def neq_iff) blast
1.137 +    by (auto simp add: disjoint_family_on_def neq_iff) blast
1.138    moreover
1.139    have "A n \<in> sets M" using A by blast
1.140    moreover have "(\<Union>i\<in>{0..<n}. A i) \<in> sets M"
1.141 @@ -440,7 +443,7 @@
1.142  next
1.143    case (Suc n)
1.144    have 2: "A n \<inter> UNION {0..<n} A = {}" using disj
1.145 -    by (force simp add: disjoint_family_def neq_iff)
1.146 +    by (force simp add: disjoint_family_on_def neq_iff)
1.147    have 3: "A n \<in> lambda_system M f" using A
1.148      by blast
1.149    have 4: "UNION {0..<n} A \<in> lambda_system M f"
1.150 @@ -505,7 +508,7 @@
1.151            by blast
1.152          moreover
1.153          have "disjoint_family (\<lambda>i. a \<inter> A i)" using disj
1.154 -          by (auto simp add: disjoint_family_def)
1.155 +          by (auto simp add: disjoint_family_on_def)
1.156          moreover
1.157          have "a \<inter> (\<Union>i. A i) \<in> sets M"
1.158            by (metis Int U_in a)
1.159 @@ -584,7 +587,7 @@
1.160    finally have "(f \<circ> (\<lambda>i. {})(0 := b)) sums f b" .
1.161    thus ?thesis using a
1.162      by (auto intro!: exI [of _ "(\<lambda>i. {})(0 := b)"]
1.163 -             simp add: measure_set_def disjoint_family_def b split_if_mem2)
1.164 +             simp add: measure_set_def disjoint_family_on_def b split_if_mem2)
1.165  qed
1.166
1.167  lemma (in algebra) inf_measure_pos0:
1.168 @@ -622,7 +625,7 @@
1.169    fix x y
1.170    assume x: "x \<in> sets M" and y: "y \<in> sets M" and "x \<inter> y = {}"
1.171    hence "disjoint_family (binaryset x y)"
1.172 -    by (auto simp add: disjoint_family_def binaryset_def)
1.173 +    by (auto simp add: disjoint_family_on_def binaryset_def)
1.174    hence "range (binaryset x y) \<subseteq> sets M \<longrightarrow>
1.175           (\<Union>i. binaryset x y i) \<in> sets M \<longrightarrow>
1.176           f (\<Union>i. binaryset x y i) = suminf (\<lambda>n. f (binaryset x y n))"
1.177 @@ -655,7 +658,7 @@
1.178        show "range (\<lambda>n. A n \<inter> s) \<subseteq> sets M" using A s
1.179          by blast
1.180        show "disjoint_family (\<lambda>n. A n \<inter> s)" using disj
1.181 -        by (auto simp add: disjoint_family_def)
1.182 +        by (auto simp add: disjoint_family_on_def)
1.183        show "(\<Union>i. A i \<inter> s) \<in> sets M" using A s
1.184          by (metis UN_extend_simps(4) s seq)
1.185      qed
```