Theory Randomized_Algorithm
section ‹Randomized Algorithms\label{sec:randomized_algorithm}›
text ‹This section introduces the @{term "random_alg"} monad, that can be used to represent
executable randomized algorithms. It is a type-definition based on the internal representation from
Section~\ref{sec:randomized_algorithm_internal} with the wellformedness restriction.
Additionally, we introduce the @{term "spmf_of_ra"} morphism, which represent the distribution of
a randomized algorithm, under the assumption that the coin flips are independent and unbiased.
We also show that it is a Scott-continuous monad-morphism and introduce transfer theorems, with
which it is possible to establish the corresponding SPMF of a randomized algorithms, even in the
case of (possibly infinite) loops.›
theory Randomized_Algorithm
imports
Randomized_Algorithm_Internal
begin
text ‹A stronger variant of @{thm [source] pmf_eqI}.›
lemma pmf_eq_iff_le:
fixes p q :: "'a pmf"
assumes "⋀x. pmf p x ≤ pmf q x"
shows "p = q"
proof -
have "(∫x. pmf q x - pmf p x ∂count_space UNIV) = 0"
by (simp_all add:integrable_pmf integral_pmf)
moreover have "integrable (count_space UNIV) (λx. pmf q x - pmf p x)"
by (simp add:integrable_pmf)
moreover have "AE x in count_space UNIV. 0 ≤ pmf q x - pmf p x"
using assms unfolding AE_count_space by auto
ultimately have "AE x in count_space UNIV. pmf q x - pmf p x = 0"
using integral_nonneg_eq_0_iff_AE by blast
hence "⋀x. pmf p x = pmf q x" unfolding AE_count_space by simp
thus ?thesis by (intro pmf_eqI) auto
qed
text ‹The following is a stronger variant of @{thm [source] "ord_spmf_eq_pmf_None_eq"}›
lemma eq_iff_ord_spmf:
assumes "weight_spmf p ≥ weight_spmf q"
assumes "ord_spmf (=) p q"
shows "p = q"
proof -
have "⋀x. spmf p x ≤ spmf q x"
using ord_spmf_eq_leD[OF assms(2)] by simp
moreover have "pmf p None ≤ pmf q None"
using assms(1) unfolding pmf_None_eq_weight_spmf by auto
ultimately have "pmf p x ≤ pmf q x" for x by (cases x) auto
thus ?thesis using pmf_eq_iff_le by auto
qed
lemma wf_empty: "wf_random (λ_. None)"
unfolding wf_random_def by auto
typedef 'a random_alg = "{(r :: 'a random_alg_int). wf_random r}"
using wf_empty by (intro exI[where x="λ_. None"]) auto
setup_lifting type_definition_random_alg
lift_definition return_ra :: "'a ⇒ 'a random_alg" is return_rai
by (rule wf_return)
lift_definition coin_ra :: "bool random_alg" is coin_rai
by (rule wf_coin)
lift_definition bind_ra :: "'a random_alg ⇒ ('a ⇒ 'b random_alg) ⇒ 'b random_alg" is bind_rai
by (rule wf_bind)
adhoc_overloading Monad_Syntax.bind bind_ra
text ‹Monad laws:›
lemma return_bind_ra:
"bind_ra (return_ra x) g = g x"
by (rule return_bind_rai[transferred])
lemma bind_ra_assoc:
"bind_ra (bind_ra f g) h = bind_ra f (λx. bind_ra (g x) h)"
by (rule bind_rai_assoc[transferred])
lemma bind_return_ra:
"bind_ra m return_ra = m"
by (rule bind_return_rai[transferred])
lift_definition lub_ra :: "'a random_alg set ⇒ 'a random_alg" is
"(λF. if Complete_Partial_Order.chain ord_rai F then lub_rai F else (λx. None))"
using wf_lub wf_empty by auto
lift_definition ord_ra :: "'a random_alg ⇒ 'a random_alg ⇒ bool" is "ord_rai" .
lift_definition run_ra :: "'a random_alg ⇒ coin_stream ⇒ 'a option" is
"(λf s. map_option fst (f s))" .
context
begin
interpretation pmf_as_measure .
lemma distr_rai_is_pmf:
assumes "wf_random f"
shows
"prob_space (distr_rai f)" (is "?A")
"sets (distr_rai f) = UNIV" (is "?B")
"AE x in distr_rai f. measure (distr_rai f) {x} ≠ 0" (is "?C")
proof -
show "prob_space (distr_rai f)"
using prob_space_distr_rai[OF assms] by simp
then interpret p: prob_space "distr_rai f"
by auto
show ?B
unfolding distr_rai_def by simp
have "AE bs in ℬ. map_option fst (f bs) ∈ Some ` range_rm f ∪ {None}"
unfolding range_rm_def
by (intro AE_I2) (auto simp:image_iff split:option.split)
hence "AE x in distr_rai f. x ∈ Some ` range_rm f ∪ {None}"
unfolding distr_rai_def using distr_rai_measurable[OF assms]
by (subst AE_distr_iff) auto
moreover have "countable (Some ` range_rm f ∪ {None})"
using countable_range[OF assms] by simp
moreover have "p.events = UNIV"
unfolding distr_rai_def by simp
ultimately show ?C
by (intro iffD2[OF p.AE_support_countable] exI[where x= "Some ` range_rm f ∪ {None}"]) auto
qed
lift_definition spmf_of_ra :: "'a random_alg ⇒ 'a spmf" is "distr_rai"
using distr_rai_is_pmf by metis
lemma used_bits_distr_is_pmf:
assumes "wf_random f"
shows
"prob_space (used_bits_distr f)" (is "?A")
"sets (used_bits_distr f) = UNIV" (is "?B")
"AE x in used_bits_distr f. measure (used_bits_distr f) {x} ≠ 0" (is "?C")
proof -
show "prob_space (used_bits_distr f)"
unfolding used_bits_distr_def
by (intro coin_space.prob_space_distr consumed_bits_measurable)
then interpret p: prob_space "used_bits_distr f"
by auto
show ?B
unfolding used_bits_distr_def by simp
have "p.events = UNIV"
unfolding used_bits_distr_def by simp
thus ?C
by (intro iffD2[OF p.AE_support_countable] exI[where x= "UNIV"]) auto
qed
lift_definition coin_usage_of_ra_aux :: "'a random_alg ⇒ nat spmf" is "used_bits_distr"
using used_bits_distr_is_pmf by auto
definition coin_usage_of_ra
where "coin_usage_of_ra p = map_pmf (case_option ∞ enat) (coin_usage_of_ra_aux p)"
end
lemma wf_rep_rand_alg:
"wf_random (Rep_random_alg f)"
using Rep_random_alg by auto
lemma set_pmf_spmf_of_ra:
"set_pmf (spmf_of_ra f) ⊆ Some ` range_rm (Rep_random_alg f) ∪ {None}"
proof
let ?f = "Rep_random_alg f"
fix x assume "x ∈ set_pmf (spmf_of_ra f)"
hence "pmf (spmf_of_ra f) x > 0"
using pmf_positive by metis
hence "measure (distr_rai ?f) {x} > 0"
by (subst spmf_of_ra.rep_eq[symmetric]) (simp add: pmf.rep_eq)
hence "0 < measure ℬ {ω. map_option fst (?f ω) = x}"
using distr_rai_measurable[OF wf_rep_rand_alg] unfolding distr_rai_def
by (subst (asm) measure_distr) (simp_all add:vimage_def space_coin_space)
moreover have "{ω. map_option fst (?f ω) = x} = {}" if "x ∉ range (map_option fst ∘ ?f)"
using that by (auto simp:set_eq_iff image_iff)
hence "measure ℬ {ω. map_option fst (?f ω) = x} = 0" if "x ∉ range (map_option fst ∘ ?f)"
using that by simp
ultimately have "x ∈ range (map_option fst ∘ ?f)"
by auto
thus "x ∈ Some ` range_rm (Rep_random_alg f) ∪ {None}"
unfolding range_rm_def by (cases x) auto
qed
lemma spmf_of_ra_return: "spmf_of_ra (return_ra x) = return_spmf x"
proof -
have "measure_pmf (spmf_of_ra (return_ra x)) = measure_pmf (return_spmf x)"
unfolding spmf_of_ra.rep_eq distr_rai_return'[symmetric]
by (simp add: return_ra.rep_eq)
thus ?thesis
using measure_pmf_inject by blast
qed
lemma spmf_of_ra_coin: "spmf_of_ra coin_ra = coin_spmf"
proof -
have "measure_pmf (spmf_of_ra coin_ra) = measure_pmf coin_spmf"
unfolding spmf_of_ra.rep_eq distr_rai_coin[symmetric]
by (simp add: coin_ra.rep_eq)
thus ?thesis
using measure_pmf_inject by blast
qed
lemma spmf_of_ra_bind:
"spmf_of_ra (bind_ra f g) = bind_spmf (spmf_of_ra f) (λx. spmf_of_ra (g x))" (is "?L = ?R")
proof -
let ?f = "Rep_random_alg f"
let ?g = "λx. Rep_random_alg (g x)"
have 0: "x ∈ Some ` range_rm ?f ∨ x = None" if "x ∈ set_pmf (spmf_of_ra f)" for x
using that set_pmf_spmf_of_ra by auto
have "measure_pmf ?L = distr_rai (?f ⤜ ?g)"
unfolding spmf_of_ra.rep_eq bind_ra.rep_eq by (simp add:comp_def)
also have "... = distr_rai ?f ⤜
(λx. if x ∈ Some ` range_rm ?f then distr_rai (?g (the x)) else return 𝒟 None)"
by (intro distr_rai_bind wf_rep_rand_alg)
also have "... = measure_pmf (spmf_of_ra f) ⤜
(λx. measure_pmf (if x ∈ Some ` range_rm ?f then spmf_of_ra (g (the x)) else return_pmf None))"
by (intro arg_cong2[where f="bind"] ext) (auto simp:spmf_of_ra.rep_eq return_discrete)
also have "... = measure_pmf (spmf_of_ra f ⤜
(λx. if x ∈ Some ` range_rm ?f then spmf_of_ra (g (the x)) else return_pmf None))"
unfolding bind_pmf.rep_eq by (simp add:comp_def id_def)
also have "... = measure_pmf ?R"
using 0 unfolding bind_spmf_def
by (intro arg_cong[where f="measure_pmf"] bind_pmf_cong refl) (auto split:option.split)
finally have "measure_pmf ?L = measure_pmf ?R" by simp
thus ?thesis
using measure_pmf_inject by blast
qed
lemma spmf_of_ra_mono:
assumes "ord_ra f g"
shows "ord_spmf (=) (spmf_of_ra f) (spmf_of_ra g)"
proof -
have "ord_rai (Rep_random_alg f) (Rep_random_alg g)"
using assms unfolding ord_ra.rep_eq by simp
hence "ennreal (spmf (spmf_of_ra f) x) ≤ ennreal (spmf (spmf_of_ra g) x)" for x
unfolding emeasure_pmf_single[symmetric] spmf_of_ra.rep_eq
by (intro distr_rai_ord_rai_mono wf_rep_rand_alg) auto
hence "spmf (spmf_of_ra f) x ≤ spmf (spmf_of_ra g) x" for x
by simp
thus ?thesis
by (intro ord_pmf_increaseI) auto
qed
lemma spmf_of_ra_lub_ra_empty:
"spmf_of_ra (lub_ra {}) = return_pmf None" (is "?L = ?R")
proof -
have "measure_pmf ?L = distr_rai (lub_rai {})"
unfolding spmf_of_ra.rep_eq lub_ra.rep_eq Complete_Partial_Order.chain_def by auto
also have "... = distr_rai (λ_. None)"
unfolding lub_rai_def fun_lub_def flat_lub_def by auto
also have "... = measure_pmf ?R"
unfolding distr_rai_None by simp
finally have "measure_pmf ?L = measure_pmf ?R"
by simp
thus ?thesis
using measure_pmf_inject by auto
qed
lemma spmf_of_ra_lub_ra:
fixes A :: "'a random_alg set"
assumes "Complete_Partial_Order.chain ord_ra A"
shows "spmf_of_ra (lub_ra A) = lub_spmf (spmf_of_ra ` A)" (is "?L = ?R")
proof (cases "A ≠ {}")
case True
have 0:"Complete_Partial_Order.chain ord_rai (Rep_random_alg ` A)"
using assms unfolding ord_ra.rep_eq Complete_Partial_Order.chain_def by auto
have 1:"Complete_Partial_Order.chain (ord_spmf (=)) (spmf_of_ra ` A)"
using spmf_of_ra_mono by (intro chain_imageI[OF assms]) auto
show ?thesis
proof (rule spmf_eqI)
fix x :: "'a"
have "ennreal (spmf ?L x) = emeasure (distr_rai (lub_rai (Rep_random_alg ` A))) {Some x}"
using 0 unfolding emeasure_pmf_single[symmetric] spmf_of_ra.rep_eq lub_ra.rep_eq by simp
also have "... = (SUP f∈Rep_random_alg ` A. emeasure (distr_rai f) {Some x})"
using True wf_rep_rand_alg by (intro distr_rai_lub 0) auto
also have "... = (SUP p∈A. ennreal (spmf (spmf_of_ra p) x))"
unfolding emeasure_pmf_single[symmetric] spmf_of_ra.rep_eq by (simp add:image_image)
also have "... = (SUP p∈spmf_of_ra ` A. ennreal (spmf p x))"
by (simp add:image_image)
also have "... = ennreal (spmf ?R x)"
using True by (intro ennreal_spmf_lub_spmf[symmetric] 1) auto
finally have "ennreal (spmf ?L x) = ennreal (spmf ?R x)"
by simp
thus "spmf ?L x = spmf ?R x"
by simp
qed
next
case False
thus ?thesis using spmf_of_ra_lub_ra_empty by simp
qed
lemma rep_lub_ra:
assumes "Complete_Partial_Order.chain ord_ra F"
shows "Rep_random_alg (lub_ra F) = lub_rai (Rep_random_alg ` F)"
proof -
have "Complete_Partial_Order.chain ord_rai (Rep_random_alg ` F)"
using assms unfolding ord_ra.rep_eq Complete_Partial_Order.chain_def by auto
thus ?thesis
unfolding lub_ra.rep_eq by simp
qed
lemma partial_function_image_improved:
fixes ord
assumes "⋀A. Complete_Partial_Order.chain ord (f ` A) ⟹ l1 (f ` A) = f (l2 A)"
assumes "partial_function_definitions ord l1"
assumes "inj f"
shows "partial_function_definitions (img_ord f ord) l2"
proof -
interpret pd: partial_function_definitions ord l1
using assms(2) by auto
have "img_ord f ord x x" for x
unfolding img_ord_def using pd.leq_refl by simp
moreover have "img_ord f ord x z" if "img_ord f ord x y" "img_ord f ord y z" for x y z
using that pd.leq_trans unfolding img_ord_def by blast
moreover have "x = y" if "img_ord f ord x y" "img_ord f ord y x" for x y
proof -
have "f x = f y"
using that pd.leq_antisym unfolding img_ord_def by blast
thus ?thesis
using inj_onD[OF assms(3)] by simp
qed
moreover have "img_ord f ord x (l2 A)"
if "x ∈ A" "Complete_Partial_Order.chain (img_ord f ord) A" for x A
proof -
have 0:"Complete_Partial_Order.chain ord (f ` A)"
using that(2) unfolding chain_def img_ord_def by auto
have "ord (f x) (l1 (f ` A))"
using that by (intro pd.lub_upper[OF 0]) auto
thus ?thesis
unfolding img_ord_def assms(1)[OF 0] by auto
qed
moreover have "img_ord f ord (l2 A) z"
if "Complete_Partial_Order.chain (img_ord f ord) A" "(∀x. x ∈ A ⟶ img_ord f ord x z)"
for z A
proof -
have 0:"Complete_Partial_Order.chain ord (f ` A)"
using that(1) unfolding chain_def img_ord_def by auto
have "ord (l1 (f ` A)) (f z)"
using that(2) by (intro pd.lub_least[OF 0]) (auto simp:img_ord_def)
thus ?thesis
unfolding img_ord_def assms(1)[OF 0] by auto
qed
ultimately show ?thesis
unfolding partial_function_definitions_def by blast
qed
lemma random_alg_pfd: "partial_function_definitions ord_ra lub_ra"
proof -
have 0: "inj Rep_random_alg"
using Rep_random_alg_inject unfolding inj_on_def by auto
have 1:"partial_function_definitions ord_rai lub_rai"
using random_alg_int_pd_fact by simp
have 2:"ord_ra = img_ord Rep_random_alg ord_rai"
unfolding ord_ra.rep_eq img_ord_def by auto
show ?thesis
unfolding 2 by (intro partial_function_image_improved[OF _ 1 0]) (auto simp: lub_ra.rep_eq)
qed
interpretation random_alg_pf: partial_function_definitions "ord_ra" "lub_ra"
using random_alg_pfd by auto
abbreviation "mono_ra ≡ monotone (fun_ord ord_ra) ord_ra"
lemma bind_mono_aux_ra:
assumes "ord_ra f1 f2" "⋀y. ord_ra (g1 y) (g2 y)"
shows "ord_ra (bind_ra f1 g1) (bind_ra f2 g2)"
using assms unfolding ord_ra.rep_eq bind_ra.rep_eq
by (intro bind_rai_mono) auto
lemma bind_mono_ra [partial_function_mono]:
assumes "mono_ra B" and "⋀y. mono_ra (C y)"
shows "mono_ra (λf. bind_ra (B f) (λy. C y f))"
using assms by (intro monotoneI bind_mono_aux_ra) (auto simp:monotone_def)
definition map_ra :: "('a ⇒ 'b) ⇒ 'a random_alg ⇒ 'b random_alg"
where "map_ra f p = p ⤜ (λx. return_ra (f x))"
lemma spmf_of_ra_map: "spmf_of_ra (map_ra f p) = map_spmf f (spmf_of_ra p)"
unfolding map_ra_def map_spmf_conv_bind_spmf spmf_of_ra_bind spmf_of_ra_return by simp
lemmas spmf_of_ra_simps =
spmf_of_ra_return spmf_of_ra_bind spmf_of_ra_coin spmf_of_ra_map
lemma map_mono_ra [partial_function_mono]:
assumes "mono_ra B"
shows "mono_ra (λf. map_ra g (B f))"
using assms unfolding map_ra_def by (intro bind_mono_ra) auto
definition rel_spmf_of_ra :: "'a spmf ⇒ 'a random_alg ⇒ bool" where
"rel_spmf_of_ra q p ⟷ q = spmf_of_ra p"
lemma admissible_rel_spmf_of_ra:
"ccpo.admissible (prod_lub lub_spmf lub_ra) (rel_prod (ord_spmf (=)) ord_ra) (case_prod rel_spmf_of_ra)"
(is "ccpo.admissible ?lub ?ord ?P")
proof (rule ccpo.admissibleI)
fix Y
assume chain: "Complete_Partial_Order.chain ?ord Y"
and Y: "Y ≠ {}"
and R: "∀(p, q) ∈ Y. rel_spmf_of_ra p q"
from R have R: "⋀p q. (p, q) ∈ Y ⟹ rel_spmf_of_ra p q" by auto
have chain1: "Complete_Partial_Order.chain (ord_spmf (=)) (fst ` Y)"
and chain2: "Complete_Partial_Order.chain (ord_ra) (snd ` Y)"
using chain by(rule chain_imageI; clarsimp)+
from Y have Y1: "fst ` Y ≠ {}" and Y2: "snd ` Y ≠ {}" by auto
have "lub_spmf (fst ` Y) = lub_spmf (spmf_of_ra ` snd ` Y)"
unfolding image_image using R
by (intro arg_cong[of _ _ lub_spmf] image_cong) (auto simp: rel_spmf_of_ra_def)
also have "… = spmf_of_ra (lub_ra (snd ` Y))"
by (intro spmf_of_ra_lub_ra[symmetric] chain2)
finally have "rel_spmf_of_ra (lub_spmf (fst ` Y)) (lub_ra (snd ` Y))"
unfolding rel_spmf_of_ra_def .
then show "?P (?lub Y)"
by (simp add: prod_lub_def)
qed
lemma admissible_rel_spmf_of_ra_cont [cont_intro]:
fixes ord
shows "⟦ mcont lub ord lub_spmf (ord_spmf (=)) f; mcont lub ord lub_ra ord_ra g ⟧
⟹ ccpo.admissible lub ord (λx. rel_spmf_of_ra (f x) (g x))"
by (rule admissible_subst[OF admissible_rel_spmf_of_ra, where f="λx. (f x, g x)", simplified])
(rule mcont_Pair)
lemma mcont2mcont_spmf_of_ra[THEN spmf.mcont2mcont, cont_intro]:
shows mcont_spmf_of_sampler: "mcont lub_ra ord_ra lub_spmf (ord_spmf (=)) spmf_of_ra"
unfolding mcont_def monotone_def cont_def
by (auto simp: spmf_of_ra_mono spmf_of_ra_lub_ra)
context
includes lifting_syntax
begin
lemma fixp_ra_parametric[transfer_rule]:
assumes f: "⋀x. mono_spmf (λf. F f x)"
and g: "⋀x. mono_ra (λf. G f x)"
and param: "((A ===> rel_spmf_of_ra) ===> A ===> rel_spmf_of_ra) F G"
shows "(A ===> rel_spmf_of_ra) (spmf.fixp_fun F) (random_alg_pf.fixp_fun G)"
using f g
proof(rule parallel_fixp_induct_1_1[OF
partial_function_definitions_spmf random_alg_pfd _ _ reflexive reflexive,
where P="(A ===> rel_spmf_of_ra)"])
show "ccpo.admissible (prod_lub (fun_lub lub_spmf) (fun_lub lub_ra))
(rel_prod (fun_ord (ord_spmf (=))) (fun_ord ord_ra))
(λx. (A ===> rel_spmf_of_ra) (fst x) (snd x))"
unfolding rel_fun_def
by(rule admissible_all admissible_imp cont_intro)+
show "(A ===> rel_spmf_of_ra) (λ_. lub_spmf {}) (λ_. lub_ra {})"
by (auto simp: rel_fun_def rel_spmf_of_ra_def spmf_of_ra_lub_ra_empty)
show "(A ===> rel_spmf_of_ra) (F f) (G g)" if "(A ===> rel_spmf_of_ra) f g" for f g
using that by(rule rel_funD[OF param])
qed
lemma return_ra_tranfer[transfer_rule]: "((=) ===> rel_spmf_of_ra) return_spmf return_ra"
unfolding rel_fun_def rel_spmf_of_ra_def spmf_of_ra_return by simp
lemma bind_ra_tranfer[transfer_rule]:
"(rel_spmf_of_ra ===> ((=) ===> rel_spmf_of_ra) ===> rel_spmf_of_ra) bind_spmf bind_ra"
unfolding rel_fun_def rel_spmf_of_ra_def spmf_of_ra_bind by simp presburger
lemma coin_ra_tranfer[transfer_rule]:
"rel_spmf_of_ra coin_spmf coin_ra"
unfolding rel_fun_def rel_spmf_of_ra_def spmf_of_ra_coin by simp
lemma map_ra_tranfer[transfer_rule]:
"((=) ===> rel_spmf_of_ra ===> rel_spmf_of_ra) map_spmf map_ra"
unfolding rel_fun_def rel_spmf_of_ra_def spmf_of_ra_map by simp
end
declare [[function_internals]]
declaration ‹Partial_Function.init "random_alg" \<^term>‹random_alg_pf.fixp_fun›
\<^term>‹random_alg_pf.mono_body›
@{thm random_alg_pf.fixp_rule_uc} @{thm random_alg_pf.fixp_induct_uc}
NONE›
subsection ‹Almost surely terminating randomized algorithms›
definition terminates_almost_surely :: "'a random_alg ⇒ bool"
where "terminates_almost_surely f ⟷ lossless_spmf (spmf_of_ra f)"
definition pmf_of_ra :: "'a random_alg ⇒ 'a pmf" where
"pmf_of_ra p = map_pmf the (spmf_of_ra p)"
lemma pmf_of_spmf: "map_pmf the (spmf_of_pmf x) = x"
by (simp add:map_pmf_comp spmf_of_pmf_def)
definition coin_pmf :: "bool pmf" where "coin_pmf = pmf_of_set UNIV"
lemma pmf_of_ra_coin: "pmf_of_ra (coin_ra) = coin_pmf" (is "?L = ?R")
proof -
have 0:"spmf_of_ra (coin_ra) = spmf_of_pmf (pmf_of_set UNIV)"
unfolding spmf_of_ra_coin spmf_of_set_def by simp
thus ?thesis
unfolding 0 pmf_of_ra_def pmf_of_spmf coin_pmf_def by simp
qed
lemma pmf_of_ra_return: "pmf_of_ra (return_ra x) = return_pmf x"
unfolding pmf_of_ra_def spmf_of_ra_return by simp
lemma pmf_of_ra_bind:
assumes "terminates_almost_surely f"
shows "pmf_of_ra (f ⤜ g) = pmf_of_ra f ⤜ (λx. pmf_of_ra (g x))" (is "?L = ?R")
proof -
have 0:"x ≠ None" if "x ∈ set_pmf (spmf_of_ra f)" for x
using assms that unfolding terminates_almost_surely_def
by (meson lossless_iff_set_pmf_None)
have "?L = spmf_of_ra f ⤜ (λx. map_pmf the (case_option (return_pmf None) (spmf_of_ra ∘ g) x))"
unfolding pmf_of_ra_def spmf_of_ra_bind bind_spmf_def map_bind_pmf comp_def by simp
also have "... = spmf_of_ra f ⤜
(λx. (case x of None ⇒ return_pmf (the None) | Some x ⇒ pmf_of_ra (g x)))"
unfolding map_pmf_def comp_def pmf_of_ra_def map_pmf_def
by (intro arg_cong2[where f="bind_pmf"] refl ext) (simp add:bind_return_pmf split:option.split)
also have "... = spmf_of_ra f ⤜ (λx. pmf_of_ra (g (the x)))"
using 0 by (intro bind_pmf_cong refl) (auto split:option.split)
also have "... = ?R"
unfolding pmf_of_ra_def map_pmf_def by (simp add:bind_assoc_pmf bind_return_pmf)
finally show ?thesis
by simp
qed
lemma pmf_of_ra_map:
assumes "terminates_almost_surely m"
shows "pmf_of_ra (map_ra f m) = map_pmf f (pmf_of_ra m)"
unfolding map_ra_def pmf_of_ra_bind[OF assms] pmf_of_ra_return map_pmf_def by simp
lemma terminates_almost_surely_return:
"terminates_almost_surely (return_ra x)"
unfolding terminates_almost_surely_def spmf_of_ra_return by simp
lemma terminates_almost_surely_coin:
"terminates_almost_surely coin_ra"
unfolding terminates_almost_surely_def spmf_of_ra_coin by simp
lemma terminates_almost_surely_bind:
assumes "terminates_almost_surely f"
assumes "⋀x. x ∈ set_pmf (pmf_of_ra f) ⟹ terminates_almost_surely (g x)"
shows "terminates_almost_surely (f ⤜ g)"
proof -
have 0: "None ∉ set_pmf (spmf_of_ra f)"
using assms(1) lossless_iff_set_pmf_None unfolding terminates_almost_surely_def
by blast
hence "Some x ∈ set_pmf (spmf_of_ra f) ⟷ x ∈ the ` set_pmf (spmf_of_ra f)" for x
by (metis image_iff option.collapse option.sel)
hence "set_spmf (spmf_of_ra f) = set_pmf (pmf_of_ra f)"
unfolding pmf_of_ra_def set_map_pmf by (simp add:set_eq_iff set_spmf_def)
thus ?thesis
using assms(1,2) unfolding terminates_almost_surely_def spmf_of_ra_bind lossless_bind_spmf
by auto
qed
lemma terminates_almost_surely_map:
assumes "terminates_almost_surely p"
shows "terminates_almost_surely (map_ra f p)"
unfolding map_ra_def
by (intro assms terminates_almost_surely_bind terminates_almost_surely_return)
lemmas pmf_of_ra_simps =
pmf_of_ra_return pmf_of_ra_bind pmf_of_ra_coin pmf_of_ra_map
lemmas terminates_almost_surely_intros =
terminates_almost_surely_return
terminates_almost_surely_bind
terminates_almost_surely_coin
terminates_almost_surely_map
end