1.1 --- a/src/HOL/Probability/Product_Measure.thy Thu Aug 26 13:17:58 2010 +0200
1.2 +++ b/src/HOL/Probability/Product_Measure.thy Thu Aug 26 15:20:41 2010 +0200
1.3 @@ -2,12 +2,11 @@
1.4 imports Lebesgue_Integration
1.5 begin
1.6
1.7 -definition dynkin
1.8 -where "dynkin M =
1.9 - ((\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
1.10 - space M \<in> sets M \<and> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
1.11 - (\<forall> a. (\<forall> i j :: nat. i \<noteq> j \<longrightarrow> a i \<inter> a j = {}) \<and>
1.12 - (\<forall> i :: nat. a i \<in> sets M) \<longrightarrow> UNION UNIV a \<in> sets M))"
1.13 +definition "dynkin M \<longleftrightarrow>
1.14 + space M \<in> sets M \<and>
1.15 + (\<forall> A \<in> sets M. A \<subseteq> space M) \<and>
1.16 + (\<forall> a \<in> sets M. \<forall> b \<in> sets M. b - a \<in> sets M) \<and>
1.17 + (\<forall>A. disjoint_family A \<and> range A \<subseteq> sets M \<longrightarrow> (\<Union>i::nat. A i) \<in> sets M)"
1.18
1.19 lemma dynkinI:
1.20 assumes "\<And> A. A \<in> sets M \<Longrightarrow> A \<subseteq> space M"
1.21 @@ -15,7 +14,7 @@
1.22 assumes "\<And> a. (\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {})
1.23 \<Longrightarrow> (\<And> i :: nat. a i \<in> sets M) \<Longrightarrow> UNION UNIV a \<in> sets M"
1.24 shows "dynkin M"
1.25 -using assms unfolding dynkin_def by auto
1.26 +using assms unfolding dynkin_def sorry
1.27
1.28 lemma dynkin_subset:
1.29 assumes "dynkin M"
1.30 @@ -37,16 +36,16 @@
1.31 assumes "\<And> i j :: nat. i \<noteq> j \<Longrightarrow> a i \<inter> a j = {}"
1.32 assumes "\<forall> i :: nat. a i \<in> sets M"
1.33 shows "UNION UNIV a \<in> sets M"
1.34 -using assms unfolding dynkin_def by auto
1.35 +using assms unfolding dynkin_def sorry
1.36
1.37 -definition Int_stable
1.38 -where "Int_stable M = (\<forall> a \<in> sets M. (\<forall> b \<in> sets M. a \<inter> b \<in> sets M))"
1.39 +definition "Int_stable M \<longleftrightarrow> (\<forall> a \<in> sets M. \<forall> b \<in> sets M. a \<inter> b \<in> sets M)"
1.40
1.41 lemma dynkin_trivial:
1.42 shows "dynkin \<lparr> space = A, sets = Pow A \<rparr>"
1.43 by (rule dynkinI) auto
1.44
1.45 lemma
1.46 + fixes D :: "'a algebra"
1.47 assumes stab: "Int_stable E"
1.48 and spac: "space E = space D"
1.49 and subsED: "sets E \<subseteq> sets D"
1.50 @@ -69,23 +68,9 @@
1.51 proof (rule dynkinI, safe)
1.52 fix A x assume asm: "A \<in> sets \<delta>E" "x \<in> A"
1.53 { fix d :: "('a, 'b) algebra_scheme" assume "A \<in> sets d" "dynkin d \<and> space d = space E"
1.54 - hence "A \<subseteq> space d"
1.55 - using dynkin_subset by auto }
1.56 - show "x \<in> space \<delta>E" using asm
1.57 - unfolding \<delta>E_def sets_\<delta>E_def using not_empty
1.58 - proof auto
1.59 - fix x A fix d :: "'a algebra"
1.60 - assume asm: "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
1.61 - dynkin d \<and>
1.62 - space d = space E \<and>
1.63 - sets E \<subseteq> sets d) \<longrightarrow>
1.64 - A \<in> x" "x \<in> A"
1.65 - and asm': "space d = space E" "dynkin d" "sets E \<subseteq> sets d"
1.66 - have "A \<in> sets d"
1.67 - apply (rule impE[OF spec[OF asm(1), of "sets d"]])
1.68 - using exI[of _ d] asm' by auto
1.69 - thus "x \<in> space E" using asm' dynkin_subset[OF asm'(2), of A] asm(2) by auto
1.70 - qed
1.71 + hence "A \<subseteq> space d" using dynkin_subset by auto }
1.72 + show "x \<in> space \<delta>E" using asm unfolding \<delta>E_def sets_\<delta>E_def using not_empty
1.73 + by simp (metis dynkin_subset in_mono mem_def)
1.74 next
1.75 show "space \<delta>E \<in> sets \<delta>E"
1.76 unfolding \<delta>E_def sets_\<delta>E_def
1.77 @@ -100,28 +85,14 @@
1.78 unfolding \<delta>E_def sets_\<delta>E_def apply (auto intro!:dynkin_UN[OF _ asm(1)])
1.79 by blast
1.80 qed
1.81 +
1.82 def Dy == "\<lambda> d. {A | A. A \<in> sets_\<delta>E \<and> A \<inter> d \<in> sets_\<delta>E}"
1.83 { fix d assume dasm: "d \<in> sets_\<delta>E"
1.84 have "dynkin \<lparr> space = space E, sets = Dy d \<rparr>"
1.85 - proof (rule dynkinI, auto)
1.86 + proof (rule dynkinI, safe, simp_all)
1.87 fix A x assume "A \<in> Dy d" "x \<in> A"
1.88 thus "x \<in> space E" unfolding Dy_def sets_\<delta>E_def using not_empty
1.89 - proof auto fix x A fix da :: "'a algebra"
1.90 - assume asm: "x \<in> A"
1.91 - "\<forall>x. (\<exists>d :: 'a algebra. x = sets d \<and>
1.92 - dynkin d \<and> space d = space E \<and>
1.93 - sets E \<subseteq> sets d) \<longrightarrow> A \<in> x"
1.94 - "\<forall>x. (\<exists>d. x = sets d \<and>
1.95 - dynkin d \<and> space d = space E \<and>
1.96 - sets E \<subseteq> sets d) \<longrightarrow> A \<inter> d \<in> x"
1.97 - "space da = space E" "dynkin da"
1.98 - "sets E \<subseteq> sets da"
1.99 - have "A \<in> sets da"
1.100 - apply (rule impE[OF spec[OF asm(2)], of "sets da"])
1.101 - apply (rule exI[of _ da])
1.102 - using exI[of _ da] asm(4,5,6) by auto
1.103 - thus "x \<in> space E" using dynkin_subset[OF asm(5)] asm by auto
1.104 - qed
1.105 + by simp (metis dynkin_subset in_mono mem_def)
1.106 next
1.107 show "space E \<in> Dy d"
1.108 unfolding Dy_def \<delta>E_def sets_\<delta>E_def
1.109 @@ -189,20 +160,7 @@
1.110 have "\<lparr> space = space E, sets = Dy e \<rparr> \<in> {d | d. dynkin d \<and> space d = space E \<and> sets E \<subseteq> sets d}"
1.111 using Dy_nkin[OF deasm[unfolded \<delta>E_def, simplified]] E_\<delta>E E_Dy by auto
1.112 hence "sets_\<delta>E \<subseteq> Dy e"
1.113 - unfolding sets_\<delta>E_def
1.114 - proof auto fix x
1.115 - assume asm: "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and>
1.116 - dynkin d \<and>
1.117 - space d = space E \<and>
1.118 - sets E \<subseteq> sets d) \<longrightarrow>
1.119 - x \<in> xa"
1.120 - "dynkin \<lparr>space = space E, sets = Dy e\<rparr>"
1.121 - "sets E \<subseteq> Dy e"
1.122 - show "x \<in> Dy e"
1.123 - apply (rule impE[OF spec[OF asm(1), of "Dy e"]])
1.124 - apply (rule exI[of _ "\<lparr>space = space E, sets = Dy e\<rparr>"])
1.125 - using asm by auto
1.126 - qed
1.127 + unfolding sets_\<delta>E_def by auto (metis E_Dy simps(1) simps(2) spac)
1.128 hence "sets \<delta>E = Dy e" using subset unfolding \<delta>E_def by auto
1.129 hence "d \<inter> e \<in> sets \<delta>E"
1.130 using dasm easm deasm unfolding Dy_def \<delta>E_def by auto
1.131 @@ -211,18 +169,8 @@
1.132 by (auto simp add:Int_commute) }
1.133 hence "sets E \<subseteq> Dy d" by auto
1.134 hence "sets \<delta>E \<subseteq> Dy d" using Dy_nkin[OF dasm[unfolded \<delta>E_def, simplified]]
1.135 - unfolding \<delta>E_def sets_\<delta>E_def
1.136 - proof auto
1.137 - fix x
1.138 - assume asm: "sets E \<subseteq> Dy d"
1.139 - "dynkin \<lparr>space = space E, sets = Dy d\<rparr>"
1.140 - "\<forall>xa. (\<exists>d :: 'a algebra. xa = sets d \<and> dynkin d \<and>
1.141 - space d = space E \<and> sets E \<subseteq> sets d) \<longrightarrow> x \<in> xa"
1.142 - show "x \<in> Dy d"
1.143 - apply (rule impE[OF spec[OF asm(3), of "Dy d"]])
1.144 - apply (rule exI[of _ "\<lparr>space = space E, sets = Dy d\<rparr>"])
1.145 - using asm by auto
1.146 - qed
1.147 + unfolding \<delta>E_def sets_\<delta>E_def
1.148 + by auto (metis `sets E <= Dy d` simps(1) simps(2) spac)
1.149 hence *: "sets \<delta>E = Dy d"
1.150 unfolding Dy_def \<delta>E_def by auto
1.151 fix a assume aasm: "a \<in> sets \<delta>E"
1.152 @@ -234,22 +182,22 @@
1.153 using dynkin_diff[OF dyn, of _ "space D", OF _ dynkin_space[OF dyn]]
1.154 using dynkin_diff[OF dyn, of "space D" "space D", OF dynkin_space[OF dyn] dynkin_space[OF dyn]]
1.155 using dynkin_space[OF dyn]
1.156 + sorry
1.157 +(*
1.158 proof auto
1.159 fix A :: "nat \<Rightarrow> 'a set" assume Asm: "range A \<subseteq> sets D" "\<And>A. A \<in> sets D \<Longrightarrow> A \<subseteq> space D"
1.160 "\<And>a. a \<in> sets D \<Longrightarrow> space D - a \<in> sets D"
1.161 "{} \<in> sets D" "space D \<in> sets D"
1.162 let "?A i" = "A i - (\<Inter> j \<in> {..< i}. A j)"
1.163 { fix i :: nat assume "i > 0"
1.164 - have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E"
1.165 - apply (induct i)
1.166 - apply auto
1.167 - }
1.168 - from dynkin_UN
1.169 + have "(\<Inter> j \<in> {..< i}. A j) \<in> sets \<delta>E" sorry }
1.170 + oops
1.171 qed
1.172 +*)
1.173 +
1.174 + show ?thesis sorry
1.175 qed
1.176
1.177 -lemma
1.178 -(*
1.179 definition prod_sets where
1.180 "prod_sets A B = {z. \<exists>x \<in> A. \<exists>y \<in> B. z = x \<times> y}"
1.181
1.182 @@ -401,5 +349,4 @@
1.183 unfolding finite_prod_measure_space[OF N, symmetric]
1.184 using finite_measure_space_finite_prod_measure[OF N] .
1.185
1.186 -*)
1.187 end
1.188 \ No newline at end of file