(* Author: Johannes Hölzl <hoelzl@in.tum.de> *) section ‹Discrete-Time Markov Chain› theory Discrete_Time_Markov_Chain imports Markov_Models_Auxiliary begin text ‹ Markov chain with discrete time steps and discrete state space. › lemma sstart_eq': "sstart Ω (x # xs) = {ω. shd ω = x ∧ stl ω ∈ sstart Ω xs}" by (auto simp: sstart_eq) lemma measure_eq_stream_space_coinduct[consumes 1, case_names left right cont]: assumes "R N M" assumes R_1: "⋀N M. R N M ⟹ N ∈ space (prob_algebra (stream_space (count_space UNIV)))" and R_2: "⋀N M. R N M ⟹ M ∈ space (prob_algebra (stream_space (count_space UNIV)))" and cont: "⋀N M. R N M ⟹ ∃N' M' p. (∀y∈set_pmf p. R (N' y) (M' y)) ∧ (∀x. N' x ∈ space (prob_algebra (stream_space (count_space UNIV)))) ∧ (∀x. M' x ∈ space (prob_algebra (stream_space (count_space UNIV)))) ∧ N = (measure_pmf p ⤜ (λy. distr (N' y) (stream_space (count_space UNIV)) ((##) y))) ∧ M = (measure_pmf p ⤜ (λy. distr (M' y) (stream_space (count_space UNIV)) ((##) y)))" shows "N = M" proof - let ?S = "stream_space (count_space UNIV)" have "∀N M. R N M ⟶ (∃N' M' p. (∀y∈set_pmf p. R (N' y) (M' y)) ∧ (∀x. N' x ∈ space (prob_algebra ?S)) ∧ (∀x. M' x ∈ space (prob_algebra ?S)) ∧ N = (measure_pmf p ⤜ (λy. distr (N' y) ?S ((##) y))) ∧ M = (measure_pmf p ⤜ (λy. distr (M' y) ?S ((##) y))))" using cont by auto then obtain n m p where p: "⋀N M y. R N M ⟹ y ∈ set_pmf (p N M) ⟹ R (n N M y) (m N M y)" and n: "⋀N M x. R N M ⟹ n N M x ∈ space (prob_algebra ?S)" and n_eq: "⋀N M y. R N M ⟹ N = (measure_pmf (p N M) ⤜ (λy. distr (n N M y) ?S ((##) y)))" and m: "⋀N M x. R N M ⟹ m N M x ∈ space (prob_algebra ?S)" and m_eq: "⋀N M y. R N M ⟹ M = (measure_pmf (p N M) ⤜ (λy. distr (m N M y) ?S ((##) y)))" unfolding choice_iff' choice_iff by blast define A where "A = (SIGMA nm:UNIV. (λx. (n (fst nm) (snd nm) x, m (fst nm) (snd nm) x)) ` p (fst nm) (snd nm))" have A_singleton: "A `` {nm} = (λx. (n (fst nm) (snd nm) x, m (fst nm) (snd nm) x)) ` p (fst nm) (snd nm)" for nm by (auto simp: A_def) have sets_n[measurable_cong, simp]: "sets (n N M y) = sets ?S" if "R N M" for N M y using n[OF that, of y] by (auto simp: space_prob_algebra) have sets_m[measurable_cong, simp]: "sets (m N M y) = sets ?S" if "R N M" for N M y using m[OF that, of y] by (auto simp: space_prob_algebra) have [simp]: "R N M ⟹ prob_space (n N M y)" for N M y using n[of N M y] by (auto simp: space_prob_algebra) have [simp]: "R N M ⟹ prob_space (m N M y)" for N M y using m[of N M y] by (auto simp: space_prob_algebra) have [measurable]: "R N M ⟹ n N M ∈ count_space UNIV →⇩M subprob_algebra ?S" for N M by (rule measurable_prob_algebraD) (auto intro: n) have [measurable]: "R N M ⟹ m N M ∈ count_space UNIV →⇩M subprob_algebra ?S" for N M by (rule measurable_prob_algebraD) (auto intro: m) define n' where "n' N M y = distr (n N M y) ?S ((##) y)" for N M y define m' where "m' N M y = distr (m N M y) ?S ((##) y)" for N M y have n'_eq: "R N M ⟹ N = (measure_pmf (p N M) ⤜ n' N M)" for N M unfolding n'_def by (rule n_eq) have m'_eq: "R N M ⟹ M = (measure_pmf (p N M) ⤜ m' N M)" for N M unfolding m'_def by (rule m_eq) have [measurable]: "R N M ⟹ n' N M ∈ count_space UNIV →⇩M subprob_algebra ?S" for N M unfolding n'_def by (rule measurable_distr2[where M="?S"]) measurable have [measurable]: "R N M ⟹ m' N M ∈ count_space UNIV →⇩M subprob_algebra ?S" for N M unfolding m'_def by (rule measurable_distr2[where M="?S"]) measurable have n'_shd: "R N M ⟹ distr (n' N M y) (count_space UNIV) shd = measure_pmf (return_pmf y)" for N M y unfolding n'_def by (subst distr_distr) (auto simp: comp_def prob_space.distr_const return_pmf.rep_eq) have m'_shd: "R N M ⟹ distr (m' N M y) (count_space UNIV) shd = measure_pmf (return_pmf y)" for N M y unfolding m'_def by (subst distr_distr) (auto simp: comp_def prob_space.distr_const return_pmf.rep_eq) have n'_stl: "R N M ⟹ distr (n' N M y) ?S stl = n N M y" for N M y unfolding n'_def by (subst distr_distr) (auto simp: comp_def distr_id2) have m'_stl: "R N M ⟹ distr (m' N M y) ?S stl = m N M y" for N M y unfolding m'_def by (subst distr_distr) (auto simp: comp_def distr_id2) define F where "F = (A⇧* `` {(N, M)})" have "countable F" unfolding F_def apply (intro countable_rtrancl countable_insert[of _ "(N, M)"] countable_empty) apply (rule countable_Image) apply (auto simp: A_singleton) done have F_NM[simp]: "(N, M) ∈ F" unfolding F_def by auto have R_F[simp]: "R N' M'" if "(N', M') ∈ F" for N' M' proof - have "((N, M), (N', M')) ∈ A⇧*" using that by (auto simp: F_def) then show "R N' M'" by (induction p=="(N', M')" arbitrary: N' M' rule: rtrancl_induct) (auto simp: ‹R N M› A_def p) qed have nm_F: "(n N' M' y, m N' M' y) ∈ F" if "y ∈ p N' M'" "(N', M') ∈ F" for N' M' y proof - have *: "((N, M), (N', M')) ∈ A⇧*" using that by (auto simp: F_def) with that show ?thesis apply (simp add: F_def) apply (intro rtrancl.rtrancl_into_rtrancl[OF *]) apply (auto simp: A_def) done qed define Ω where "Ω = (⋃(n, m)∈F. set_pmf (p n m))" have [measurable]: "Ω ∈ sets (count_space UNIV)" by auto have in_Ω: "(N, M) ∈ F ⟹ y ∈ p N M ⟹ y ∈ Ω" for N M y by (auto simp: Ω_def Bex_def) show ?thesis proof (intro stream_space_eq_sstart) from ‹countable F› show "countable Ω" by (auto simp add: Ω_def) show "prob_space N" "prob_space M" "sets N = sets ?S" "sets M = sets ?S" using R_1[OF ‹R N M›] R_2[OF ‹R N M›] by (auto simp add: space_prob_algebra) have "⋀N M. (N, M) ∈ F ⟹ AE x in N. x !! i ∈ Ω" for i proof (induction i) case 0 note NM = 0[THEN R_F, simp] show ?case apply (subst n'_eq[OF NM]) apply (subst AE_bind[where B="?S"]) apply measurable apply (auto intro!: AE_distrD[where f=shd and M'="count_space UNIV"] simp: AE_measure_pmf_iff n[OF NM] n'_shd in_Ω[OF 0] cong: AE_cong_simp) done next case (Suc i) note NM = Suc(2)[THEN R_F, simp] show ?case apply (subst n'_eq[OF NM]) apply (subst AE_bind[where B="?S"]) apply measurable apply (auto intro!: AE_distrD[where f=stl and M'="?S"] Suc(1)[OF nm_F] Suc(2) simp: AE_measure_pmf_iff n'_stl cong: AE_cong_simp) done qed then have AE_N: "⋀N M. (N, M) ∈ F ⟹ AE x in N. x ∈ streams Ω" unfolding streams_iff_snth AE_all_countable by auto then show "AE x in N. x ∈ streams Ω" by (blast intro: F_NM) have "⋀N M. (N, M) ∈ F ⟹ AE x in M. x !! i ∈ Ω" for i proof (induction i arbitrary: N M) case 0 note NM = 0[THEN R_F, simp] show ?case apply (subst m'_eq[OF NM]) apply (subst AE_bind[where B="?S"]) apply measurable apply (auto intro!: AE_distrD[where f=shd and M'="count_space UNIV"] simp: AE_measure_pmf_iff m[OF NM] m'_shd in_Ω[OF 0] cong: AE_cong_simp) done next case (Suc i) note NM = Suc(2)[THEN R_F, simp] show ?case apply (subst m'_eq[OF NM]) apply (subst AE_bind[where B="?S"]) apply measurable apply (auto intro!: AE_distrD[where f=stl and M'="?S"] Suc(1)[OF nm_F] Suc(2) simp: AE_measure_pmf_iff m'_stl cong: AE_cong_simp) done qed then have AE_M: "⋀N M. (N, M) ∈ F ⟹ AE x in M. x ∈ streams Ω" unfolding streams_iff_snth AE_all_countable by auto then show "AE x in M. x ∈ streams Ω" by (blast intro: F_NM) fix xs assume "xs ∈ lists Ω" with ‹(N, M) ∈ F› show "emeasure N (sstart Ω xs) = emeasure M (sstart Ω xs)" proof (induction xs arbitrary: N M) case Nil have "prob_space N" "prob_space M" "sets N = sets ?S" "sets M = sets ?S" using R_1[OF R_F[OF Nil(1)]] R_2[OF R_F[OF Nil(1)]] by (auto simp add: space_prob_algebra) have "emeasure N (streams Ω) = 1" by (rule prob_space.emeasure_eq_1_AE[OF ‹prob_space N› _ AE_N[OF Nil(1)]]) (auto simp add: ‹sets N = sets ?S› intro!: streams_sets) moreover have "emeasure M (streams Ω) = 1" by (rule prob_space.emeasure_eq_1_AE[OF ‹prob_space M› _ AE_M[OF Nil(1)]]) (auto simp add: ‹sets M = sets ?S› intro!: streams_sets) ultimately show ?case by simp next case (Cons x xs) note NM = Cons(2)[THEN R_F, simp] have *: "(##) y -` sstart Ω (x # xs) = (if x = y then sstart Ω xs else {})" for y by auto show ?case apply (subst n'_eq[OF NM]) apply (subst (3) m'_eq[OF NM]) apply (subst emeasure_bind[OF _ _ sstart_sets]) apply simp [] apply measurable [] apply (subst emeasure_bind[OF _ _ sstart_sets]) apply simp [] apply measurable [] apply (intro nn_integral_cong_AE AE_pmfI) apply (subst n'_def) apply (subst m'_def) using Cons(3) apply (auto intro!: Cons nm_F simp add: emeasure_distr sets_eq_imp_space_eq[OF sets_n] sets_eq_imp_space_eq[OF sets_m] space_stream_space *) done qed qed qed subsection ‹Discrete Markov Kernel› locale MC_syntax = fixes K :: "'s ⇒ 's pmf" begin abbreviation acc :: "('s × 's) set" where "acc ≡ (SIGMA s:UNIV. K s)⇧*" abbreviation acc_on :: "'s set ⇒ ('s × 's) set" where "acc_on S ≡ (SIGMA s:UNIV. K s ∩ S)⇧*" lemma countable_reachable: "countable (acc `` {s})" by (auto intro!: countable_rtrancl countable_set_pmf simp: Sigma_Image) lemma countable_acc: "countable X ⟹ countable (acc `` X)" apply (rule countable_Image) apply (rule countable_reachable) apply assumption done context notes [[inductive_internals]] begin coinductive enabled where "enabled (shd ω) (stl ω) ⟹ shd ω ∈ K s ⟹ enabled s ω" end lemma alw_enabled: "enabled (shd ω) (stl ω) ⟹ alw (λω. enabled (shd ω) (stl ω)) ω" by (coinduction arbitrary: ω rule: alw_coinduct) (auto elim: enabled.cases) abbreviation "S ≡ stream_space (count_space UNIV)" lemma in_S [measurable (raw)]: "x ∈ space S" by (simp add: space_stream_space) inductive_simps enabled_iff: "enabled s ω" lemma enabled_Stream: "enabled x (y ## ω) ⟷ y ∈ K x ∧ enabled y ω" by (subst enabled_iff) auto lemma measurable_enabled[measurable]: "Measurable.pred (stream_space (count_space UNIV)) (enabled s)" (is "Measurable.pred ?S _") unfolding enabled_def proof (coinduction arbitrary: s rule: measurable_gfp2_coinduct) case (step A s) then have [measurable]: "⋀t. Measurable.pred ?S (A t)" by auto have *: "⋀x. (∃ω t. s = t ∧ x = ω ∧ A (shd ω) (stl ω) ∧ shd ω ∈ set_pmf (K t)) ⟷ (∃t∈K s. A t (stl x) ∧ t = shd x)" by auto note countable_set_pmf[simp] show ?case unfolding * by measurable qed (auto simp: inf_continuous_def) lemma enabled_iff_snth: "enabled s ω ⟷ (∀i. ω !! i ∈ K ((s ## ω) !! i))" proof safe fix i assume "enabled s ω" then show "ω !! i ∈ K ((s ## ω) !! i)" by (induct i arbitrary: s ω) (force elim: enabled.cases)+ next assume "∀i. ω !! i ∈ set_pmf (K ((s ## ω) !! i))" then show "enabled s ω" by (coinduction arbitrary: s ω) (auto elim: allE[of _ "Suc i" for i] allE[of _ 0]) qed primcorec force_enabled where "force_enabled x ω = (let y = if shd ω ∈ K x then shd ω else (SOME y. y ∈ K x) in y ## force_enabled y (stl ω))" lemma force_enabled_in_set_pmf[simp, intro]: "shd (force_enabled x ω) ∈ K x" by (auto simp: some_in_eq set_pmf_not_empty) lemma enabled_force_enabled: "enabled x (force_enabled x ω)" by (coinduction arbitrary: x ω) (auto simp: some_in_eq set_pmf_not_empty) lemma force_enabled: "enabled x ω ⟹ force_enabled x ω = ω" by (coinduction arbitrary: x ω) (auto elim: enabled.cases) lemma Ex_enabled: "∃ω. enabled x ω" by (rule exI[of _ "force_enabled x undefined"] enabled_force_enabled)+ lemma measurable_force_enabled: "force_enabled x ∈ measurable S S" proof (rule measurable_stream_space2) fix n show "(λω. force_enabled x ω !! n) ∈ measurable S (count_space UNIV)" proof (induction n arbitrary: x) case (Suc n) show ?case apply simp apply (rule measurable_compose_countable'[OF measurable_compose[OF measurable_stl Suc], where I="set_pmf (K x)"]) apply (rule measurable_compose[OF measurable_shd]) apply (auto simp: countable_set_pmf some_in_eq set_pmf_not_empty) done qed (auto intro!: measurable_compose[OF measurable_shd]) qed abbreviation "D ≡ stream_space (Π⇩M s∈UNIV. K s)" lemma sets_D: "sets D = sets (stream_space (Π⇩M s∈UNIV. count_space UNIV))" by (intro sets_stream_space_cong sets_PiM_cong) simp_all lemma space_D: "space D = space (stream_space (Π⇩M s∈UNIV. count_space UNIV))" using sets_eq_imp_space_eq[OF sets_D] . lemma measurable_D_D: "measurable D D = measurable (stream_space (Π⇩M s∈UNIV. count_space UNIV)) (stream_space (Π⇩M s∈UNIV. count_space UNIV))" by (simp add: measurable_def space_D sets_D) primcorec walk :: "'s ⇒ ('s ⇒ 's) stream ⇒ 's stream" where "shd (walk s ω) = (if shd ω s ∈ K s then shd ω s else (SOME t. t ∈ K s))" | "stl (walk s ω) = walk (if shd ω s ∈ K s then shd ω s else (SOME t. t ∈ K s)) (stl ω)" lemma enabled_walk: "enabled s (walk s ω)" by (coinduction arbitrary: s ω) (auto simp: some_in_eq set_pmf_not_empty) lemma measurable_walk[measurable]: "walk s ∈ measurable D S" proof - note measurable_compose[OF measurable_snth, intro!] note measurable_compose[OF measurable_component_singleton, intro!] note if_weak_cong[cong del] note measurable_g = measurable_compose_countable'[OF _ _ countable_reachable] define n :: nat where "n = 0" define g where "g = (λ_::('s ⇒ 's) stream. s)" then have "g ∈ measurable D (count_space (acc `` {s}))" by auto then have "(λx. walk (g x) (sdrop n x)) ∈ measurable D S" proof (coinduction arbitrary: g n rule: measurable_stream_coinduct) case (shd g) show ?case by (fastforce intro: measurable_g[OF _ shd]) next case (stl g) show ?case by (fastforce simp add: sdrop.simps[symmetric] some_in_eq set_pmf_not_empty simp del: sdrop.simps intro: rtrancl_into_rtrancl measurable_g[OF _ stl]) qed then show ?thesis by (simp add: g_def n_def) qed subsection ‹Trace Space for Discrete-Time Markov Chains› definition T :: "'s ⇒ 's stream measure" where "T s = distr (stream_space (Π⇩M s∈UNIV. K s)) S (walk s)" lemma space_T[simp]: "space (T s) = space S" by (simp add: T_def) lemma sets_T[simp, measurable_cong]: "sets (T s) = sets S" by (simp add: T_def) lemma measurable_T1[simp]: "measurable (T s) M = measurable S M" by (intro measurable_cong_sets) simp_all lemma measurable_T2[simp]: "measurable M (T s) = measurable M S" by (intro measurable_cong_sets) simp_all lemma in_measurable_T1[measurable (raw)]: "f ∈ measurable S M ⟹ f ∈ measurable (T s) M" by simp lemma in_measurable_T2[measurable (raw)]: "f ∈ measurable M S ⟹ f ∈ measurable M (T s)" by simp lemma AE_T_enabled: "AE ω in T s. enabled s ω" unfolding T_def by (simp add: AE_distr_iff enabled_walk) sublocale T: prob_space "T s" for s proof - interpret P: product_prob_space K UNIV .. interpret prob_space "stream_space (Π⇩M s∈UNIV. K s)" by (rule P.prob_space_stream_space) fix s show "prob_space (T s)" by (simp add: T_def prob_space_distr) qed lemma emeasure_T_const[simp]: "emeasure (T s) (space S) = 1" using T.emeasure_space_1[of s] by simp lemma nn_integral_T: assumes f[measurable]: "f ∈ borel_measurable S" shows "(∫⇧+X. f X ∂T s) = (∫⇧+t. (∫⇧+ω. f (t ## ω) ∂T t) ∂K s)" proof - interpret product_prob_space K UNIV .. interpret D: prob_space "stream_space (Π⇩M s∈UNIV. K s)" by (rule prob_space_stream_space) have T: "⋀f s. f ∈ borel_measurable S ⟹ (∫⇧+X. f X ∂T s) = (∫⇧+ω. f (walk s ω) ∂D)" by (simp add: T_def nn_integral_distr) have "(∫⇧+X. f X ∂T s) = (∫⇧+ω. f (walk s ω) ∂D)" by (rule T) measurable also have "… = (∫⇧+d. ∫⇧+ω. f (walk s (d ## ω)) ∂D ∂Π⇩M i∈UNIV. K i)" by (simp add: P.nn_integral_stream_space) also have "… = (∫⇧+d. (∫⇧+ω. f (d s ## walk (d s) ω) * indicator {t. t ∈ K s} (d s) ∂D) ∂Π⇩M i∈UNIV. K i)" apply (rule nn_integral_cong_AE) apply (subst walk.ctr) apply (simp add: frequently_def cong del: if_weak_cong) apply (auto simp: AE_measure_pmf_iff intro: AE_component) done also have "… = (∫⇧+d. ∫⇧+ω. f (d s ## ω) * indicator (K s) (d s) ∂T (d s) ∂Π⇩M i∈UNIV. K i)" by (subst T) (simp_all split: split_indicator) also have "… = (∫⇧+t. ∫⇧+ω. f (t ## ω) * indicator (K s) t ∂T t ∂K s)" by (subst (2) PiM_component[symmetric]) (simp_all add: nn_integral_distr) also have "… = (∫⇧+t. ∫⇧+ω. f (t ## ω) ∂T t ∂K s)" by (rule nn_integral_cong_AE) (simp add: AE_measure_pmf_iff) finally show ?thesis . qed lemma nn_integral_T_gfp: fixes g defines "l ≡ λf ω. g (shd ω) (f (stl ω))" assumes [measurable]: "case_prod g ∈ borel_measurable (count_space UNIV ⨂⇩M borel)" assumes cont_g[THEN inf_continuous_compose, order_continuous_intros]: "⋀s. inf_continuous (g s)" assumes int_g: "⋀f s. f ∈ borel_measurable S ⟹ (∫⇧+ω. g s (f ω) ∂T s) = g s (∫⇧+ω. f ω ∂T s)" assumes bnd_g: "⋀f s. g s f ≤ b" "0 ≤ b" "b < ∞" shows "(∫⇧+ω. gfp l ω ∂T s) = gfp (λf s. ∫⇧+t. g t (f t) ∂K s) s" proof (rule nn_integral_gfp) show "⋀s. sets (T s) = sets S" "⋀F. F ∈ borel_measurable S ⟹ l F ∈ borel_measurable S" by (auto simp: l_def) show "⋀s. emeasure (T s) (space (T s)) ≠ 0" by (rewrite T.emeasure_space_1) simp { fix s F have "integral⇧N (T s) (l F) ≤ (∫⇧+x. b ∂T s)" by (intro nn_integral_mono) (simp add: l_def bnd_g) also have "… < ∞" using bnd_g by simp finally show "integral⇧N (T s) (l F) < ∞" . } show "inf_continuous (λf s. ∫⇧+ t. g t (f t) ∂K s)" proof (intro order_continuous_intros) fix f s have "(∫⇧+ t. g t (f t) ∂K s) ≤ (∫⇧+ t. b ∂K s)" by (intro nn_integral_mono bnd_g) also have "… < ∞" using bnd_g by simp finally show "(∫⇧+ t. g t (f t) ∂K s) ≠ ∞" by simp qed simp next fix s and F :: "'s stream ⇒ ennreal" assume "F ∈ borel_measurable S" then show "integral⇧N (T s) (l F) = (∫⇧+ t. g t (integral⇧N (T t) F) ∂K s) " by (rewrite nn_integral_T) (simp_all add: l_def int_g) qed (auto intro!: order_continuous_intros simp: l_def) lemma nn_integral_T_lfp: fixes g defines "l ≡ λf ω. g (shd ω) (f (stl ω))" assumes [measurable]: "case_prod g ∈ borel_measurable (count_space UNIV ⨂⇩M borel)" assumes cont_g[THEN sup_continuous_compose, order_continuous_intros]: "⋀s. sup_continuous (g s)" assumes int_g: "⋀f s. f ∈ borel_measurable S ⟹ (∫⇧+ω. g s (f ω) ∂T s) = g s (∫⇧+ω. f ω ∂T s)" shows "(∫⇧+ω. lfp l ω ∂T s) = lfp (λf s. ∫⇧+t. g t (f t) ∂K s) s" proof (rule nn_integral_lfp) show "⋀s. sets (T s) = sets S" "⋀F. F ∈ borel_measurable S ⟹ l F ∈ borel_measurable S" by (auto simp: l_def) next fix s and F :: "'s stream ⇒ ennreal" assume "F ∈ borel_measurable S" then show "integral⇧N (T s) (l F) = (∫⇧+ t. g t (integral⇧N (T t) F) ∂K s) " by (rewrite nn_integral_T) (simp_all add: l_def int_g) qed (auto simp: l_def intro!: order_continuous_intros) lemma emeasure_Collect_T: assumes f[measurable]: "Measurable.pred S P" shows "emeasure (T s) {x∈space (T s). P x} = (∫⇧+t. emeasure (T t) {x∈space (T t). P (t ## x)} ∂K s)" apply (subst (1 2) nn_integral_indicator[symmetric]) apply simp apply simp apply (subst nn_integral_T) apply (auto intro!: nn_integral_cong simp add: space_stream_space indicator_def) done lemma AE_T_iff: assumes [measurable]: "Measurable.pred S P" shows "(AE ω in T x. P ω) ⟷ (∀y∈K x. AE ω in T y. P (y ## ω))" by (simp add: AE_iff_nn_integral nn_integral_T[where s=x]) (auto simp add: nn_integral_0_iff_AE AE_measure_pmf_iff split: split_indicator) lemma AE_T_alw: assumes [measurable]: "Measurable.pred S P" assumes P: "⋀s. (x, s) ∈ acc ⟹ AE ω in T s. P ω" shows "AE ω in T x. alw P ω" proof - define F where "F = (λp x. P x ∧ p (stl x))" have [measurable]: "⋀p. Measurable.pred S p ⟹ Measurable.pred S (F p)" by (auto simp: F_def) have "almost_everywhere (T s) ((F ^^ i) top)" if "(x, s) ∈ acc" for i s using that proof (induction i arbitrary: s) case (Suc i) then show ?case apply simp apply (subst F_def) apply (simp add: P) apply (subst AE_T_iff) apply (measurable; simp) apply (auto dest: rtrancl_into_rtrancl) done qed simp then have "almost_everywhere (T x) (gfp F)" by (subst inf_continuous_gfp) (auto simp: inf_continuous_def AE_all_countable F_def) then show ?thesis by (simp add: alw_def F_def) qed lemma emeasure_suntil_disj: assumes [measurable]: "Measurable.pred S P" assumes *: "⋀t. AE ω in T t. ¬ (P ⊓ (HLD X ⊓ nxt (HLD X suntil P))) ω" shows "emeasure (T s) {ω∈space (T s). (HLD X suntil P) ω} = lfp (λF s. emeasure (T s) {ω∈space (T s). P ω} + (∫⇧+t. F t * indicator X t ∂K s)) s" unfolding suntil_lfp proof (rule emeasure_lfp[where s=s]) fix F t assume [measurable]: "Measurable.pred (T s) F" and F: "F ≤ lfp (λa b. P b ∨ HLD X b ∧ a (stl b))" have "emeasure (T t) {ω ∈ space (T s). P ω ∨ HLD X ω ∧ F (stl ω)} = emeasure (T t) {ω ∈ space (T t). P ω} + emeasure (T t) {ω∈space (T t). HLD X ω ∧ F (stl ω)}" proof (rule emeasure_add_AE) show "AE x in T t. ¬ (x ∈ {ω ∈ space (T t). P ω} ∧ x ∈ {ω ∈ space (T t). HLD X ω ∧ F (stl ω)})" using * by eventually_elim (insert F, auto simp: suntil_lfp[symmetric]) qed auto also have "emeasure (T t) {ω∈space (T t). HLD X ω ∧ F (stl ω)} = (∫⇧+t. emeasure (T t) {ω ∈ space (T s). F ω} * indicator X t ∂K t)" by (subst emeasure_Collect_T) (auto intro!: nn_integral_cong split: split_indicator) finally show "emeasure (T t) {ω ∈ space (T s). P ω ∨ HLD X ω ∧ F (stl ω)} = emeasure (T t) {ω ∈ space (T t). P ω} + (∫⇧+ t. emeasure (T t) {ω ∈ space (T s). F ω} * indicator X t ∂K t)" . qed (auto intro!: order_continuous_intros split: split_indicator) lemma emeasure_HLD_nxt: assumes [measurable]: "Measurable.pred S P" shows "emeasure (T s) {ω∈space (T s). (X ⋅ P) ω} = (∫⇧+x. emeasure (T x) {ω∈space (T x). P ω} * indicator X x ∂K s)" by (subst emeasure_Collect_T) (auto intro!: nn_integral_cong_AE simp: AE_measure_pmf_iff split: split_indicator) lemma emeasure_HLD: "emeasure (T s) {ω∈space (T s). HLD X ω} = emeasure (K s) X" using emeasure_HLD_nxt[of "λω. True" s X] T.emeasure_space_1 by simp lemma emeasure_suntil_HLD: assumes [measurable]: "Measurable.pred S P" shows "emeasure (T s) {x∈space (T s). (not (HLD {t}) suntil (HLD {t} aand nxt P)) x} = emeasure (T s) {x∈space (T s). ev (HLD {t}) x} * emeasure (T t) {x∈space (T t). P x}" proof - let ?P = "emeasure (T t) {ω∈space (T t). P ω}" let ?F = "λQ F s. emeasure (T s) {ω∈space (T s). Q ω} + (∫⇧+t'. F t' * indicator (- {t}) t' ∂K s)" have "emeasure (T s) {x∈space (T s). (HLD (-{t}) suntil ({t} ⋅ P)) x} = lfp (?F ({t} ⋅ P)) s" by (rule emeasure_suntil_disj) (auto simp: HLD_iff) also have "lfp (?F ({t} ⋅ P)) = (λs. lfp (?F (HLD {t})) s * ?P)" proof (rule lfp_transfer[symmetric, where α="λx s. x s * emeasure (T t) {ω∈space (T t). P ω}"]) fix F show "(λs. ?F (HLD {t}) F s * ?P) = ?F ({t} ⋅ P) (λs. F s * ?P)" unfolding emeasure_HLD emeasure_HLD_nxt[OF assms] distrib_right by (auto simp: fun_eq_iff nn_integral_multc[symmetric] intro!: arg_cong2[where f="(+)"] nn_integral_cong ac_simps split: split_indicator) qed (auto intro!: order_continuous_intros sup_continuous_mono lfp_upperbound intro: le_funI add_nonneg_nonneg simp: bot_ennreal split: split_indicator) also have "lfp (?F (HLD {t})) s = emeasure (T s) {x∈space (T s). (HLD (-{t}) suntil HLD {t}) x}" by (rule emeasure_suntil_disj[symmetric]) (auto simp: HLD_iff) finally show ?thesis by (simp add: HLD_iff[abs_def] ev_eq_suntil) qed lemma AE_suntil: assumes [measurable]: "Measurable.pred S P" shows "(AE x in T s. (not (HLD {t}) suntil (HLD {t} aand nxt P)) x) ⟷ (AE x in T s. ev (HLD {t}) x) ∧ (AE x in T t. P x)" apply (subst (1 2 3) T.prob_Collect_eq_1[symmetric]) apply simp apply simp apply simp apply (simp_all add: measure_def emeasure_suntil_HLD del: space_T nxt.simps) apply (auto simp: T.emeasure_eq_measure mult_eq_1) done subsection ‹Fairness› definition fair :: "'s ⇒ 's ⇒ 's stream ⇒ bool" where "fair s t = alw (ev (HLD {s})) impl alw (ev (HLD {s} aand nxt (HLD {t})))" lemma AE_T_fair: assumes "t' ∈ K t" shows "AE ω in T s. fair t t' ω" proof - let ?M = "λP s. emeasure (T s) {ω∈space (T s). P ω}" let ?t = "HLD {t}" and ?t' = "HLD {t'}" define N where "N = alw (ev ?t) aand alw (not (?t aand nxt ?t'))" let ?until = "not ?t suntil (?t aand nxt (not ?t' aand nxt N))" have N_stl: "⋀ω. N ω ⟹ N (stl ω)" by (auto simp: N_def) have [measurable]: "Measurable.pred S N" unfolding N_def by measurable let ?c = "pmf (K t) t'" let ?R = "λx. 1 ⊓ x * (1 - ennreal ?c)" have "mono ?R" by (intro monoI mult_right_mono inf_mono) (auto simp: mono_def field_simps ) have "⋀s. ?M N s ≤ gfp ?R" proof (induction rule: gfp_ordinal_induct[OF ‹mono ?R›]) fix x s assume x: "⋀s. ?M N s ≤ x" { fix ω assume "N ω" then have "ev (HLD {t}) ω" "N ω" by (auto simp: N_def) then have "?until ω" by (induct rule: ev_induct_strong) (auto simp: N_def intro: suntil.intros dest: N_stl) } then have "?M N s ≤ ?M ?until s" by (intro emeasure_mono_AE) auto also have "… = ?M (ev ?t) s * ?M (not ?t' aand nxt N) t" by (simp_all add: emeasure_suntil_HLD del: nxt.simps space_T) also have "… ≤ ?M (ev ?t) s * (∫⇧+s'. 1 ⊓ x * indicator (UNIV - {t'}) s' ∂K t)" by (auto intro!: mult_left_mono nn_integral_mono T.measure_le_1 emeasure_mono split: split_indicator simp add: x emeasure_Collect_T[of _ t] simp del: space_T) also have "… ≤ 1 * (∫⇧+s'. 1 ⊓ x * indicator (UNIV - {t'}) s' ∂K t)" by (intro mult_right_mono T.measure_le_1) simp finally show "?M N s ≤ 1 ⊓ x * (1 - ennreal ?c)" by (subst (asm) nn_integral_cmult_indicator) (auto simp: emeasure_Diff emeasure_pmf_single) qed (auto intro: Inf_greatest) also from ‹mono ?R› have "gfp ?R = ?R (gfp ?R)" by (rule gfp_unfold) then have "gfp ?R ≤ ?R (gfp ?R)" by simp with assms[THEN pmf_positive] have "gfp ?R ≤ 0" by (cases "gfp ?R") (auto simp: top_unique inf_ennreal.rep_eq field_simps mult_le_0_iff ennreal_1[symmetric] pmf_le_1 ennreal_minus ennreal_mult[symmetric] ennreal_le_iff2 inf_min min_def simp del: ennreal_1 split: if_split_asm) finally have "⋀s. AE ω in T s. ¬ N ω" by (subst AE_iff_measurable[OF _ refl]) (auto intro: antisym simp: le_fun_def) then have "AE ω in T s. alw (not N) ω" by (intro AE_T_alw) auto moreover { fix ω assume "alw (ev (HLD {t})) ω" then have "alw (alw (ev (HLD {t}))) ω" unfolding alw_alw . moreover assume "alw (not N) ω" then have "alw (alw (ev (HLD {t})) impl ev (HLD {t} aand nxt (HLD {t'}))) ω" unfolding N_def not_alw_iff not_ev_iff de_Morgan_disj de_Morgan_conj not_not imp_conv_disj . ultimately have "alw (ev (HLD {t} aand nxt (HLD {t'}))) ω" by (rule alw_mp) } then have "∀ω. alw (not N) ω ⟶ fair t t' ω" by (auto simp: fair_def) ultimately show ?thesis by (simp add: eventually_mono) qed lemma enabled_imp_trancl: assumes "alw (HLD B) ω" "enabled s ω" shows "alw (HLD (acc_on B `` {s})) ω" proof - define t where "t = s" then have "(s, t) ∈ acc_on B" by auto moreover note ‹alw (HLD B) ω› moreover note ‹enabled s ω›[unfolded ‹t == s›[symmetric]] ultimately show ?thesis proof (coinduction arbitrary: t ω rule: alw_coinduct) case stl from this(1,2,3) show ?case by (auto simp: enabled.simps[of _ ω] alw.simps[of _ ω] HLD_iff intro!: exI[of _ "shd ω"] rtrancl_trans[of s t]) next case (alw t ω) then show ?case by (auto simp: HLD_iff enabled.simps[of _ ω] alw.simps[of _ ω] intro!: rtrancl_trans[of s t]) qed qed lemma AE_T_reachable: "AE ω in T s. alw (HLD (acc `` {s})) ω" using AE_T_enabled proof eventually_elim fix ω assume "enabled s ω" from enabled_imp_trancl[of UNIV, OF _ this] show "alw (HLD (acc `` {s})) ω" by (auto simp: HLD_iff[abs_def] all_imp_alw) qed lemma AE_T_all_fair: "AE ω in T s. ∀(t,t')∈SIGMA t:UNIV. K t. fair t t' ω" proof - let ?Rn = "SIGMA s:(acc `` {s}). K s" have "AE ω in T s. ∀(t,t')∈?Rn. fair t t' ω" proof (subst AE_ball_countable) show "countable ?Rn" by (intro countable_SIGMA countable_rtrancl[OF countable_Image]) (auto simp: Image_def) qed (auto intro!: AE_T_fair) then show ?thesis using AE_T_reachable proof (eventually_elim, safe) fix ω t t' assume "∀(t,t')∈?Rn. fair t t' ω" "t' ∈ K t" and alw: "alw (HLD (acc `` {s})) ω" moreover { assume "t ∉ acc `` {s}" then have "alw (not (HLD {t})) ω" by (intro alw_mono[OF alw]) (auto simp: HLD_iff) then have "not (alw (ev (HLD {t}))) ω" unfolding not_alw_iff not_ev_iff by auto then have "fair t t' ω" unfolding fair_def by auto } ultimately show "fair t t' ω" by auto qed qed lemma fair_imp: assumes "fair t t' ω" "alw (ev (HLD {t})) ω" shows "alw (ev (HLD {t'})) ω" proof - { fix ω assume "ev (HLD {t} aand nxt (HLD {t'})) ω" then have "ev (HLD {t'}) ω" by induction auto } with assms show ?thesis by (auto simp: fair_def elim!: alw_mp intro: all_imp_alw) qed lemma AE_T_ev_HLD: assumes exiting: "⋀t. (s, t) ∈ acc_on (-B) ⟹ ∃t'∈B. (t, t') ∈ acc" assumes fin: "finite (acc_on (-B) `` {s})" shows "AE ω in T s. ev (HLD B) ω" using AE_T_all_fair AE_T_enabled proof eventually_elim fix ω assume fair: "∀(t, t')∈(SIGMA s:UNIV. K s). fair t t' ω" and "enabled s ω" show "ev (HLD B) ω" proof (rule ccontr) assume "¬ ev (HLD B) ω" then have "alw (HLD (- B)) ω" by (simp add: not_ev_iff HLD_iff[abs_def]) from enabled_imp_trancl[OF this ‹enabled s ω›] have "alw (HLD (acc_on (-B) `` {s})) ω" by (simp add: Diff_eq) from pigeonhole_stream[OF this fin] obtain t where "(s, t) ∈ acc_on (-B)" "alw (ev (HLD {t})) ω" by auto from exiting[OF this(1)] obtain t' where "(t, t') ∈ acc" "t' ∈ B" by auto from this(1) have "alw (ev (HLD {t'})) ω" proof induction case (step u w) then show ?case using fair fair_imp[of u w ω] by auto qed fact { assume "ev (HLD {t'}) ω" then have "ev (HLD B) ω" by (rule ev_mono) (auto simp: HLD_iff ‹t' ∈ B›) } then show False using ‹alw (ev (HLD {t'})) ω› ‹¬ ev (HLD B) ω› by auto qed qed lemma AE_T_ev_HLD': assumes exiting: "⋀s. s ∉ X ⟹ ∃t∈X. (s, t) ∈ acc" assumes fin: "finite (-X)" shows "AE ω in T s. ev (HLD X) ω" proof (rule AE_T_ev_HLD) show "⋀t. (s, t) ∈ acc_on (- X) ⟹ ∃t'∈X. (t, t') ∈ acc" using exiting by (auto elim: rtrancl.cases) have "acc_on (- X) `` {s} ⊆ -X ∪ {s}" by (auto elim: rtrancl.cases) with fin show "finite (acc_on (- X) `` {s})" by (auto dest: finite_subset ) qed lemma AE_T_max_sfirst: assumes [measurable]: "Measurable.pred S X" assumes AE: "AE ω in T c. sfirst X (c ## ω) < ∞" and "0 < e" shows "∃N::nat. 𝒫(ω in T c. N < sfirst X (c ## ω)) < e" (is "∃N. ?P N < e") proof - have "?P ⇢ measure (T c) (⋂N::nat. {bT ∈ space (T c). N < sfirst X (c ## bT)})" using dual_order.strict_trans enat_ord_simps(2) by (intro T.finite_Lim_measure_decseq) (force simp: decseq_Suc_iff simp del: enat_ord_simps)+ also have "measure (T c) (⋂N::nat. {bT ∈ space (T c). N < sfirst X (c ## bT)}) = 𝒫(bT in T c. sfirst X (c ## bT) = ∞)" by (auto simp del: not_infinity_eq intro!: arg_cong[where f="measure (T c)"]) (metis less_irrefl not_infinity_eq) also have "𝒫(bT in T c. sfirst X (c ## bT) = ∞) = 0" using AE by (intro T.prob_eq_0_AE) auto finally have "∃N. ∀n≥N. norm (?P n - 0) < e" using ‹0 < e› by (rule LIMSEQ_D) then show ?thesis by (auto simp: measure_nonneg) qed subsection ‹First Hitting Time› lemma nn_integral_sfirst_finite': assumes "s ∉ H" assumes [simp]: "finite (acc_on (-H) `` {s})" assumes until: "AE ω in T s. ev (HLD H) ω" shows "(∫⇧+ ω. sfirst (HLD H) ω ∂T s) ≠ ∞" proof - have R_ne[simp]: "acc_on (-H) `` {s} ≠ {}" by auto have [measurable]: "H ∈ sets (count_space UNIV)" by simp let ?Pf = "λn t. 𝒫(ω in T t. enat n < sfirst (HLD H) (t ## ω))" have Pf_mono: "⋀N n t. N ≤ n ⟹ ?Pf n t ≤ ?Pf N t" by (auto intro!: T.finite_measure_mono simp del: enat_ord_code(1) simp: enat_ord_code(1)[symmetric]) have not_H: "⋀t. (s, t) ∈ acc_on (-H) ⟹ t ∉ H" using ‹s ∉ H› by (auto elim: rtrancl.cases) have "∀⇩F n in sequentially. ∀t∈acc_on (-H)``{s}. ?Pf n t < 1" proof (safe intro!: eventually_ball_finite) fix t assume "(s, t) ∈ acc_on (-H)" then have "AE ω in T t. sfirst (HLD H) (t ## ω) < ∞" unfolding sfirst_finite proof induction case (step t u) with step.IH show ?case by (subst (asm) AE_T_iff) (auto simp: ev_Stream not_H) qed (simp add: ev_Stream eventually_frequently_simps until) from AE_T_max_sfirst[OF _ this, of 1] obtain N where "?Pf N t < 1" by auto with Pf_mono[of N] show "∀⇩F n in sequentially. ?Pf n t < 1" by (auto simp: eventually_sequentially intro: le_less_trans) qed simp then obtain n where "⋀t. (s, t) ∈ acc_on (-H) ⟹ ?Pf n t < 1" by (auto simp: eventually_sequentially) moreover define d where "d = Max (?Pf n ` acc_on (-H) `` {s})" ultimately have d: "0 ≤ d" "d < 1" "⋀t. (s, t) ∈ acc_on (-H) ⟹ ?Pf (Suc n) t ≤ d" using Pf_mono[of n "Suc n"] by (auto simp: Max_ge_iff measure_nonneg) let ?F = "λF ω. if shd ω ∈ H then 0 else F (stl ω) + 1 :: ennreal" have "sup_continuous ?F" by (intro order_continuous_intros) then have "mono ?F" by (rule sup_continuous_mono) have lfp_nonneg[simp]: "⋀ω. 0 ≤ lfp ?F ω" by (subst lfp_unfold[OF ‹mono ?F›]) auto let ?I = "λF s. ∫⇧+t. (if t ∈ H then 0 else F t + 1) ∂K s" have "sup_continuous ?I" by (intro order_continuous_intros) auto then have "mono ?I" by (rule sup_continuous_mono) define p where "p = Suc n / (1 - d)" have p: "p = Suc n + d * p" unfolding p_def using d(1,2) by (auto simp: field_simps) have [simp]: "0 ≤ p" using d(1,2) by (auto simp: p_def) have "(∫⇧+ ω. sfirst (HLD H) ω ∂T s) = (∫⇧+ ω. lfp ?F ω ∂T s)" proof (intro nn_integral_cong_AE) show "AE x in T s. sfirst (HLD H) x = lfp ?F x" using until proof eventually_elim fix ω assume "ev (HLD H) ω" then show "sfirst (HLD H) ω = lfp ?F ω" by (induction rule: ev_induct_strong; subst lfp_unfold[OF ‹mono ?F›], simp add: HLD_iff[abs_def] ac_simps max_absorb2) qed qed also have "… = lfp (?I^^Suc n) s" unfolding lfp_funpow[OF ‹mono ?I›] by (subst nn_integral_T_lfp) (auto simp: nn_integral_add max_absorb2 intro!: order_continuous_intros) also have "lfp (?I^^Suc n) t ≤ p" if "(s, t) ∈ acc_on (-H)" for t using that proof (induction arbitrary: t rule: lfp_ordinal_induct[of "?I^^Suc n"]) case (step S) have "(?I^^i) S t ≤ i + ?Pf i t * ennreal p" for i using step(3) proof (induction i arbitrary: t) case 0 then show ?case using T.prob_space step(1) by (auto simp add: zero_ennreal_def[symmetric] not_H zero_enat_def[symmetric] one_ennreal_def[symmetric]) next case (Suc i) then have "t ∉ H" by (auto simp: not_H) from Suc.prems have "⋀t'. t' ∈ K t ⟹ t' ∉ H ⟹ (s, t') ∈ acc_on (-H)" by (rule rtrancl_into_rtrancl) (insert Suc.prems, auto dest: not_H) then have "(?I ^^ Suc i) S t ≤ ?I (λt. i + ennreal (?Pf i t) * p) t" by (auto simp: AE_measure_pmf_iff simp del: sfirst_eSuc space_T intro!: nn_integral_mono_AE add_mono max.mono Suc) also have "… ≤ (∫⇧+ t. ennreal (Suc i) + ennreal 𝒫(ω in T t. enat i < sfirst (HLD H) (t ## ω)) * p ∂K t)" by (intro nn_integral_mono) auto also have "… ≤ Suc i + ennreal (?Pf (Suc i) t) * p" unfolding T.emeasure_eq_measure[symmetric] by (subst (2) emeasure_Collect_T) (auto simp: ‹t ∉ H› eSuc_enat[symmetric] nn_integral_add nn_integral_multc ennreal_of_nat_eq_real_of_nat) finally show ?case by (simp add: ennreal_of_nat_eq_real_of_nat) qed then have "(?I^^Suc n) S t ≤ Suc n + ?Pf (Suc n) t * ennreal p" . also have "… ≤ p" using d step by (subst (2) p) (auto intro!: mult_right_mono simp: ennreal_of_nat_eq_real_of_nat ennreal_mult) finally show ?case . qed (auto simp: SUP_least intro!: mono_pow ‹mono ?I› simp del: funpow.simps) finally show ?thesis unfolding p_def by (auto simp: top_unique) qed lemma nn_integral_sfirst_finite: assumes [simp]: "finite (acc_on (-H) `` {s})" assumes until: "AE ω in T s. ev (HLD H) ω" shows "(∫⇧+ ω. sfirst (HLD H) (s ## ω) ∂T s) ≠ ∞" proof cases assume "s ∉ H" then show ?thesis using nn_integral_sfirst_finite'[of s H] until by (simp add: nn_integral_add) qed (simp add: sfirst.simps) lemma prob_T: assumes P: "Measurable.pred S P" shows "𝒫(ω in T s. P ω) = (∫t. 𝒫(ω in T t. P (t ## ω)) ∂K s)" using emeasure_Collect_T[OF P, of s] unfolding T.emeasure_eq_measure by (subst (asm) nn_integral_eq_integral) (auto intro!: measure_pmf.integrable_const_bound[where B=1]) lemma T_subprob[measurable]: "T ∈ measurable (measure_pmf I) (subprob_algebra S)" by (auto intro!: space_bind simp: space_subprob_algebra) unfold_locales subsection ‹Markov chain with Initial Distribution› definition T' :: "'s pmf ⇒ 's stream measure" where "T' I = bind I (λs. distr (T s) S ((##) s))" lemma distr_Stream_subprob: "(λs. distr (T s) S ((##) s)) ∈ measurable (measure_pmf I) (subprob_algebra S)" apply (intro measurable_distr2[OF _ T_subprob]) apply (subst measurable_cong_sets[where M'="count_space UNIV ⨂⇩M S" and N'=S]) apply (rule sets_pair_measure_cong) apply auto done lemma sets_T': "sets (T' I) = sets S" by (simp add: T'_def) lemma prob_space_T': "prob_space (T' I)" unfolding T'_def proof (rule measure_pmf.prob_space_bind) show "AE s in I. prob_space (distr (T s) S ((##) s))" by (intro AE_measure_pmf_iff[THEN iffD2] ballI T.prob_space_distr) simp qed (rule distr_Stream_subprob) lemma AE_T': assumes [measurable]: "Measurable.pred S P" shows "(AE x in T' I. P x) ⟷ (∀s∈I. AE x in T s. P (s ## x))" unfolding T'_def by (simp add: AE_bind[OF distr_Stream_subprob] AE_measure_pmf_iff AE_distr_iff) lemma emeasure_T': assumes [measurable]: "X ∈ sets S" shows "emeasure (T' I) X = (∫⇧+s. emeasure (T s) {ω∈space S. s ## ω ∈ X} ∂I)" unfolding T'_def by (simp add: emeasure_bind[OF _ distr_Stream_subprob] emeasure_distr vimage_def Int_def conj_ac) lemma prob_T': assumes [measurable]: "Measurable.pred S P" shows "𝒫(x in T' I. P x) = (∫s. 𝒫(x in T s. P (s ## x)) ∂I)" proof - interpret T': prob_space "T' I" by (rule prob_space_T') show ?thesis using emeasure_T'[of "{x∈space (T' I). P x}" I] unfolding T'.emeasure_eq_measure T.emeasure_eq_measure sets_eq_imp_space_eq[OF sets_T'] apply simp apply (subst (asm) nn_integral_eq_integral) apply (auto intro!: measure_pmf.integrable_const_bound[where B=1] integral_cong arg_cong2[where f=measure] simp: AE_measure_pmf measure_nonneg space_stream_space) done qed lemma T_eq_T': "T s = T' (K s)" proof (rule measure_eqI) fix X assume X: "X ∈ sets (T s)" then have [measurable]: "X ∈ sets S" by simp have X_eq: "X = {x∈space (T s). x ∈ X}" using sets.sets_into_space[OF X] by auto show "emeasure (T s) X = emeasure (T' (K s)) X" apply (subst X_eq) apply (subst emeasure_Collect_T, simp) apply (subst emeasure_T', simp) apply simp done qed (simp add: sets_T') lemma T_eq_bind: "T s = (measure_pmf (K s) ⤜ (λt. distr (T t) S ((##) t)))" by (subst T_eq_T') (simp add: T'_def) lemma T_split: "T s = (T s ⤜ (λω. distr (T ((s ## ω) !! n)) S (λω'. stake n ω @- ω')))" proof (induction n arbitrary: s) case 0 then show ?case apply (simp add: distr_cong[OF refl sets_T[symmetric, of s] refl]) apply (subst bind_const') apply unfold_locales .. next case (Suc n) let ?K = "measure_pmf (K s)" and ?m = "λn ω ω'. stake n ω @- ω'" note sets_stream_space_cong[simp, measurable_cong] have "T s = (?K ⤜ (λt. distr (T t) S ((##) t)))" by (rule T_eq_bind) also have "… = (?K ⤜ (λt. distr (T t ⤜ (λω. distr (T ((t ## ω) !! n)) S (?m n ω))) S ((##) t)))" unfolding Suc[symmetric] .. also have "… = (?K ⤜ (λt. T t ⤜ (λω. distr (distr (T ((t ## ω) !! n)) S (?m n ω)) S ((##) t))))" by (simp add: distr_bind[where K=S, OF measurable_distr2[where M=S]] space_stream_space) also have "… = (?K ⤜ (λt. T t ⤜ (λω. distr (T ((t ## ω) !! n)) S (?m (Suc n) (t ## ω)))))" by (simp add: distr_distr space_stream_space comp_def) also have "… = (?K ⤜ (λt. distr (T t) S ((##) t) ⤜ (λω. distr (T (ω !! n)) S (?m (Suc n) ω))))" by (simp add: space_stream_space bind_distr[OF _ measurable_distr2[where M=S]] del: stake.simps) also have "… = (T s ⤜ (λω. distr (T (ω !! n)) S (?m (Suc n) ω)))" unfolding T_eq_bind[of s] by (subst bind_assoc[OF measurable_distr2[where M=S] measurable_distr2[where M=S], OF _ T_subprob]) (simp_all add: space_stream_space del: stake.simps) finally show ?case by simp qed lemma nn_integral_T_split: assumes f[measurable]: "f ∈ borel_measurable S" shows "(∫⇧+ω. f ω ∂T s) = (∫⇧+ω. (∫⇧+ω'. f (stake n ω @- ω') ∂T ((s ## ω) !! n)) ∂T s)" apply (subst T_split[of s n]) apply (simp add: nn_integral_bind[OF f measurable_distr2[where M=S]]) apply (subst nn_integral_distr) apply (simp_all add: space_stream_space) done lemma emeasure_T_split: assumes P[measurable]: "Measurable.pred S P" shows "emeasure (T s) {ω∈space (T s). P ω} = (∫⇧+ω. emeasure (T ((s ## ω) !! n)) {ω'∈space (T ((s ## ω) !! n)). P (stake n ω @- ω')} ∂T s)" apply (subst T_split[of s n]) apply (subst emeasure_bind[OF _ measurable_distr2[where M=S]]) apply (simp_all add: ) apply (simp add: space_stream_space) apply (subst emeasure_distr) apply simp_all apply (simp_all add: space_stream_space) done lemma prob_T_split: assumes P[measurable]: "Measurable.pred S P" shows "𝒫(ω in T s. P ω) = (∫ω. 𝒫(ω' in T ((s ## ω) !! n). P (stake n ω @- ω')) ∂T s)" using emeasure_T_split[OF P, of s n] unfolding T.emeasure_eq_measure by (subst (asm) nn_integral_eq_integral) (auto intro!: T.integrable_const_bound[where B=1] measure_measurable_subprob_algebra2[where N=S] simp: T.emeasure_eq_measure SIGMA_Collect_eq) lemma enabled_imp_alw: "(⋃s∈X. set_pmf (K s)) ⊆ X ⟹ x ∈ X ⟹ enabled x ω ⟹ alw (HLD X) ω" proof (coinduction arbitrary: ω x) case alw then show ?case unfolding enabled.simps[of _ ω] by (auto simp: HLD_iff) qed lemma alw_HLD_iff_sconst: "alw (HLD {x}) ω ⟷ ω = sconst x" proof assume "alw (HLD {x}) ω" then show "ω = sconst x" by (coinduction arbitrary: ω) (auto simp: HLD_iff) qed (auto simp: alw_sconst HLD_iff) lemma enabled_iff_sconst: assumes [simp]: "set_pmf (K x) = {x}" shows "enabled x ω ⟷ ω = sconst x" proof assume "enabled x ω" then show "ω = sconst x" by (coinduction arbitrary: ω) (auto elim: enabled.cases) next assume "ω = sconst x" then show "enabled x ω" by (coinduction arbitrary: ω) auto qed lemma AE_sconst: assumes [simp]: "set_pmf (K x) = {x}" shows "(AE ω in T x. P ω) ⟷ P (sconst x)" proof - have "(AE ω in T x. P ω) ⟷ (AE ω in T x. P ω ∧ ω = sconst x)" using AE_T_enabled[of x] by (simp add: enabled_iff_sconst) also have "… = (AE ω in T x. P (sconst x) ∧ ω = sconst x)" by (simp del: AE_conj_iff cong: rev_conj_cong) also have "… = (AE ω in T x. P (sconst x))" using AE_T_enabled[of x] by (simp add: enabled_iff_sconst) finally show ?thesis by simp qed lemma ev_eq_lfp: "ev P = lfp (λF ω. P ω ∨ (¬ P ω ∧ F (stl ω)))" unfolding ev_def by (intro antisym lfp_mono) blast+ lemma INF_eq_zero_iff_ennreal: "((⨅i∈A. f i) = (0::ennreal)) = (∀x>0. ∃i∈A. f i < x)" using INF_eq_bot_iff[where 'a=ennreal] unfolding bot_ennreal_def zero_ennreal_def by auto lemma inf_continuous_cmul: fixes c :: ennreal assumes f: "inf_continuous f" and c: "c < ⊤" shows "inf_continuous (λx. c * f x)" proof (rule inf_continuous_compose[OF _ f], clarsimp simp add: inf_continuous_def) fix M :: "nat ⇒ ennreal" assume M: "decseq M" show "c * (⨅i. M i) = (⨅i. c * M i)" using M by (intro LIMSEQ_unique[OF ennreal_tendsto_cmult[OF c] LIMSEQ_INF] LIMSEQ_INF) (auto simp: decseq_def mult_left_mono) qed lemma AE_T_ev_HLD_infinite: fixes X :: "'s set" and r :: real assumes "r < 1" assumes r: "⋀x. x ∈ X ⟹ measure (K x) X ≤ r" shows "AE ω in T x. ev (HLD (- X)) ω" proof - { fix x assume "x ∈ X" have "0 ≤ r" using r[OF ‹x ∈ X›] measure_nonneg[of "K x" X] by (blast intro: order.trans) define P where "P F x = ∫⇧+y. indicator X y * (F y ⊓ 1) ∂K x" for F x have [measurable]: "X ∈ sets (count_space UNIV)" by auto have bnd: "(∫⇧+ y. indicator X y * (f y ⊓ 1) ∂K x) ≤ 1" for x f by (intro measure_pmf.nn_integral_le_const AE_pmfI) (auto split: split_indicator) have "emeasure (T x) {ω∈space (T x). alw (HLD X) ω} = emeasure (T x) {ω∈space (T x). gfp (λF ω. shd ω ∈ X ∧ F (stl ω)) ω}" by (simp add: alw_def HLD_def) also have "… = gfp P x" apply (rule emeasure_gfp) apply (auto intro!: order_continuous_intros inf_continuous_cmul split: split_indicator simp: P_def) subgoal for x f using bnd[of x f] by (auto simp: top_unique) subgoal for P x apply (subst T_eq_bind) apply (subst emeasure_bind[where N=S]) apply simp apply (rule measurable_distr2[where M=S]) apply (auto intro: T_subprob[THEN measurable_space] intro!: nn_integral_cong_AE AE_pmfI simp: emeasure_distr split: split_indicator) apply (simp_all add: space_stream_space T.emeasure_le_1 inf.absorb1) done apply (intro le_funI) apply (subst nn_integral_indicator[symmetric]) apply simp apply (intro nn_integral_mono) apply (auto split: split_indicator) done also have "… ≤ (INF n. ennreal r ^ n)" proof (intro INF_greatest) have mono_P: "mono P" by (force simp: le_fun_def mono_def P_def intro!: nn_integral_mono intro: le_infI1 split: split_indicator) fix n show "gfp P x ≤ ennreal r ^ n" using ‹x ∈ X› proof (induction n arbitrary: x) case 0 then show ?case by (subst gfp_unfold[OF mono_P]) (auto intro!: measure_pmf.nn_integral_le_const AE_pmfI split: split_indicator simp: P_def) next case (Suc n x) have "gfp P x = P (gfp P) x" by (subst gfp_unfold[OF mono_P]) rule also have "… ≤ P (λx. ennreal r ^ n) x" unfolding P_def[of _ x] by (auto intro!: nn_integral_mono le_infI1 Suc split: split_indicator) also have "… ≤ ennreal r ^ (Suc n)" using Suc by (auto simp: P_def nn_integral_multc measure_pmf.emeasure_eq_measure intro!: mult_mono ennreal_leI r) finally show ?case . qed qed also have "… = 0" unfolding ennreal_power[OF ‹0 ≤ r›] proof (intro LIMSEQ_unique[OF LIMSEQ_INF]) show "decseq (λi. ennreal (r ^ i))" using ‹0 ≤ r› ‹r < 1› by (auto intro!: ennreal_leI power_decreasing simp: decseq_def) have "(λi. ennreal (r ^ i)) ⇢ ennreal 0" using ‹0 ≤ r› ‹r < 1› by (intro tendsto_ennrealI LIMSEQ_power_zero) auto then show "(λi. ennreal (r ^ i)) ⇢ 0" by simp qed finally have *: "emeasure (T x) {ω∈space (T x). alw (HLD X) ω} = 0" by auto have "AE ω in T x. ev (HLD (- X)) ω" by (rule AE_I[OF _ *]) (auto simp: not_ev_iff not_HLD[symmetric]) } note * = this show ?thesis apply (clarsimp simp add: AE_T_iff[of _ x]) subgoal for x' by (cases "x' ∈ X") (auto simp add: ev_Stream *) done qed subsection ‹Trace space with Restriction› definition "rT x = restrict_space (T x) {ω. enabled x ω}" lemma space_rT: "ω ∈ space (rT x) ⟷ enabled x ω" by (auto simp: rT_def space_restrict_space space_stream_space) lemma Collect_enabled_S[measurable]: "Collect (enabled x) ∈ sets S" proof - have "Collect (enabled x) = {ω∈space S. enabled x ω}" by (auto simp: space_stream_space) then show ?thesis by simp qed lemma space_rT_in_S: "space (rT x) ∈ sets S" by (simp add: rT_def space_restrict_space) lemma sets_rT: "A ∈ sets (rT x) ⟷ A ∈ sets S ∧ A ⊆ {ω. enabled x ω}" by (auto simp: rT_def sets_restrict_space space_stream_space) lemma prob_space_rT: "prob_space (rT x)" unfolding rT_def by (auto intro!: prob_space_restrict_space T.emeasure_eq_1_AE AE_T_enabled) lemma measurable_force_enabled2[measurable]: "force_enabled x ∈ measurable S (rT x)" unfolding rT_def by (rule measurable_restrict_space2) (auto intro: measurable_force_enabled enabled_force_enabled) lemma space_rT_not_empty[simp]: "space (rT x) ≠ {}" by (simp add: rT_def space_restrict_space Ex_enabled) lemma T_eq_bind': "T x = do { y ← measure_pmf (K x) ; ω ← T y ; return S (y ## ω) }" apply (subst T_eq_bind) apply (subst bind_return_distr[symmetric]) apply (simp_all add: space_stream_space comp_def) done lemma rT_eq_bind: "rT x = do { y ← measure_pmf (K x) ; ω ← rT y ; return (rT x) (y ## ω) }" unfolding rT_def apply (subst T_eq_bind) apply (subst restrict_space_bind[where K=S]) apply (rule measurable_distr2[where M=S]) apply (auto simp del: measurable_pmf_measure1 simp add: Ex_enabled return_restrict_space intro!: bind_cong ) apply (subst restrict_space_bind[symmetric, where K=S]) apply (auto simp add: Ex_enabled space_restrict_space return_cong[OF sets_T] intro!: measurable_restrict_space1 measurable_compose[OF _ return_measurable] arg_cong2[where f=restrict_space]) apply (subst bind_return_distr[unfolded comp_def]) apply (simp add: space_restrict_space Ex_enabled) apply (simp add: measurable_restrict_space1) apply (rule measure_eqI) apply simp apply (subst (1 2) emeasure_distr) apply (auto simp: measurable_restrict_space1) apply (subst emeasure_restrict_space) apply (auto simp: space_restrict_space intro!: emeasure_eq_AE) using AE_T_enabled apply eventually_elim apply (simp add: space_stream_space) apply (rule sets_Int_pred) apply auto apply (simp add: space_stream_space) done lemma snth_rT: "(λx. x !! n) ∈ measurable (rT x) (count_space (acc `` {x}))" proof - have "⋀ω. enabled x ω ⟹ (x, ω !! n) ∈ acc" proof (induction n arbitrary: x) case (Suc n) from Suc.prems Suc.IH[of "shd ω" "stl ω"] show ?case by (auto simp: enabled.simps[of x ω] intro: rtrancl_trans) qed (auto elim: enabled.cases) moreover { fix X :: "'s set" have [measurable]: "X ∈ count_space UNIV" by simp have *: "(λx. x !! n) -` X ∩ space (rT x) = {ω∈space S. ω !! n ∈ X ∧ enabled x ω}" by (auto simp: space_stream_space space_rT) have "(λx. x !! n) -` X ∩ space (rT x) ∈ sets S" unfolding * by measurable } ultimately show ?thesis by (auto simp: measurable_def space_rT sets_rT) qed subsection ‹Bisimulation› lemma T_coinduct[consumes 1, case_names prob sets cont]: assumes "R x M" assumes prob: "⋀x M. R x M ⟹ prob_space M" and sets: "⋀x M. R x M ⟹ sets M = sets S" and cont': "⋀x M. R x M ⟹ ∃M'. (∀y∈K x. R y (M' y)) ∧ (∀y. sets (M' y) = S ∧ prob_space (M' y)) ∧ M = (measure_pmf (K x) ⤜ (λy. distr (M' y) S ((##) y)))" shows "T x = M" using ‹R x M› proof (coinduction arbitrary: x M rule: measure_eq_stream_space_coinduct) case left then show ?case using T.prob_space_axioms[of x] sets_T[of x] by (auto simp: space_prob_algebra) next case (right M) with prob[of M] sets[of M] show ?case by (auto simp: space_prob_algebra) next case (cont x M) with cont'[OF cont] obtain M' where *: "(∀y∈K x. R y (M' y))" "(∀y. sets (M' y) = S ∧ prob_space (M' y))" "M = (measure_pmf (K x) ⤜ (λy. distr (M' y) S ((##) y)))" by auto show ?case apply (rule exI[of _ T]) apply (rule exI[of _ M']) apply (rule exI[of _ "K x"]) using * T.prob_space_axioms sets_T[of x] apply (auto simp: space_prob_algebra intro: T_eq_bind) done qed lemma T_bisim: assumes M: "⋀x. prob_space (M x)" "⋀x. sets (M x) = sets S" and M_eq: "⋀x. M x = (measure_pmf (K x) ⤜ (λs. distr (M s) S ((##) s)))" shows "T = M" proof fix x show "T x = M x" proof (coinduction arbitrary: x rule: T_coinduct) case (cont x) then show ?case apply (intro exI[of _ M]) apply (subst M_eq[of x]) apply (simp add: M) done qed fact+ qed lemma T_subprob'[measurable]: "T ∈ measurable (count_space UNIV) (subprob_algebra S)" by (auto intro!: space_bind simp: space_subprob_algebra) unfold_locales lemma T_subprob''[simp]: "T a ∈ space (subprob_algebra S)" using measurable_space[OF T_subprob', of a] by simp lemma AE_not_suntil_coinduct [consumes 1, case_names ψ φ]: assumes "P s" assumes ψ: "⋀s. P s ⟹ s ∉ ψ" assumes φ: "⋀s t. P s ⟹ s ∈ φ ⟹ t ∈ K s ⟹ P t" shows "AE ω in T s. not (HLD φ suntil HLD ψ) (s ## ω)" proof - { fix ω have "¬ (HLD φ suntil HLD ψ) (s ## ω) ⟷ (∀n. ¬ ((λR. HLD ψ or (HLD φ aand nxt R)) ^^ n) ⊥ (s ## ω))" unfolding suntil_def by (subst sup_continuous_lfp) (auto simp add: sup_continuous_def) } moreover { fix n from ‹P s› have "AE ω in T s. ¬ ((λR. HLD ψ or (HLD φ aand nxt R)) ^^ n) ⊥ (s ## ω)" proof (induction n arbitrary: s) case (Suc n) then show ?case apply (subst AE_T_iff) apply (rule measurable_compose[OF measurable_Stream, where M1="count_space UNIV"]) apply measurable apply simp apply (auto simp: bot_fun_def intro!: AE_impI dest: φ ψ) done qed simp } ultimately show ?thesis by (simp add: AE_all_countable) qed lemma AE_not_suntil_coinduct_strong [consumes 1, case_names ψ φ]: assumes "P s" assumes P_ψ: "⋀s. P s ⟹ s ∉ ψ" assumes P_φ: "⋀s t. P s ⟹ s ∈ φ ⟹ t ∈ K s ⟹ P t ∨ (AE ω in T t. not (HLD φ suntil HLD ψ) (t ## ω))" shows "AE ω in T s. not (HLD φ suntil HLD ψ) (s ## ω)" (is "?nuntil s") proof - have "P s ∨ ?nuntil s" using ‹P s› by auto then show ?thesis proof (coinduction arbitrary: s rule: AE_not_suntil_coinduct) case (φ t s) then show ?case by (auto simp: AE_T_iff[of _ s] suntil_Stream[of _ _ s] dest: P_φ) qed (auto simp: suntil_Stream dest: P_ψ) qed end subsection ‹Reward Structure on Markov Chains› locale MC_with_rewards = MC_syntax K for K :: "'s ⇒ 's pmf" + fixes ι :: "'s ⇒ 's ⇒ ennreal" and ρ :: "'s ⇒ ennreal" assumes ι_nonneg: "⋀s t. 0 ≤ ι s t" and ρ_nonneg: "⋀s. 0 ≤ ρ s" assumes measurable_ι[measurable]: "(λ(a, b). ι a b) ∈ borel_measurable (count_space UNIV ⨂⇩M count_space UNIV)" begin definition reward_until :: "'s set ⇒ 's ⇒ 's stream ⇒ ennreal" where "reward_until X = lfp (λF s ω. if s ∈ X then 0 else ρ s + ι s (shd ω) + (F (shd ω) (stl ω)))" lemma measurable_ρ[measurable]: "ρ ∈ borel_measurable (count_space UNIV)" by simp lemma measurable_reward_until[measurable (raw)]: assumes [measurable]: "f ∈ measurable M (count_space UNIV)" assumes [measurable]: "g ∈ measurable M S" shows "(λx. reward_until X (f x) (g x)) ∈ borel_measurable M" proof - let ?F = "λF (s, ω). if s ∈ X then 0 else ρ s + ι s (shd ω) + (F (shd ω, stl ω))" { fix s ω have "reward_until X s ω = lfp ?F (s, ω)" unfolding reward_until_def lfp_pair[symmetric] .. } note * = this have [measurable]: "lfp ?F ∈ borel_measurable (count_space UNIV ⨂⇩M S)" proof (rule borel_measurable_lfp) fix f :: "('s × 's stream) ⇒ ennreal" assume [measurable]: "f ∈ borel_measurable (count_space UNIV ⨂⇩M S)" show "?F f ∈ borel_measurable (count_space UNIV ⨂⇩M S)" unfolding split_beta' apply (intro measurable_If) apply measurable [] apply measurable [] apply (rule predE) apply (rule measurable_compose[OF measurable_fst]) apply measurable [] done qed (auto intro!: ι_nonneg ρ_nonneg order_continuous_intros) show ?thesis unfolding * by measurable qed lemma continuous_reward_until: "sup_continuous (λF s ω. if s ∈ X then 0 else ρ s + ι s (shd ω) + (F (shd ω) (stl ω)))" by (intro ι_nonneg ρ_nonneg order_continuous_intros) (auto simp: sup_continuous_def image_comp) lemma shows reward_until_unfold: "reward_until X s ω = (if s ∈ X then 0 else ρ s + ι s (shd ω) + reward_until X (shd ω) (stl ω))" (is ?unfold) proof - let ?F = "λF s ω. if s ∈ X then 0 else ρ s + ι s (shd ω) + (F (shd ω) (stl ω))" { fix s ω have "reward_until X s ω = ?F (reward_until X) s ω" unfolding reward_until_def apply (subst lfp_unfold) apply (rule continuous_reward_until[THEN sup_continuous_mono, of X]) apply rule done } note step = this show ?unfold by (subst step) (auto intro!: arg_cong2[where f="(+)"]) qed lemma reward_until_simps[simp]: shows "s ∈ X ⟹ reward_until X s ω = 0" and "s ∉ X ⟹ reward_until X s ω = ρ s + ι s (shd ω) + reward_until X (shd ω) (stl ω)" unfolding reward_until_unfold[of X s ω] by simp_all lemma reward_until_SCons[simp]: "reward_until X s (t ## ω) = (if s ∈ X then 0 else ρ s + ι s t + reward_until X t ω)" by simp lemma nn_integral_reward_until_finite: assumes [simp]: "finite (acc `` {s})" (is "finite (?R `` {s})") assumes ρ: "⋀t. (s, t) ∈ acc_on (-H) ⟹ ρ t < ∞" assumes ι: "⋀t t'. (s, t) ∈ acc_on (-H) ⟹ t' ∈ K t ⟹ ι t t' < ∞" assumes ev: "AE ω in T s. ev (HLD H) ω" shows "(∫⇧+ ω. reward_until H s ω ∂T s) ≠ ∞" proof cases assume "s ∈ H" then show ?thesis by simp next assume "s ∉ H" let ?L = "acc_on (-H)" define M where "M = Max ((λ(s, t). ρ s + ι s t) ` (SIGMA t:?L``{s}. K t))" have "?L ⊆ ?R" by (intro rtrancl_mono) auto with ‹s ∉ H› have subset: "(SIGMA t:?L``{s}. K t) ⊆ (?R``{s} × ?R``{s})" by (auto intro: rtrancl_into_rtrancl elim: rtrancl.cases) then have [simp, intro!]: "finite ((λ(s, t). ρ s + ι s t) ` (SIGMA t:?L``{s}. K t))" by (intro finite_imageI) (auto dest: finite_subset) { fix t t' assume "(s, t) ∈ ?L" "t ∉ H" "t' ∈ K t" then have "(t, t') ∈ (SIGMA t:?L``{s}. K t)" by (auto intro: rtrancl_into_rtrancl) then have "ρ t + ι t t' ≤ M" unfolding M_def by (intro Max_ge) auto } note le_M = this have fin_L: "finite (?L `` {s})" by (intro finite_subset[OF _ assms(1)] Image_mono ‹?L ⊆ ?R› order_refl) have "M < ∞" unfolding M_def proof (subst Max_less_iff, safe) show "(SIGMA x:?L `` {s}. set_pmf (K x)) = {} ⟹ False" using ‹s ∉ H› by (auto simp add: Sigma_empty_iff set_pmf_not_empty) fix t t' assume "(s, t) ∈ ?L" "t' ∈ K t" then show "ρ t + ι t t' < ∞" using ρ[of t] ι[of t t'] by simp qed from set_pmf_not_empty[of "K s"] obtain t where "t ∈ K s" by auto with le_M[of s t] have "0 ≤ M" using set_pmf_not_empty[of "K s"] ‹s ∉ H› le_M[of s] ι_nonneg[of s] ρ_nonneg[of s] by (intro order_trans[OF _ le_M]) auto have "AE ω in T s. reward_until H s ω ≤ M * sfirst (HLD H) (s ## ω)" using ev AE_T_enabled proof eventually_elim fix ω assume "ev (HLD H) ω" "enabled s ω" moreover define t where "t = s" ultimately have "ev (HLD H) ω" "enabled t ω" "t ∈ ?L``{s}" by auto then show "reward_until H t ω ≤ M * sfirst (HLD H) (t ## ω)" proof (induction arbitrary: t rule: ev_induct_strong) case (base ω t) then show ?case by (auto simp: HLD_iff sfirst_Stream elim: enabled.cases intro: le_M) next case (step ω t) from step.IH[of "shd ω"] step.prems step.hyps show ?case by (auto simp add: HLD_iff enabled.simps[of t] distrib_left sfirst_Stream reward_until_simps[of t] simp del: reward_until_simps intro!: add_mono le_M intro: rtrancl_into_rtrancl) qed qed then have "(∫⇧+ω. reward_until H s ω ∂T s) ≤ (∫⇧+ω. M * sfirst (HLD H) (s ## ω) ∂T s)" by (rule nn_integral_mono_AE) also have "… < ∞" using ‹0 ≤ M› ‹M < ∞› nn_integral_sfirst_finite[OF fin_L ev] by (simp add: nn_integral_cmult less_top[symmetric] ennreal_mult_eq_top_iff) finally show ?thesis by simp qed end subsection ‹Bisimulation on a relation› definition rel_set_strong :: "('a ⇒ 'b ⇒ bool) ⇒ 'a set ⇒ 'b set ⇒ bool" where "rel_set_strong R A B ⟷ (∀x y. R x y ⟶ (x ∈ A ⟷ y ∈ B))" lemma T_eq_rel_half[consumes 4, case_names prob sets cont]: fixes R :: "'s ⇒ 't ⇒ bool" and f :: "'s ⇒ 't" and S :: "'s set" assumes R_def: "⋀s t. R s t ⟷ (s ∈ S ∧ f s = t)" assumes A[measurable]: "A ∈ sets (stream_space (count_space UNIV))" and B[measurable]: "B ∈ sets (stream_space (count_space UNIV))" and AB: "rel_set_strong (stream_all2 R) A B" and KL: "rel_fun R (rel_pmf R) K L" and xy: "R x y" shows "MC_syntax.T K x A = MC_syntax.T L y B" proof - interpret K: MC_syntax K by unfold_locales interpret L: MC_syntax L by unfold_locales have "x ∈ S" using ‹R x y› by (auto simp: R_def) define g where "g t = (SOME s. R s t)" for t have measurable_g: "g ∈ count_space UNIV →⇩M count_space UNIV" by auto have g: "R i j ⟹ R (g j) j" for i j unfolding g_def by (rule someI) have K_subset: "x ∈ S ⟹ K x ⊆ S" for x using KL[THEN rel_funD, of x "f x", THEN rel_pmf_imp_rel_set] by (auto simp: rel_set_def R_def) have in_S: "AE ω in K.T x. ω ∈ streams S" using K.AE_T_enabled proof eventually_elim case (elim ω) with ‹x ∈ S› show ?case apply (coinduction arbitrary: x ω) subgoal for x ω using K_subset by (cases ω) (auto simp: K.enabled_Stream) done qed have L_eq: "L y = map_pmf f (K x)" if xy: "R x y" for x y proof - have "rel_pmf (λx y. x = y) (map_pmf f (K x)) (L y)" using KL[THEN rel_funD, OF xy] by (auto intro: pmf.rel_mono_strong simp: R_def pmf.rel_map) then show ?thesis unfolding pmf.rel_eq by simp qed let ?D = "λx. distr (K.T x) K.S (smap f)" have prob_space_D: "?D x ∈ space (prob_algebra K.S)" for x by (auto simp: space_prob_algebra K.T.prob_space_distr) have D_eq_D: "?D x = ?D x'" if "R x y" "R x' y" for x x' y proof (rule stream_space_eq_sstart) define A where "A = K.acc `` {x, x'}" have x_A: "x ∈ A" "x' ∈ A" by (auto simp: A_def) let ?Ω = "f ` A" show "countable ?Ω" unfolding A_def by (intro countable_image K.countable_acc) auto show "prob_space (?D x)" "prob_space (?D x')" by (auto intro!: K.T.prob_space_distr) show "sets (?D x) = sets L.S" "sets (?D x') = sets L.S" by auto have AE_streams: "AE x in ?D x''. x ∈ streams ?Ω" if "x'' ∈ A" for x'' apply (simp add: space_stream_space streams_sets AE_distr_iff) using K.AE_T_reachable[of x''] unfolding alw_HLD_iff_streams proof eventually_elim fix s assume "s ∈ streams (K.acc `` {x''})" moreover have "K.acc `` {x''} ⊆ A" using ‹x'' ∈ A› by (auto simp: A_def Image_def intro: rtrancl_trans) ultimately show "smap f s ∈ streams (f ` A)" by (auto intro: smap_streams) qed with x_A show "AE x in ?D x'. x ∈ streams ?Ω" "AE x in ?D x. x ∈ streams ?Ω" by auto from ‹x ∈ A› ‹x' ∈ A› that show "?D x (sstart (f ` A) xs) = ?D x' (sstart (f ` A) xs)" for xs proof (induction xs arbitrary: x x' y) case Nil moreover have "?D x (streams (f ` A)) = 1" if "x ∈ A" for x using AE_streams[of x] that by (intro prob_space.emeasure_eq_1_AE[OF K.T.prob_space_distr]) (auto simp: streams_sets) ultimately show ?case by simp next case (Cons z zs x x' y) have "rel_pmf (R OO R¯¯) (K x) (K x')" using KL[THEN rel_funD, OF Cons(4)] KL[THEN rel_funD, OF Cons(5)] unfolding pmf.rel_compp pmf.rel_flip by auto then obtain p :: "('s × 's) pmf" where p: "⋀a b. (a, b) ∈ p ⟹ (R OO R¯¯) a b" and eq: "map_pmf fst p = K x" "map_pmf snd p = K x'" by (auto simp: pmf.in_rel) let ?S = "stream_space (count_space UNIV)" have *: "(##) y -` smap f -` sstart (f ` A) (z # zs) = (if f y = z then smap f -` sstart (f ` A) zs else {})" for y z zs by auto have **: "?D x (sstart (f ` A) (z # zs)) = (∫⇧+ y'. (if f y' = z then ?D y' (sstart (f ` A) zs) else 0) ∂K x)" for x apply (simp add: emeasure_distr) apply (subst K.T_eq_bind) apply (subst emeasure_bind[where N="?S"]) apply simp apply (rule measurable_distr2[where M="?S"]) apply measurable apply (intro nn_integral_cong_AE AE_pmfI) apply (auto simp add: emeasure_distr) apply (simp_all add: * space_stream_space) done have fst_A: "fst ab ∈ A" if "ab ∈ p" for ab proof - have "fst ab ∈ K x" using ‹ab ∈ p› set_map_pmf [of fst p] by (auto simp: eq) with ‹x ∈ A› show "fst ab ∈ A" by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl) qed have snd_A: "snd ab ∈ A" if "ab ∈ p" for ab proof - have "snd ab ∈ K x'" using ‹ab ∈ p› set_map_pmf [of snd p] by (auto simp: eq) with ‹x' ∈ A› show "snd ab ∈ A" by (auto simp: A_def intro: rtrancl.rtrancl_into_rtrancl) qed show ?case unfolding ** eq[symmetric] nn_integral_map_pmf apply (intro nn_integral_cong_AE AE_pmfI) subgoal for ab using p[of "fst ab" "snd ab"] by (auto simp: R_def intro!: Cons(1) fst_A snd_A) done qed qed have L_eq_D: "L.T y = ?D x" using ‹R x y› proof (coinduction arbitrary: x y rule: L.T_coinduct) case (cont x y) then have Kx_Ly: "rel_pmf R (K x) (L y)" by (rule KL[THEN rel_funD]) then have *: "y' ∈ L y ⟹ ∃x'∈K x. R x' y'" for y' by (auto dest!: rel_pmf_imp_rel_set simp: rel_set_def) have **: "y' ∈ L y ⟹ R (g y') y'" for y' using *[of y'] unfolding g_def by (auto intro: someI) have D_SCons_eq_D_D: "distr (K.T i) K.S (λx. z ## smap f x) = distr (?D i) K.S (λx. z ## x)" for i z by (subst distr_distr) (auto simp: comp_def) have D_eq_D_gi: "?D i = ?D (g (f i))" if i: "i ∈ K x" for i proof - obtain j where "j ∈ L y" "R i j" "f i = j" using Kx_Ly i by (force dest!: rel_pmf_imp_rel_set simp: rel_set_def R_def) then show ?thesis by (auto intro!: D_eq_D[OF ‹R i j›] g) qed have ***: "?D x = measure_pmf (L y) ⤜ (λy. distr (?D (g y)) K.S ((##) y))" apply (subst K.T_eq_bind) apply (subst distr_bind[of _ _ K.S]) apply (rule measurable_distr2[of _ _ "K.S"]) apply (simp_all add: Pi_iff) apply (simp add: distr_distr comp_def L_eq[OF cont] map_pmf_rep_eq) apply (subst bind_distr[where K=K.S]) apply measurable [] apply (rule measurable_distr2[of _ _ "K.S"]) apply measurable [] apply (rule measurable_compose[OF measurable_g]) apply measurable [] apply simp apply (rule bind_measure_pmf_cong[where N="K.S"]) apply (auto simp: space_subprob_algebra space_stream_space intro!: K.T.subprob_space_distr) unfolding D_SCons_eq_D_D D_eq_D_gi .. show ?case by (intro exI[of _ "λt. distr (K.T (g t)) (stream_space (count_space UNIV)) (smap f)"]) (auto simp add: K.T.prob_space_distr *** dest: **) qed (auto intro: K.T.prob_space_distr) have "stream_all2 R s t ⟷ (s ∈ streams S ∧ smap f s = t)" for s t proof safe show "stream_all2 R s t ⟹ s ∈ streams S" apply (coinduction arbitrary: s t) subgoal for s t by (cases s; cases t) (auto simp: R_def) done show "stream_all2 R s t ⟹ smap f s = t" apply (coinduction arbitrary: s t) subgoal for s t by (cases s; cases t) (auto simp: R_def) done qed (auto intro!: stream.rel_refl_strong simp: stream.rel_map R_def streams_iff_sset) then have "ω ∈ streams S ⟹ ω ∈ A ⟷ smap f ω ∈ B" for ω using AB by (auto simp: rel_set_strong_def) with in_S have "K.T x A = K.T x (smap f -` B ∩ space (K.T x))" by (auto intro!: emeasure_eq_AE streams_sets) also have "… = (distr (K.T x) K.S (smap f)) B" by (intro emeasure_distr[symmetric]) auto also have "… = (L.T y) B" unfolding L_eq_D .. finally show ?thesis . qed subsection ‹Product Construction› locale MC_pair = K1: MC_syntax K1 + K2: MC_syntax K2 for K1 K2 begin definition "Kp ≡ λ(a, b). pair_pmf (K1 a) (K2 b)" sublocale MC_syntax Kp . definition "szip⇩E a b ≡ λ(ω1, ω2). szip (K1.force_enabled a ω1) (K2.force_enabled b ω2)" lemma szip_rT[measurable]: "(λ(ω1, ω2). szip ω1 ω2) ∈ measurable (K1.rT x1 ⨂⇩M K2.rT x2) S" proof (rule measurable_stream_space2) fix n have "(λx. (case x of (ω1, ω2) ⇒ szip ω1 ω2) !! n) = (λω. (fst ω !! n, snd ω !! n))" by auto also have "… ∈ measurable (K1.rT x1 ⨂⇩M K2.rT x2) (count_space UNIV)" apply (rule measurable_compose_countable'[OF _ measurable_compose[OF measurable_fst K1.snth_rT, of n]]) apply (rule measurable_compose_countable'[OF _ measurable_compose[OF measurable_snd K2.snth_rT, of n]]) apply (auto intro!: K1.countable_acc K2.countable_acc) done finally show "(λx. (case x of (ω1, ω2) ⇒ szip ω1 ω2) !! n) ∈ measurable (K1.rT x1 ⨂⇩M K2.rT x2) (count_space UNIV)" . qed lemma measurable_szipE[measurable]: "szip⇩E a b ∈ measurable (K1.S ⨂⇩M K2.S) S" unfolding szip⇩E_def by measurable lemma T_eq_prod: "T = (λ(x1, x2). do { ω1 ← K1.T x1 ; ω2 ← K2.T x2 ; return S (szip⇩E x1 x2 (ω1, ω2)) })" (is "_ = ?B") proof (rule T_bisim) have T1x: "⋀x. subprob_space (K1.T x)" by (rule prob_space_imp_subprob_space) unfold_locales interpret T12: pair_prob_space "K1.T x" "K2.T y" for x y by unfold_locales interpret T1K2: pair_prob_space "K1.T x" "K2 y" for x y by unfold_locales let ?P = "λx1 x2. K1.T x1 ⨂⇩M K2.T x2" fix x show "prob_space (?B x)" by (auto simp: space_stream_space split: prod.splits intro!: prob_space.prob_space_bind prob_space_return measurable_bind[where N=S] measurable_compose[OF _ return_measurable] AE_I2) unfold_locales show "sets (?B x) = sets S" by (simp split: prod.splits add: measurable_bind[where N=S] sets_bind[where N=S] space_stream_space) obtain a b where x_eq: "x = (a, b)" by (cases x) auto show "?B x = (measure_pmf (Kp x) ⤜ (λs. distr (?B s) S ((##) s)))" unfolding x_eq apply (subst K1.T_eq_bind') apply (subst K2.T_eq_bind') apply (auto simp add: space_stream_space bind_assoc[where R=S and N=S] bind_return_distr[symmetric] Kp_def T1K2.bind_rotate[where N=S] split_beta' set_pair_pmf space_subprob_algebra bind_pair_pmf[of "case_prod M" for M, unfolded split, symmetric, where N=S] szip⇩E_def stream_eq_Stream_iff bind_return[where N=S] space_bind[where N=S] simp del: measurable_pmf_measure1 intro!: bind_measure_pmf_cong[where N=S] subprob_space_bind[where N=S] subprob_space_measure_pmf T1x bind_cong[where M="MC_syntax.T K x" for K x] arg_cong2[where f=return]) done qed lemma nn_integral_pT: fixes f assumes [measurable]: "f ∈ borel_measurable S" shows "(∫⇧+ω. f ω ∂T (x, y)) = (∫⇧+ω1. ∫⇧+ω2. f (szip⇩E x y (ω1, ω2)) ∂K2.T y ∂K1.T x)" by (simp add: nn_integral_bind[where B=S] nn_integral_return in_S T_eq_prod) lemma prod_eq_prob_T: assumes [measurable]: "Measurable.pred K1.S P1" "Measurable.pred K2.S P2" shows "𝒫(ω in K1.T x1. P1 ω) * 𝒫(ω in K2.T x2. P2 ω) = 𝒫(ω in T (x1, x2). P1 (smap fst ω) ∧ P2 (smap snd ω))" proof - have "𝒫(ω in T (x1, x2). P1 (smap fst ω) ∧ P2 (smap snd ω)) = (∫ x. ∫ xa. indicator {ω ∈ space S. P1 (smap fst ω) ∧ P2 (smap snd ω)} (szip⇩E x1 x2 (x, xa)) ∂MC_syntax.T K2 x2 ∂MC_syntax.T K1 x1)" by (subst T_eq_prod) (simp add: K1.T.measure_bind[where N=S] K2.T.measure_bind[where N=S] measure_return) also have "... = (∫ω1. ∫ω2. indicator {ω∈space K1.S. P1 ω} ω1 * indicator {ω∈space K2.S. P2 ω} ω2 ∂K2.T x2 ∂K1.T x1)" apply (intro integral_cong_AE) apply measurable using K1.AE_T_enabled apply eventually_elim apply (intro integral_cong_AE) apply measurable using K2.AE_T_enabled apply eventually_elim apply (auto simp: space_stream_space szip⇩E_def K1.force_enabled K2.force_enabled smap_szip_snd[where g="λx. x"] smap_szip_fst[where f="λx. x"] split: split_indicator) done also have "… = 𝒫(ω in K1.T x1. P1 ω) * 𝒫(ω in K2.T x2. P2 ω)" by simp finally show ?thesis .. qed end end