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.18    by (auto simp add: additive_def)
    1.19  
    1.20  lemma countably_additiveD:
    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.24 -  by (simp add: countably_additive_def) 
    1.25 +  by (simp add: countably_additive_def)
    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.77  lemma (in algebra) countably_subadditive_subadditive:
    1.78    assumes f: "positive M f" and cs: "countably_subadditive M f"
    1.79    shows  "subadditive M f"
    1.80 -proof (auto simp add: subadditive_def) 
    1.81 +proof (auto simp add: subadditive_def)
    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.93 -    using cs by (simp add: countably_subadditive_def) 
    1.94 -  hence "{x,y,{}} \<subseteq> sets M \<longrightarrow> x \<union> y \<in> sets M \<longrightarrow> 
    1.95 +    using cs by (simp add: countably_subadditive_def)
    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