author  hoelzl 
Thu, 26 May 2011 14:12:06 +0200  
changeset 42987  73e2d802ea41 
parent 42984  43864e7475df 
child 42988  d8f3fc934ff6 
permissions  rwrr 
41983  1 
(* Title: HOL/Probability/Sigma_Algebra.thy 
42067  2 
Author: Stefan Richter, Markus Wenzel, TU München 
3 
Author: Johannes Hölzl, TU München 

41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

4 
Plus material from the Hurd/Coble measure theory development, 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

5 
translated by Lawrence Paulson. 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

6 
*) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

7 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

8 
header {* Sigma Algebras *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

9 

41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

10 
theory Sigma_Algebra 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

11 
imports 
42145  12 
Complex_Main 
41413
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

13 
"~~/src/HOL/Library/Countable" 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

14 
"~~/src/HOL/Library/FuncSet" 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

15 
"~~/src/HOL/Library/Indicator_Function" 
64cd30d6b0b8
explicit file specifications  avoid secondary load path;
wenzelm
parents:
41095
diff
changeset

16 
begin 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

17 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

18 
text {* Sigma algebras are an elementary concept in measure 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

19 
theory. To measure  that is to integrate  functions, we first have 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

20 
to measure sets. Unfortunately, when dealing with a large universe, 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

21 
it is often not possible to consistently assign a measure to every 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

22 
subset. Therefore it is necessary to define the set of measurable 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

23 
subsets of the universe. A sigma algebra is such a set that has 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

24 
three very natural and desirable properties. *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

25 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

26 
subsection {* Algebras *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

27 

38656  28 
record 'a algebra = 
29 
space :: "'a set" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

30 
sets :: "'a set set" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

31 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

32 
locale subset_class = 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

33 
fixes M :: "('a, 'b) algebra_scheme" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

34 
assumes space_closed: "sets M \<subseteq> Pow (space M)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

35 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

36 
lemma (in subset_class) sets_into_space: "x \<in> sets M \<Longrightarrow> x \<subseteq> space M" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

37 
by (metis PowD contra_subsetD space_closed) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

38 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

39 
locale ring_of_sets = subset_class + 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

40 
assumes empty_sets [iff]: "{} \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

41 
and Diff [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a  b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

42 
and Un [intro]: "\<And>a b. a \<in> sets M \<Longrightarrow> b \<in> sets M \<Longrightarrow> a \<union> b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

43 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

44 
lemma (in ring_of_sets) Int [intro]: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

45 
assumes a: "a \<in> sets M" and b: "b \<in> sets M" shows "a \<inter> b \<in> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

46 
proof  
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

47 
have "a \<inter> b = a  (a  b)" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

48 
by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

49 
then show "a \<inter> b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

50 
using a b by auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

51 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

52 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

53 
lemma (in ring_of_sets) finite_Union [intro]: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

54 
"finite X \<Longrightarrow> X \<subseteq> sets M \<Longrightarrow> Union X \<in> sets M" 
38656  55 
by (induct set: finite) (auto simp add: Un) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

56 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

57 
lemma (in ring_of_sets) finite_UN[intro]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

58 
assumes "finite I" and "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

59 
shows "(\<Union>i\<in>I. A i) \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

60 
using assms by induct auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

61 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

62 
lemma (in ring_of_sets) finite_INT[intro]: 
41981
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

63 
assumes "finite I" "I \<noteq> {}" "\<And>i. i \<in> I \<Longrightarrow> A i \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

64 
shows "(\<Inter>i\<in>I. A i) \<in> sets M" 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

65 
using assms by (induct rule: finite_ne_induct) auto 
cdf7693bbe08
reworked Probability theory: measures are not type restricted to positive extended reals
hoelzl
parents:
41959
diff
changeset

66 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

67 
lemma (in ring_of_sets) insert_in_sets: 
38656  68 
assumes "{x} \<in> sets M" "A \<in> sets M" shows "insert x A \<in> sets M" 
69 
proof  

70 
have "{x} \<union> A \<in> sets M" using assms by (rule Un) 

71 
thus ?thesis by auto 

72 
qed 

73 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

74 
lemma (in ring_of_sets) Int_space_eq1 [simp]: "x \<in> sets M \<Longrightarrow> space M \<inter> x = x" 
38656  75 
by (metis Int_absorb1 sets_into_space) 
76 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

77 
lemma (in ring_of_sets) Int_space_eq2 [simp]: "x \<in> sets M \<Longrightarrow> x \<inter> space M = x" 
38656  78 
by (metis Int_absorb2 sets_into_space) 
79 

42867  80 
lemma (in ring_of_sets) sets_Collect_conj: 
81 
assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M" 

82 
shows "{x\<in>space M. Q x \<and> P x} \<in> sets M" 

83 
proof  

84 
have "{x\<in>space M. Q x \<and> P x} = {x\<in>space M. Q x} \<inter> {x\<in>space M. P x}" 

85 
by auto 

86 
with assms show ?thesis by auto 

87 
qed 

88 

89 
lemma (in ring_of_sets) sets_Collect_disj: 

90 
assumes "{x\<in>space M. P x} \<in> sets M" "{x\<in>space M. Q x} \<in> sets M" 

91 
shows "{x\<in>space M. Q x \<or> P x} \<in> sets M" 

92 
proof  

93 
have "{x\<in>space M. Q x \<or> P x} = {x\<in>space M. Q x} \<union> {x\<in>space M. P x}" 

94 
by auto 

95 
with assms show ?thesis by auto 

96 
qed 

97 

98 
lemma (in ring_of_sets) sets_Collect_finite_All: 

99 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S" "S \<noteq> {}" 

100 
shows "{x\<in>space M. \<forall>i\<in>S. P i x} \<in> sets M" 

101 
proof  

102 
have "{x\<in>space M. \<forall>i\<in>S. P i x} = (\<Inter>i\<in>S. {x\<in>space M. P i x})" 

103 
using `S \<noteq> {}` by auto 

104 
with assms show ?thesis by auto 

105 
qed 

106 

107 
lemma (in ring_of_sets) sets_Collect_finite_Ex: 

108 
assumes "\<And>i. i \<in> S \<Longrightarrow> {x\<in>space M. P i x} \<in> sets M" "finite S" 

109 
shows "{x\<in>space M. \<exists>i\<in>S. P i x} \<in> sets M" 

110 
proof  

111 
have "{x\<in>space M. \<exists>i\<in>S. P i x} = (\<Union>i\<in>S. {x\<in>space M. P i x})" 

112 
by auto 

113 
with assms show ?thesis by auto 

114 
qed 

115 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

116 
locale algebra = ring_of_sets + 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

117 
assumes top [iff]: "space M \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

118 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

119 
lemma (in algebra) compl_sets [intro]: 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

120 
"a \<in> sets M \<Longrightarrow> space M  a \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

121 
by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

122 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

123 
lemma algebra_iff_Un: 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

124 
"algebra M \<longleftrightarrow> 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

125 
sets M \<subseteq> Pow (space M) & 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

126 
{} \<in> sets M & 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

127 
(\<forall>a \<in> sets M. space M  a \<in> sets M) & 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

128 
(\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<union> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Un") 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

129 
proof 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

130 
assume "algebra M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

131 
then interpret algebra M . 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

132 
show ?Un using sets_into_space by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

133 
next 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

134 
assume ?Un 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

135 
show "algebra M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

136 
proof 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

137 
show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" "space M \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

138 
using `?Un` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

139 
fix a b assume a: "a \<in> sets M" and b: "b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

140 
then show "a \<union> b \<in> sets M" using `?Un` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

141 
have "a  b = space M  ((space M  a) \<union> b)" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

142 
using space a b by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

143 
then show "a  b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

144 
using a b `?Un` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

145 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

146 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

147 

2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

148 
lemma algebra_iff_Int: 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

149 
"algebra M \<longleftrightarrow> 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

150 
sets M \<subseteq> Pow (space M) & {} \<in> sets M & 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

151 
(\<forall>a \<in> sets M. space M  a \<in> sets M) & 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

152 
(\<forall>a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)" (is "_ \<longleftrightarrow> ?Int") 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

153 
proof 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

154 
assume "algebra M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

155 
then interpret algebra M . 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

156 
show ?Int using sets_into_space by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

157 
next 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

158 
assume ?Int 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

159 
show "algebra M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

160 
proof (unfold algebra_iff_Un, intro conjI ballI) 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

161 
show space: "sets M \<subseteq> Pow (space M)" "{} \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

162 
using `?Int` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

163 
from `?Int` show "\<And>a. a \<in> sets M \<Longrightarrow> space M  a \<in> sets M" by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

164 
fix a b assume sets: "a \<in> sets M" "b \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

165 
hence "a \<union> b = space M  ((space M  a) \<inter> (space M  b))" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

166 
using space by blast 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

167 
also have "... \<in> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

168 
using sets `?Int` by auto 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

169 
finally show "a \<union> b \<in> sets M" . 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

170 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

171 
qed 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

172 

42867  173 
lemma (in algebra) sets_Collect_neg: 
174 
assumes "{x\<in>space M. P x} \<in> sets M" 

175 
shows "{x\<in>space M. \<not> P x} \<in> sets M" 

176 
proof  

177 
have "{x\<in>space M. \<not> P x} = space M  {x\<in>space M. P x}" by auto 

178 
with assms show ?thesis by auto 

179 
qed 

180 

181 
lemma (in algebra) sets_Collect_imp: 

182 
"{x\<in>space M. P x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x} \<in> sets M \<Longrightarrow> {x\<in>space M. Q x \<longrightarrow> P x} \<in> sets M" 

183 
unfolding imp_conv_disj by (intro sets_Collect_disj sets_Collect_neg) 

184 

185 
lemma (in algebra) sets_Collect_const: 

186 
"{x\<in>space M. P} \<in> sets M" 

187 
by (cases P) auto 

188 

42984  189 
lemma algebra_single_set: 
190 
assumes "X \<subseteq> S" 

191 
shows "algebra \<lparr> space = S, sets = { {}, X, S  X, S }\<rparr>" 

192 
by default (insert `X \<subseteq> S`, auto) 

193 

39092  194 
section {* Restricted algebras *} 
195 

196 
abbreviation (in algebra) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

197 
"restricted_space A \<equiv> \<lparr> space = A, sets = (\<lambda>S. (A \<inter> S)) ` sets M, \<dots> = more M \<rparr>" 
39092  198 

38656  199 
lemma (in algebra) restricted_algebra: 
39092  200 
assumes "A \<in> sets M" shows "algebra (restricted_space A)" 
38656  201 
using assms by unfold_locales auto 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

202 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

203 
subsection {* Sigma Algebras *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

204 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

205 
locale sigma_algebra = algebra + 
38656  206 
assumes countable_nat_UN [intro]: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

207 
"!!A. range A \<subseteq> sets M \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

208 

42984  209 
lemma (in algebra) is_sigma_algebra: 
210 
assumes "finite (sets M)" 

211 
shows "sigma_algebra M" 

212 
proof 

213 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets M" 

214 
then have "(\<Union>i. A i) = (\<Union>s\<in>sets M \<inter> range A. s)" 

215 
by auto 

216 
also have "(\<Union>s\<in>sets M \<inter> range A. s) \<in> sets M" 

217 
using `finite (sets M)` by (auto intro: finite_UN) 

218 
finally show "(\<Union>i. A i) \<in> sets M" . 

219 
qed 

220 

38656  221 
lemma countable_UN_eq: 
222 
fixes A :: "'i::countable \<Rightarrow> 'a set" 

223 
shows "(range A \<subseteq> sets M \<longrightarrow> (\<Union>i. A i) \<in> sets M) \<longleftrightarrow> 

224 
(range (A \<circ> from_nat) \<subseteq> sets M \<longrightarrow> (\<Union>i. (A \<circ> from_nat) i) \<in> sets M)" 

225 
proof  

226 
let ?A' = "A \<circ> from_nat" 

227 
have *: "(\<Union>i. ?A' i) = (\<Union>i. A i)" (is "?l = ?r") 

228 
proof safe 

229 
fix x i assume "x \<in> A i" thus "x \<in> ?l" 

230 
by (auto intro!: exI[of _ "to_nat i"]) 

231 
next 

232 
fix x i assume "x \<in> ?A' i" thus "x \<in> ?r" 

233 
by (auto intro!: exI[of _ "from_nat i"]) 

234 
qed 

235 
have **: "range ?A' = range A" 

40702  236 
using surj_from_nat 
38656  237 
by (auto simp: image_compose intro!: imageI) 
238 
show ?thesis unfolding * ** .. 

239 
qed 

240 

241 
lemma (in sigma_algebra) countable_UN[intro]: 

242 
fixes A :: "'i::countable \<Rightarrow> 'a set" 

243 
assumes "A`X \<subseteq> sets M" 

244 
shows "(\<Union>x\<in>X. A x) \<in> sets M" 

245 
proof  

246 
let "?A i" = "if i \<in> X then A i else {}" 

247 
from assms have "range ?A \<subseteq> sets M" by auto 

248 
with countable_nat_UN[of "?A \<circ> from_nat"] countable_UN_eq[of ?A M] 

249 
have "(\<Union>x. ?A x) \<in> sets M" by auto 

250 
moreover have "(\<Union>x. ?A x) = (\<Union>x\<in>X. A x)" by (auto split: split_if_asm) 

251 
ultimately show ?thesis by simp 

252 
qed 

253 

33533
40b44cb20c8c
New theory Probability/Borel.thy, and some associated lemmas
paulson
parents:
33271
diff
changeset

254 
lemma (in sigma_algebra) countable_INT [intro]: 
38656  255 
fixes A :: "'i::countable \<Rightarrow> 'a set" 
256 
assumes A: "A`X \<subseteq> sets M" "X \<noteq> {}" 

257 
shows "(\<Inter>i\<in>X. A i) \<in> sets M" 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

258 
proof  
38656  259 
from A have "\<forall>i\<in>X. A i \<in> sets M" by fast 
260 
hence "space M  (\<Union>i\<in>X. space M  A i) \<in> sets M" by blast 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

261 
moreover 
38656  262 
have "(\<Inter>i\<in>X. A i) = space M  (\<Union>i\<in>X. space M  A i)" using space_closed A 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

263 
by blast 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

264 
ultimately show ?thesis by metis 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

265 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

266 

42145  267 
lemma ring_of_sets_Pow: 
268 
"ring_of_sets \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>" 

269 
by default auto 

270 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

271 
lemma algebra_Pow: 
42145  272 
"algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>" 
273 
by default auto 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

274 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

275 
lemma sigma_algebra_Pow: 
38656  276 
"sigma_algebra \<lparr> space = sp, sets = Pow sp, \<dots> = X \<rparr>" 
42145  277 
by default auto 
38656  278 

279 
lemma sigma_algebra_iff: 

280 
"sigma_algebra M \<longleftrightarrow> 

281 
algebra M \<and> (\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 

282 
by (simp add: sigma_algebra_def sigma_algebra_axioms_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

283 

42867  284 
lemma (in sigma_algebra) sets_Collect_countable_All: 
285 
assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M" 

286 
shows "{x\<in>space M. \<forall>i::'i::countable. P i x} \<in> sets M" 

287 
proof  

288 
have "{x\<in>space M. \<forall>i::'i::countable. P i x} = (\<Inter>i. {x\<in>space M. P i x})" by auto 

289 
with assms show ?thesis by auto 

290 
qed 

291 

292 
lemma (in sigma_algebra) sets_Collect_countable_Ex: 

293 
assumes "\<And>i. {x\<in>space M. P i x} \<in> sets M" 

294 
shows "{x\<in>space M. \<exists>i::'i::countable. P i x} \<in> sets M" 

295 
proof  

296 
have "{x\<in>space M. \<exists>i::'i::countable. P i x} = (\<Union>i. {x\<in>space M. P i x})" by auto 

297 
with assms show ?thesis by auto 

298 
qed 

299 

300 
lemmas (in sigma_algebra) sets_Collect = 

301 
sets_Collect_imp sets_Collect_disj sets_Collect_conj sets_Collect_neg sets_Collect_const 

302 
sets_Collect_countable_All sets_Collect_countable_Ex sets_Collect_countable_All 

303 

42984  304 
lemma sigma_algebra_single_set: 
305 
assumes "X \<subseteq> S" 

306 
shows "sigma_algebra \<lparr> space = S, sets = { {}, X, S  X, S }\<rparr>" 

307 
using algebra.is_sigma_algebra[OF algebra_single_set[OF `X \<subseteq> S`]] by simp 

308 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

309 
subsection {* Binary Unions *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

310 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

311 
definition binary :: "'a \<Rightarrow> 'a \<Rightarrow> nat \<Rightarrow> 'a" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

312 
where "binary a b = (\<lambda>\<^isup>x. b)(0 := a)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

313 

38656  314 
lemma range_binary_eq: "range(binary a b) = {a,b}" 
315 
by (auto simp add: binary_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

316 

38656  317 
lemma Un_range_binary: "a \<union> b = (\<Union>i::nat. binary a b i)" 
318 
by (simp add: UNION_eq_Union_image range_binary_eq) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

319 

38656  320 
lemma Int_range_binary: "a \<inter> b = (\<Inter>i::nat. binary a b i)" 
321 
by (simp add: INTER_eq_Inter_image range_binary_eq) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

322 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

323 
lemma sigma_algebra_iff2: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

324 
"sigma_algebra M \<longleftrightarrow> 
38656  325 
sets M \<subseteq> Pow (space M) \<and> 
326 
{} \<in> sets M \<and> (\<forall>s \<in> sets M. space M  s \<in> sets M) \<and> 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

327 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 
38656  328 
by (auto simp add: range_binary_eq sigma_algebra_def sigma_algebra_axioms_def 
42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

329 
algebra_iff_Un Un_range_binary) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

330 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

331 
subsection {* Initial Sigma Algebra *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

332 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

333 
text {*Sigma algebras can naturally be created as the closure of any set of 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

334 
sets with regard to the properties just postulated. *} 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

335 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

336 
inductive_set 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

337 
sigma_sets :: "'a set \<Rightarrow> 'a set set \<Rightarrow> 'a set set" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

338 
for sp :: "'a set" and A :: "'a set set" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

339 
where 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

340 
Basic: "a \<in> A \<Longrightarrow> a \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

341 
 Empty: "{} \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

342 
 Compl: "a \<in> sigma_sets sp A \<Longrightarrow> sp  a \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

343 
 Union: "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Union>i. a i) \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

344 

40859  345 
definition 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

346 
"sigma M = \<lparr> space = space M, sets = sigma_sets (space M) (sets M), \<dots> = more M \<rparr>" 
41543  347 

348 
lemma (in sigma_algebra) sigma_sets_subset: 

349 
assumes a: "a \<subseteq> sets M" 

350 
shows "sigma_sets (space M) a \<subseteq> sets M" 

351 
proof 

352 
fix x 

353 
assume "x \<in> sigma_sets (space M) a" 

354 
from this show "x \<in> sets M" 

355 
by (induct rule: sigma_sets.induct, auto) (metis a subsetD) 

356 
qed 

357 

358 
lemma sigma_sets_into_sp: "A \<subseteq> Pow sp \<Longrightarrow> x \<in> sigma_sets sp A \<Longrightarrow> x \<subseteq> sp" 

359 
by (erule sigma_sets.induct, auto) 

360 

361 
lemma sigma_algebra_sigma_sets: 

362 
"a \<subseteq> Pow (space M) \<Longrightarrow> sets M = sigma_sets (space M) a \<Longrightarrow> sigma_algebra M" 

363 
by (auto simp add: sigma_algebra_iff2 dest: sigma_sets_into_sp 

364 
intro!: sigma_sets.Union sigma_sets.Empty sigma_sets.Compl) 

365 

366 
lemma sigma_sets_least_sigma_algebra: 

367 
assumes "A \<subseteq> Pow S" 

368 
shows "sigma_sets S A = \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}" 

369 
proof safe 

370 
fix B X assume "A \<subseteq> B" and sa: "sigma_algebra \<lparr> space = S, sets = B \<rparr>" 

371 
and X: "X \<in> sigma_sets S A" 

372 
from sigma_algebra.sigma_sets_subset[OF sa, simplified, OF `A \<subseteq> B`] X 

373 
show "X \<in> B" by auto 

374 
next 

375 
fix X assume "X \<in> \<Inter>{B. A \<subseteq> B \<and> sigma_algebra \<lparr>space = S, sets = B\<rparr>}" 

376 
then have [intro!]: "\<And>B. A \<subseteq> B \<Longrightarrow> sigma_algebra \<lparr>space = S, sets = B\<rparr> \<Longrightarrow> X \<in> B" 

377 
by simp 

378 
have "A \<subseteq> sigma_sets S A" using assms 

379 
by (auto intro!: sigma_sets.Basic) 

380 
moreover have "sigma_algebra \<lparr>space = S, sets = sigma_sets S A\<rparr>" 

381 
using assms by (intro sigma_algebra_sigma_sets[of A]) auto 

382 
ultimately show "X \<in> sigma_sets S A" by auto 

383 
qed 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

384 

40859  385 
lemma sets_sigma: "sets (sigma M) = sigma_sets (space M) (sets M)" 
38656  386 
unfolding sigma_def by simp 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

387 

40859  388 
lemma space_sigma [simp]: "space (sigma M) = space M" 
38656  389 
by (simp add: sigma_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

390 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

391 
lemma sigma_sets_top: "sp \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

392 
by (metis Diff_empty sigma_sets.Compl sigma_sets.Empty) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

393 

38656  394 
lemma sigma_sets_Un: 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

395 
"a \<in> sigma_sets sp A \<Longrightarrow> b \<in> sigma_sets sp A \<Longrightarrow> a \<union> b \<in> sigma_sets sp A" 
38656  396 
apply (simp add: Un_range_binary range_binary_eq) 
40859  397 
apply (rule Union, simp add: binary_def) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

398 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

399 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

400 
lemma sigma_sets_Inter: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

401 
assumes Asb: "A \<subseteq> Pow sp" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

402 
shows "(\<And>i::nat. a i \<in> sigma_sets sp A) \<Longrightarrow> (\<Inter>i. a i) \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

403 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

404 
assume ai: "\<And>i::nat. a i \<in> sigma_sets sp A" 
38656  405 
hence "\<And>i::nat. sp(a i) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

406 
by (rule sigma_sets.Compl) 
38656  407 
hence "(\<Union>i. sp(a i)) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

408 
by (rule sigma_sets.Union) 
38656  409 
hence "sp(\<Union>i. sp(a i)) \<in> sigma_sets sp A" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

410 
by (rule sigma_sets.Compl) 
38656  411 
also have "sp(\<Union>i. sp(a i)) = sp Int (\<Inter>i. a i)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

412 
by auto 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

413 
also have "... = (\<Inter>i. a i)" using ai 
38656  414 
by (blast dest: sigma_sets_into_sp [OF Asb]) 
415 
finally show ?thesis . 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

416 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

417 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

418 
lemma sigma_sets_INTER: 
38656  419 
assumes Asb: "A \<subseteq> Pow sp" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

420 
and ai: "\<And>i::nat. i \<in> S \<Longrightarrow> a i \<in> sigma_sets sp A" and non: "S \<noteq> {}" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

421 
shows "(\<Inter>i\<in>S. a i) \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

422 
proof  
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

423 
from ai have "\<And>i. (if i\<in>S then a i else sp) \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

424 
by (simp add: sigma_sets.intros sigma_sets_top) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

425 
hence "(\<Inter>i. (if i\<in>S then a i else sp)) \<in> sigma_sets sp A" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

426 
by (rule sigma_sets_Inter [OF Asb]) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

427 
also have "(\<Inter>i. (if i\<in>S then a i else sp)) = (\<Inter>i\<in>S. a i)" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

428 
by auto (metis ai non sigma_sets_into_sp subset_empty subset_iff Asb)+ 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

429 
finally show ?thesis . 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

430 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

431 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

432 
lemma (in sigma_algebra) sigma_sets_eq: 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

433 
"sigma_sets (space M) (sets M) = sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

434 
proof 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

435 
show "sets M \<subseteq> sigma_sets (space M) (sets M)" 
37032  436 
by (metis Set.subsetI sigma_sets.Basic) 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

437 
next 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

438 
show "sigma_sets (space M) (sets M) \<subseteq> sets M" 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

439 
by (metis sigma_sets_subset subset_refl) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

440 
qed 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

441 

42981  442 
lemma sigma_sets_eqI: 
443 
assumes A: "\<And>a. a \<in> A \<Longrightarrow> a \<in> sigma_sets M B" 

444 
assumes B: "\<And>b. b \<in> B \<Longrightarrow> b \<in> sigma_sets M A" 

445 
shows "sigma_sets M A = sigma_sets M B" 

446 
proof (intro set_eqI iffI) 

447 
fix a assume "a \<in> sigma_sets M A" 

448 
from this A show "a \<in> sigma_sets M B" 

449 
by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic) 

450 
next 

451 
fix b assume "b \<in> sigma_sets M B" 

452 
from this B show "b \<in> sigma_sets M A" 

453 
by induct (auto intro!: sigma_sets.intros del: sigma_sets.Basic) 

454 
qed 

455 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

456 
lemma sigma_algebra_sigma: 
40859  457 
"sets M \<subseteq> Pow (space M) \<Longrightarrow> sigma_algebra (sigma M)" 
38656  458 
apply (rule sigma_algebra_sigma_sets) 
459 
apply (auto simp add: sigma_def) 

33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

460 
done 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

461 

7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

462 
lemma (in sigma_algebra) sigma_subset: 
40859  463 
"sets N \<subseteq> sets M \<Longrightarrow> space N = space M \<Longrightarrow> sets (sigma N) \<subseteq> (sets M)" 
33271
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

464 
by (simp add: sigma_def sigma_sets_subset) 
7be66dee1a5a
New theory Probability, which contains a development of measure theory
paulson
parents:
diff
changeset

465 

42984  466 
lemma sigma_sets_subseteq: assumes "A \<subseteq> B" shows "sigma_sets X A \<subseteq> sigma_sets X B" 
467 
proof 

468 
fix x assume "x \<in> sigma_sets X A" then show "x \<in> sigma_sets X B" 

469 
by induct (insert `A \<subseteq> B`, auto intro: sigma_sets.intros) 

470 
qed 

471 

38656  472 
lemma (in sigma_algebra) restriction_in_sets: 
473 
fixes A :: "nat \<Rightarrow> 'a set" 

474 
assumes "S \<in> sets M" 

475 
and *: "range A \<subseteq> (\<lambda>A. S \<inter> A) ` sets M" (is "_ \<subseteq> ?r") 

476 
shows "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M" 

477 
proof  

478 
{ fix i have "A i \<in> ?r" using * by auto 

479 
hence "\<exists>B. A i = B \<inter> S \<and> B \<in> sets M" by auto 

480 
hence "A i \<subseteq> S" "A i \<in> sets M" using `S \<in> sets M` by auto } 

481 
thus "range A \<subseteq> sets M" "(\<Union>i. A i) \<in> (\<lambda>A. S \<inter> A) ` sets M" 

482 
by (auto intro!: image_eqI[of _ _ "(\<Union>i. A i)"]) 

483 
qed 

484 

485 
lemma (in sigma_algebra) restricted_sigma_algebra: 

486 
assumes "S \<in> sets M" 

39092  487 
shows "sigma_algebra (restricted_space S)" 
38656  488 
unfolding sigma_algebra_def sigma_algebra_axioms_def 
489 
proof safe 

39092  490 
show "algebra (restricted_space S)" using restricted_algebra[OF assms] . 
38656  491 
next 
39092  492 
fix A :: "nat \<Rightarrow> 'a set" assume "range A \<subseteq> sets (restricted_space S)" 
38656  493 
from restriction_in_sets[OF assms this[simplified]] 
39092  494 
show "(\<Union>i. A i) \<in> sets (restricted_space S)" by simp 
38656  495 
qed 
496 

40859  497 
lemma sigma_sets_Int: 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

498 
assumes "A \<in> sigma_sets sp st" "A \<subseteq> sp" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

499 
shows "op \<inter> A ` sigma_sets sp st = sigma_sets A (op \<inter> A ` st)" 
40859  500 
proof (intro equalityI subsetI) 
501 
fix x assume "x \<in> op \<inter> A ` sigma_sets sp st" 

502 
then obtain y where "y \<in> sigma_sets sp st" "x = y \<inter> A" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

503 
then have "x \<in> sigma_sets (A \<inter> sp) (op \<inter> A ` st)" 
40859  504 
proof (induct arbitrary: x) 
505 
case (Compl a) 

506 
then show ?case 

507 
by (force intro!: sigma_sets.Compl simp: Diff_Int_distrib ac_simps) 

508 
next 

509 
case (Union a) 

510 
then show ?case 

511 
by (auto intro!: sigma_sets.Union 

512 
simp add: UN_extend_simps simp del: UN_simps) 

513 
qed (auto intro!: sigma_sets.intros) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

514 
then show "x \<in> sigma_sets A (op \<inter> A ` st)" 
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

515 
using `A \<subseteq> sp` by (simp add: Int_absorb2) 
40859  516 
next 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

517 
fix x assume "x \<in> sigma_sets A (op \<inter> A ` st)" 
40859  518 
then show "x \<in> op \<inter> A ` sigma_sets sp st" 
519 
proof induct 

520 
case (Compl a) 

521 
then obtain x where "a = A \<inter> x" "x \<in> sigma_sets sp st" by auto 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

522 
then show ?case using `A \<subseteq> sp` 
40859  523 
by (force simp add: image_iff intro!: bexI[of _ "sp  x"] sigma_sets.Compl) 
524 
next 

525 
case (Union a) 

526 
then have "\<forall>i. \<exists>x. x \<in> sigma_sets sp st \<and> a i = A \<inter> x" 

527 
by (auto simp: image_iff Bex_def) 

528 
from choice[OF this] guess f .. 

529 
then show ?case 

530 
by (auto intro!: bexI[of _ "(\<Union>x. f x)"] sigma_sets.Union 

531 
simp add: image_iff) 

532 
qed (auto intro!: sigma_sets.intros) 

533 
qed 

534 

535 
lemma sigma_sets_single[simp]: "sigma_sets {X} {{X}} = {{}, {X}}" 

536 
proof (intro set_eqI iffI) 

537 
fix x assume "x \<in> sigma_sets {X} {{X}}" 

538 
from sigma_sets_into_sp[OF _ this] 

539 
show "x \<in> {{}, {X}}" by auto 

540 
next 

541 
fix x assume "x \<in> {{}, {X}}" 

542 
then show "x \<in> sigma_sets {X} {{X}}" 

543 
by (auto intro: sigma_sets.Empty sigma_sets_top) 

544 
qed 

545 

40869  546 
lemma (in sigma_algebra) sets_sigma_subset: 
547 
assumes "space N = space M" 

548 
assumes "sets N \<subseteq> sets M" 

549 
shows "sets (sigma N) \<subseteq> sets M" 

550 
by (unfold assms sets_sigma, rule sigma_sets_subset, rule assms) 

551 

40871  552 
lemma in_sigma[intro, simp]: "A \<in> sets M \<Longrightarrow> A \<in> sets (sigma M)" 
553 
unfolding sigma_def by (auto intro!: sigma_sets.Basic) 

554 

555 
lemma (in sigma_algebra) sigma_eq[simp]: "sigma M = M" 

556 
unfolding sigma_def sigma_sets_eq by simp 

557 

42987  558 
lemma sigma_sigma_eq: 
559 
assumes "sets M \<subseteq> Pow (space M)" 

560 
shows "sigma (sigma M) = sigma M" 

561 
using sigma_algebra.sigma_eq[OF sigma_algebra_sigma, OF assms] . 

562 

563 
lemma sigma_sets_sigma_sets_eq: 

564 
"M \<subseteq> Pow S \<Longrightarrow> sigma_sets S (sigma_sets S M) = sigma_sets S M" 

565 
using sigma_sigma_eq[of "\<lparr> space = S, sets = M \<rparr>"] 

566 
by (simp add: sigma_def) 

567 

42984  568 
lemma sigma_sets_singleton: 
569 
assumes "X \<subseteq> S" 

570 
shows "sigma_sets S { X } = { {}, X, S  X, S }" 

571 
proof  

572 
interpret sigma_algebra "\<lparr> space = S, sets = { {}, X, S  X, S }\<rparr>" 

573 
by (rule sigma_algebra_single_set) fact 

574 
have "sigma_sets S { X } \<subseteq> sigma_sets S { {}, X, S  X, S }" 

575 
by (rule sigma_sets_subseteq) simp 

576 
moreover have "\<dots> = { {}, X, S  X, S }" 

577 
using sigma_eq unfolding sigma_def by simp 

578 
moreover 

579 
{ fix A assume "A \<in> { {}, X, S  X, S }" 

580 
then have "A \<in> sigma_sets S { X }" 

581 
by (auto intro: sigma_sets.intros sigma_sets_top) } 

582 
ultimately have "sigma_sets S { X } = sigma_sets S { {}, X, S  X, S }" 

583 
by (intro antisym) auto 

584 
with sigma_eq show ?thesis 

585 
unfolding sigma_def by simp 

586 
qed 

587 

42863  588 
lemma restricted_sigma: 
589 
assumes S: "S \<in> sets (sigma M)" and M: "sets M \<subseteq> Pow (space M)" 

590 
shows "algebra.restricted_space (sigma M) S = sigma (algebra.restricted_space M S)" 

591 
proof  

592 
from S sigma_sets_into_sp[OF M] 

593 
have "S \<in> sigma_sets (space M) (sets M)" "S \<subseteq> space M" 

594 
by (auto simp: sigma_def) 

595 
from sigma_sets_Int[OF this] 

596 
show ?thesis 

597 
by (simp add: sigma_def) 

598 
qed 

599 

42987  600 
lemma sigma_sets_vimage_commute: 
601 
assumes X: "X \<in> space M \<rightarrow> space M'" 

602 
shows "{X ` A \<inter> space M A. A \<in> sets (sigma M')} 

603 
= sigma_sets (space M) {X ` A \<inter> space M A. A \<in> sets M'}" (is "?L = ?R") 

604 
proof 

605 
show "?L \<subseteq> ?R" 

606 
proof clarify 

607 
fix A assume "A \<in> sets (sigma M')" 

608 
then have "A \<in> sigma_sets (space M') (sets M')" by (simp add: sets_sigma) 

609 
then show "X ` A \<inter> space M \<in> ?R" 

610 
proof induct 

611 
case (Basic B) then show ?case 

612 
by (auto intro!: sigma_sets.Basic) 

613 
next 

614 
case Empty then show ?case 

615 
by (auto intro!: sigma_sets.Empty) 

616 
next 

617 
case (Compl B) 

618 
have [simp]: "X ` (space M'  B) \<inter> space M = space M  (X ` B \<inter> space M)" 

619 
by (auto simp add: funcset_mem [OF X]) 

620 
with Compl show ?case 

621 
by (auto intro!: sigma_sets.Compl) 

622 
next 

623 
case (Union F) 

624 
then show ?case 

625 
by (auto simp add: vimage_UN UN_extend_simps(4) simp del: UN_simps 

626 
intro!: sigma_sets.Union) 

627 
qed 

628 
qed 

629 
show "?R \<subseteq> ?L" 

630 
proof clarify 

631 
fix A assume "A \<in> ?R" 

632 
then show "\<exists>B. A = X ` B \<inter> space M \<and> B \<in> sets (sigma M')" 

633 
proof induct 

634 
case (Basic B) then show ?case by auto 

635 
next 

636 
case Empty then show ?case 

637 
by (auto simp: sets_sigma intro!: sigma_sets.Empty exI[of _ "{}"]) 

638 
next 

639 
case (Compl B) 

640 
then obtain A where A: "B = X ` A \<inter> space M" "A \<in> sets (sigma M')" by auto 

641 
then have [simp]: "space M  B = X ` (space M'  A) \<inter> space M" 

642 
by (auto simp add: funcset_mem [OF X]) 

643 
with A(2) show ?case 

644 
by (auto simp: sets_sigma intro: sigma_sets.Compl) 

645 
next 

646 
case (Union F) 

647 
then have "\<forall>i. \<exists>B. F i = X ` B \<inter> space M \<and> B \<in> sets (sigma M')" by auto 

648 
from choice[OF this] guess A .. note A = this 

649 
with A show ?case 

650 
by (auto simp: sets_sigma vimage_UN[symmetric] intro: sigma_sets.Union) 

651 
qed 

652 
qed 

653 
qed 

654 

38656  655 
section {* Measurable functions *} 
656 

657 
definition 

658 
"measurable A B = {f \<in> space A > space B. \<forall>y \<in> sets B. f ` y \<inter> space A \<in> sets A}" 

659 

660 
lemma (in sigma_algebra) measurable_sigma: 

40859  661 
assumes B: "sets N \<subseteq> Pow (space N)" 
662 
and f: "f \<in> space M > space N" 

663 
and ba: "\<And>y. y \<in> sets N \<Longrightarrow> (f ` y) \<inter> space M \<in> sets M" 

664 
shows "f \<in> measurable M (sigma N)" 

38656  665 
proof  
40859  666 
have "sigma_sets (space N) (sets N) \<subseteq> {y . (f ` y) \<inter> space M \<in> sets M & y \<subseteq> space N}" 
38656  667 
proof clarify 
668 
fix x 

40859  669 
assume "x \<in> sigma_sets (space N) (sets N)" 
670 
thus "f ` x \<inter> space M \<in> sets M \<and> x \<subseteq> space N" 

38656  671 
proof induct 
672 
case (Basic a) 

673 
thus ?case 

674 
by (auto simp add: ba) (metis B subsetD PowD) 

675 
next 

676 
case Empty 

677 
thus ?case 

678 
by auto 

679 
next 

680 
case (Compl a) 

40859  681 
have [simp]: "f ` space N \<inter> space M = space M" 
38656  682 
by (auto simp add: funcset_mem [OF f]) 
683 
thus ?case 

684 
by (auto simp add: vimage_Diff Diff_Int_distrib2 compl_sets Compl) 

685 
next 

686 
case (Union a) 

687 
thus ?case 

40859  688 
by (simp add: vimage_UN, simp only: UN_extend_simps(4)) blast 
38656  689 
qed 
690 
qed 

691 
thus ?thesis 

692 
by (simp add: measurable_def sigma_algebra_axioms sigma_algebra_sigma B f) 

693 
(auto simp add: sigma_def) 

694 
qed 

695 

696 
lemma measurable_cong: 

697 
assumes "\<And> w. w \<in> space M \<Longrightarrow> f w = g w" 

698 
shows "f \<in> measurable M M' \<longleftrightarrow> g \<in> measurable M M'" 

699 
unfolding measurable_def using assms 

700 
by (simp cong: vimage_inter_cong Pi_cong) 

701 

702 
lemma measurable_space: 

703 
"f \<in> measurable M A \<Longrightarrow> x \<in> space M \<Longrightarrow> f x \<in> space A" 

704 
unfolding measurable_def by auto 

705 

706 
lemma measurable_sets: 

707 
"f \<in> measurable M A \<Longrightarrow> S \<in> sets A \<Longrightarrow> f ` S \<inter> space M \<in> sets M" 

708 
unfolding measurable_def by auto 

709 

710 
lemma (in sigma_algebra) measurable_subset: 

40859  711 
"(\<And>S. S \<in> sets A \<Longrightarrow> S \<subseteq> space A) \<Longrightarrow> measurable M A \<subseteq> measurable M (sigma A)" 
38656  712 
by (auto intro: measurable_sigma measurable_sets measurable_space) 
713 

714 
lemma measurable_eqI: 

715 
"\<lbrakk> space m1 = space m1' ; space m2 = space m2' ; 

716 
sets m1 = sets m1' ; sets m2 = sets m2' \<rbrakk> 

717 
\<Longrightarrow> measurable m1 m2 = measurable m1' m2'" 

718 
by (simp add: measurable_def sigma_algebra_iff2) 

719 

720 
lemma (in sigma_algebra) measurable_const[intro, simp]: 

721 
assumes "c \<in> space M'" 

722 
shows "(\<lambda>x. c) \<in> measurable M M'" 

723 
using assms by (auto simp add: measurable_def) 

724 

725 
lemma (in sigma_algebra) measurable_If: 

726 
assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'" 

727 
assumes P: "{x\<in>space M. P x} \<in> sets M" 

728 
shows "(\<lambda>x. if P x then f x else g x) \<in> measurable M M'" 

729 
unfolding measurable_def 

730 
proof safe 

731 
fix x assume "x \<in> space M" 

732 
thus "(if P x then f x else g x) \<in> space M'" 

733 
using measure unfolding measurable_def by auto 

734 
next 

735 
fix A assume "A \<in> sets M'" 

736 
hence *: "(\<lambda>x. if P x then f x else g x) ` A \<inter> space M = 

737 
((f ` A \<inter> space M) \<inter> {x\<in>space M. P x}) \<union> 

738 
((g ` A \<inter> space M) \<inter> (space M  {x\<in>space M. P x}))" 

739 
using measure unfolding measurable_def by (auto split: split_if_asm) 

740 
show "(\<lambda>x. if P x then f x else g x) ` A \<inter> space M \<in> sets M" 

741 
using `A \<in> sets M'` measure P unfolding * measurable_def 

742 
by (auto intro!: Un) 

743 
qed 

744 

745 
lemma (in sigma_algebra) measurable_If_set: 

746 
assumes measure: "f \<in> measurable M M'" "g \<in> measurable M M'" 

747 
assumes P: "A \<in> sets M" 

748 
shows "(\<lambda>x. if x \<in> A then f x else g x) \<in> measurable M M'" 

749 
proof (rule measurable_If[OF measure]) 

750 
have "{x \<in> space M. x \<in> A} = A" using `A \<in> sets M` sets_into_space by auto 

751 
thus "{x \<in> space M. x \<in> A} \<in> sets M" using `A \<in> sets M` by auto 

752 
qed 

753 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

754 
lemma (in ring_of_sets) measurable_ident[intro, simp]: "id \<in> measurable M M" 
38656  755 
by (auto simp add: measurable_def) 
756 

757 
lemma measurable_comp[intro]: 

758 
fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 

759 
shows "f \<in> measurable a b \<Longrightarrow> g \<in> measurable b c \<Longrightarrow> (g o f) \<in> measurable a c" 

760 
apply (auto simp add: measurable_def vimage_compose) 

761 
apply (subgoal_tac "f ` g ` y \<inter> space a = f ` (g ` y \<inter> space b) \<inter> space a") 

762 
apply force+ 

763 
done 

764 

765 
lemma measurable_strong: 

766 
fixes f :: "'a \<Rightarrow> 'b" and g :: "'b \<Rightarrow> 'c" 

767 
assumes f: "f \<in> measurable a b" and g: "g \<in> (space b > space c)" 

768 
and a: "sigma_algebra a" and b: "sigma_algebra b" and c: "sigma_algebra c" 

769 
and t: "f ` (space a) \<subseteq> t" 

770 
and cb: "\<And>s. s \<in> sets c \<Longrightarrow> (g ` s) \<inter> t \<in> sets b" 

771 
shows "(g o f) \<in> measurable a c" 

772 
proof  

773 
have fab: "f \<in> (space a > space b)" 

774 
and ba: "\<And>y. y \<in> sets b \<Longrightarrow> (f ` y) \<inter> (space a) \<in> sets a" using f 

775 
by (auto simp add: measurable_def) 

776 
have eq: "f ` g ` y \<inter> space a = f ` (g ` y \<inter> t) \<inter> space a" using t 

777 
by force 

778 
show ?thesis 

779 
apply (auto simp add: measurable_def vimage_compose a c) 

780 
apply (metis funcset_mem fab g) 

781 
apply (subst eq, metis ba cb) 

782 
done 

783 
qed 

784 

785 
lemma measurable_mono1: 

786 
"a \<subseteq> b \<Longrightarrow> sigma_algebra \<lparr>space = X, sets = b\<rparr> 

787 
\<Longrightarrow> measurable \<lparr>space = X, sets = a\<rparr> c \<subseteq> measurable \<lparr>space = X, sets = b\<rparr> c" 

788 
by (auto simp add: measurable_def) 

789 

790 
lemma measurable_up_sigma: 

40859  791 
"measurable A M \<subseteq> measurable (sigma A) M" 
38656  792 
unfolding measurable_def 
793 
by (auto simp: sigma_def intro: sigma_sets.Basic) 

794 

795 
lemma (in sigma_algebra) measurable_range_reduce: 

796 
"\<lbrakk> f \<in> measurable M \<lparr>space = s, sets = Pow s\<rparr> ; s \<noteq> {} \<rbrakk> 

797 
\<Longrightarrow> f \<in> measurable M \<lparr>space = s \<inter> (f ` space M), sets = Pow (s \<inter> (f ` space M))\<rparr>" 

798 
by (simp add: measurable_def sigma_algebra_Pow del: Pow_Int_eq) blast 

799 

800 
lemma (in sigma_algebra) measurable_Pow_to_Pow: 

801 
"(sets M = Pow (space M)) \<Longrightarrow> f \<in> measurable M \<lparr>space = UNIV, sets = Pow UNIV\<rparr>" 

802 
by (auto simp add: measurable_def sigma_algebra_def sigma_algebra_axioms_def algebra_def) 

803 

804 
lemma (in sigma_algebra) measurable_Pow_to_Pow_image: 

805 
"sets M = Pow (space M) 

806 
\<Longrightarrow> f \<in> measurable M \<lparr>space = f ` space M, sets = Pow (f ` space M)\<rparr>" 

807 
by (simp add: measurable_def sigma_algebra_Pow) intro_locales 

808 

40859  809 
lemma (in sigma_algebra) measurable_iff_sigma: 
810 
assumes "sets E \<subseteq> Pow (space E)" and "f \<in> space M \<rightarrow> space E" 

811 
shows "f \<in> measurable M (sigma E) \<longleftrightarrow> (\<forall>A\<in>sets E. f ` A \<inter> space M \<in> sets M)" 

812 
using measurable_sigma[OF assms] 

813 
by (fastsimp simp: measurable_def sets_sigma intro: sigma_sets.intros) 

38656  814 

815 
section "Disjoint families" 

816 

817 
definition 

818 
disjoint_family_on where 

819 
"disjoint_family_on A S \<longleftrightarrow> (\<forall>m\<in>S. \<forall>n\<in>S. m \<noteq> n \<longrightarrow> A m \<inter> A n = {})" 

820 

821 
abbreviation 

822 
"disjoint_family A \<equiv> disjoint_family_on A UNIV" 

823 

824 
lemma range_subsetD: "range f \<subseteq> B \<Longrightarrow> f i \<in> B" 

825 
by blast 

826 

827 
lemma Int_Diff_disjoint: "A \<inter> B \<inter> (A  B) = {}" 

828 
by blast 

829 

830 
lemma Int_Diff_Un: "A \<inter> B \<union> (A  B) = A" 

831 
by blast 

832 

833 
lemma disjoint_family_subset: 

834 
"disjoint_family A \<Longrightarrow> (!!x. B x \<subseteq> A x) \<Longrightarrow> disjoint_family B" 

835 
by (force simp add: disjoint_family_on_def) 

836 

40859  837 
lemma disjoint_family_on_bisimulation: 
838 
assumes "disjoint_family_on f S" 

839 
and "\<And>n m. n \<in> S \<Longrightarrow> m \<in> S \<Longrightarrow> n \<noteq> m \<Longrightarrow> f n \<inter> f m = {} \<Longrightarrow> g n \<inter> g m = {}" 

840 
shows "disjoint_family_on g S" 

841 
using assms unfolding disjoint_family_on_def by auto 

842 

38656  843 
lemma disjoint_family_on_mono: 
844 
"A \<subseteq> B \<Longrightarrow> disjoint_family_on f B \<Longrightarrow> disjoint_family_on f A" 

845 
unfolding disjoint_family_on_def by auto 

846 

847 
lemma disjoint_family_Suc: 

848 
assumes Suc: "!!n. A n \<subseteq> A (Suc n)" 

849 
shows "disjoint_family (\<lambda>i. A (Suc i)  A i)" 

850 
proof  

851 
{ 

852 
fix m 

853 
have "!!n. A n \<subseteq> A (m+n)" 

854 
proof (induct m) 

855 
case 0 show ?case by simp 

856 
next 

857 
case (Suc m) thus ?case 

858 
by (metis Suc_eq_plus1 assms nat_add_commute nat_add_left_commute subset_trans) 

859 
qed 

860 
} 

861 
hence "!!m n. m < n \<Longrightarrow> A m \<subseteq> A n" 

862 
by (metis add_commute le_add_diff_inverse nat_less_le) 

863 
thus ?thesis 

864 
by (auto simp add: disjoint_family_on_def) 

865 
(metis insert_absorb insert_subset le_SucE le_antisym not_leE) 

866 
qed 

867 

39092  868 
lemma setsum_indicator_disjoint_family: 
869 
fixes f :: "'d \<Rightarrow> 'e::semiring_1" 

870 
assumes d: "disjoint_family_on A P" and "x \<in> A j" and "finite P" and "j \<in> P" 

871 
shows "(\<Sum>i\<in>P. f i * indicator (A i) x) = f j" 

872 
proof  

873 
have "P \<inter> {i. x \<in> A i} = {j}" 

874 
using d `x \<in> A j` `j \<in> P` unfolding disjoint_family_on_def 

875 
by auto 

876 
thus ?thesis 

877 
unfolding indicator_def 

878 
by (simp add: if_distrib setsum_cases[OF `finite P`]) 

879 
qed 

880 

38656  881 
definition disjointed :: "(nat \<Rightarrow> 'a set) \<Rightarrow> nat \<Rightarrow> 'a set " 
882 
where "disjointed A n = A n  (\<Union>i\<in>{0..<n}. A i)" 

883 

884 
lemma finite_UN_disjointed_eq: "(\<Union>i\<in>{0..<n}. disjointed A i) = (\<Union>i\<in>{0..<n}. A i)" 

885 
proof (induct n) 

886 
case 0 show ?case by simp 

887 
next 

888 
case (Suc n) 

889 
thus ?case by (simp add: atLeastLessThanSuc disjointed_def) 

890 
qed 

891 

892 
lemma UN_disjointed_eq: "(\<Union>i. disjointed A i) = (\<Union>i. A i)" 

893 
apply (rule UN_finite2_eq [where k=0]) 

894 
apply (simp add: finite_UN_disjointed_eq) 

895 
done 

896 

897 
lemma less_disjoint_disjointed: "m<n \<Longrightarrow> disjointed A m \<inter> disjointed A n = {}" 

898 
by (auto simp add: disjointed_def) 

899 

900 
lemma disjoint_family_disjointed: "disjoint_family (disjointed A)" 

901 
by (simp add: disjoint_family_on_def) 

902 
(metis neq_iff Int_commute less_disjoint_disjointed) 

903 

904 
lemma disjointed_subset: "disjointed A n \<subseteq> A n" 

905 
by (auto simp add: disjointed_def) 

906 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

907 
lemma (in ring_of_sets) UNION_in_sets: 
38656  908 
fixes A:: "nat \<Rightarrow> 'a set" 
909 
assumes A: "range A \<subseteq> sets M " 

910 
shows "(\<Union>i\<in>{0..<n}. A i) \<in> sets M" 

911 
proof (induct n) 

912 
case 0 show ?case by simp 

913 
next 

914 
case (Suc n) 

915 
thus ?case 

916 
by (simp add: atLeastLessThanSuc) (metis A Un UNIV_I image_subset_iff) 

917 
qed 

918 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

919 
lemma (in ring_of_sets) range_disjointed_sets: 
38656  920 
assumes A: "range A \<subseteq> sets M " 
921 
shows "range (disjointed A) \<subseteq> sets M" 

922 
proof (auto simp add: disjointed_def) 

923 
fix n 

924 
show "A n  (\<Union>i\<in>{0..<n}. A i) \<in> sets M" using UNION_in_sets 

925 
by (metis A Diff UNIV_I image_subset_iff) 

926 
qed 

927 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

928 
lemma (in algebra) range_disjointed_sets': 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

929 
"range A \<subseteq> sets M \<Longrightarrow> range (disjointed A) \<subseteq> sets M" 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

930 
using range_disjointed_sets . 
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

931 

42145  932 
lemma disjointed_0[simp]: "disjointed A 0 = A 0" 
933 
by (simp add: disjointed_def) 

934 

935 
lemma incseq_Un: 

936 
"incseq A \<Longrightarrow> (\<Union>i\<le>n. A i) = A n" 

937 
unfolding incseq_def by auto 

938 

939 
lemma disjointed_incseq: 

940 
"incseq A \<Longrightarrow> disjointed A (Suc n) = A (Suc n)  A n" 

941 
using incseq_Un[of A] 

942 
by (simp add: disjointed_def atLeastLessThanSuc_atLeastAtMost atLeast0AtMost) 

943 

38656  944 
lemma sigma_algebra_disjoint_iff: 
945 
"sigma_algebra M \<longleftrightarrow> 

946 
algebra M & 

947 
(\<forall>A. range A \<subseteq> sets M \<longrightarrow> disjoint_family A \<longrightarrow> 

948 
(\<Union>i::nat. A i) \<in> sets M)" 

949 
proof (auto simp add: sigma_algebra_iff) 

950 
fix A :: "nat \<Rightarrow> 'a set" 

951 
assume M: "algebra M" 

952 
and A: "range A \<subseteq> sets M" 

953 
and UnA: "\<forall>A. range A \<subseteq> sets M \<longrightarrow> 

954 
disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

955 
hence "range (disjointed A) \<subseteq> sets M \<longrightarrow> 

956 
disjoint_family (disjointed A) \<longrightarrow> 

957 
(\<Union>i. disjointed A i) \<in> sets M" by blast 

958 
hence "(\<Union>i. disjointed A i) \<in> sets M" 

42065
2b98b4c2e2f1
add ring_of_sets and subset_class as basis for algebra
hoelzl
parents:
41983
diff
changeset

959 
by (simp add: algebra.range_disjointed_sets' M A disjoint_family_disjointed) 
38656  960 
thus "(\<Union>i::nat. A i) \<in> sets M" by (simp add: UN_disjointed_eq) 
961 
qed 

962 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

963 
subsection {* Sigma algebra generated by function preimages *} 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

964 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

965 
definition (in sigma_algebra) 
41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

966 
"vimage_algebra S f = \<lparr> space = S, sets = (\<lambda>A. f ` A \<inter> S) ` sets M, \<dots> = more M \<rparr>" 
39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

967 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

968 
lemma (in sigma_algebra) in_vimage_algebra[simp]: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

969 
"A \<in> sets (vimage_algebra S f) \<longleftrightarrow> (\<exists>B\<in>sets M. A = f ` B \<inter> S)" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

970 
by (simp add: vimage_algebra_def image_iff) 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

971 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

972 
lemma (in sigma_algebra) space_vimage_algebra[simp]: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

973 
"space (vimage_algebra S f) = S" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

974 
by (simp add: vimage_algebra_def) 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

975 

40859  976 
lemma (in sigma_algebra) sigma_algebra_preimages: 
977 
fixes f :: "'x \<Rightarrow> 'a" 

978 
assumes "f \<in> A \<rightarrow> space M" 

979 
shows "sigma_algebra \<lparr> space = A, sets = (\<lambda>M. f ` M \<inter> A) ` sets M \<rparr>" 

980 
(is "sigma_algebra \<lparr> space = _, sets = ?F ` sets M \<rparr>") 

981 
proof (simp add: sigma_algebra_iff2, safe) 

982 
show "{} \<in> ?F ` sets M" by blast 

983 
next 

984 
fix S assume "S \<in> sets M" 

985 
moreover have "A  ?F S = ?F (space M  S)" 

986 
using assms by auto 

987 
ultimately show "A  ?F S \<in> ?F ` sets M" 

988 
by blast 

989 
next 

990 
fix S :: "nat \<Rightarrow> 'x set" assume *: "range S \<subseteq> ?F ` sets M" 

991 
have "\<forall>i. \<exists>b. b \<in> sets M \<and> S i = ?F b" 

992 
proof safe 

993 
fix i 

994 
have "S i \<in> ?F ` sets M" using * by auto 

995 
then show "\<exists>b. b \<in> sets M \<and> S i = ?F b" by auto 

996 
qed 

997 
from choice[OF this] obtain b where b: "range b \<subseteq> sets M" "\<And>i. S i = ?F (b i)" 

998 
by auto 

999 
then have "(\<Union>i. S i) = ?F (\<Union>i. b i)" by auto 

1000 
then show "(\<Union>i. S i) \<in> ?F ` sets M" using b(1) by blast 

1001 
qed 

1002 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1003 
lemma (in sigma_algebra) sigma_algebra_vimage: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1004 
fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1005 
shows "sigma_algebra (vimage_algebra S f)" 
40859  1006 
proof  
1007 
from sigma_algebra_preimages[OF assms] 

1008 
show ?thesis unfolding vimage_algebra_def by (auto simp: sigma_algebra_iff2) 

1009 
qed 

39090
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1010 

a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1011 
lemma (in sigma_algebra) measurable_vimage_algebra: 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1012 
fixes S :: "'c set" assumes "f \<in> S \<rightarrow> space M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1013 
shows "f \<in> measurable (vimage_algebra S f) M" 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1014 
unfolding measurable_def using assms by force 
a2d38b8b693e
Introduced sigma algebra generated by function preimages.
hoelzl
parents:
38656
diff
changeset

1015 

40859  1016 
lemma (in sigma_algebra) measurable_vimage: 
1017 
fixes g :: "'a \<Rightarrow> 'c" and f :: "'d \<Rightarrow> 'a" 

1018 
assumes "g \<in> measurable M M2" "f \<in> S \<rightarrow> space M" 

1019 
shows "(\<lambda>x. g (f x)) \<in> measurable (vimage_algebra S f) M2" 

1020 
proof  

1021 
note measurable_vimage_algebra[OF assms(2)] 

1022 
from measurable_comp[OF this assms(1)] 

1023 
show ?thesis by (simp add: comp_def) 

1024 
qed 

1025 

1026 
lemma sigma_sets_vimage: 

1027 
assumes "f \<in> S' \<rightarrow> S" and "A \<subseteq> Pow S" 

1028 
shows "sigma_sets S' ((\<lambda>X. f ` X \<inter> S') ` A) = (\<lambda>X. f ` X \<inter> S') ` sigma_sets S A" 

1029 
proof (intro set_eqI iffI) 

1030 
let ?F = "\<lambda>X. f ` X \<inter> S'" 

1031 
fix X assume "X \<in> sigma_sets S' (?F ` A)" 

1032 
then show "X \<in> ?F ` sigma_sets S A" 

1033 
proof induct 

1034 
case (Basic X) then obtain X' where "X = ?F X'" "X' \<in> A" 

1035 
by auto 

1036 
then show ?case by (auto intro!: sigma_sets.Basic) 

1037 
next 

1038 
case Empty then show ?case 

1039 
by (auto intro!: image_eqI[of _ _ "{}"] sigma_sets.Empty) 

1040 
next 

1041 
case (Compl X) then obtain X' where X: "X = ?F X'" and "X' \<in> sigma_sets S A" 

1042 
by auto 

1043 
then have "S  X' \<in> sigma_sets S A" 

1044 
by (auto intro!: sigma_sets.Compl) 

1045 
then show ?case 

1046 
using X assms by (auto intro!: image_eqI[where x="S  X'"]) 

1047 
next 

1048 
case (Union F) 

1049 
then have "\<forall>i. \<exists>F'. F' \<in> sigma_sets S A \<and> F i = f ` F' \<inter> S'" 

1050 
by (auto simp: image_iff Bex_def) 

1051 
from choice[OF this] obtain F' where 

1052 
"\<And>i. F' i \<in> sigma_sets S A" and "\<And>i. F i = f ` F' i \<inter> S'" 

1053 
by auto 

1054 
then show ?case 

1055 
by (auto intro!: sigma_sets.Union image_eqI[where x="\<Union>i. F' i"]) 

1056 
qed 

1057 
next 

1058 
let ?F = "\<lambda>X. f ` X \<inter> S'" 

1059 
fix X assume "X \<in> ?F ` sigma_sets S A" 

1060 
then obtain X' where "X' \<in> sigma_sets S A" "X = ?F X'" by auto 

1061 
then show "X \<in> sigma_sets S' (?F ` A)" 

1062 
proof (induct arbitrary: X) 

1063 
case (Basic X') then show ?case by (auto intro: sigma_sets.Basic) 

1064 
next 

1065 
case Empty then show ?case by (auto intro: sigma_sets.Empty) 

1066 
next 

1067 
case (Compl X') 

1068 
have "S'  (S'  X) \<in> sigma_sets S' (?F ` A)" 

1069 
apply (rule sigma_sets.Compl) 

1070 
using assms by (auto intro!: Compl.hyps simp: Compl.prems) 

1071 
also have "S'  (S'  X) = X" 

1072 
using assms Compl by auto 

1073 
finally show ?case . 

1074 
next 

1075 
case (Union F) 

1076 
have "(\<Union>i. f ` F i \<inter> S') \<in> sigma_sets S' (?F ` A)" 

1077 
by (intro sigma_sets.Union Union.hyps) simp 

1078 
also have "(\<Union>i. f ` F i \<inter> S') = X" 

1079 
using assms Union by auto 

1080 
finally show ?case . 

1081 
qed 

1082 
qed 

1083 

39092  1084 
section {* Conditional space *} 
1085 

1086 
definition (in algebra) 

41689
3e39b0e730d6
the measure valuation is again part of the measure_space type, instead of an explicit parameter to the locale;
hoelzl
parents:
41543
diff
changeset

1087 
"image_space X = \<lparr> space = X`space M, sets = (\<lambda>S. X`S) ` sets M, \<dots> = more M \<rparr>" 
39092  1088 

1089 
definition (in algebra) 

1090 
"conditional_space X A = algebra.image_space (restricted_space A) X" 

1091 

1092 
lemma (in algebra) space_conditional_space: 

1093 
assumes "A \<in> sets M" shows "space (conditional_space X A) = X`A" 

1094 
proof  

1095 
interpret r: algebra "restricted_space A" using assms by (rule restricted_algebra) 

1096 
show ?thesis unfolding conditional_space_def r.image_space_def 

1097 
by simp 

1098 
qed 

1099 

38656  1100 
subsection {* A TwoElement Series *} 
1101 

1102 
definition binaryset :: "'a set \<Rightarrow> 'a set \<Rightarrow> nat \<Rightarrow> 'a set " 

1103 
where "binaryset A B = (\<lambda>\<^isup>x. {})(0 := A, Suc 0 := B)" 

1104 

1105 
lemma range_binaryset_eq: "range(binaryset A B) = {A,B,{}}" 

1106 
apply (simp add: binaryset_def) 

39302
d7728f65b353
renamed lemmas: ext_iff > fun_eq_iff, set_ext_iff > set_eq_iff, set_ext > set_eqI
nipkow
parents:
39092
diff
changeset

1107 
apply (rule set_eqI) 
38656  1108 
apply (auto simp add: image_iff) 
1109 
done 

1110 

1111 
lemma UN_binaryset_eq: "(\<Union>i. binaryset A B i) = A \<union> B" 

1112 
by (simp add: UNION_eq_Union_image range_binaryset_eq) 

1113 

1114 
section {* Closed CDI *} 

1115 

1116 
definition 

1117 
closed_cdi where 

1118 
"closed_cdi M \<longleftrightarrow> 

1119 
sets M \<subseteq> Pow (space M) & 

1120 
(\<forall>s \<in> sets M. space M  s \<in> sets M) & 

1121 
(\<forall>A. (range A \<subseteq> sets M) & (A 0 = {}) & (\<forall>n. A n \<subseteq> A (Suc n)) \<longrightarrow> 

1122 
(\<Union>i. A i) \<in> sets M) & 

1123 
(\<forall>A. (range A \<subseteq> sets M) & disjoint_family A \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)" 

1124 

1125 
inductive_set 

1126 
smallest_ccdi_sets :: "('a, 'b) algebra_scheme \<Rightarrow> 'a set set" 

1127 
for M 

1128 
where 

1129 
Basic [intro]: 

1130 
"a \<in> sets M \<Longrightarrow> a \<in> smallest_ccdi_sets M" 

1131 
 Compl [intro]: 

1132 
"a \<in> smallest_ccdi_sets M \<Longrightarrow> space M  a \<in> smallest_ccdi_sets M" 

1133 
 Inc: 

1134 
"range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> A 0 = {} \<Longrightarrow> (\<And>n. A n \<subseteq> A (Suc n)) 

1135 
\<Longrightarrow> (\<Union>i. A i) \<in> smallest_ccdi_sets M" 

1136 
 Disj: 

1137 
"range A \<in> Pow(smallest_ccdi_sets M) \<Longrightarrow> disjoint_family A 

1138 
\<Longrightarrow> (\<Union>i::nat. A i) \<in> smallest_ccdi_sets M" 

1139 
monos Pow_mono 

1140 

1141 

1142 
definition 

1143 
smallest_closed_cdi where 

1144 
"smallest_closed_cdi M = (space = space M, sets = smallest_ccdi_sets M)" 

1145 

1146 
lemma space_smallest_closed_cdi [simp]: 

1147 
"space (smallest_closed_cdi M) = space M" 

1148 
by (simp add: smallest_closed_cdi_def) 

1149 

1150 
lemma (in algebra) smallest_closed_cdi1: "sets M \<subseteq> sets (smallest_closed_cdi M)" 

1151 
by (auto simp add: smallest_closed_cdi_def) 

1152 

1153 
lemma (in algebra) smallest_ccdi_sets: 

1154 
"smallest_ccdi_sets M \<subseteq> Pow (space M)" 

1155 
apply (rule subsetI) 

1156 
apply (erule smallest_ccdi_sets.induct) 

1157 
apply (auto intro: range_subsetD dest: sets_into_space) 

1158 
done 

1159 

1160 
lemma (in algebra) smallest_closed_cdi2: "closed_cdi (smallest_closed_cdi M)" 

1161 
apply (auto simp add: closed_cdi_def smallest_closed_cdi_def smallest_ccdi_sets) 

1162 
apply (blast intro: smallest_ccdi_sets.Inc smallest_ccdi_sets.Disj) + 

1163 
done 

1164 

1165 
lemma (in algebra) smallest_closed_cdi3: 

1166 
"sets (smallest_closed_cdi M) \<subseteq> Pow (space M)" 

1167 
by (simp add: smallest_closed_cdi_def smallest_ccdi_sets) 

1168 

1169 
lemma closed_cdi_subset: "closed_cdi M \<Longrightarrow> sets M \<subseteq> Pow (space M)" 

1170 
by (simp add: closed_cdi_def) 

1171 

1172 
lemma closed_cdi_Compl: "closed_cdi M \<Longrightarrow> s \<in> sets M \<Longrightarrow> space M  s \<in> sets M" 

1173 
by (simp add: closed_cdi_def) 

1174 

1175 
lemma closed_cdi_Inc: 

1176 
"closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> A 0 = {} \<Longrightarrow> (!!n. A n \<subseteq> A (Suc n)) \<Longrightarrow> 

1177 
(\<Union>i. A i) \<in> sets M" 

1178 
by (simp add: closed_cdi_def) 

1179 

1180 
lemma closed_cdi_Disj: 

1181 
"closed_cdi M \<Longrightarrow> range A \<subseteq> sets M \<Longrightarrow> disjoint_family A \<Longrightarrow> (\<Union>i::nat. A i) \<in> sets M" 

1182 
by (simp add: closed_cdi_def) 

1183 

1184 
lemma closed_cdi_Un: 

1185 
assumes cdi: "closed_cdi M" and empty: "{} \<in> sets M" 

1186 
and A: "A \<in> sets M" and B: "B \<in> sets M" 

1187 
and disj: "A \<inter> B = {}" 

1188 
shows "A \<union> B \<in> sets M" 

1189 
proof  

1190 
have ra: "range (binaryset A B) \<subseteq> sets M" 

1191 
by (simp add: range_binaryset_eq empty A B) 

1192 
have di: "disjoint_family (binaryset A B)" using disj 

1193 
by (simp add: disjoint_family_on_def binaryset_def Int_commute) 

1194 
from closed_cdi_Disj [OF cdi ra di] 

1195 
show ?thesis 

1196 
by (simp add: UN_binaryset_eq) 

1197 
qed 

1198 

1199 
lemma (in algebra) smallest_ccdi_sets_Un: 

1200 
assumes A: "A \<in> smallest_ccdi_sets M" and B: "B \<in> smallest_ccdi_sets M" 

1201 
and disj: "A \<inter> B = {}" 

1202 
shows "A \<union> B \<in> smallest_ccdi_sets M" 

1203 
proof  

1204 
have ra: "range (binaryset A B) \<in> Pow (smallest_ccdi_sets M)" 

1205 
by (simp add: range_binaryset_eq A B smallest_ccdi_sets.Basic) 

1206 
have di: "disjoint_family (binaryset A B)" using disj 

1207 
by (simp add: disjoint_family_on_def binaryset_def Int_commute) 

1208 
from Disj [OF ra di] 

1209 
show ?thesis 

1210 
by (simp add: UN_binaryset_eq) 

1211 
qed 

1212 

1213 
lemma (in algebra) smallest_ccdi_sets_Int1: 

1214 
assumes a: "a \<in> sets M" 

1215 
shows "b \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M" 

1216 
proof (induct rule: smallest_ccdi_sets.induct) 

1217 
case (Basic x) 

1218 
thus ?case 

1219 
by (metis a Int smallest_ccdi_sets.Basic) 

1220 
next 

1221 
case (Compl x) 

1222 
have "a \<inter> (space M  x) = space M  ((space M  a) \<union> (a \<inter> x))" 

1223 
by blast 

1224 
also have "... \<in> smallest_ccdi_sets M" 

1225 
by (metis smallest_ccdi_sets.Compl a Compl(2) Diff_Int2 Diff_Int_distrib2 

1226 
Diff_disjoint Int_Diff Int_empty_right Un_commute 

1227 
smallest_ccdi_sets.Basic smallest_ccdi_sets.Compl 

1228 
smallest_ccdi_sets_Un) 

1229 
finally show ?case . 

1230 
next 

1231 
case (Inc A) 

1232 
have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" 

1233 
by blast 

1234 
have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Inc 

1235 
by blast 

1236 
moreover have "(\<lambda>i. a \<inter> A i) 0 = {}" 

1237 
by (simp add: Inc) 

1238 
moreover have "!!n. (\<lambda>i. a \<inter> A i) n \<subseteq> (\<lambda>i. a \<inter> A i) (Suc n)" using Inc 

1239 
by blast 

1240 
ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M" 

1241 
by (rule smallest_ccdi_sets.Inc) 

1242 
show ?case 

1243 
by (metis 1 2) 

1244 
next 

1245 
case (Disj A) 

1246 
have 1: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) = a \<inter> (\<Union>i. A i)" 

1247 
by blast 

1248 
have "range (\<lambda>i. a \<inter> A i) \<in> Pow(smallest_ccdi_sets M)" using Disj 

1249 
by blast 

1250 
moreover have "disjoint_family (\<lambda>i. a \<inter> A i)" using Disj 

1251 
by (auto simp add: disjoint_family_on_def) 

1252 
ultimately have 2: "(\<Union>i. (\<lambda>i. a \<inter> A i) i) \<in> smallest_ccdi_sets M" 

1253 
by (rule smallest_ccdi_sets.Disj) 

1254 
show ?case 

1255 
by (metis 1 2) 

1256 
qed 

1257 

1258 

1259 
lemma (in algebra) smallest_ccdi_sets_Int: 

1260 
assumes b: "b \<in> smallest_ccdi_sets M" 

1261 
shows "a \<in> smallest_ccdi_sets M \<Longrightarrow> a \<inter> b \<in> smallest_ccdi_sets M" 

