src/HOL/Probability/Tree_Space.thy
 author haftmann Sun Nov 18 18:07:51 2018 +0000 (8 months ago) changeset 69313 b021008c5397 parent 69219 d4cec24a1d87 child 69655 2b56cbb02e8a permissions -rw-r--r--
removed legacy input syntax
```     1 (*  Title:      HOL/Probability/Tree_Space.thy
```
```     2     Author:     Johannes Hölzl, CMU *)
```
```     3
```
```     4 theory Tree_Space
```
```     5   imports "HOL-Analysis.Analysis" "HOL-Library.Tree"
```
```     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 inductive_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
```
```    29 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)"
```
```    30   by (subst trees.simps) auto
```
```    31
```
```    32 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}))))"
```
```    33 proof
```
```    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
```
```    44 qed
```
```    45
```
```    46 lemma countable_trees: "countable A \<Longrightarrow> countable (trees A)"
```
```    47 proof (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
```
```    59 qed auto
```
```    60
```
```    61 lemma trees_UNIV[simp]: "trees UNIV = UNIV"
```
```    62 proof -
```
```    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
```
```    66 qed
```
```    67
```
```    68 instance tree :: (countable) countable
```
```    69 proof
```
```    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)
```
```    74 qed
```
```    75
```
```    76 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"
```
```    77   by (induction t) (auto intro: trees.intros(2))
```
```    78
```
```    79 primrec 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
```
```    83 definition tree_sigma :: "'a measure \<Rightarrow> 'a tree measure"
```
```    84 where
```
```    85   "tree_sigma M = sigma (trees (space M)) (trees_cyl ` trees (sets M))"
```
```    86
```
```    87 lemma 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
```
```    91 lemma 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)
```
```    94 proof induction
```
```    95   case (2 l v r) with \<open>A \<subseteq> Pow B\<close> show ?case
```
```    96     by (auto intro!: trees.intros(2))
```
```    97 qed auto
```
```    98
```
```    99 lemma 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
```
```   102 lemma space_tree_sigma: "space (tree_sigma M) = trees (space M)"
```
```   103   unfolding tree_sigma_def by (rule space_measure_of_conv)
```
```   104
```
```   105 lemma 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
```
```   108 lemma Leaf_in_space_tree_sigma [measurable, simp, intro]: "Leaf \<in> space (tree_sigma M)"
```
```   109   by (auto simp: space_tree_sigma)
```
```   110
```
```   111 lemma 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
```
```   115 lemma 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
```
```   118 lemma 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
```
```   122 lemma 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)"
```
```   125 proof -
```
```   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
```
```   204 qed
```
```   205
```
```   206 lemma measurable_left[measurable]: "left \<in> tree_sigma M \<rightarrow>\<^sub>M tree_sigma M"
```
```   207 proof (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
```
```   218 qed
```
```   219
```
```   220 lemma measurable_right[measurable]: "right \<in> tree_sigma M \<rightarrow>\<^sub>M tree_sigma M"
```
```   221 proof (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
```
```   232 qed
```
```   233
```
```   234 lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M"
```
```   235 proof (rule measurableI)
```
```   236   show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val 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 "root_val -` 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 "root_val -` 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)
```
```   248 qed
```
```   249
```
```   250 lemma measurable_restrict_mono:
```
```   251   assumes f: "f \<in> restrict_space M A \<rightarrow>\<^sub>M N" and "B \<subseteq> A"
```
```   252   shows "f \<in> restrict_space M B \<rightarrow>\<^sub>M N"
```
```   253 by (rule measurable_compose[OF measurable_restrict_space3 f])
```
```   254    (insert \<open>B \<subseteq> A\<close>, auto)
```
```   255
```
```   256
```
```   257 lemma measurable_root_val[measurable (raw)]:
```
```   258   assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M"
```
```   259     and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf"
```
```   260   shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M"
```
```   261 proof -
```
```   262   from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})"
```
```   263     by (intro measurable_restrict_space2) auto
```
```   264   from this and measurable_root_val' show ?thesis by (rule measurable_compose)
```
```   265 qed
```
```   266
```
```   267
```
```   268 lemma measurable_Node [measurable]:
```
```   269   "(\<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"
```
```   270 proof (rule measurable_sigma_sets)
```
```   271   show "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))"
```
```   272     by (simp add: sets_tree_sigma_eq)
```
```   273   show "trees_cyl ` trees (sets M) \<subseteq> Pow (trees (space M))"
```
```   274     by (rule trees_cyl_sets_in_space)
```
```   275   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)"
```
```   276     by (auto simp: space_pair_measure space_tree_sigma)
```
```   277   fix A assume t: "A \<in> trees_cyl ` trees (sets M)"
```
```   278   then obtain t where t: "t \<in> trees (sets M)" "A = trees_cyl t" by auto
```
```   279   show "(\<lambda>(l, x, r). \<langle>l, x, r\<rangle>) -` A \<inter>
```
```   280          space (tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M)
```
```   281          \<in> sets (tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M)"
```
```   282   proof (cases t)
```
```   283     case Leaf
```
```   284     have "(\<lambda>(l, x, r). \<langle>l, x, r\<rangle>) -` {Leaf :: 'a tree} = {}" by auto
```
```   285     with Leaf show ?thesis using t by simp
```
```   286   next
```
```   287     case (Node l B r)
```
```   288     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) =
```
```   289              trees_cyl l \<times> B \<times> trees_cyl r"
```
```   290       using t and Node and trees_cyl_sub_trees[of _ "sets M" "space M"]
```
```   291       by (auto simp: space_pair_measure space_tree_sigma
```
```   292                dest: sets.sets_into_space[of _ M])
```
```   293     thus ?thesis using t and Node
```
```   294       by (auto intro!: pair_measureI simp: sets_tree_sigma_eq)
```
```   295   qed
```
```   296 qed
```
```   297
```
```   298 lemma measurable_Node' [measurable (raw)]:
```
```   299   assumes [measurable]: "l \<in> B \<rightarrow>\<^sub>M tree_sigma A"
```
```   300   assumes [measurable]: "x \<in> B \<rightarrow>\<^sub>M A"
```
```   301   assumes [measurable]: "r \<in> B \<rightarrow>\<^sub>M tree_sigma A"
```
```   302   shows   "(\<lambda>y. Node (l y) (x y) (r y)) \<in> B \<rightarrow>\<^sub>M tree_sigma A"
```
```   303 proof -
```
```   304   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))"
```
```   305     by (simp add: o_def)
```
```   306   also have "\<dots> \<in> B \<rightarrow>\<^sub>M tree_sigma A"
```
```   307     by (intro measurable_comp[OF _ measurable_Node]) simp_all
```
```   308   finally show ?thesis .
```
```   309 qed
```
```   310
```
```   311 lemma measurable_rec_tree[measurable (raw)]:
```
```   312   assumes t: "t \<in> B \<rightarrow>\<^sub>M tree_sigma M"
```
```   313   assumes l: "l \<in> B \<rightarrow>\<^sub>M A"
```
```   314   assumes n: "(\<lambda>(x, l, v, r, al, ar). n x l v r al ar) \<in>
```
```   315     (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")
```
```   316   shows "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> B \<rightarrow>\<^sub>M A"
```
```   317 proof (rule measurable_piecewise_restrict)
```
```   318   let ?C = "\<lambda>t. \<lambda>s::unit tree. t -` trees_cyl (map_tree (\<lambda>_. space M) s)"
```
```   319   show "countable (range (?C t))" by (intro countable_image countableI_type)
```
```   320   show "space B \<subseteq> (\<Union>s. ?C t s)"
```
```   321   proof (safe; clarsimp)
```
```   322     fix x assume x: "x \<in> space B" have "t x \<in> trees (space M)"
```
```   323       using t[THEN measurable_space, OF x] by (simp add: space_tree_sigma)
```
```   324     then show "\<exists>xa::unit tree. t x \<in> trees_cyl (map_tree (\<lambda>_. space M) xa)"
```
```   325       by (intro exI[of _ "map_tree (\<lambda>_. ()) (t x)"])
```
```   326          (simp add: tree.map_comp comp_def trees_cyl_map_treeI)
```
```   327   qed
```
```   328   fix \<Omega> assume "\<Omega> \<in> range (?C t)"
```
```   329   then obtain s :: "unit tree" where \<Omega>: "\<Omega> = ?C t s" by auto
```
```   330   then show "\<Omega> \<inter> space B \<in> sets B"
```
```   331     by (safe intro!: measurable_sets[OF t] trees_cyl_map_in_sets)
```
```   332   show "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> restrict_space B \<Omega> \<rightarrow>\<^sub>M A"
```
```   333     unfolding \<Omega> using t
```
```   334   proof (induction s arbitrary: t)
```
```   335     case Leaf
```
```   336     show ?case
```
```   337     proof (rule measurable_cong[THEN iffD2])
```
```   338       fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t Leaf))"
```
```   339       then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = l \<omega>"
```
```   340         by (auto simp: space_restrict_space)
```
```   341     next
```
```   342       show "l \<in> restrict_space B (?C t Leaf) \<rightarrow>\<^sub>M A"
```
```   343         using l by (rule measurable_restrict_space1)
```
```   344     qed
```
```   345   next
```
```   346     case (Node ls u rs)
```
```   347     let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>),
```
```   348         rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))"
```
```   349     show ?case
```
```   350     proof (rule measurable_cong[THEN iffD2])
```
```   351       fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t (Node ls u rs)))"
```
```   352       then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = ?F \<omega>"
```
```   353         by (auto simp: space_restrict_space)
```
```   354     next
```
```   355       show "?F \<in> (restrict_space B (?C t (Node ls u rs))) \<rightarrow>\<^sub>M A"
```
```   356         apply (intro measurable_compose[OF _ n] measurable_Pair[rotated])
```
```   357         subgoal
```
```   358           apply (rule measurable_restrict_mono[OF Node(2)])
```
```   359           apply (rule measurable_compose[OF Node(3) measurable_right])
```
```   360           by auto
```
```   361         subgoal
```
```   362           apply (rule measurable_restrict_mono[OF Node(1)])
```
```   363           apply (rule measurable_compose[OF Node(3) measurable_left])
```
```   364           by auto
```
```   365         subgoal
```
```   366           by (rule measurable_restrict_space1)
```
```   367              (rule measurable_compose[OF Node(3) measurable_right])
```
```   368         subgoal
```
```   369           apply (rule measurable_compose[OF _ measurable_root_val'])
```
```   370           apply (rule measurable_restrict_space3[OF Node(3)])
```
```   371           by auto
```
```   372         subgoal
```
```   373           by (rule measurable_restrict_space1)
```
```   374              (rule measurable_compose[OF Node(3) measurable_left])
```
```   375         by (rule measurable_restrict_space1) auto
```
```   376     qed
```
```   377   qed
```
```   378 qed
```
```   379
```
```   380 lemma measurable_case_tree [measurable (raw)]:
```
```   381   assumes "t \<in> B \<rightarrow>\<^sub>M tree_sigma M"
```
```   382   assumes "l \<in> B \<rightarrow>\<^sub>M A"
```
```   383   assumes "(\<lambda>(x, l, v, r). n x l v r)
```
```   384              \<in> B \<Otimes>\<^sub>M tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M \<rightarrow>\<^sub>M A"
```
```   385   shows   "(\<lambda>x. case_tree (l x) (n x) (t x)) \<in> B \<rightarrow>\<^sub>M (A :: 'a measure)"
```
```   386 proof -
```
```   387   define n' where "n' = (\<lambda>x l v r (_::'a) (_::'a). n x l v r)"
```
```   388   have "(\<lambda>x. case_tree (l x) (n x) (t x)) = (\<lambda>x. rec_tree (l x) (n' x) (t x))"
```
```   389     (is "_ = (\<lambda>x. rec_tree _ (?n' x) _)") by (rule ext) (auto split: tree.splits simp: n'_def)
```
```   390   also have "\<dots> \<in> B \<rightarrow>\<^sub>M A"
```
```   391   proof (rule measurable_rec_tree)
```
```   392     have "(\<lambda>(x, l, v, r, al, ar). n' x l v r al ar) =
```
```   393             (\<lambda>(x,l,v,r). n x l v r) \<circ> (\<lambda>(x,l,v,r,al,ar). (x,l,v,r))"
```
```   394       by (simp add: n'_def o_def case_prod_unfold)
```
```   395     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"
```
```   396       using assms(3) by measurable
```
```   397     finally show "(\<lambda>(x, l, v, r, al, ar). n' x l v r al ar) \<in> \<dots>" .
```
```   398   qed (insert assms, simp_all)
```
```   399   finally show ?thesis .
```
```   400 qed
```
```   401
```
```   402 hide_const (open) left
```
```   403 hide_const (open) right
```
```   404
```
```   405 end
```