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