|
1 (* Title: HOL/Probability/Tree_Space.thy |
|
2 Author: Johannes Hölzl, CMU *) |
|
3 |
|
4 theory Tree_Space |
|
5 imports Analysis |
|
6 begin |
|
7 |
|
8 lemma countable_lfp: |
|
9 assumes step: "\<And>Y. countable Y \<Longrightarrow> countable (F Y)" |
|
10 and cont: "Order_Continuity.sup_continuous F" |
|
11 shows "countable (lfp F)" |
|
12 by(subst sup_continuous_lfp[OF cont])(simp add: countable_funpow[OF step]) |
|
13 |
|
14 lemma countable_lfp_apply: |
|
15 assumes step: "\<And>Y x. (\<And>x. countable (Y x)) \<Longrightarrow> countable (F Y x)" |
|
16 and cont: "Order_Continuity.sup_continuous F" |
|
17 shows "countable (lfp F x)" |
|
18 proof - |
|
19 { fix n |
|
20 have "\<And>x. countable ((F ^^ n) bot x)" |
|
21 by(induct n)(auto intro: step) } |
|
22 thus ?thesis using cont by(simp add: sup_continuous_lfp) |
|
23 qed |
|
24 |
|
25 datatype 'a tree = Leaf |
|
26 | Node (left: "'a tree") (val: 'a) (right: "'a tree") |
|
27 where |
|
28 "left Leaf = Leaf" |
|
29 | "right Leaf = Leaf" |
|
30 | "val Leaf = undefined" |
|
31 |
|
32 inductive_set trees :: "'a set \<Rightarrow> 'a tree set" for S :: "'a set" where |
|
33 [intro!]: "Leaf \<in> trees S" |
|
34 | "l \<in> trees S \<Longrightarrow> r \<in> trees S \<Longrightarrow> v \<in> S \<Longrightarrow> Node l v r \<in> trees S" |
|
35 |
|
36 lemma Node_in_trees_iff[simp]: "Node l v r \<in> trees S \<longleftrightarrow> (l \<in> trees S \<and> v \<in> S \<and> r \<in> trees S)" |
|
37 by (subst trees.simps) auto |
|
38 |
|
39 lemma trees_sub_lfp: "trees S \<subseteq> lfp (\<lambda>T. T \<union> {Leaf} \<union> (\<Union>l\<in>T. (\<Union>v\<in>S. (\<Union>r\<in>T. {Node l v r}))))" |
|
40 proof |
|
41 have mono: "mono (\<lambda>T. T \<union> {Leaf} \<union> (\<Union>l\<in>T. (\<Union>v\<in>S. (\<Union>r\<in>T. {Node l v r}))))" |
|
42 by (auto simp: mono_def) |
|
43 fix t assume "t \<in> trees S" then show "t \<in> lfp (\<lambda>T. T \<union> {Leaf} \<union> (\<Union>l\<in>T. (\<Union>v\<in>S. (\<Union>r\<in>T. {Node l v r}))))" |
|
44 proof induction |
|
45 case 1 then show ?case |
|
46 by (subst lfp_unfold[OF mono]) auto |
|
47 next |
|
48 case 2 then show ?case |
|
49 by (subst lfp_unfold[OF mono]) auto |
|
50 qed |
|
51 qed |
|
52 |
|
53 lemma countable_trees: "countable A \<Longrightarrow> countable (trees A)" |
|
54 apply (rule countable_subset[OF trees_sub_lfp]) |
|
55 apply (rule countable_lfp) |
|
56 subgoal by auto |
|
57 apply (intro sup_continuous_sup sup_continuous_const) |
|
58 subgoal by (simp add: sup_continuous_def) |
|
59 subgoal apply (auto simp add: sup_continuous_def) |
|
60 subgoal premises prems for M x c a y d |
|
61 using prems(3,5) prems(2)[THEN incseqD, of x "max x y"] prems(2)[THEN incseqD, of y "max x y"] |
|
62 by (intro exI[of _ "max x y"]) auto |
|
63 done |
|
64 done |
|
65 |
|
66 lemma trees_UNIV[simp]: "trees UNIV = UNIV" |
|
67 proof - |
|
68 have "t \<in> trees UNIV" for t :: "'a tree" |
|
69 by (induction t) (auto intro: trees.intros(2)) |
|
70 then show ?thesis by auto |
|
71 qed |
|
72 |
|
73 instance tree :: (countable) countable |
|
74 proof |
|
75 have "countable (UNIV :: 'a tree set)" |
|
76 by (subst trees_UNIV[symmetric]) (intro countable_trees[OF countableI_type]) |
|
77 then show "\<exists>to_nat::'a tree \<Rightarrow> nat. inj to_nat" |
|
78 by (auto simp: countable_def) |
|
79 qed |
|
80 |
|
81 lemma map_in_trees[intro]: "(\<And>x. x \<in> set_tree t \<Longrightarrow> f x \<in> S) \<Longrightarrow> map_tree f t \<in> trees S" |
|
82 by (induction t) (auto intro: trees.intros(2)) |
|
83 |
|
84 primrec trees_cyl :: "'a set tree \<Rightarrow> 'a tree set" where |
|
85 "trees_cyl Leaf = {Leaf} " |
|
86 | "trees_cyl (Node l v r) = (\<Union>l'\<in>trees_cyl l. (\<Union>v'\<in>v. (\<Union>r'\<in>trees_cyl r. {Node l' v' r'})))" |
|
87 |
|
88 definition tree_sigma :: "'a measure \<Rightarrow> 'a tree measure" |
|
89 where |
|
90 "tree_sigma M = sigma (trees (space M)) (trees_cyl ` trees (sets M))" |
|
91 |
|
92 lemma Node_in_trees_cyl: "Node l' v' r' \<in> trees_cyl t \<longleftrightarrow> |
|
93 (\<exists>l v r. t = Node l v r \<and> l' \<in> trees_cyl l \<and> r' \<in> trees_cyl r \<and> v' \<in> v)" |
|
94 by (cases t) auto |
|
95 |
|
96 lemma trees_cyl_sub_trees: |
|
97 assumes "t \<in> trees A" "A \<subseteq> Pow B" shows "trees_cyl t \<subseteq> trees B" |
|
98 using assms(1) |
|
99 proof induction |
|
100 case (2 l v r) with \<open>A \<subseteq> Pow B\<close> show ?case |
|
101 by (auto intro!: trees.intros(2)) |
|
102 qed auto |
|
103 |
|
104 lemma trees_cyl_sets_in_space: "trees_cyl ` trees (sets M) \<subseteq> Pow (trees (space M))" |
|
105 using trees_cyl_sub_trees[OF _ sets.space_closed, of _ M] by auto |
|
106 |
|
107 lemma space_tree_sigma: "space (tree_sigma M) = trees (space M)" |
|
108 unfolding tree_sigma_def by (rule space_measure_of_conv) |
|
109 |
|
110 lemma sets_tree_sigma_eq: "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))" |
|
111 unfolding tree_sigma_def by (rule sets_measure_of) (rule trees_cyl_sets_in_space) |
|
112 |
|
113 lemma Leaf_in_tree_sigma[measurable]: "{Leaf} \<in> sets (tree_sigma M)" |
|
114 unfolding sets_tree_sigma_eq |
|
115 by (rule sigma_sets.Basic) (auto intro: trees.intros(2) image_eqI[where x=Leaf]) |
|
116 |
|
117 lemma trees_cyl_map_treeI: "t \<in> trees_cyl (map_tree (\<lambda>x. A) t)" if *: "t \<in> trees A" |
|
118 using * by induction auto |
|
119 |
|
120 lemma trees_cyl_map_in_sets: |
|
121 "(\<And>x. x \<in> set_tree t \<Longrightarrow> f x \<in> sets M) \<Longrightarrow> trees_cyl (map_tree f t) \<in> sets (tree_sigma M)" |
|
122 by (subst sets_tree_sigma_eq) auto |
|
123 |
|
124 lemma Node_in_tree_sigma: |
|
125 assumes L: "X \<in> sets (M \<Otimes>\<^sub>M (tree_sigma M \<Otimes>\<^sub>M tree_sigma M))" |
|
126 shows "{Node l v r | l v r. (v, l, r) \<in> X} \<in> sets (tree_sigma M)" |
|
127 proof - |
|
128 let ?E = "\<lambda>s::unit tree. trees_cyl (map_tree (\<lambda>_. space M) s)" |
|
129 have 1: "countable (range ?E)" |
|
130 by (intro countable_image countableI_type) |
|
131 have 2: "trees_cyl ` trees (sets M) \<subseteq> Pow (space (tree_sigma M))" |
|
132 using trees_cyl_sets_in_space[of M] by (simp add: space_tree_sigma) |
|
133 have 3: "sets (tree_sigma M) = sigma_sets (space (tree_sigma M)) (trees_cyl ` trees (sets M))" |
|
134 unfolding sets_tree_sigma_eq by (simp add: space_tree_sigma) |
|
135 have 4: "(\<Union>s. ?E s) = space (tree_sigma M)" |
|
136 proof (safe; clarsimp simp: space_tree_sigma) |
|
137 fix t s assume "t \<in> trees_cyl (map_tree (\<lambda>_::unit. space M) s)" |
|
138 then show "t \<in> trees (space M)" |
|
139 by (induction s arbitrary: t) auto |
|
140 next |
|
141 fix t assume "t \<in> trees (space M)" |
|
142 then show "\<exists>t'. t \<in> ?E t'" |
|
143 by (intro exI[of _ "map_tree (\<lambda>_. ()) t"]) |
|
144 (auto simp: tree.map_comp comp_def intro: trees_cyl_map_treeI) |
|
145 qed |
|
146 have 5: "range ?E \<subseteq> trees_cyl ` trees (sets M)" by auto |
|
147 let ?P = "{A \<times> B | A B. A \<in> trees_cyl ` trees (sets M) \<and> B \<in> trees_cyl ` trees (sets M)}" |
|
148 have P: "sets (tree_sigma M \<Otimes>\<^sub>M tree_sigma M) = sets (sigma (space (tree_sigma M) \<times> space (tree_sigma M)) ?P)" |
|
149 by (rule sets_pair_eq[OF 2 3 1 5 4 2 3 1 5 4]) |
|
150 |
|
151 have "sets (M \<Otimes>\<^sub>M (tree_sigma M \<Otimes>\<^sub>M tree_sigma M)) = |
|
152 sets (sigma (space M \<times> space (tree_sigma M \<Otimes>\<^sub>M tree_sigma M)) {A \<times> BC | A BC. A \<in> sets M \<and> BC \<in> ?P})" |
|
153 proof (rule sets_pair_eq) |
|
154 show "sets M \<subseteq> Pow (space M)" "sets M = sigma_sets (space M) (sets M)" |
|
155 by (auto simp: sets.sigma_sets_eq sets.space_closed) |
|
156 show "countable {space M}" "{space M} \<subseteq> sets M" "\<Union>{space M} = space M" |
|
157 by auto |
|
158 show "?P \<subseteq> Pow (space (tree_sigma M \<Otimes>\<^sub>M tree_sigma M))" |
|
159 using trees_cyl_sets_in_space[of M] |
|
160 by (auto simp: space_pair_measure space_tree_sigma subset_eq) |
|
161 then show "sets (tree_sigma M \<Otimes>\<^sub>M tree_sigma M) = |
|
162 sigma_sets (space (tree_sigma M \<Otimes>\<^sub>M tree_sigma M)) ?P" |
|
163 by (subst P, subst sets_measure_of) (auto simp: space_tree_sigma space_pair_measure) |
|
164 show "countable ((\<lambda>(a, b). a \<times> b) ` (range ?E \<times> range ?E))" |
|
165 by (intro countable_image countable_SIGMA countableI_type) |
|
166 show "(\<lambda>(a, b). a \<times> b) ` (range ?E \<times> range ?E) \<subseteq> ?P" |
|
167 by auto |
|
168 qed (insert 4, auto simp: space_pair_measure space_tree_sigma set_eq_iff) |
|
169 also have "\<dots> = sigma_sets (space M \<times> trees (space M) \<times> trees (space M)) |
|
170 {A \<times> trees_cyl B \<times> trees_cyl C | A B C. A \<in> sets M \<and> B \<in> trees (sets M) \<and> C \<in> trees (sets M) }" |
|
171 apply (subst sets_measure_of) |
|
172 subgoal |
|
173 using sets.space_closed[of M] trees_cyl_sets_in_space[of M] |
|
174 by (clarsimp simp: space_pair_measure space_tree_sigma) blast |
|
175 apply (rule arg_cong2[where f=sigma_sets]) |
|
176 apply (auto simp: space_pair_measure space_tree_sigma) |
|
177 subgoal premises prems for A B C |
|
178 apply (rule exI conjI refl prems)+ |
|
179 using trees_cyl_sets_in_space[of M] prems |
|
180 by auto |
|
181 done |
|
182 finally have "X \<in> sigma_sets (space M \<times> trees (space M) \<times> trees (space M)) |
|
183 {A \<times> trees_cyl B \<times> trees_cyl C | A B C. A \<in> sets M \<and> B \<in> trees (sets M) \<and> C \<in> trees (sets M) }" |
|
184 using assms by auto |
|
185 then show ?thesis |
|
186 proof induction |
|
187 case (Basic A') |
|
188 then obtain A B C where "A' = A \<times> trees_cyl B \<times> trees_cyl C" |
|
189 and *: "A \<in> sets M" "B \<in> trees (sets M)" "C \<in> trees (sets M)" |
|
190 by auto |
|
191 then have "{Node l v r |l v r. (v, l, r) \<in> A'} = trees_cyl (Node B A C)" |
|
192 by auto |
|
193 then show ?case |
|
194 by (auto simp del: trees_cyl.simps simp: sets_tree_sigma_eq intro!: sigma_sets.Basic *) |
|
195 next |
|
196 case Empty show ?case by auto |
|
197 next |
|
198 case (Compl A) |
|
199 have "{Node l v r |l v r. (v, l, r) \<in> space M \<times> trees (space M) \<times> trees (space M) - A} = |
|
200 (space (tree_sigma M) - {Node l v r |l v r. (v, l, r) \<in> A}) - {Leaf}" |
|
201 apply (auto simp: space_tree_sigma) |
|
202 subgoal for t |
|
203 by (cases t) auto |
|
204 done |
|
205 also have "\<dots> \<in> sets (tree_sigma M)" |
|
206 by (intro sets.Diff Compl) auto |
|
207 finally show ?case . |
|
208 next |
|
209 case (Union I) |
|
210 have *: "{Node l v r |l v r. (v, l, r) \<in> UNION UNIV I} = |
|
211 (\<Union>i. {Node l v r |l v r. (v, l, r) \<in> I i})" by auto |
|
212 show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto |
|
213 qed |
|
214 qed |
|
215 |
|
216 lemma measurable_left[measurable]: "left \<in> tree_sigma M \<rightarrow>\<^sub>M tree_sigma M" |
|
217 proof (rule measurableI) |
|
218 show "t \<in> space (tree_sigma M) \<Longrightarrow> left t \<in> space (tree_sigma M)" for t |
|
219 by (cases t) (auto simp: space_tree_sigma) |
|
220 fix A assume A: "A \<in> sets (tree_sigma M)" |
|
221 from sets.sets_into_space[OF this] |
|
222 have *: "left -` A \<inter> space (tree_sigma M) = |
|
223 (if Leaf \<in> A then {Leaf} else {}) \<union> |
|
224 {Node a v r | a v r. (v, a, r) \<in> space M \<times> A \<times> space (tree_sigma M)}" |
|
225 by (auto simp: space_tree_sigma elim: trees.cases) |
|
226 show "left -` A \<inter> space (tree_sigma M) \<in> sets (tree_sigma M)" |
|
227 unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto |
|
228 qed |
|
229 |
|
230 lemma measurable_right[measurable]: "right \<in> tree_sigma M \<rightarrow>\<^sub>M tree_sigma M" |
|
231 proof (rule measurableI) |
|
232 show "t \<in> space (tree_sigma M) \<Longrightarrow> right t \<in> space (tree_sigma M)" for t |
|
233 by (cases t) (auto simp: space_tree_sigma) |
|
234 fix A assume A: "A \<in> sets (tree_sigma M)" |
|
235 from sets.sets_into_space[OF this] |
|
236 have *: "right -` A \<inter> space (tree_sigma M) = |
|
237 (if Leaf \<in> A then {Leaf} else {}) \<union> |
|
238 {Node l v a | l v a. (v, l, a) \<in> space M \<times> space (tree_sigma M) \<times> A}" |
|
239 by (auto simp: space_tree_sigma elim: trees.cases) |
|
240 show "right -` A \<inter> space (tree_sigma M) \<in> sets (tree_sigma M)" |
|
241 unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto |
|
242 qed |
|
243 |
|
244 lemma measurable_val': "val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M" |
|
245 proof (rule measurableI) |
|
246 show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> val t \<in> space M" for t |
|
247 by (cases t) (auto simp: space_restrict_space space_tree_sigma) |
|
248 fix A assume A: "A \<in> sets M" |
|
249 from sets.sets_into_space[OF this] |
|
250 have "val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) = |
|
251 {Node l a r | l a r. (a, l, r) \<in> A \<times> space (tree_sigma M) \<times> space (tree_sigma M)}" |
|
252 by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases) |
|
253 also have "\<dots> \<in> sets (tree_sigma M)" |
|
254 using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto |
|
255 finally show "val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in> |
|
256 sets (restrict_space (tree_sigma M) (- {Leaf}))" |
|
257 by (auto simp: sets_restrict_space_iff space_restrict_space) |
|
258 qed |
|
259 |
|
260 lemma measurable_restrict_mono: |
|
261 assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A" |
|
262 shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N" |
|
263 by (rule measurable_compose[OF measurable_restrict_space3 f]) |
|
264 (insert \<open>B \<subseteq> A\<close>, auto) |
|
265 |
|
266 (* |
|
267 lemma measurable_val[measurable (raw)]: |
|
268 assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M" |
|
269 and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf" |
|
270 shows "(\<lambda>\<omega>. val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M" |
|
271 sorry |
|
272 *) |
|
273 |
|
274 lemma measurable_rec_tree[measurable (raw)]: |
|
275 assumes t: "t \<in> B \<rightarrow>\<^sub>M tree_sigma M" |
|
276 assumes l: "l \<in> B \<rightarrow>\<^sub>M A" |
|
277 assumes n: "(\<lambda>(x, l, v, r, al, ar). n x l v r al ar) \<in> |
|
278 (B \<Otimes>\<^sub>M tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M \<Otimes>\<^sub>M A \<Otimes>\<^sub>M A) \<rightarrow>\<^sub>M A" (is "?N \<in> ?M \<rightarrow>\<^sub>M A") |
|
279 shows "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> B \<rightarrow>\<^sub>M A" |
|
280 proof (rule measurable_piecewise_restrict) |
|
281 let ?C = "\<lambda>t. \<lambda>s::unit tree. t -` trees_cyl (map_tree (\<lambda>_. space M) s)" |
|
282 show "countable (range (?C t))" by (intro countable_image countableI_type) |
|
283 show "space B \<subseteq> (\<Union>s. ?C t s)" |
|
284 proof (safe; clarsimp) |
|
285 fix x assume x: "x \<in> space B" have "t x \<in> trees (space M)" |
|
286 using t[THEN measurable_space, OF x] by (simp add: space_tree_sigma) |
|
287 then show "\<exists>xa::unit tree. t x \<in> trees_cyl (map_tree (\<lambda>_. space M) xa)" |
|
288 by (intro exI[of _ "map_tree (\<lambda>_. ()) (t x)"]) |
|
289 (simp add: tree.map_comp comp_def trees_cyl_map_treeI) |
|
290 qed |
|
291 fix \<Omega> assume "\<Omega> \<in> range (?C t)" |
|
292 then obtain s :: "unit tree" where \<Omega>: "\<Omega> = ?C t s" by auto |
|
293 then show "\<Omega> \<inter> space B \<in> sets B" |
|
294 by (safe intro!: measurable_sets[OF t] trees_cyl_map_in_sets) |
|
295 show "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> restrict_space B \<Omega> \<rightarrow>\<^sub>M A" |
|
296 unfolding \<Omega> using t |
|
297 proof (induction s arbitrary: t) |
|
298 case Leaf |
|
299 show ?case |
|
300 proof (rule measurable_cong[THEN iffD2]) |
|
301 fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t Leaf))" |
|
302 then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = l \<omega>" |
|
303 by (auto simp: space_restrict_space) |
|
304 next |
|
305 show "l \<in> restrict_space B (?C t Leaf) \<rightarrow>\<^sub>M A" |
|
306 using l by (rule measurable_restrict_space1) |
|
307 qed |
|
308 next |
|
309 case (Node ls u rs) |
|
310 let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), val (t \<omega>), right (t \<omega>), |
|
311 rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))" |
|
312 show ?case |
|
313 proof (rule measurable_cong[THEN iffD2]) |
|
314 fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t (Node ls u rs)))" |
|
315 then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = ?F \<omega>" |
|
316 by (auto simp: space_restrict_space) |
|
317 next |
|
318 show "?F \<in> (restrict_space B (?C t (Node ls u rs))) \<rightarrow>\<^sub>M A" |
|
319 apply (intro measurable_compose[OF _ n] measurable_Pair[rotated]) |
|
320 subgoal |
|
321 apply (rule measurable_restrict_mono[OF Node(2)]) |
|
322 apply (rule measurable_compose[OF Node(3) measurable_right]) |
|
323 by auto |
|
324 subgoal |
|
325 apply (rule measurable_restrict_mono[OF Node(1)]) |
|
326 apply (rule measurable_compose[OF Node(3) measurable_left]) |
|
327 by auto |
|
328 subgoal |
|
329 by (rule measurable_restrict_space1) |
|
330 (rule measurable_compose[OF Node(3) measurable_right]) |
|
331 subgoal |
|
332 apply (rule measurable_compose[OF _ measurable_val']) |
|
333 apply (rule measurable_restrict_space3[OF Node(3)]) |
|
334 by auto |
|
335 subgoal |
|
336 by (rule measurable_restrict_space1) |
|
337 (rule measurable_compose[OF Node(3) measurable_left]) |
|
338 by (rule measurable_restrict_space1) auto |
|
339 qed |
|
340 qed |
|
341 qed |
|
342 |
|
343 end |