author | wenzelm |
Thu, 14 Jun 2018 17:50:23 +0200 | |
changeset 68449 | 6d0f1a5a16ea |
parent 66453 | cc19f7ca2ed6 |
child 69218 | 59aefb3b9e95 |
permissions | -rw-r--r-- |
66026 | 1 |
(* Title: HOL/Probability/Tree_Space.thy |
2 |
Author: Johannes Hölzl, CMU *) |
|
3 |
||
4 |
theory Tree_Space |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
66059
diff
changeset
|
5 |
imports "HOL-Analysis.Analysis" "HOL-Library.Tree" |
66026 | 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 |
||
66049
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
25 |
primrec left :: "'a tree \<Rightarrow> 'a tree" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
26 |
where |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
27 |
"left (Node l v r) = l" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
28 |
| "left Leaf = Leaf" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
29 |
|
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
30 |
primrec right :: "'a tree \<Rightarrow> 'a tree" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
31 |
where |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
32 |
"right (Node l v r) = r" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
33 |
| "right Leaf = Leaf" |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
34 |
|
66026 | 35 |
inductive_set trees :: "'a set \<Rightarrow> 'a tree set" for S :: "'a set" where |
36 |
[intro!]: "Leaf \<in> trees S" |
|
37 |
| "l \<in> trees S \<Longrightarrow> r \<in> trees S \<Longrightarrow> v \<in> S \<Longrightarrow> Node l v r \<in> trees S" |
|
38 |
||
39 |
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)" |
|
40 |
by (subst trees.simps) auto |
|
41 |
||
42 |
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}))))" |
|
43 |
proof |
|
44 |
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}))))" |
|
45 |
by (auto simp: mono_def) |
|
46 |
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}))))" |
|
47 |
proof induction |
|
48 |
case 1 then show ?case |
|
49 |
by (subst lfp_unfold[OF mono]) auto |
|
50 |
next |
|
51 |
case 2 then show ?case |
|
52 |
by (subst lfp_unfold[OF mono]) auto |
|
53 |
qed |
|
54 |
qed |
|
55 |
||
56 |
lemma countable_trees: "countable A \<Longrightarrow> countable (trees A)" |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
57 |
proof (intro countable_subset[OF trees_sub_lfp] countable_lfp |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
58 |
sup_continuous_sup sup_continuous_const sup_continuous_id) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
59 |
show "sup_continuous (\<lambda>T. (\<Union>l\<in>T. \<Union>v\<in>A. \<Union>r\<in>T. {\<langle>l, v, r\<rangle>}))" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
60 |
unfolding sup_continuous_def |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
61 |
proof (intro allI impI equalityI subsetI, goal_cases) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
62 |
case (1 M t) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
63 |
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" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
64 |
by auto |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
65 |
hence "l \<in> M (max i j)" "r \<in> M (max i j)" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
66 |
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 |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
67 |
with \<open>t = Node l x r\<close> and \<open>x \<in> A\<close> show ?case by auto |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
68 |
qed auto |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
69 |
qed auto |
66026 | 70 |
|
71 |
lemma trees_UNIV[simp]: "trees UNIV = UNIV" |
|
72 |
proof - |
|
73 |
have "t \<in> trees UNIV" for t :: "'a tree" |
|
74 |
by (induction t) (auto intro: trees.intros(2)) |
|
75 |
then show ?thesis by auto |
|
76 |
qed |
|
77 |
||
78 |
instance tree :: (countable) countable |
|
79 |
proof |
|
80 |
have "countable (UNIV :: 'a tree set)" |
|
81 |
by (subst trees_UNIV[symmetric]) (intro countable_trees[OF countableI_type]) |
|
82 |
then show "\<exists>to_nat::'a tree \<Rightarrow> nat. inj to_nat" |
|
83 |
by (auto simp: countable_def) |
|
84 |
qed |
|
85 |
||
86 |
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" |
|
87 |
by (induction t) (auto intro: trees.intros(2)) |
|
88 |
||
89 |
primrec trees_cyl :: "'a set tree \<Rightarrow> 'a tree set" where |
|
90 |
"trees_cyl Leaf = {Leaf} " |
|
91 |
| "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'})))" |
|
92 |
||
93 |
definition tree_sigma :: "'a measure \<Rightarrow> 'a tree measure" |
|
94 |
where |
|
95 |
"tree_sigma M = sigma (trees (space M)) (trees_cyl ` trees (sets M))" |
|
96 |
||
97 |
lemma Node_in_trees_cyl: "Node l' v' r' \<in> trees_cyl t \<longleftrightarrow> |
|
98 |
(\<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)" |
|
99 |
by (cases t) auto |
|
100 |
||
101 |
lemma trees_cyl_sub_trees: |
|
102 |
assumes "t \<in> trees A" "A \<subseteq> Pow B" shows "trees_cyl t \<subseteq> trees B" |
|
103 |
using assms(1) |
|
104 |
proof induction |
|
105 |
case (2 l v r) with \<open>A \<subseteq> Pow B\<close> show ?case |
|
106 |
by (auto intro!: trees.intros(2)) |
|
107 |
qed auto |
|
108 |
||
109 |
lemma trees_cyl_sets_in_space: "trees_cyl ` trees (sets M) \<subseteq> Pow (trees (space M))" |
|
110 |
using trees_cyl_sub_trees[OF _ sets.space_closed, of _ M] by auto |
|
111 |
||
112 |
lemma space_tree_sigma: "space (tree_sigma M) = trees (space M)" |
|
113 |
unfolding tree_sigma_def by (rule space_measure_of_conv) |
|
114 |
||
115 |
lemma sets_tree_sigma_eq: "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))" |
|
116 |
unfolding tree_sigma_def by (rule sets_measure_of) (rule trees_cyl_sets_in_space) |
|
117 |
||
66059
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
118 |
lemma Leaf_in_space_tree_sigma [measurable, simp, intro]: "Leaf \<in> space (tree_sigma M)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
119 |
by (auto simp: space_tree_sigma) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
120 |
|
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
121 |
lemma Leaf_in_tree_sigma [measurable, simp, intro]: "{Leaf} \<in> sets (tree_sigma M)" |
66026 | 122 |
unfolding sets_tree_sigma_eq |
123 |
by (rule sigma_sets.Basic) (auto intro: trees.intros(2) image_eqI[where x=Leaf]) |
|
124 |
||
125 |
lemma trees_cyl_map_treeI: "t \<in> trees_cyl (map_tree (\<lambda>x. A) t)" if *: "t \<in> trees A" |
|
126 |
using * by induction auto |
|
127 |
||
128 |
lemma trees_cyl_map_in_sets: |
|
129 |
"(\<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)" |
|
130 |
by (subst sets_tree_sigma_eq) auto |
|
131 |
||
132 |
lemma Node_in_tree_sigma: |
|
133 |
assumes L: "X \<in> sets (M \<Otimes>\<^sub>M (tree_sigma M \<Otimes>\<^sub>M tree_sigma M))" |
|
134 |
shows "{Node l v r | l v r. (v, l, r) \<in> X} \<in> sets (tree_sigma M)" |
|
135 |
proof - |
|
136 |
let ?E = "\<lambda>s::unit tree. trees_cyl (map_tree (\<lambda>_. space M) s)" |
|
137 |
have 1: "countable (range ?E)" |
|
138 |
by (intro countable_image countableI_type) |
|
139 |
have 2: "trees_cyl ` trees (sets M) \<subseteq> Pow (space (tree_sigma M))" |
|
140 |
using trees_cyl_sets_in_space[of M] by (simp add: space_tree_sigma) |
|
141 |
have 3: "sets (tree_sigma M) = sigma_sets (space (tree_sigma M)) (trees_cyl ` trees (sets M))" |
|
142 |
unfolding sets_tree_sigma_eq by (simp add: space_tree_sigma) |
|
143 |
have 4: "(\<Union>s. ?E s) = space (tree_sigma M)" |
|
144 |
proof (safe; clarsimp simp: space_tree_sigma) |
|
145 |
fix t s assume "t \<in> trees_cyl (map_tree (\<lambda>_::unit. space M) s)" |
|
146 |
then show "t \<in> trees (space M)" |
|
147 |
by (induction s arbitrary: t) auto |
|
148 |
next |
|
149 |
fix t assume "t \<in> trees (space M)" |
|
150 |
then show "\<exists>t'. t \<in> ?E t'" |
|
151 |
by (intro exI[of _ "map_tree (\<lambda>_. ()) t"]) |
|
152 |
(auto simp: tree.map_comp comp_def intro: trees_cyl_map_treeI) |
|
153 |
qed |
|
154 |
have 5: "range ?E \<subseteq> trees_cyl ` trees (sets M)" by auto |
|
155 |
let ?P = "{A \<times> B | A B. A \<in> trees_cyl ` trees (sets M) \<and> B \<in> trees_cyl ` trees (sets M)}" |
|
156 |
have P: "sets (tree_sigma M \<Otimes>\<^sub>M tree_sigma M) = sets (sigma (space (tree_sigma M) \<times> space (tree_sigma M)) ?P)" |
|
157 |
by (rule sets_pair_eq[OF 2 3 1 5 4 2 3 1 5 4]) |
|
158 |
||
159 |
have "sets (M \<Otimes>\<^sub>M (tree_sigma M \<Otimes>\<^sub>M tree_sigma M)) = |
|
160 |
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})" |
|
161 |
proof (rule sets_pair_eq) |
|
162 |
show "sets M \<subseteq> Pow (space M)" "sets M = sigma_sets (space M) (sets M)" |
|
163 |
by (auto simp: sets.sigma_sets_eq sets.space_closed) |
|
164 |
show "countable {space M}" "{space M} \<subseteq> sets M" "\<Union>{space M} = space M" |
|
165 |
by auto |
|
166 |
show "?P \<subseteq> Pow (space (tree_sigma M \<Otimes>\<^sub>M tree_sigma M))" |
|
167 |
using trees_cyl_sets_in_space[of M] |
|
168 |
by (auto simp: space_pair_measure space_tree_sigma subset_eq) |
|
169 |
then show "sets (tree_sigma M \<Otimes>\<^sub>M tree_sigma M) = |
|
170 |
sigma_sets (space (tree_sigma M \<Otimes>\<^sub>M tree_sigma M)) ?P" |
|
171 |
by (subst P, subst sets_measure_of) (auto simp: space_tree_sigma space_pair_measure) |
|
172 |
show "countable ((\<lambda>(a, b). a \<times> b) ` (range ?E \<times> range ?E))" |
|
173 |
by (intro countable_image countable_SIGMA countableI_type) |
|
174 |
show "(\<lambda>(a, b). a \<times> b) ` (range ?E \<times> range ?E) \<subseteq> ?P" |
|
175 |
by auto |
|
176 |
qed (insert 4, auto simp: space_pair_measure space_tree_sigma set_eq_iff) |
|
177 |
also have "\<dots> = sigma_sets (space M \<times> trees (space M) \<times> trees (space M)) |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
178 |
{A \<times> BC |A BC. A \<in> sets M \<and> BC \<in> {A \<times> B |A B. |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
179 |
A \<in> trees_cyl ` trees (sets M) \<and> B \<in> trees_cyl ` trees (sets M)}}" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
180 |
(is "_ = sigma_sets ?X ?Y") using sets.space_closed[of M] trees_cyl_sub_trees[of _ "sets M" "space M"] |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
181 |
by (subst sets_measure_of) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
182 |
(auto simp: space_pair_measure space_tree_sigma) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
183 |
also have "?Y = {A \<times> trees_cyl B \<times> trees_cyl C | A B C. A \<in> sets M \<and> |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
184 |
B \<in> trees (sets M) \<and> C \<in> trees (sets M)}" by blast |
66026 | 185 |
finally have "X \<in> sigma_sets (space M \<times> trees (space M) \<times> trees (space M)) |
186 |
{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) }" |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
187 |
using assms by blast |
66026 | 188 |
then show ?thesis |
189 |
proof induction |
|
190 |
case (Basic A') |
|
191 |
then obtain A B C where "A' = A \<times> trees_cyl B \<times> trees_cyl C" |
|
192 |
and *: "A \<in> sets M" "B \<in> trees (sets M)" "C \<in> trees (sets M)" |
|
193 |
by auto |
|
194 |
then have "{Node l v r |l v r. (v, l, r) \<in> A'} = trees_cyl (Node B A C)" |
|
195 |
by auto |
|
196 |
then show ?case |
|
197 |
by (auto simp del: trees_cyl.simps simp: sets_tree_sigma_eq intro!: sigma_sets.Basic *) |
|
198 |
next |
|
199 |
case Empty show ?case by auto |
|
200 |
next |
|
201 |
case (Compl A) |
|
202 |
have "{Node l v r |l v r. (v, l, r) \<in> space M \<times> trees (space M) \<times> trees (space M) - A} = |
|
203 |
(space (tree_sigma M) - {Node l v r |l v r. (v, l, r) \<in> A}) - {Leaf}" |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
204 |
by (auto simp: space_tree_sigma elim: trees.cases) |
66026 | 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 |
||
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
244 |
lemma measurable_root_val': "root_val \<in> restrict_space (tree_sigma M) (-{Leaf}) \<rightarrow>\<^sub>M M" |
66026 | 245 |
proof (rule measurableI) |
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
246 |
show "t \<in> space (restrict_space (tree_sigma M) (- {Leaf})) \<Longrightarrow> root_val t \<in> space M" for t |
66026 | 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] |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
250 |
have "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) = |
66026 | 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 |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
255 |
finally show "root_val -` A \<inter> space (restrict_space (tree_sigma M) (- {Leaf})) \<in> |
66026 | 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 |
||
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
266 |
|
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
267 |
lemma measurable_root_val[measurable (raw)]: |
66026 | 268 |
assumes "f \<in> X \<rightarrow>\<^sub>M tree_sigma M" |
269 |
and "\<And>x. x \<in> space X \<Longrightarrow> f x \<noteq> Leaf" |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
270 |
shows "(\<lambda>\<omega>. root_val (f \<omega>)) \<in> X \<rightarrow>\<^sub>M M" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
271 |
proof - |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
272 |
from assms have "f \<in> X \<rightarrow>\<^sub>M restrict_space (tree_sigma M) (- {Leaf})" |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
273 |
by (intro measurable_restrict_space2) auto |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
274 |
from this and measurable_root_val' show ?thesis by (rule measurable_compose) |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
275 |
qed |
66026 | 276 |
|
66059
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
277 |
|
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
278 |
lemma measurable_Node [measurable]: |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
279 |
"(\<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" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
280 |
proof (rule measurable_sigma_sets) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
281 |
show "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
282 |
by (simp add: sets_tree_sigma_eq) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
283 |
show "trees_cyl ` trees (sets M) \<subseteq> Pow (trees (space M))" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
284 |
by (rule trees_cyl_sets_in_space) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
285 |
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)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
286 |
by (auto simp: space_pair_measure space_tree_sigma) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
287 |
fix A assume t: "A \<in> trees_cyl ` trees (sets M)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
288 |
then obtain t where t: "t \<in> trees (sets M)" "A = trees_cyl t" by auto |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
289 |
show "(\<lambda>(l, x, r). \<langle>l, x, r\<rangle>) -` A \<inter> |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
290 |
space (tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
291 |
\<in> sets (tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
292 |
proof (cases t) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
293 |
case Leaf |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
294 |
have "(\<lambda>(l, x, r). \<langle>l, x, r\<rangle>) -` {Leaf :: 'a tree} = {}" by auto |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
295 |
with Leaf show ?thesis using t by simp |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
296 |
next |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
297 |
case (Node l B r) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
298 |
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) = |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
299 |
trees_cyl l \<times> B \<times> trees_cyl r" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
300 |
using t and Node and trees_cyl_sub_trees[of _ "sets M" "space M"] |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
301 |
by (auto simp: space_pair_measure space_tree_sigma |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
302 |
dest: sets.sets_into_space[of _ M]) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
303 |
thus ?thesis using t and Node |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
304 |
by (auto intro!: pair_measureI simp: sets_tree_sigma_eq) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
305 |
qed |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
306 |
qed |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
307 |
|
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
308 |
lemma measurable_Node' [measurable (raw)]: |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
309 |
assumes [measurable]: "l \<in> B \<rightarrow>\<^sub>M tree_sigma A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
310 |
assumes [measurable]: "x \<in> B \<rightarrow>\<^sub>M A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
311 |
assumes [measurable]: "r \<in> B \<rightarrow>\<^sub>M tree_sigma A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
312 |
shows "(\<lambda>y. Node (l y) (x y) (r y)) \<in> B \<rightarrow>\<^sub>M tree_sigma A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
313 |
proof - |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
314 |
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))" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
315 |
by (simp add: o_def) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
316 |
also have "\<dots> \<in> B \<rightarrow>\<^sub>M tree_sigma A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
317 |
by (intro measurable_comp[OF _ measurable_Node]) simp_all |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
318 |
finally show ?thesis . |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
319 |
qed |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
320 |
|
66026 | 321 |
lemma measurable_rec_tree[measurable (raw)]: |
322 |
assumes t: "t \<in> B \<rightarrow>\<^sub>M tree_sigma M" |
|
323 |
assumes l: "l \<in> B \<rightarrow>\<^sub>M A" |
|
324 |
assumes n: "(\<lambda>(x, l, v, r, al, ar). n x l v r al ar) \<in> |
|
325 |
(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") |
|
326 |
shows "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> B \<rightarrow>\<^sub>M A" |
|
327 |
proof (rule measurable_piecewise_restrict) |
|
328 |
let ?C = "\<lambda>t. \<lambda>s::unit tree. t -` trees_cyl (map_tree (\<lambda>_. space M) s)" |
|
329 |
show "countable (range (?C t))" by (intro countable_image countableI_type) |
|
330 |
show "space B \<subseteq> (\<Union>s. ?C t s)" |
|
331 |
proof (safe; clarsimp) |
|
332 |
fix x assume x: "x \<in> space B" have "t x \<in> trees (space M)" |
|
333 |
using t[THEN measurable_space, OF x] by (simp add: space_tree_sigma) |
|
334 |
then show "\<exists>xa::unit tree. t x \<in> trees_cyl (map_tree (\<lambda>_. space M) xa)" |
|
335 |
by (intro exI[of _ "map_tree (\<lambda>_. ()) (t x)"]) |
|
336 |
(simp add: tree.map_comp comp_def trees_cyl_map_treeI) |
|
337 |
qed |
|
338 |
fix \<Omega> assume "\<Omega> \<in> range (?C t)" |
|
339 |
then obtain s :: "unit tree" where \<Omega>: "\<Omega> = ?C t s" by auto |
|
340 |
then show "\<Omega> \<inter> space B \<in> sets B" |
|
341 |
by (safe intro!: measurable_sets[OF t] trees_cyl_map_in_sets) |
|
342 |
show "(\<lambda>x. rec_tree (l x) (n x) (t x)) \<in> restrict_space B \<Omega> \<rightarrow>\<^sub>M A" |
|
343 |
unfolding \<Omega> using t |
|
344 |
proof (induction s arbitrary: t) |
|
345 |
case Leaf |
|
346 |
show ?case |
|
347 |
proof (rule measurable_cong[THEN iffD2]) |
|
348 |
fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t Leaf))" |
|
349 |
then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = l \<omega>" |
|
350 |
by (auto simp: space_restrict_space) |
|
351 |
next |
|
352 |
show "l \<in> restrict_space B (?C t Leaf) \<rightarrow>\<^sub>M A" |
|
353 |
using l by (rule measurable_restrict_space1) |
|
354 |
qed |
|
355 |
next |
|
356 |
case (Node ls u rs) |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
357 |
let ?F = "\<lambda>\<omega>. ?N (\<omega>, left (t \<omega>), root_val (t \<omega>), right (t \<omega>), |
66026 | 358 |
rec_tree (l \<omega>) (n \<omega>) (left (t \<omega>)), rec_tree (l \<omega>) (n \<omega>) (right (t \<omega>)))" |
359 |
show ?case |
|
360 |
proof (rule measurable_cong[THEN iffD2]) |
|
361 |
fix \<omega> assume "\<omega> \<in> space (restrict_space B (?C t (Node ls u rs)))" |
|
362 |
then show "rec_tree (l \<omega>) (n \<omega>) (t \<omega>) = ?F \<omega>" |
|
363 |
by (auto simp: space_restrict_space) |
|
364 |
next |
|
365 |
show "?F \<in> (restrict_space B (?C t (Node ls u rs))) \<rightarrow>\<^sub>M A" |
|
366 |
apply (intro measurable_compose[OF _ n] measurable_Pair[rotated]) |
|
367 |
subgoal |
|
368 |
apply (rule measurable_restrict_mono[OF Node(2)]) |
|
369 |
apply (rule measurable_compose[OF Node(3) measurable_right]) |
|
370 |
by auto |
|
371 |
subgoal |
|
372 |
apply (rule measurable_restrict_mono[OF Node(1)]) |
|
373 |
apply (rule measurable_compose[OF Node(3) measurable_left]) |
|
374 |
by auto |
|
375 |
subgoal |
|
376 |
by (rule measurable_restrict_space1) |
|
377 |
(rule measurable_compose[OF Node(3) measurable_right]) |
|
378 |
subgoal |
|
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
379 |
apply (rule measurable_compose[OF _ measurable_root_val']) |
66026 | 380 |
apply (rule measurable_restrict_space3[OF Node(3)]) |
381 |
by auto |
|
382 |
subgoal |
|
383 |
by (rule measurable_restrict_space1) |
|
384 |
(rule measurable_compose[OF Node(3) measurable_left]) |
|
385 |
by (rule measurable_restrict_space1) auto |
|
386 |
qed |
|
387 |
qed |
|
388 |
qed |
|
389 |
||
66059
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
390 |
lemma measurable_case_tree [measurable (raw)]: |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
391 |
assumes "t \<in> B \<rightarrow>\<^sub>M tree_sigma M" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
392 |
assumes "l \<in> B \<rightarrow>\<^sub>M A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
393 |
assumes "(\<lambda>(x, l, v, r). n x l v r) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
394 |
\<in> B \<Otimes>\<^sub>M tree_sigma M \<Otimes>\<^sub>M M \<Otimes>\<^sub>M tree_sigma M \<rightarrow>\<^sub>M A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
395 |
shows "(\<lambda>x. case_tree (l x) (n x) (t x)) \<in> B \<rightarrow>\<^sub>M (A :: 'a measure)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
396 |
proof - |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
397 |
define n' where "n' = (\<lambda>x l v r (_::'a) (_::'a). n x l v r)" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
398 |
have "(\<lambda>x. case_tree (l x) (n x) (t x)) = (\<lambda>x. rec_tree (l x) (n' x) (t x))" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
399 |
(is "_ = (\<lambda>x. rec_tree _ (?n' x) _)") by (rule ext) (auto split: tree.splits simp: n'_def) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
400 |
also have "\<dots> \<in> B \<rightarrow>\<^sub>M A" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
401 |
proof (rule measurable_rec_tree) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
402 |
have "(\<lambda>(x, l, v, r, al, ar). n' x l v r al ar) = |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
403 |
(\<lambda>(x,l,v,r). n x l v r) \<circ> (\<lambda>(x,l,v,r,al,ar). (x,l,v,r))" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
404 |
by (simp add: n'_def o_def case_prod_unfold) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
405 |
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" |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
406 |
using assms(3) by measurable |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
407 |
finally show "(\<lambda>(x, l, v, r, al, ar). n' x l v r al ar) \<in> \<dots>" . |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
408 |
qed (insert assms, simp_all) |
5a6b67e42c4a
More rules for Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66050
diff
changeset
|
409 |
finally show ?thesis . |
66050
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
410 |
qed |
3804a9640088
Cleaned up and extended Probability/Tree_Space
eberlm <eberlm@in.tum.de>
parents:
66049
diff
changeset
|
411 |
|
66049
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
412 |
hide_const (open) left |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
413 |
hide_const (open) right |
d20d5a3bf6cf
HOL-Probability: use tree datastructure from Libary/Tree; hide left/right/var projections
hoelzl
parents:
66026
diff
changeset
|
414 |
|
66026 | 415 |
end |