Theory Executable_Randomized_Algorithms.Randomized_Algorithm_Internal
section ‹Randomized Algorithms (Internal Representation)\label{sec:randomized_algorithm_internal}›
theory Randomized_Algorithm_Internal
imports
"HOL-Probability.Probability"
"Coin_Space"
"Tau_Additivity"
"Zeta_Function.Zeta_Library"
begin
text ‹This section introduces the internal representation for randomized algorithms. For ease of
use, we will introduce in Section~\ref{sec:randomized_algorithm} a @{command "typedef"} for the
monad which is easier to work with.›
text ‹This is the inverse of @{term "set_option"}›
definition the_elem_opt :: "'a set ⇒ 'a option"
where "the_elem_opt S = (if Set.is_singleton S then Some (the_elem S) else None)"
lemma the_elem_opt_empty[simp]: "the_elem_opt {} = None"
unfolding the_elem_opt_def is_singleton_def by (simp split:if_split_asm)
lemma the_elem_opt_single[simp]: "the_elem_opt {x} = Some x"
unfolding the_elem_opt_def by simp
definition at_most_one :: "'a set ⇒ bool"
where "at_most_one S ⟷ (∀x y. x ∈ S ∧ y ∈ S ⟶ x = y)"
lemma at_most_one_cases[consumes 1]:
assumes "at_most_one S"
assumes "P {the_elem S}"
assumes "P {}"
shows "P S"
proof (cases "S = {}")
case True
then show ?thesis using assms by auto
next
case False
then obtain x where "x ∈ S" by auto
hence "S = {x}" using assms(1) unfolding at_most_one_def by auto
thus ?thesis using assms(2) by simp
qed
lemma the_elem_opt_Some_iff[simp]: "at_most_one S ⟹ the_elem_opt S = Some x ⟷ S = {x}"
by (induction S rule:at_most_one_cases) auto
lemma the_elem_opt_None_iff[simp]: "at_most_one S ⟹ the_elem_opt S = None ⟷ S = {}"
by (induction S rule:at_most_one_cases) auto
text ‹The following is the fundamental type of the randomized algorithms, which are represented
as functions that take an infinite stream of coin flips and return the unused suffix of coin-flips
together with the result. We use the @{typ "'a option"} type to be able to introduce the
denotational semantics for the monad.›
type_synonym 'a random_alg_int = "coin_stream ⇒ ('a × coin_stream) option"
text ‹The @{term "return_rai"} combinator, does not consume any coin-flips and thus returns the
entire stream together with the result.›
definition return_rai :: "'a ⇒ 'a random_alg_int"
where "return_rai x bs = Some (x, bs)"
text ‹The @{term "bind_rai"} combinator passes the coin-flips to the first algorithm, then passes
the remaining coin flips to the second function, and returns the unused coin-flips from both
steps.›
definition bind_rai :: "'a random_alg_int ⇒ ('a ⇒ 'b random_alg_int) ⇒ 'b random_alg_int"
where "bind_rai m f bs =
do {
(r, bs') ← m bs;
f r bs'
}"
adhoc_overloading Monad_Syntax.bind bind_rai
text ‹The @{term "coin_rai"} combinator consumes one coin-flip and return it as the result, while the
tail of the coin flips are returned as unused.›
definition coin_rai :: "bool random_alg_int"
where "coin_rai bs = Some (chd bs, ctl bs)"
text ‹This representation is similar to the model proposed by Hurd~\cite{hurd2003formal}
\footnote{Although we were not aware of the technical report, when initially considering this
representation.}. It is also closely related to the construction of parser monads in functional
languages~\cite{hutton1998}.
We also had following alternatives considered, with various advantages and drawbacks:
\begin{itemize}
\item \emph{Returning the count of used coin flips:} Instead of returning a suffix of the input
stream a randomized algorithm could also return the number of used coin flips, which then would
allow the definition of the bind function, in a way that performs the appropriate shift in the
stream according to the returned number. An advantage of this model, is that it makes the number
of used coin-flips immediately available. (As we will see below, this is still possible
even in the formalized model, albeit with some more work.) The main disadvantage of this model is
that in scenarios, where the coin-flips cannot be computed in a random-access way, it leads to
performance degradation. Indeed it is easy to construct example algorithms, which incur
asymptotically quadratic slow-down compared to the formalized model.
\item \emph{Trees of coin-flips:} Another model we were considering is to require an infinite tree
of coin-flips as input instead of a stream. Here the idea is that each bind operation would pass
the left sub-tree to the first algorithm and the right sub-tree to the second algorithm. This
model has the dis-advantage that the resulting `'monad'', does not fulfill the associativity law.
Moreover many PRG's are designed and tested in the streaming sense, and there is not a lot of
research into the performance of PRGs with tree structured output. (A related idea was to still
use a stream as input, and split it into two sub-streams for example by the parity of the stream
position. This alternative also suffers from the lack of associativity problem and may lead to
a lot of unused coin flips.)
\end{itemize}
Another reason for using the formalized representation is compatibility with
linear types~\cite{bernardy2018}, if support for them are introduced in Isabelle in future.›
text ‹Monad laws:›
lemma return_bind_rai: "bind_rai (return_rai x) g = g x"
unfolding bind_rai_def return_rai_def by simp
lemma bind_rai_assoc: "bind_rai (bind_rai f g) h = bind_rai f (λx. bind_rai (g x) h)"
unfolding bind_rai_def by (simp add:case_prod_beta')
lemma bind_return_rai: "bind_rai m return_rai = m"
unfolding bind_rai_def return_rai_def by simp
definition wf_on_prefix :: "'a random_alg_int ⇒ bool list ⇒ 'a ⇒ bool" where
"wf_on_prefix f p r = (∀cs. f (cshift p cs) = Some (r,cs))"
definition wf_random :: "'a random_alg_int ⇒ bool" where
"wf_random f ⟷ (∀bs.
case f bs of
None ⇒ True |
Some (r,bs') ⇒ (∃p. cprefix p bs ∧ wf_on_prefix f p r))"
definition range_rm :: "'a random_alg_int ⇒ 'a set"
where "range_rm f = Some -` (range (map_option fst ∘ f))"
lemma in_range_rmI:
assumes "r bs = Some (y, n)"
shows "y ∈ range_rm r"
proof -
have "Some (y, n) ∈ range r"
using assms[symmetric] by auto
thus ?thesis
unfolding range_rm_def using fun.set_map by force
qed
definition distr_rai :: "'a random_alg_int ⇒ 'a option measure"
where "distr_rai f = distr ℬ 𝒟 (map_option fst ∘ f)"
lemma wf_randomI:
assumes "⋀bs. f bs ≠ None ⟹ (∃p r. cprefix p bs ∧ wf_on_prefix f p r)"
shows "wf_random f"
proof -
have "∃p. cprefix p bs ∧ wf_on_prefix f p r" if 0:"f bs = Some (r, bs')" for bs r bs'
proof -
obtain p r' where 1:"cprefix p bs" and 2:"wf_on_prefix f p r'"
using assms 0 by force
have "f bs = f (cshift p (cdrop (length p) bs))"
using 1 unfolding cprefix_def by (metis ctake_cdrop)
also have "... = Some (r', cdrop (length p) bs)"
using 2 unfolding wf_on_prefix_def by auto
finally have "f bs = Some (r', cdrop (length p) bs)"
by simp
hence "r = r'" using 0 by simp
thus ?thesis using 1 2 by auto
qed
thus ?thesis
unfolding wf_random_def by (auto split:option.split)
qed
lemma wf_on_prefix_bindI:
assumes "wf_on_prefix m p r"
assumes "wf_on_prefix (f r) q s"
shows "wf_on_prefix (m ⤜ f) (p@q) s"
proof -
have "(m ⤜ f) (cshift (p@q) cs) = Some (s, cs)" for cs
proof -
have "(m ⤜ f) (cshift (p@q) cs) = (m ⤜ f) (cshift p (cshift q cs))"
by simp
also have "... = (f r) (cshift q cs)"
using assms unfolding wf_on_prefix_def bind_rai_def by simp
also have "... = Some (s,cs)"
using assms unfolding wf_on_prefix_def by simp
finally show ?thesis by simp
qed
thus ?thesis
unfolding wf_on_prefix_def by simp
qed
lemma wf_bind:
assumes "wf_random m"
assumes "⋀x. x ∈ range_rm m ⟹ wf_random (f x)"
shows "wf_random (m ⤜ f)"
proof (rule wf_randomI)
fix bs
assume "(m ⤜ f) bs ≠ None"
then obtain x bs' y bs'' where 1: "m bs = Some (x,bs')" and 2:"f x bs' = Some (y, bs'')"
unfolding bind_rai_def by (cases "m bs") auto
hence wf: "wf_random (f x)"
by (intro assms(2) in_range_rmI) auto
obtain p where 5:"wf_on_prefix m p x" and 3:"cprefix p bs"
using assms(1) 1 unfolding wf_random_def by (auto split:option.split_asm)
have 4:"bs = cshift p (cdrop (length p) bs)"
using 3 unfolding cprefix_def by (metis ctake_cdrop)
hence "m bs = Some (x, cdrop (length p) bs)"
using 5 unfolding wf_on_prefix_def by metis
hence "bs' = cdrop (length p) bs"
using 1 by auto
hence 6:"bs = cshift p bs'"
using 4 by auto
obtain q where 7:"wf_on_prefix (f x) q y" and 8:"cprefix q bs'"
using wf 2 unfolding wf_random_def by (auto split:option.split_asm)
have "cprefix (p@q) bs"
unfolding 6 using 8 unfolding cprefix_def by auto
moreover have "wf_on_prefix (m ⤜ f) (p@q) y"
by (intro wf_on_prefix_bindI[OF 5] 7)
ultimately show "∃p r. cprefix p bs ∧ wf_on_prefix (m ⤜ f) p r"
by auto
qed
lemma wf_return:
"wf_random (return_rai x)"
proof (rule wf_randomI)
fix bs assume "return_rai x bs ≠ None"
have "wf_on_prefix (return_rai x) [] x"
unfolding wf_on_prefix_def return_rai_def by auto
moreover have "cprefix [] bs"
unfolding cprefix_def by auto
ultimately show "∃p r. cprefix p bs ∧ wf_on_prefix (return_rai x) p r"
by auto
qed
lemma wf_coin:
"wf_random (coin_rai)"
proof (rule wf_randomI)
fix bs assume "coin_rai bs ≠ None"
have "wf_on_prefix coin_rai [chd bs] (chd bs)"
unfolding wf_on_prefix_def coin_rai_def by auto
moreover have "cprefix [chd bs] bs"
unfolding cprefix_def by auto
ultimately show "∃p r. cprefix p bs ∧ wf_on_prefix coin_rai p r"
by auto
qed
definition ptree_rm :: "'a random_alg_int ⇒ bool list set"
where "ptree_rm f = {p. ∃r. wf_on_prefix f p r}"
definition eval_rm :: "'a random_alg_int ⇒ bool list ⇒ 'a" where
"eval_rm f p = fst (the (f (cshift p (cconst False))))"
lemma eval_rmD:
assumes "wf_on_prefix f p r"
shows "eval_rm f p = r"
using assms unfolding wf_on_prefix_def eval_rm_def by auto
lemma wf_on_prefixD:
assumes "wf_on_prefix f p r"
assumes "cprefix p bs"
shows "f bs = Some (eval_rm f p, cdrop (length p) bs)"
proof -
have 0:"bs = cshift p (cdrop (length p) bs)"
using assms(2) unfolding cprefix_def by (metis ctake_cdrop)
hence "f bs = Some (r, cdrop (length p) bs)"
using assms(1) 0 unfolding wf_on_prefix_def by metis
thus ?thesis
using eval_rmD[OF assms(1)] by simp
qed
lemma prefixes_parallel_helper:
assumes "p ∈ ptree_rm f"
assumes "q ∈ ptree_rm f"
assumes "prefix p q"
shows "p = q"
proof -
obtain h where 0:"q = p@h"
using assms(3) prefixE that by auto
obtain r1 where 1:"wf_on_prefix f p r1"
using assms(1) unfolding ptree_rm_def by auto
obtain r2 where 2:"wf_on_prefix f q r2"
using assms(2) unfolding ptree_rm_def by auto
have "x = cshift h x" for x :: "coin_stream"
proof -
have "Some (r2, x) = f (cshift q x)"
using 2 unfolding wf_on_prefix_def by auto
also have "... = f (cshift p (cshift h x))"
using 0 by auto
also have "... = Some (r1, cshift h x)"
using 1 unfolding wf_on_prefix_def by auto
finally show "x = cshift h x"
by simp
qed
hence "h = []"
using empty_if_shift_idem by simp
thus ?thesis using 0 by simp
qed
lemma prefixes_parallel:
assumes "p ∈ ptree_rm f"
assumes "q ∈ ptree_rm f"
shows "p = q ∨ p ∥ q"
using prefixes_parallel_helper assms by blast
lemma prefixes_singleton:
assumes "p ∈ {p. p ∈ ptree_rm f ∧ cprefix p bs}"
shows "{p ∈ ptree_rm f. cprefix p bs} = {p}"
proof
have "q = p" if "q ∈ ptree_rm f" "cprefix q bs" for q
using same_prefix_not_parallel assms prefixes_parallel that by blast
thus "{p ∈ ptree_rm f. cprefix p bs} ⊆ {p}"
by (intro subsetI) simp
next
show "{p} ⊆ {p ∈ ptree_rm f. cprefix p bs}"
using assms by auto
qed
lemma prefixes_at_most_one:
"at_most_one {p ∈ ptree_rm f. cprefix p x}"
unfolding at_most_one_def using same_prefix_not_parallel prefixes_parallel by blast
definition "consumed_prefix f bs = the_elem_opt {p ∈ ptree_rm f. cprefix p bs}"
lemma wf_random_alt:
assumes "wf_random f"
shows "f bs = map_option (λp. (eval_rm f p, cdrop (length p) bs)) (consumed_prefix f bs)"
proof (cases "f bs")
case None
have "False" if p_in: "p ∈ ptree_rm f" and p_pref: "cprefix p bs" for p
proof -
obtain r where wf: "wf_on_prefix f p r" using that p_in unfolding ptree_rm_def by auto
have "bs = cshift p (cdrop (length p) bs)"
using p_pref unfolding cprefix_def by (metis ctake_cdrop)
hence "f bs ≠ None"
using wf unfolding wf_on_prefix_def
by (metis option.simps(3))
thus "False" using None by simp
qed
hence 0:"{p ∈ ptree_rm f. cprefix p bs} = {}"
by auto
show ?thesis unfolding 0 None consumed_prefix_def by simp
next
case (Some a)
moreover obtain r cs where "a = (r, cs)" by (cases a) auto
ultimately have "f bs = Some (r, cs)" by simp
hence "∃p. cprefix p bs ∧ wf_on_prefix f p r"
using assms(1) unfolding wf_random_def by (auto split:option.split_asm)
then obtain p where sp: "cprefix p bs" and wf: "wf_on_prefix f p r"
by auto
hence "p ∈ {p ∈ ptree_rm f. cprefix p bs}"
unfolding ptree_rm_def by auto
hence 0:"{p ∈ ptree_rm f. cprefix p bs} = {p}"
using prefixes_singleton by auto
show ?thesis unfolding 0 wf_on_prefixD[OF wf sp] consumed_prefix_def by simp
qed
lemma range_rm_alt:
assumes "wf_random f"
shows "range_rm f = eval_rm f ` ptree_rm f" (is "?L = ?R")
proof -
have 0:"cprefix p (cshift p (cconst False))" for p
unfolding cprefix_def by auto
have "?L = {x. ∃bs. map_option (eval_rm f) (consumed_prefix f bs) = Some x}"
unfolding range_rm_def comp_def by (subst wf_random_alt[OF assms])
(simp add:map_option.compositionality comp_def vimage_def image_iff eq_commute)
also have "... = {x. ∃p bs. x = eval_rm f p ∧ consumed_prefix f bs = Some p}"
unfolding map_option_eq_Some
by (intro Collect_cong) metis
also have "... = {x. ∃p. p ∈ptree_rm f ∧ x = eval_rm f p}"
unfolding consumed_prefix_def the_elem_opt_Some_iff[OF prefixes_at_most_one]
using 0 prefixes_singleton
by (intro Collect_cong) blast
also have "... = ?R"
by auto
finally show ?thesis
by simp
qed
lemma consumed_prefix_some_iff:
"consumed_prefix f bs = Some p ⟷ (p ∈ ptree_rm f ∧ cprefix p bs)"
proof -
have "p ∈ ptree_rm f ⟹ cprefix p bs ⟹ x ∈ ptree_rm f ⟹ cprefix x bs ⟹ x = p" for x
using same_prefix_not_parallel prefixes_parallel by blast
thus ?thesis
unfolding consumed_prefix_def the_elem_opt_Some_iff[OF prefixes_at_most_one]
by auto
qed
definition consumed_bits where
"consumed_bits f bs = map_option length (consumed_prefix f bs)"
definition used_bits_distr :: "'a random_alg_int ⇒ nat option measure"
where "used_bits_distr f = distr ℬ 𝒟 (consumed_bits f)"
lemma wf_random_alt2:
assumes "wf_random f"
shows "f bs = map_option (λn. (eval_rm f (ctake n bs), cdrop n bs)) (consumed_bits f bs)"
(is "?L = ?R")
proof -
have 0:"cprefix x bs" if "consumed_prefix f bs = Some x" for x
using that the_elem_opt_Some_iff[OF prefixes_at_most_one] unfolding consumed_prefix_def by auto
have "?L = map_option (λp. (eval_rm f p, cdrop (length p) bs)) (consumed_prefix f bs)"
by (subst wf_random_alt[OF assms]) simp
also have "... = ?R"
using 0 unfolding consumed_bits_def map_option.compositionality comp_def cprefix_def
by (cases "consumed_prefix f bs") auto
finally show ?thesis by simp
qed
lemma consumed_prefix_none_iff:
assumes "wf_random f"
shows "f bs = None ⟷ consumed_prefix f bs = None"
using wf_random_alt[OF assms] by (simp)
lemma consumed_bits_inf_iff:
assumes "wf_random f"
shows "f bs = None ⟷ consumed_bits f bs = None"
using wf_random_alt2[OF assms] by (simp)
lemma consumed_bits_enat_iff:
"consumed_bits f bs = Some n ⟷ ctake n bs ∈ ptree_rm f" (is "?L = ?R")
proof
assume "consumed_bits f bs = Some n"
then obtain p where "the_elem_opt {p ∈ ptree_rm f. cprefix p bs} = Some p" and 0: "length p = n"
unfolding consumed_bits_def consumed_prefix_def by (auto split:option.split_asm)
hence "p ∈ ptree_rm f" "cprefix p bs"
unfolding the_elem_opt_Some_iff[OF prefixes_at_most_one] by auto
thus "ctake n bs ∈ ptree_rm f"
using 0 unfolding cprefix_def by auto
next
assume "ctake n bs ∈ ptree_rm f"
hence "ctake n bs ∈ {p ∈ ptree_rm f. cprefix p bs}"
unfolding cprefix_def by auto
hence "{p ∈ ptree_rm f. cprefix p bs} = {ctake n bs}"
using prefixes_singleton by auto
thus "consumed_bits f bs = Some n"
unfolding consumed_bits_def consumed_prefix_def by simp
qed
lemma consumed_bits_measurable: "consumed_bits f ∈ ℬ →⇩M 𝒟"
proof -
have 0: "consumed_bits f -` {x} ∩ space ℬ ∈ sets ℬ" (is "?L ∈ _")
if x_ne_inf: "x ≠ None" for x
proof -
obtain n where x_def: "x = Some n"
using x_ne_inf that by auto
have "?L = {bs. ∃z. consumed_prefix f bs = Some z ∧ length z = n}"
unfolding consumed_bits_def vimage_def space_coin_space x_def by simp
also have "... = {bs. ∃p. {p ∈ ptree_rm f. cprefix p bs} = {p} ∧ length p = n}"
unfolding consumed_prefix_def x_def the_elem_opt_Some_iff[OF prefixes_at_most_one] by simp
also have "... = {bs. ∃p. cprefix p bs ∧ length p = n ∧ p ∈ ptree_rm f}"
using prefixes_singleton by (intro Collect_cong ex_cong1) auto
also have "... = {bs. ctake n bs ∈ ptree_rm f}"
unfolding cprefix_def by (intro Collect_cong) (metis length_ctake)
also have "... ∈ sets ℬ"
by (intro measurable_sets_coin_space[OF ctake_measurable]) simp
finally show ?thesis
by simp
qed
thus ?thesis
by (intro measurable_sigma_sets_with_exception[where d="None"])
qed
lemma R_sets:
assumes wf:"wf_random f"
shows "{bs. f bs = None} ∈ sets ℬ" "{bs. f bs ≠ None} ∈ sets ℬ"
proof -
show 0: "{bs. f bs = None} ∈ sets ℬ"
unfolding consumed_bits_inf_iff[OF wf]
by (intro measurable_sets_coin_space[OF consumed_bits_measurable]) simp
have "{bs. f bs ≠ None} = space ℬ - {bs. f bs = None}"
unfolding space_coin_space by (simp add:set_eq_iff del:not_None_eq)
also have "... ∈ sets ℬ"
by (intro sets.compl_sets 0)
finally show "{bs. f bs ≠ None} ∈ sets ℬ"
by simp
qed
lemma countable_range:
assumes wf:"wf_random f"
shows "countable (range_rm f)"
proof -
have "countable (eval_rm f ` UNIV)"
by (intro countable_image) simp
moreover have "range_rm f ⊆ eval_rm f ` UNIV"
unfolding range_rm_alt[OF wf] by auto
ultimately show ?thesis using countable_subset by blast
qed
lemma consumed_prefix_continuous:
"continuous_map euclidean option_ud (consumed_prefix f)"
proof (intro contionuos_into_option_udI)
fix x :: "bool list"
have "open ((consumed_prefix f) -` {Some x})" (is "open ?T")
proof (cases "x ∈ ptree_rm f")
case True
hence 0:"?T = {bs. cprefix x bs}"
unfolding vimage_def comp_def by (simp add:consumed_prefix_some_iff)
show ?thesis
unfolding 0 by (intro coin_steam_open)
next
case False
hence "?T = {}"
unfolding vimage_def comp_def by (simp add:consumed_prefix_some_iff)
thus ?thesis
by simp
qed
thus "openin euclidean ((consumed_prefix f) -` {Some x} ∩ topspace euclidean)"
by simp
qed
text ‹Randomized algorithms are continuous with respect to the product topology on the domain
and the upper topology on the range.›
lemma f_continuous:
assumes wf:"wf_random f"
shows "continuous_map euclidean option_ud (map_option fst ∘ f)"
proof -
have 0: "map_option fst ∘ (λbs. f bs) =
map_option (eval_rm f) ∘ (consumed_prefix f)"
by (subst wf_random_alt[OF wf]) (simp add:map_option.compositionality comp_def)
show ?thesis unfolding 0
by (intro continuous_map_compose[OF consumed_prefix_continuous] map_option_continuous)
qed
lemma none_measure_subprob_algebra:
"return 𝒟 None ∈ space (subprob_algebra 𝒟)"
by (metis measure_subprob return_pmf.rep_eq)
context
fixes f :: "'a random_alg_int"
fixes R
assumes wf: "wf_random f"
defines "R ≡ restrict_space ℬ {bs. f bs ≠ None}"
begin
lemma the_f_measurable: "the ∘ f ∈ R →⇩M 𝒟 ⨂⇩M ℬ"
proof -
define h where "h = the ∘ consumed_bits f"
define g where "g bs = (ctake (h bs) bs, cdrop (h bs) bs)" for bs
have "consumed_bits f bs ≠ None" if "bs ∈ space R" for bs
using that consumed_bits_inf_iff[OF wf] unfolding R_def space_restrict_space space_coin_space
by (simp del:not_infinity_eq not_None_eq)
hence 0:"the (f bs) = map_prod (eval_rm f) id (g bs)" if "bs ∈ space R" for bs
unfolding g_def h_def using that
by (subst wf_random_alt2[OF wf]) (cases "consumed_bits f bs", auto simp del: not_None_eq)
have 1:"h ∈ R →⇩M 𝒟"
unfolding R_def h_def
by (intro measurable_restrict_space1 measurable_comp[OF consumed_bits_measurable]) simp
have "ctake k ∈ R →⇩M 𝒟" for k
unfolding R_def by (intro measurable_restrict_space1 ctake_measurable)
moreover have "cdrop k ∈ R →⇩M ℬ" for k
unfolding R_def by (intro measurable_restrict_space1 cdrop_measurable)
ultimately have "g ∈ R →⇩M 𝒟 ⨂⇩M ℬ"
unfolding g_def
by (intro measurable_Pair measurable_Pair_compose_split[OF _ 1 measurable_id]) simp_all
hence "(map_prod (eval_rm f) id ∘ g) ∈ R →⇩M 𝒟 ⨂⇩M ℬ"
by (intro measurable_comp[where N="𝒟 ⨂⇩M ℬ"] map_prod_measurable) auto
moreover have "(the ∘ f) ∈ R →⇩M 𝒟 ⨂⇩M ℬ ⟷ (map_prod (eval_rm f) id ∘ g) ∈ R →⇩M 𝒟 ⨂⇩M ℬ"
using 0 by (intro measurable_cong) (simp add:comp_def)
ultimately show ?thesis
by auto
qed
lemma distr_rai_measurable: "map_option fst ∘ f ∈ ℬ →⇩M 𝒟"
proof -
have 0:"countable {{bs. f bs ≠ None}, {bs. f bs = None}}"
by simp
have 1: "Ω ∈ sets ℬ ∧ map_option fst ∘ f ∈ restrict_space ℬ Ω →⇩M 𝒟"
if "Ω ∈ {{bs. f bs ≠ None}, {bs. f bs = None}}" for Ω
proof (cases "Ω = {bs. f bs ≠ None}")
case True
have "Some ∘ fst ∘ (the ∘ f) ∈ R →⇩M 𝒟"
by (intro measurable_comp[OF the_f_measurable]) auto
hence "map_option fst ∘ f ∈ R →⇩M 𝒟"
unfolding R_def by (subst measurable_cong[where g="Some ∘ fst ∘ (the ∘ f)"])
(auto simp add: space_restrict_space space_coin_space)
thus "Ω ∈ sets ℬ ∧ map_option fst ∘ f ∈ restrict_space ℬ Ω →⇩M 𝒟"
unfolding R_def True using R_sets[OF wf] by auto
next
case False
hence 2:"Ω = {bs. f bs = None}"
using that by simp
have "map_option fst ∘ f ∈ restrict_space ℬ {bs. f bs = None} →⇩M 𝒟"
by (subst measurable_cong[where g="λ_. None"])
(simp_all add:space_restrict_space)
thus "Ω ∈ sets ℬ ∧ map_option fst ∘ f ∈ restrict_space ℬ Ω →⇩M 𝒟"
unfolding 2 using R_sets[OF wf] by auto
qed
have 3: "space ℬ ⊆ ⋃ {{bs. f bs ≠ None}, {bs. f bs = None}}"
unfolding space_coin_space by auto
show ?thesis
by (rule measurable_piecewise_restrict[OF 0]) (use 1 3 space_coin_space in ‹auto›)
qed
lemma distr_rai_subprob_space:
"distr_rai f ∈ space (subprob_algebra 𝒟)"
proof -
have "prob_space (distr_rai f)"
unfolding distr_rai_def using distr_rai_measurable
by (intro coin_space.prob_space_distr ) auto
moreover have "sets (distr_rai f) = 𝒟"
unfolding distr_rai_def by simp
ultimately show ?thesis
unfolding space_subprob_algebra using prob_space_imp_subprob_space
by auto
qed
lemma fst_the_f_measurable: "fst ∘ the ∘ f ∈ R →⇩M 𝒟"
proof -
have "fst ∘ (the ∘ f) ∈ R →⇩M 𝒟"
by (intro measurable_comp[OF the_f_measurable]) simp
thus ?thesis by (simp add:comp_def)
qed
lemma prob_space_distr_rai:
"prob_space (distr_rai f)"
unfolding distr_rai_def by (intro coin_space.prob_space_distr distr_rai_measurable)
text ‹This is the central correctness property for the monad. The returned stream of coins
is independent of the result of the randomized algorithm.›
lemma remainder_indep:
"distr R (𝒟 ⨂⇩M ℬ) (the ∘ f) = distr R 𝒟 (fst ∘ the ∘ f) ⨂⇩M ℬ"
proof -
define C where "C k = consumed_bits f -` {Some k}" for k
have 2: "(∃k. x ∈ C k) ⟷ f x ≠ None" for x
using consumed_bits_inf_iff[OF wf] unfolding C_def
by auto
hence 5: "C k ⊆ space R" for k
unfolding R_def space_restrict_space space_coin_space
by auto
have 1:"{bs. f bs ≠ None} ∩ space ℬ ∈ sets ℬ"
using R_sets[OF wf] by simp
have 6: "C k ∈ sets ℬ" for k
unfolding C_def vimage_def
by (intro measurable_sets_coin_space[OF consumed_bits_measurable]) simp
have 8: "x ∈ C k ⟷ ctake k x ∈ ptree_rm f" for x k
unfolding C_def using consumed_bits_enat_iff by auto
have 7: "the (f (cshift (ctake k x) y)) = (fst (the (f x)), y)" if "x ∈ C k" for x y k
proof -
have "cshift (ctake k x) y ∈ C k"
using that 8 by simp
hence "the (f (cshift (ctake k x) y)) = (eval_rm f (ctake k x), y)"
using wf_random_alt2[OF wf] unfolding C_def by simp
also have "... = (fst (the (f x)), y)"
using that wf_random_alt2[OF wf] unfolding C_def by simp
finally show ?thesis by simp
qed
have C_disj: "disjoint_family C"
unfolding disjoint_family_on_def C_def by auto
have 0:
"emeasure (distr R (𝒟 ⨂⇩M ℬ) (the ∘ f)) (A × B) =
emeasure (distr R 𝒟 (fst ∘ the ∘ f)) A * emeasure ℬ B"
(is "?L = ?R") if "A ∈ sets 𝒟" "B ∈ sets ℬ" for A B
proof -
have 3: "{bs. fst (the (f bs)) ∈ A ∧ bs ∈ C k} ∈ sets ℬ" (is "?L1 ∈ _") for k
proof -
have "?L1 = (fst ∘ the ∘ f) -` A ∩ space (restrict_space R (C k))"
using 5 unfolding vimage_def space_restrict_space R_def space_coin_space by auto
also have "... ∈ sets (restrict_space R (C k))"
by (intro measurable_sets[OF _ that(1)] measurable_restrict_space1 fst_the_f_measurable)
also have "... = sets (restrict_space ℬ (C k))"
using 5 unfolding R_def sets_restrict_restrict_space space_restrict_space space_coin_space
by (intro arg_cong2[where f="restrict_space"] arg_cong[where f="sets"] refl) auto
finally have "?L1 ∈ sets (restrict_space ℬ (C k))"
by simp
thus "?L1 ∈ sets ℬ"
using 6 space_coin_space sets_restrict_space_iff[where M="ℬ" and Ω="C k"] by auto
qed
have 4: "{bs. the (f bs) ∈ A × B ∧ bs ∈ C k} ∈ sets ℬ" (is "?L1 ∈ _") for k
proof -
have "?L1 = (the ∘ f) -` (A × B) ∩ space (restrict_space R (C k))"
using 5 unfolding vimage_def space_restrict_space R_def space_coin_space by auto
also have "... ∈ sets (restrict_space R (C k))"
using that by (intro measurable_sets[where A="𝒟 ⨂⇩M ℬ"] measurable_restrict_space1
the_f_measurable) auto
also have "... = sets (restrict_space ℬ (C k))"
using 5 unfolding R_def sets_restrict_restrict_space space_restrict_space space_coin_space
by (intro arg_cong2[where f="restrict_space"] arg_cong[where f="sets"] refl) auto
finally have "?L1 ∈ sets (restrict_space ℬ (C k))"
by simp
thus "?L1 ∈ sets ℬ"
using 6 space_coin_space sets_restrict_space_iff[where M="ℬ" and Ω="C k"] by auto
qed
have "?L = emeasure R ((the ∘ f) -` (A × B) ∩ space R)"
using that the_f_measurable by (intro emeasure_distr) auto
also have "... = emeasure R {x. the (f x) ∈ A × B ∧ f x ≠ None}"
unfolding vimage_def R_def Int_def
by (simp add:space_restrict_space space_coin_space)
also have "... = emeasure ℬ {x. the (f x) ∈ A × B ∧ (∃k. x ∈ C k)}"
unfolding R_def 2 using 1 by (intro emeasure_restrict_space) auto
also have "... = emeasure ℬ (⋃k. {x. the (f x) ∈ A × B ∧ x ∈ C k})"
by (intro arg_cong2[where f="emeasure"]) auto
also have "... = (∑k. emeasure ℬ {x. the (f x) ∈ A × B ∧ x ∈ C k})"
using 4 C_disj
by (intro suminf_emeasure[symmetric] subsetI) (auto simp:disjoint_family_on_def)
also have "... = (∑k. emeasure (distr (ℬ ⨂⇩M ℬ) ℬ (λ(x,y). (cshift (ctake k x) y)))
{x. the (f x) ∈ A × B ∧ x ∈ C k})"
by (intro suminf_cong arg_cong2[where f="emeasure"] branch_coin_space(2)[symmetric] refl)
also have "... = (∑k. emeasure (ℬ ⨂⇩M ℬ)
{x. the (f (cshift (ctake k (fst x)) (snd x))) ∈ A × B ∧ (cshift (ctake k (fst x)) (snd x)) ∈ C k})"
using branch_coin_space(1) 4 by (subst emeasure_distr)
(simp_all add:case_prod_beta Int_def space_pair_measure space_coin_space)
also have "... = (∑k. emeasure (ℬ ⨂⇩M ℬ)
{x. the (f (cshift (ctake k (fst x)) (snd x))) ∈ A × B ∧ fst x ∈ C k})"
using 8 by (intro suminf_cong arg_cong2[where f="emeasure"] refl Collect_cong) auto
also have "... = (∑k. emeasure (ℬ ⨂⇩M ℬ) ({x. fst (the (f x)) ∈ A ∧ x ∈ C k} × B))"
using 7 by (intro suminf_cong arg_cong2[where f="emeasure"] refl)
(auto simp add:mem_Times_iff set_eq_iff)
also have "... = (∑k. emeasure ℬ {x. fst (the (f x)) ∈ A ∧ x ∈ C k} * emeasure ℬ B)"
using 3 that(2)
by (intro suminf_cong coin_space.emeasure_pair_measure_Times) auto
also have "... = (∑k. emeasure ℬ {x. fst (the (f x)) ∈ A ∧ x ∈ C k}) * emeasure ℬ B"
by simp
also have "... = emeasure ℬ (⋃k. {x. fst (the (f x)) ∈ A ∧ x ∈ C k}) * emeasure ℬ B"
using 3 C_disj
by (intro arg_cong2[where f="(*)"] suminf_emeasure refl image_subsetI)
(auto simp add:disjoint_family_on_def)
also have "... = emeasure ℬ {x. fst (the (f x)) ∈ A ∧ (∃k. x ∈ C k)} * emeasure ℬ B"
by (intro arg_cong2[where f="emeasure"] arg_cong2[where f="(*)"]) auto
also have "... = emeasure R {x. fst (the (f x)) ∈ A ∧ f x ≠ None} * emeasure ℬ B"
unfolding R_def 2 using 1
by (intro arg_cong2[where f="(*)"] emeasure_restrict_space[symmetric] subsetI) simp_all
also have "... = emeasure R ((fst ∘ the ∘ f) -` A ∩ space R) * emeasure ℬ B"
unfolding vimage_def R_def Int_def by (simp add:space_restrict_space space_coin_space)
also have "... = ?R"
using that
by (intro arg_cong2[where f="(*)"] emeasure_distr[symmetric] fst_the_f_measurable) auto
finally show ?thesis by simp
qed
have "finite_measure R"
using 1 unfolding R_def space_coin_space
by (intro finite_measure_restrict_space) simp_all
hence "finite_measure (distr R 𝒟 (fst ∘ the ∘ f))"
by (intro finite_measure.finite_measure_distr fst_the_f_measurable)
hence 1:"sigma_finite_measure (distr R 𝒟 (fst ∘ the ∘ f))"
unfolding finite_measure_def by auto
have 2:"sigma_finite_measure ℬ"
using prob_space_imp_sigma_finite[OF coin_space.prob_space_axioms] by simp
show ?thesis
using 0 by (intro pair_measure_eqI[symmetric] 1 2) (simp_all add:sets_pair_measure)
qed
end
lemma distr_rai_bind:
assumes wf_m: "wf_random m"
assumes wf_f: "⋀x. x ∈ range_rm m ⟹ wf_random (f x)"
shows "distr_rai (m ⤜ f) = distr_rai m ⤜
(λx. if x ∈ Some ` range_rm m then distr_rai (f (the x)) else return 𝒟 None)"
(is "?L = ?RHS")
proof (rule measure_eqI)
have "sets ?L = UNIV"
unfolding distr_rai_def by simp
also have "... = sets ?RHS"
unfolding distr_rai_def by (subst sets_bind[where N="𝒟"])
(simp_all add:option.case_distrib option.case_eq_if)
finally show "sets ?L = sets ?RHS" by simp
next
let ?m = "distr_rai"
let ?H = "count_space (range_rm m)"
let ?R = "restrict_space ℬ {bs. m bs ≠ None}"
fix A assume "A ∈ sets (distr_rai (m ⤜ f))"
define N where "N = {x. m x ≠ None}"
have N_meas: "N ∈ sets coin_space"
unfolding N_def using R_sets[OF wf_m] by simp
hence N_meas': "-N ∈ sets coin_space"
unfolding Compl_eq_Diff_UNIV using space_coin_space by (metis sets.compl_sets)
have wf_bind: "wf_random (m ⤜ f)"
using wf_bind[OF assms] by auto
have 0: "(map_option fst ∘ (m ⤜ f)) ∈ coin_space →⇩M 𝒟"
using distr_rai_measurable[OF wf_bind] by auto
have 1: "(map_option fst ∘ (m ⤜ f)) -` A ∈ sets ℬ"
unfolding vimage_def by (intro measurable_sets_coin_space[OF 0]) simp
have "{(v, bs). map_option fst (f v bs) ∈ A ∧ v ∈ range_rm m} =
(map_option fst ∘ case_prod f) -` A ∩ space (?H ⨂⇩M ℬ)"
unfolding vimage_def space_pair_measure space_coin_space by auto
also have "... ∈ sets (?H ⨂⇩M ℬ)"
using distr_rai_measurable[OF wf_f]
by (intro measurable_sets[where A="𝒟"] measurable_pair_measure_countable1 countable_range wf_m)
(simp_all add:comp_def)
also have "... = sets (restrict_space 𝒟 (range_rm m) ⨂⇩M ℬ)"
unfolding restrict_count_space inf_top_right by simp
also have "... = sets (restrict_space (𝒟 ⨂⇩M ℬ) (range_rm m × space coin_space))"
by (subst coin_space.restrict_space_pair_lift) auto
finally have "{(v, bs). map_option fst (f v bs) ∈ A ∧ v ∈ range_rm m} ∈
sets (restrict_space (𝒟 ⨂⇩M ℬ) (range_rm m × UNIV))"
unfolding space_coin_space by simp
moreover have "range_rm m × space coin_space ∈ sets (𝒟 ⨂⇩M ℬ)"
by (intro pair_measureI sets.top) auto
ultimately have 2: "{(v, bs). map_option fst (f v bs) ∈ A ∧ v∈ range_rm m} ∈ sets (𝒟 ⨂⇩M ℬ)"
by (subst (asm) sets_restrict_space_iff) (auto simp: space_coin_space)
have space_R: "space ?R = {x. m x ≠ None}"
by (simp add:space_restrict_space space_coin_space)
have 3: "distr_rai (f (the x)) ∈ space (subprob_algebra 𝒟)"
if "x ∈ Some ` range_rm m" for x
using distr_rai_subprob_space[OF wf_f] that by fastforce
have "(λx. emeasure (distr_rai (f (fst (the (m x))))) A * indicator N x) =
(λx. emeasure (if m x ≠ None then distr_rai (f (fst (the (m x)))) else null_measure 𝒟) A)"
unfolding N_def by (intro ext) simp
also have "... = (λv. emeasure (if v∈Some`range_rm m then ?m (f (the v)) else null_measure 𝒟) A)
∘ (map_option fst ∘ m)"
unfolding comp_def by (intro ext arg_cong2[where f="emeasure"] refl if_cong)
(auto intro:in_range_rmI simp add:vimage_def image_iff)
also have "... ∈ borel_measurable coin_space"
using 3 by (intro distr_rai_measurable[OF wf_m] measurable_comp[where N="𝒟"]
measurable_emeasure_kernel[where N="𝒟"]) simp_all
finally have 4:"(λx. emeasure (distr_rai (f (fst (the (m x))))) A * indicator N x)
∈ coin_space →⇩M borel" by simp
let ?N = "emeasure ℬ {bs. bs ∉ N ∧ None ∈ A}"
have "emeasure ?L A = emeasure ℬ ((map_option fst ∘ (m ⤜ f)) -` A)"
unfolding distr_rai_def using 0 by (subst emeasure_distr) (simp_all add:space_coin_space)
also have "... =
emeasure ℬ ((map_option fst∘(m⤜f))-`A ∩ -N) + emeasure ℬ ((map_option fst∘(m⤜f))-`A ∩ N)"
using N_meas N_meas' 1
by (subst emeasure_Un'[symmetric]) (simp_all add:Int_Un_distrib[symmetric])
also have "... =
emeasure ℬ ((map_option fst∘(m⤜f))-`A∩ -N) + emeasure ?R ((map_option fst∘(m⤜f))-`A∩ N)"
using N_meas unfolding N_def
by (intro arg_cong2[where f="(+)"] refl emeasure_restrict_space[symmetric]) simp_all
also have "... =?N + emeasure ?R ((the ∘ m) -`
{(v, bs). map_option fst (f v bs) ∈ A ∧ v∈ range_rm m} ∩ space ?R)"
unfolding bind_rai_def N_def space_R apfst_def
by (intro arg_cong2[where f="(+)"] arg_cong2[where f="emeasure"])
(simp_all add: set_eq_iff in_range_rmI split:option.split bind_splits)
also have "... = ?N + emeasure (distr ?R (𝒟⨂⇩Mℬ) (the ∘ m))
{(v,bs). map_option fst (f v bs)∈A ∧ v∈ range_rm m}"
using 2 by (intro arg_cong2[where f="(+)"] emeasure_distr[symmetric]
the_f_measurable map_prod_measurable wf_m) simp_all
also have "... = ?N + emeasure (distr ?R 𝒟 (fst ∘ the ∘ m) ⨂⇩M ℬ)
{(v,bs). map_option fst (f v bs) ∈ A ∧ v ∈ range_rm m}"
unfolding N_def remainder_indep[OF wf_m] by simp
also have "... = ?N + ∫⇧+ v. emeasure ℬ
{bs. map_option fst (f v bs) ∈ A ∧ v ∈ range_rm m} ∂distr ?R 𝒟 (fst ∘ (the ∘ m))"
using 2 by (subst coin_space.emeasure_pair_measure_alt) (simp_all add:vimage_def comp_assoc)
also have "... = ?N + ∫⇧+ x. emeasure ℬ
{bs. map_option fst (f ((fst ∘ (the ∘ m)) x) bs) ∈ A ∧ (fst ∘ (the ∘ m)) x ∈ range_rm m} ∂?R"
using the_f_measurable[OF wf_m]
by (intro arg_cong2[where f="(+)"] refl nn_integral_distr) simp_all
also have "... = ?N + (∫⇧+x∈{bs. m bs ≠ None}. emeasure ℬ
{bs. map_option fst (f (fst (the (m x))) bs) ∈ A ∧ fst (the (m x)) ∈ range_rm m} ∂ℬ)"
using N_meas unfolding N_def using nn_integral_restrict_space
by (subst nn_integral_restrict_space) simp_all
also have "... = ?N + (∫⇧+x∈{bs. m bs ≠ None}.
emeasure ℬ ((map_option fst ∘ f (fst (the (m x)))) -` A ∩ space ℬ) ∂ℬ)"
by (intro arg_cong2[where f="(+)"] set_nn_integral_cong refl arg_cong2[where f="emeasure"])
(auto intro:in_range_rmI simp:space_coin_space)
also have "... = ?N + (∫⇧+x∈N. emeasure (distr_rai(f(fst(the(m x))))) A ∂ℬ)"
unfolding distr_rai_def N_def
by (intro arg_cong2[where f="(+)"] set_nn_integral_cong refl emeasure_distr[symmetric]
distr_rai_measurable[OF wf_f]) (auto intro:in_range_rmI)
also have "... = (∫⇧+x. (indicator {bs. bs ∉ N ∧ None ∈ A}) x ∂ℬ) +
(∫⇧+x∈N. emeasure (distr_rai(f(fst(the(m x))))) A ∂ℬ)"
using N_meas N_meas'
by (intro arg_cong2[where f="(+)"] nn_integral_indicator[symmetric] refl)
(cases "None ∈ A"; auto simp:Collect_neg_eq)
also have "... = ∫⇧+ x. indicator {bs. bs ∉ N ∧ None ∈ A} x +
emeasure (distr_rai (f (fst (the (m x))))) A * indicator N x ∂ℬ"
using N_meas' N_meas by (intro nn_integral_add[symmetric] 4) simp
also have "... = ∫⇧+ x. indicator (-N) x * indicator A None +
indicator N x * emeasure (distr_rai (f (fst (the (m x))))) A ∂ℬ"
unfolding N_def by (intro arg_cong2[where f="nn_integral"] ext refl arg_cong2[where f="(+)"])
(simp_all split:split_indicator)
also have "... =
∫⇧+ x. emeasure (case m x of None ⇒ return 𝒟 None | Some x ⇒ distr_rai (f (fst x))) A ∂ℬ"
unfolding N_def by (intro arg_cong2[where f="nn_integral"] ext)
(auto split:split_indicator option.split)
also have "... = ∫⇧+ x. emeasure (if (map_option fst ∘ m) x ∈ Some ` range_rm m
then distr_rai (f (the ((map_option fst ∘ m) x)))
else return 𝒟 None) A ∂ℬ"
by (intro arg_cong2[where f="nn_integral"] arg_cong2[where f="emeasure"] refl ext)
(auto simp add: in_range_rmI vimage_def split:option.splits)
also have "... =
∫⇧+ x. emeasure (if x ∈ Some ` range_rm m then ?m (f (the x)) else return 𝒟 None) A ∂?m m"
unfolding distr_rai_def using distr_rai_measurable[OF wf_m]
by (intro nn_integral_distr[symmetric]) (simp_all add:comp_def)
also have "... = emeasure ?RHS A"
using 3 none_measure_subprob_algebra
by (intro emeasure_bind[symmetric, where N="𝒟"]) (auto simp add:distr_rai_def Pi_def)
finally show "emeasure ?L A = emeasure ?RHS A"
by simp
qed
lemma return_discrete: "return 𝒟 x = return_pmf x"
by (intro measure_eqI) auto
lemma distr_rai_return: "distr_rai (return_rai x) = return 𝒟 (Some x)"
unfolding return_rai_def distr_rai_def by (simp add:comp_def)
lemma distr_rai_return': "distr_rai (return_rai x) = return_spmf x"
unfolding distr_rai_return return_discrete by auto
lemma distr_rai_coin: "distr_rai coin_rai = coin_spmf" (is "?L = ?R")
proof -
have "?L = distr ℬ 𝒟 (λx. Some (chd x))"
unfolding coin_rai_def distr_rai_def by (simp add:comp_def)
also have "... = distr (distr ℬ 𝒟 chd) 𝒟 Some"
by (subst distr_distr) (auto simp add:comp_def chd_measurable)
also have "... = map_pmf Some (pmf_of_set UNIV)"
unfolding distr_shd map_pmf_rep_eq by simp
also have "... = spmf_of_pmf (pmf_of_set UNIV)"
by (simp add:spmf_of_pmf_def)
also have "... = coin_spmf"
by auto
finally show ?thesis by simp
qed
definition ord_rai :: "'a random_alg_int ⇒ 'a random_alg_int ⇒ bool"
where "ord_rai = fun_ord (flat_ord None)"
definition lub_rai :: "'a random_alg_int set ⇒ 'a random_alg_int"
where "lub_rai = fun_lub (flat_lub None)"
lemma random_alg_int_pd_fact:
"partial_function_definitions ord_rai lub_rai"
unfolding ord_rai_def lub_rai_def
by (intro partial_function_lift flat_interpretation)
interpretation random_alg_int_pd: partial_function_definitions "ord_rai" "lub_rai"
by (rule random_alg_int_pd_fact)
lemma wf_lub_helper:
assumes "ord_rai f g"
assumes "wf_on_prefix f p r"
shows "wf_on_prefix g p r"
proof -
have "g (cshift p cs) = Some (r, cs)" for cs
proof -
have "f (cshift p cs) = Some (r,cs)"
using assms(2) unfolding wf_on_prefix_def by auto
moreover have "flat_ord None (f (cshift p cs)) (g (cshift p cs))"
using assms(1) unfolding ord_rai_def fun_ord_def by simp
ultimately show ?thesis
unfolding flat_ord_def by auto
qed
thus ?thesis
unfolding wf_on_prefix_def by auto
qed
lemma wf_lub:
assumes "Complete_Partial_Order.chain ord_rai R"
assumes "⋀r. r ∈ R ⟹ wf_random r"
shows "wf_random (lub_rai R)"
proof (rule wf_randomI)
fix bs
assume a:"lub_rai R bs ≠ None"
define S where "S = ((λx. x bs) ` R)"
have 0:"lub_rai R bs = flat_lub None S"
unfolding S_def lub_rai_def fun_lub_def
by (intro arg_cong2[where f="flat_lub"]) auto
have "lub_rai R bs = None" if "S ⊆ {None}"
using that unfolding 0 flat_lub_def by auto
hence "¬ (S ⊆ {None})"
using a by auto
then obtain r where 1:"r ∈ R" and 2: "r bs ≠ None"
unfolding S_def by blast
then obtain p y where 3:"cprefix p bs" and 4:"wf_on_prefix r p y"
using assms(2)[OF 1] 2 unfolding wf_random_def by (auto split:option.split_asm)
have "wf_on_prefix (lub_rai R) p y"
by (intro wf_lub_helper[OF _ 4] random_alg_int_pd.lub_upper 1 assms(1))
thus "∃p r. cprefix p bs ∧ wf_on_prefix (lub_rai R) p r "
using 3 by auto
qed
lemma ord_rai_mono:
assumes "ord_rai f g"
assumes "¬ (P None)"
assumes "P (f bs)"
shows "P (g bs)"
using assms unfolding ord_rai_def fun_ord_def flat_ord_def by metis
lemma lub_rai_empty:
"lub_rai {} = Map.empty"
unfolding lub_rai_def fun_lub_def flat_lub_def by simp
lemma distr_rai_lub:
assumes "F ≠ {}"
assumes "Complete_Partial_Order.chain ord_rai F"
assumes wf_f: "⋀f. f ∈ F ⟹ wf_random f"
assumes "None ∉ A"
shows "emeasure (distr_rai (lub_rai F)) A = (SUP f ∈ F. emeasure (distr_rai f) A)" (is "?L = ?R")
proof -
have wf_lub: "wf_random (lub_rai F)"
by (intro wf_lub assms)
have 4: "ord_rai f (lub_rai F)" if "f ∈ F" for f
using that random_alg_int_pd.lub_upper[OF assms(2)] by simp
have 0:"map_option fst (lub_rai F bs) ∈ A ⟷ (∃f ∈ F. map_option fst (f bs) ∈ A)" for bs
proof
assume "∃f∈F. map_option fst (f bs) ∈ A"
then obtain f where 3:"map_option fst (f bs) ∈ A" and 5:"f ∈ F"
by auto
show "map_option fst (lub_rai F bs) ∈ A"
by (rule ord_rai_mono[OF 4[OF 5]]) (use 3 assms(4) in auto)
next
assume "map_option fst (lub_rai F bs) ∈ A"
then obtain y where 6:"lub_rai F bs = Some y" "Some (fst y) ∈ A"
using assms(4) by (cases "lub_rai F bs") auto
hence "f bs = None ∨ f bs = Some y" if "f ∈ F" for f
using 4[OF that] unfolding ord_rai_def fun_ord_def flat_ord_def by auto
moreover have "lub_rai F bs = None" if "⋀f. f ∈ F ⟹ f bs = None"
using that unfolding lub_rai_def flat_lub_def fun_lub_def by auto
ultimately obtain f where "f bs = Some y" "f ∈ F"
using 6(1) by auto
thus "∃f∈F. map_option fst (f bs) ∈ A"
using 6(2) by force
qed
have 1: "Complete_Partial_Order.chain (⊆) ((λf. {bs. map_option fst (f bs) ∈ A}) ` F)"
using assms(4) by (intro chain_imageI[OF assms(2)] Collect_mono impI) (auto intro:ord_rai_mono)
have 2: "open {bs. map_option fst (f bs) ∈ A}" (is "open ?T") if "f ∈ F" for f
proof -
have wf_f': "wf_random f"
by (intro assms that)
have 4:"?T = {bs ∈ topspace euclidean. (map_option fst ∘ f) bs ∈ A}"
by simp
have "openin option_ud A"
using assms(4) unfolding openin_option_ud by simp
hence "openin euclidean ?T"
unfolding 4 by (intro openin_continuous_map_preimage[OF f_continuous] wf_f')
thus ?thesis
using open_openin by simp
qed
have 3: "{bs. map_option fst (f bs) ∈ A} ∈ sets ℬ" (is "?L1 ∈ _") if "wf_random f" for f
using distr_rai_measurable[OF that]
by (intro measurable_sets_coin_space[where P="λx. x ∈ A" and A="𝒟"]) (auto simp:comp_def)
have "?L = emeasure ℬ ((map_option fst ∘ lub_rai F) -` A ∩ space ℬ)"
unfolding distr_rai_def by (intro emeasure_distr distr_rai_measurable[OF wf_lub]) auto
also have "... = emeasure ℬ {x. map_option fst (lub_rai F x) ∈ A}"
unfolding space_coin_space by (simp add:vimage_def)
also have "... = emeasure ℬ (⋃f ∈ F. {bs. map_option fst (f bs) ∈ A})"
unfolding 0 by (intro arg_cong2[where f="emeasure"]) auto
also have "... = Sup (emeasure ℬ ` (λf. {bs. map_option fst (f bs) ∈ A}) ` F)"
using 2 by (intro tau_additivity[OF coin_space_is_borel_measure] chain_imp_union_stable 1) auto
also have "... = (SUP f ∈ F. (emeasure ℬ {bs. map_option fst (f bs) ∈ A}))"
unfolding image_image by simp
also have "... = (SUP f∈F. emeasure ℬ ((map_option fst ∘ f) -` A ∩ space ℬ))"
by (simp add:image_image space_coin_space vimage_def)
also have "... = ?R"
unfolding distr_rai_def using distr_rai_measurable[OF wf_f]
by (intro arg_cong[where f="(Sup)"] image_cong ext emeasure_distr[symmetric]) auto
finally show ?thesis
by simp
qed
lemma distr_rai_ord_rai_mono:
assumes "wf_random f" "wf_random g" "ord_rai f g"
assumes "None ∉ A"
shows "emeasure (distr_rai f) A ≤ emeasure (distr_rai g) A" (is "?L ≤ ?R")
proof -
have 0:"Complete_Partial_Order.chain ord_rai {f,g}"
using assms(3) unfolding Complete_Partial_Order.chain_def
using random_alg_int_pd.leq_refl by auto
have "ord_rai (lub_rai {f,g}) g"
using assms(3) random_alg_int_pd.leq_refl
by (intro random_alg_int_pd.lub_least 0) auto
moreover have "ord_rai g (lub_rai {f,g})"
by (intro random_alg_int_pd.lub_upper 0) simp
ultimately have 1:"g = lub_rai {f,g}"
by (intro random_alg_int_pd.leq_antisym) auto
have "emeasure (distr_rai f) A ≤ (SUP x ∈ {f,g}. emeasure (distr_rai x) A)"
using prob_space_distr_rai assms(1,2) prob_space.measure_le_1
by (intro cSup_upper bdd_aboveI[where M="1"]) auto
also have "... = emeasure (distr_rai (lub_rai {f,g})) A"
using assms by (intro distr_rai_lub[symmetric] 0) auto
also have "... = emeasure (distr_rai g) A"
using 1 by auto
finally show ?thesis
by simp
qed
lemma distr_rai_None: "distr_rai (λ_. None) = measure_pmf (return_pmf (None :: 'a option))"
proof -
have "emeasure (distr_rai Map.empty) A = emeasure (measure_pmf (return_pmf None)) A"
for A :: "'a option set"
using coin_space.emeasure_space_1 unfolding distr_rai_def
by (subst emeasure_distr) simp_all
thus ?thesis
by (intro measure_eqI) (simp_all add:distr_rai_def)
qed
lemma bind_rai_mono:
assumes "ord_rai f1 f2" "⋀y. ord_rai (g1 y) (g2 y)"
shows "ord_rai (bind_rai f1 g1) (bind_rai f2 g2)"
proof -
have "flat_ord None (bind_rai f1 g1 bs) (bind_rai f2 g2 bs)" for bs
proof (cases "(f1 ⤜ g1) bs")
case None
then show ?thesis by (simp add:flat_ord_def)
next
case (Some a)
then obtain y bs' where 0: "f1 bs = Some (y,bs')" and 1:"g1 y bs' ≠ None" and "f1 bs ≠ None"
by (cases "f1 bs", auto simp:bind_rai_def)
hence "f2 bs = f1 bs"
using assms(1) unfolding ord_rai_def fun_ord_def flat_ord_def by metis
hence "f2 bs = Some (y,bs')"
using 0 by auto
moreover have "g1 y bs' = g2 y bs'"
using assms(2) 1 unfolding ord_rai_def fun_ord_def flat_ord_def by metis
ultimately have "(f1 ⤜ g1) bs = (f2 ⤜ g2) bs"
unfolding bind_rai_def 0 by auto
thus ?thesis unfolding flat_ord_def by auto
qed
thus ?thesis
unfolding ord_rai_def fun_ord_def by simp
qed
end