(* Title: HOL/Probability/Tree_Space.thy
Author: Johannes Hölzl, CMU *)
theory Tree_Space
imports "HOL-Analysis.Analysis" "HOL-Library.Tree"
begin
lemma countable_lfp:
assumes step: "\Y. countable Y \ countable (F Y)"
and cont: "Order_Continuity.sup_continuous F"
shows "countable (lfp F)"
by(subst sup_continuous_lfp[OF cont])(simp add: countable_funpow[OF step])
lemma countable_lfp_apply:
assumes step: "\Y x. (\x. countable (Y x)) \ countable (F Y x)"
and cont: "Order_Continuity.sup_continuous F"
shows "countable (lfp F x)"
proof -
{ fix n
have "\x. countable ((F ^^ n) bot x)"
by(induct n)(auto intro: step) }
thus ?thesis using cont by(simp add: sup_continuous_lfp)
qed
inductive_set trees :: "'a set \ 'a tree set" for S :: "'a set" where
[intro!]: "Leaf \ trees S"
| "l \ trees S \ r \ trees S \ v \ S \ Node l v r \ trees S"
lemma Node_in_trees_iff[simp]: "Node l v r \ trees S \ (l \ trees S \ v \ S \ r \ trees S)"
by (subst trees.simps) auto
lemma trees_sub_lfp: "trees S \ lfp (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))"
proof
have mono: "mono (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))"
by (auto simp: mono_def)
fix t assume "t \ trees S" then show "t \ lfp (\T. T \ {Leaf} \ (\l\T. (\v\S. (\r\T. {Node l v r}))))"
proof induction
case 1 then show ?case
by (subst lfp_unfold[OF mono]) auto
next
case 2 then show ?case
by (subst lfp_unfold[OF mono]) auto
qed
qed
lemma countable_trees: "countable A \ countable (trees A)"
proof (intro countable_subset[OF trees_sub_lfp] countable_lfp
sup_continuous_sup sup_continuous_const sup_continuous_id)
show "sup_continuous (\T. (\l\T. \v\A. \r\T. {\l, v, r\}))"
unfolding sup_continuous_def
proof (intro allI impI equalityI subsetI, goal_cases)
case (1 M t)
then obtain i j :: nat and l x r where "t = Node l x r" "x \ A" "l \ M i" "r \ M j"
by auto
hence "l \ M (max i j)" "r \ M (max i j)"
using incseqD[OF \incseq M\, of i "max i j"] incseqD[OF \incseq M\, of j "max i j"] by auto
with \t = Node l x r\ and \x \ A\ show ?case by auto
qed auto
qed auto
lemma trees_UNIV[simp]: "trees UNIV = UNIV"
proof -
have "t \ trees UNIV" for t :: "'a tree"
by (induction t) (auto intro: trees.intros(2))
then show ?thesis by auto
qed
instance tree :: (countable) countable
proof
have "countable (UNIV :: 'a tree set)"
by (subst trees_UNIV[symmetric]) (intro countable_trees[OF countableI_type])
then show "\to_nat::'a tree \ nat. inj to_nat"
by (auto simp: countable_def)
qed
lemma map_in_trees[intro]: "(\x. x \ set_tree t \ f x \ S) \ map_tree f t \ trees S"
by (induction t) (auto intro: trees.intros(2))
primrec trees_cyl :: "'a set tree \ 'a tree set" where
"trees_cyl Leaf = {Leaf} "
| "trees_cyl (Node l v r) = (\l'\trees_cyl l. (\v'\v. (\r'\trees_cyl r. {Node l' v' r'})))"
definition tree_sigma :: "'a measure \ 'a tree measure"
where
"tree_sigma M = sigma (trees (space M)) (trees_cyl ` trees (sets M))"
lemma Node_in_trees_cyl: "Node l' v' r' \ trees_cyl t \
(\l v r. t = Node l v r \ l' \ trees_cyl l \ r' \ trees_cyl r \ v' \ v)"
by (cases t) auto
lemma trees_cyl_sub_trees:
assumes "t \ trees A" "A \ Pow B" shows "trees_cyl t \ trees B"
using assms(1)
proof induction
case (2 l v r) with \A \ Pow B\ show ?case
by (auto intro!: trees.intros(2))
qed auto
lemma trees_cyl_sets_in_space: "trees_cyl ` trees (sets M) \ Pow (trees (space M))"
using trees_cyl_sub_trees[OF _ sets.space_closed, of _ M] by auto
lemma space_tree_sigma: "space (tree_sigma M) = trees (space M)"
unfolding tree_sigma_def by (rule space_measure_of_conv)
lemma sets_tree_sigma_eq: "sets (tree_sigma M) = sigma_sets (trees (space M)) (trees_cyl ` trees (sets M))"
unfolding tree_sigma_def by (rule sets_measure_of) (rule trees_cyl_sets_in_space)
lemma Leaf_in_space_tree_sigma [measurable, simp, intro]: "Leaf \ space (tree_sigma M)"
by (auto simp: space_tree_sigma)
lemma Leaf_in_tree_sigma [measurable, simp, intro]: "{Leaf} \ sets (tree_sigma M)"
unfolding sets_tree_sigma_eq
by (rule sigma_sets.Basic) (auto intro: trees.intros(2) image_eqI[where x=Leaf])
lemma trees_cyl_map_treeI: "t \ trees_cyl (map_tree (\x. A) t)" if *: "t \ trees A"
using * by induction auto
lemma trees_cyl_map_in_sets:
"(\x. x \ set_tree t \ f x \ sets M) \ trees_cyl (map_tree f t) \ sets (tree_sigma M)"
by (subst sets_tree_sigma_eq) auto
lemma Node_in_tree_sigma:
assumes L: "X \ sets (M \\<^sub>M (tree_sigma M \\<^sub>M tree_sigma M))"
shows "{Node l v r | l v r. (v, l, r) \ X} \ sets (tree_sigma M)"
proof -
let ?E = "\s::unit tree. trees_cyl (map_tree (\_. space M) s)"
have 1: "countable (range ?E)"
by (intro countable_image countableI_type)
have 2: "trees_cyl ` trees (sets M) \ Pow (space (tree_sigma M))"
using trees_cyl_sets_in_space[of M] by (simp add: space_tree_sigma)
have 3: "sets (tree_sigma M) = sigma_sets (space (tree_sigma M)) (trees_cyl ` trees (sets M))"
unfolding sets_tree_sigma_eq by (simp add: space_tree_sigma)
have 4: "(\s. ?E s) = space (tree_sigma M)"
proof (safe; clarsimp simp: space_tree_sigma)
fix t s assume "t \ trees_cyl (map_tree (\_::unit. space M) s)"
then show "t \ trees (space M)"
by (induction s arbitrary: t) auto
next
fix t assume "t \ trees (space M)"
then show "\t'. t \ ?E t'"
by (intro exI[of _ "map_tree (\_. ()) t"])
(auto simp: tree.map_comp comp_def intro: trees_cyl_map_treeI)
qed
have 5: "range ?E \ trees_cyl ` trees (sets M)" by auto
let ?P = "{A \ B | A B. A \ trees_cyl ` trees (sets M) \ B \ trees_cyl ` trees (sets M)}"
have P: "sets (tree_sigma M \\<^sub>M tree_sigma M) = sets (sigma (space (tree_sigma M) \ space (tree_sigma M)) ?P)"
by (rule sets_pair_eq[OF 2 3 1 5 4 2 3 1 5 4])
have "sets (M \\<^sub>M (tree_sigma M \\<^sub>M tree_sigma M)) =
sets (sigma (space M \ space (tree_sigma M \\<^sub>M tree_sigma M)) {A \ BC | A BC. A \ sets M \ BC \ ?P})"
proof (rule sets_pair_eq)
show "sets M \ Pow (space M)" "sets M = sigma_sets (space M) (sets M)"
by (auto simp: sets.sigma_sets_eq sets.space_closed)
show "countable {space M}" "{space M} \ sets M" "\{space M} = space M"
by auto
show "?P \ Pow (space (tree_sigma M \\<^sub>M tree_sigma M))"
using trees_cyl_sets_in_space[of M]
by (auto simp: space_pair_measure space_tree_sigma subset_eq)
then show "sets (tree_sigma M \\<^sub>M tree_sigma M) =
sigma_sets (space (tree_sigma M \\<^sub>M tree_sigma M)) ?P"
by (subst P, subst sets_measure_of) (auto simp: space_tree_sigma space_pair_measure)
show "countable ((\(a, b). a \ b) ` (range ?E \ range ?E))"
by (intro countable_image countable_SIGMA countableI_type)
show "(\(a, b). a \ b) ` (range ?E \ range ?E) \ ?P"
by auto
qed (insert 4, auto simp: space_pair_measure space_tree_sigma set_eq_iff)
also have "\ = sigma_sets (space M \ trees (space M) \ trees (space M))
{A \ BC |A BC. A \ sets M \ BC \ {A \ B |A B.
A \ trees_cyl ` trees (sets M) \ B \ trees_cyl ` trees (sets M)}}"
(is "_ = sigma_sets ?X ?Y") using sets.space_closed[of M] trees_cyl_sub_trees[of _ "sets M" "space M"]
by (subst sets_measure_of)
(auto simp: space_pair_measure space_tree_sigma)
also have "?Y = {A \ trees_cyl B \ trees_cyl C | A B C. A \ sets M \
B \ trees (sets M) \ C \ trees (sets M)}" by blast
finally have "X \ sigma_sets (space M \ trees (space M) \ trees (space M))
{A \ trees_cyl B \ trees_cyl C | A B C. A \ sets M \ B \ trees (sets M) \ C \ trees (sets M) }"
using assms by blast
then show ?thesis
proof induction
case (Basic A')
then obtain A B C where "A' = A \ trees_cyl B \ trees_cyl C"
and *: "A \ sets M" "B \ trees (sets M)" "C \ trees (sets M)"
by auto
then have "{Node l v r |l v r. (v, l, r) \ A'} = trees_cyl (Node B A C)"
by auto
then show ?case
by (auto simp del: trees_cyl.simps simp: sets_tree_sigma_eq intro!: sigma_sets.Basic *)
next
case Empty show ?case by auto
next
case (Compl A)
have "{Node l v r |l v r. (v, l, r) \ space M \ trees (space M) \ trees (space M) - A} =
(space (tree_sigma M) - {Node l v r |l v r. (v, l, r) \ A}) - {Leaf}"
by (auto simp: space_tree_sigma elim: trees.cases)
also have "\ \ sets (tree_sigma M)"
by (intro sets.Diff Compl) auto
finally show ?case .
next
case (Union I)
have *: "{Node l v r |l v r. (v, l, r) \ \(I ` UNIV)} =
(\i. {Node l v r |l v r. (v, l, r) \ I i})" by auto
show ?case unfolding * using Union(2) by (intro sets.countable_UN) auto
qed
qed
lemma measurable_left[measurable]: "left \ tree_sigma M \\<^sub>M tree_sigma M"
proof (rule measurableI)
show "t \ space (tree_sigma M) \ left t \ space (tree_sigma M)" for t
by (cases t) (auto simp: space_tree_sigma)
fix A assume A: "A \ sets (tree_sigma M)"
from sets.sets_into_space[OF this]
have *: "left -` A \ space (tree_sigma M) =
(if Leaf \ A then {Leaf} else {}) \
{Node a v r | a v r. (v, a, r) \ space M \ A \ space (tree_sigma M)}"
by (auto simp: space_tree_sigma elim: trees.cases)
show "left -` A \ space (tree_sigma M) \ sets (tree_sigma M)"
unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
qed
lemma measurable_right[measurable]: "right \ tree_sigma M \\<^sub>M tree_sigma M"
proof (rule measurableI)
show "t \ space (tree_sigma M) \ right t \ space (tree_sigma M)" for t
by (cases t) (auto simp: space_tree_sigma)
fix A assume A: "A \ sets (tree_sigma M)"
from sets.sets_into_space[OF this]
have *: "right -` A \ space (tree_sigma M) =
(if Leaf \ A then {Leaf} else {}) \
{Node l v a | l v a. (v, l, a) \ space M \ space (tree_sigma M) \ A}"
by (auto simp: space_tree_sigma elim: trees.cases)
show "right -` A \ space (tree_sigma M) \ sets (tree_sigma M)"
unfolding * using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
qed
lemma measurable_root_val': "root_val \ restrict_space (tree_sigma M) (-{Leaf}) \\<^sub>M M"
proof (rule measurableI)
show "t \ space (restrict_space (tree_sigma M) (- {Leaf})) \ root_val t \ space M" for t
by (cases t) (auto simp: space_restrict_space space_tree_sigma)
fix A assume A: "A \ sets M"
from sets.sets_into_space[OF this]
have "root_val -` A \ space (restrict_space (tree_sigma M) (- {Leaf})) =
{Node l a r | l a r. (a, l, r) \ A \ space (tree_sigma M) \ space (tree_sigma M)}"
by (auto simp: space_tree_sigma space_restrict_space elim: trees.cases)
also have "\ \ sets (tree_sigma M)"
using A by (intro sets.Un Node_in_tree_sigma pair_measureI) auto
finally show "root_val -` A \ space (restrict_space (tree_sigma M) (- {Leaf})) \
sets (restrict_space (tree_sigma M) (- {Leaf}))"
by (auto simp: sets_restrict_space_iff space_restrict_space)
qed
lemma measurable_restrict_mono:
assumes f: "f \ restrict_space M A \\<^sub>M N" and "B \ A"
shows "f \ restrict_space M B \