Theory Discrete_Time_Markov_Chain

(* 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. (yset_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. (yset_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)) 
    (tK 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 sUNIV. K s)"

lemma sets_D: "sets D = sets (stream_space (ΠM sUNIV. count_space UNIV))"
  by (intro sets_stream_space_cong sets_PiM_cong) simp_all

lemma space_D: "space D = space (stream_space (ΠM sUNIV. count_space UNIV))"
  using sets_eq_imp_space_eq[OF sets_D] .

lemma measurable_D_D: "measurable D D =
    measurable (stream_space (ΠM sUNIV. count_space UNIV)) (stream_space (ΠM sUNIV. 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 sUNIV. 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 sUNIV. 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 sUNIV. 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 iUNIV. 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 iUNIV. K i)"
    apply (rule nn_integral_cong_AE)
    apply (subst walk.ctr)
    apply (simp cong del: if_weak_cong)
    apply (intro UNIV_I AE_component)
    apply (auto simp: AE_measure_pmf_iff)
    done
  also have " = (+d. +ω. f (d s ## ω) * indicator (K s) (d s) T (d s) ΠM iUNIV. 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 "integralN (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 "integralN (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 "integralN (T s) (l F) = (+ t. g t (integralN (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 "integralN (T s) (l F) = (+ t. g t (integralN (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) {xspace (T s). P x} = (+t. emeasure (T t) {xspace (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 ω)  (yK 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) {xspace (T s). (not (HLD {t}) suntil (HLD {t} aand nxt P)) x} =
   emeasure (T s) {xspace (T s). ev (HLD {t}) x} * emeasure (T t) {xspace (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) {xspace (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) {xspace (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  tX. (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. nN. 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. tacc_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)  (sI. 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 "{xspace (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 = {xspace (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:
  "(sX. 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: "((iA. f i) = (0::ennreal)) = (x>0. iA. 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