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