Theory Lib

theory Lib
  imports
    MDP_Aux
    Timed_Automata.Timed_Automata
    Timed_Automata.Approx_Beta
    Finiteness
begin

section ‹Misc›

lemma measurable_pred_stream[measurable]:
  fixes P shows "Measurable.pred (stream_space (count_space UNIV)) (pred_stream P)"
proof -
  have [measurable]: "Measurable.pred (count_space UNIV) P"
    by measurable
  then show ?thesis
    unfolding stream.pred_set sset_range by simp
qed

lemma pmf_map_pmf_cong:
  fixes f g and μ :: "'a pmf"
  assumes " x. x  μ  f x = y1  g x = y2"
  shows "pmf (map_pmf f μ) y1 = pmf (map_pmf g μ) y2"
  unfolding pmf_map
  by (rule measure_pmf.finite_measure_eq_AE;
      simp add: AE_measure_pmf_iff assms split: split_indicator
     )

lemma collect_pair_finite[intro]:
  notes finite_subset[intro]
  assumes "finite {x. P x}" "finite {x. Q x}"
  shows "finite {(x, y) . P x  Q y  R x y}"
using assms
proof -
  from assms have "finite {(x, y) . P x  Q y}" by auto
  moreover have "{(x, y) . P x  (Q y  R x y)}  {(x, y) . P x  Q y}" by auto
  ultimately show ?thesis by blast
qed

lemma collect_pair_finite'[intro]:
  notes finite_subset[intro]
  assumes "finite {(x, y). P x y}"
  shows "finite {(x, y) . P x y  R x y}"
using assms
proof -
  from assms have "finite {(x, y) . P x y}" by auto
  moreover have "{(x, y) . P x y  R x y}  {(x, y) . P x y}" by auto
  ultimately show ?thesis by blast
qed

text ‹This is what we actually need in this theory›
lemma collect_pair_finite''[intro]:
  notes finite_subset[intro]
  assumes "finite {(x, y). P x  Q y}"
  shows "finite {(x, y) . P x  Q y  R x y}"
using assms
proof -
  from assms have "finite {(x, y) . P x  Q y}" by auto
  moreover have "{(x, y) . P x  Q y  R x y}  {(x, y) . P x  Q y}" by auto
  ultimately show ?thesis by blast
qed

lemma finite_imageI'[intro]:
  assumes "finite {(x, y). P x y}"
  shows "finite {f x y | x y. P x y}"
proof -
  from assms have "finite ((λ (x, y). f x y) ` {(x, y). P x y})" by auto
  moreover have "((λ (x, y). f x y) ` {(x, y). P x y}) = {f x y | x y. P x y}" by auto
  ultimately show ?thesis by auto
qed

lemma finite_imageI''[intro]:
  assumes "finite (A × B)"
  shows "finite {f x y | x y. x  A  y  B  R x y}"
proof -
  from assms have "finite {f x y | x y. x  A  y  B}" by auto
  moreover have "{f x y | x y. x  A  y  B  R x y}  {f x y | x y. x  A  y  B}" by auto
  ultimately show ?thesis by (blast intro: finite_subset)
qed

thm stream_pred_cases
(* TODO: Move/should be somewhere already *)
lemma pred_stream_stl: "pred_stream φ xs  pred_stream φ (stl xs)"
  by (cases xs) auto

(* TODO: Should be somewhere already *)
lemma stream_all_pred_stream:
  "stream_all = pred_stream"
  by (intro ext) (simp add: stream.pred_set)

lemma pred_stream_iff: "pred_stream P s  Ball (sset s) P"
  using stream_all_iff[unfolded stream_all_pred_stream] .

(* TODO: Move *)
lemma measure_pmf_eq_1_iff:
  "emeasure (measure_pmf μ) {x} = 1  μ = return_pmf x"
  using measure_pmf.prob_eq_1[of "{x}" μ] set_pmf_subset_singleton[of μ x]
  by (auto simp: measure_pmf.emeasure_eq_measure AE_measure_pmf_iff)

lemma HLD_mono:
  "HLD S ω" if "HLD R ω" "R  S"
  using that unfolding HLD_iff by auto

lemma alw_HLD_smap:
  "alw (HLD (f ` S)) (smap f ω)" if "alw (HLD S) ω"
  using that by (fastforce elim: HLD_mono alw_mono)

lemma alw_disjoint_ccontr:
  assumes "alw (HLD S) ω" "ev (alw (HLD R)) ω" "R  S = {}"
  shows False
proof -
  from assms(1,2) obtain ω where "alw (HLD S) ω" "alw (HLD R) ω"
    by (auto intro: alw_sdrop sdrop_wait)
  with R  S = {} show False
    by (auto 4 3 simp: HLD_iff dest: alwD)
qed

(* TODO: Move *)
lemma stream_all2_refl: "stream_all2 P x x = pred_stream (λ x. P x x) x"
  by (simp add: stream.pred_rel eq_onp_def) (standard; coinduction arbitrary: x; auto)

lemma AE_all_imp_countable:
  assumes "countable {x. Q x}"
  shows "(AE x in M. y. Q y  P x y) = (y. Q y  (AE x in M. P x y))"
  using assms by (auto dest: AE_ball_countable)

lemma AE_conj:
  "almost_everywhere M P = almost_everywhere M (λ x. P x  Q x)" if "almost_everywhere M Q"
  by (auto intro: AE_mp[OF that])

(* TODO: move *)
lemma list_hd_lastD:
  assumes "length xs > 1"
  obtains x y ys where "xs = x # ys @ [y]"
  using assms by atomize_elim (cases xs; simp; metis rev_exhaust)

(* TODO: Move *)
lemma SUP_eq_and_INF_eq:
  assumes "i. i  A  jB. f i = g j"
      and "j. j  B  iA. g j = f i"
    shows "((f :: _  _ :: complete_lattice) ` A) = (g ` B)  (f ` A) = (g ` B)"
  by (auto 4 3 intro!: INF_eq SUP_eq dest: assms)

(* TODO: Move *)
lemma measurable_alw_stream[measurable]:
  fixes P assumes [measurable]: "Measurable.pred (stream_space (count_space UNIV)) P"
  shows "Measurable.pred (stream_space (count_space UNIV)) (alw P)"
  unfolding alw_iff_sdrop by measurable

(* TODO: Move *)
lemma ev_neq_start_implies_ev_neq:
  assumes "ev (Not o HLD {y}) (y ## xs)"
  shows "ev (λ xs. shd xs  shd (stl xs)) (y ## xs)"
  using assms
  apply (induction "y ## xs" arbitrary: xs rule: ev.induct)
   apply (simp; fail)
  subgoal for xs
    apply (cases "shd xs = y")
    subgoal
      apply safe
      apply (rule ev.step)
      apply simp
      using stream.collapse[of xs, symmetric]
      by blast
    subgoal
      by auto
    done
  done

(* TODO: Move *)
lemma ev_sdropD:
  assumes "ev P xs"
  obtains i where "P (sdrop i xs)"
  using assms
  apply atomize_elim
  apply (induction rule: ev.induct)
   apply (inst_existentials "0 :: nat"; simp; fail)
  apply (erule exE)
  subgoal for xs i
    by (inst_existentials "i + 1") simp
  done

(* TODO: Move *)
lemma pred_stream_sconst:
  "pred_stream ((=) x) (sconst x)"
  by coinduction simp

(* TODO: Move *)
lemma alw_Stream: "alw P (x ## s)  P (x ## s)  alw P s"
  by (subst alw.simps) simp

(* TODO: Move *)
lemma alw_True: "alw (λx. True) ω"
  by (auto intro: all_imp_alw)

(* TODO: Move *)
lemma alw_conjI:
  "alw (P aand Q) xs" if "alw P xs" "alw Q xs"
  using that by (simp add: alw_aand)

(* TODO: Move *)
lemma alw_ev_cong:
  "alw (ev S) xs = alw (ev R) xs" if "alw P xs" " x. P x  S x  R x"
  by (rule alw_cong[where P = "alw P"]) (auto simp: HLD_iff that elim!: ev_cong)

lemma alw_ev_HLD_cong:
  "alw (ev (HLD S)) xs = alw (ev (HLD R)) xs" if "alw (HLD P) xs" " x. x  P  x  S  x  R"
  by (rule alw_ev_cong, rule that; simp add: HLD_iff that)

(* TODO: Move *)
lemma measurable_eq_stream_space[measurable (raw)]:
  assumes [measurable]: "f  M M stream_space (count_space UNIV)"
  shows "Measurable.pred M (λx. f x = c)"
proof -
  have *: "(λx. f x = c) = (λx. i. f x !! i = c !! i)"
    by (auto intro: eqI_snth simp: fun_eq_iff)
  show ?thesis
    unfolding * by measurable
qed

(* TODO: rename, and change to LTL constants i.e. HLD, aand, nxt etc. *)
lemma prop_nth_sdrop:
  assumes " ij. P (ω !! i)"
  shows " i. P (sdrop j ω !! i)"
using assms by (induction j arbitrary: ω) fastforce+

lemma prop_nth_sdrop_pair:
  assumes " i. P (ω !! i) (ω' !! i)"
  shows " i. P (sdrop j ω !! i) (sdrop j ω' !! i)"
  using assms by (induction j arbitrary: ω ω') (auto, metis snth.simps(2))

lemma prop_nth_stl:
  " i. P (xs !! i)   i. P (stl xs !! i)"
  by (metis snth.simps(2))

context Graph_Defs
begin

lemma steps_SCons_iff:
  "steps (x # y # xs)  E x y  steps (y # xs)"
  by (auto elim: steps.cases)

lemma steps_Single_True:
  "steps [x] = True"
  by auto

lemma add_step_iff:
  "( xs y. steps (x # xs @ [y])  length xs = Suc n  P xs y)
   ( z xs y. steps (x # z # xs @ [y])  length xs = n  P (z # xs) y)"
  apply safe
   apply fastforce
  subgoal for xs y
    by (cases xs) auto
  done

lemma compower_stepsD:
  assumes "(E ^^ n) s s'"
  obtains xs where "steps xs" "hd xs = s" "last xs = s'" "length xs = n + 1"
  using assms
  apply atomize_elim
proof (induction n arbitrary: s')
  case 0
  then show ?case
    by auto
next
  case (Suc n)
  from Suc.prems show ?case
    by (auto 4 4 intro: steps_append_single dest: Suc.IH)
qed

lemma compower_stepsD':
  assumes "(E ^^ n) s s'" "n > 0"
  obtains xs where "steps (s # xs @ [s'])" "length xs + 1 = n"
  apply (rule compower_stepsD[OF assms(1)])
  subgoal for xs
    by (auto simp: n > 0 intro: list_hd_lastD[of xs])
  done

end

context MC_syntax
begin

theorem AE_T_iff_n:
  fixes P :: "'s stream  bool" 
    and x :: "'s" 
  assumes "Measurable.pred (stream_space (count_space UNIV)) P" "n > 0"
  shows "almost_everywhere (T x) P =
    (xs y. Graph_Defs.steps (λ a b. b  K a) (x # xs @ [y])  length xs + 1 = n
       (AE ω in T y. P (xs @- y ## ω)))"
  using assms
  apply (induction n arbitrary: x P)
   apply (simp; fail)
  subgoal for n x P
    apply (cases n)
    subgoal
      by (subst AE_T_iff) (auto simp: Graph_Defs.steps_SCons_iff Graph_Defs.steps_Single_True)
    subgoal premises prems for n'
    proof -
      have *: "Measurable.pred (stream_space (count_space UNIV)) (λ ω. P (y ## ω))" for y
        using prems(2) by measurable
      with prems(1)[OF *] prems(3-) show ?thesis
        by (auto simp: AE_T_iff[OF prems(2)] Graph_Defs.steps_SCons_iff Graph_Defs.add_step_iff)
    qed
    done
  done

lemma AE_alw_accD:
  fixes P assumes P: "Measurable.pred (stream_space (count_space UNIV)) P"
  assumes *: "almost_everywhere (T s) (alw P)" "(s, s')  acc"
  shows "almost_everywhere (T s') (alw P)"
  using *(2,1)
proof induction
  case (step y z)
  then have "almost_everywhere (T y) (alw P)" "z  K y" by auto
  then have "AE ω in T z. alw P (z ## ω)"
    unfolding AE_T_iff[OF measurable_alw_stream[OF P], of y] by auto
  then show ?case
    by eventually_elim auto
qed 

lemma acc_relfunD:
  assumes "(s, s')  acc"
  obtains n where "((λ a b. b  K a) ^^ n) s s'"
  using assms
  apply atomize_elim
  apply (drule rtrancl_imp_relpow)
  apply (erule exE)
  subgoal for n
    by (inst_existentials n) (induction n arbitrary: s'; auto)
  done

(* TODO: If we can show measurable_alw_stream, then this subsumed by the lemma above *)
lemma AE_all_accD:
  assumes "almost_everywhere (T s) (pred_stream P)" "(s, s')  acc"
  shows "almost_everywhere (T s') (pred_stream P)"
proof -
  from acc_relfunD[OF _  acc] obtain n where *: "((λ a b. b  K a) ^^ n) s s'" .
  show ?thesis
  proof (cases "n = 0")
    case True
    with * assms(1) show ?thesis
      by auto
  next
    case False
    then have "n > 0"
      by simp
    with * obtain xs where
      "Graph_Defs.steps (λa b. b  set_pmf (K a)) (s # xs @ [s'])" "Suc (length xs) = n"
      by (auto elim: Graph_Defs.compower_stepsD')
    with assms(1)[unfolded AE_T_iff_n[OF measurable_pred_stream n > 0, of P s]] show ?thesis
      by auto
  qed
qed

lemma AE_T_ev_HLD_infinite_strong':
  assumes "0  r" "r < 1"
    and r: "x. x  X  Y  measure_pmf.prob (K x) Y  r"
    and ae: "AE ω in T x. alw (λ ω. HLD Y ω  ev (HLD X) ω) ω"
  shows "AE ω in T x. ev (HLD (- Y)) ω"
proof -
  define run where "run F = (HLD (Y - X)) suntil ((X  Y)  Y  F)" for F

  have le_gfp: "alw (HLD Y) aand alw (λ ω. HLD Y ω  ev (HLD X) ω)  gfp run"
  proof (rule gfp_upperbound; clarsimp)
    fix ω assume "alw (HLD Y) ω" "alw (λω. HLD Y ω  ev (HLD X) ω) ω"
    then have "ev (HLD X) ω" "alw (HLD Y) ω" "alw (λω. HLD Y ω  ev (HLD X) ω) ω"
      by auto
    then show "run (λxs. alw (HLD Y) xs  alw (λω. HLD Y ω  ev (HLD X) ω) xs) ω"
    proof (induction ω rule: ev_induct_strong)
      case (base ω) then show ?case by (cases ω) (auto intro!: suntil.base simp: alw_Stream run_def)
    next
      case (step ω)
      show ?case
        unfolding run_def
        using ¬ HLD X ω alw (HLD Y) ω step(3)[unfolded run_def] step(4,5)
        by (auto 0 4 simp: HLD_def intro: suntil.step)
    qed
  qed

  have cont_run: "inf_continuous run"
    apply (auto simp: inf_continuous_def fun_eq_iff run_def)
    subgoal premises that for M x f
      by (rule suntil_mono[OF _ _ that(2) alw_True]) auto
    subgoal premises that for M x
      using that(2)[THEN spec, of 0] that(2)
      proof (induction rule: suntil_induct_strong)
        case (base ω) then show ?case 
          by (cases ω) (simp add: suntil_Stream)
      next
        case (step ω) then show ?case
          by (cases ω) (simp add: suntil_Stream)
      qed
      done
  have [measurable]: "Measurable.pred (stream_space (count_space UNIV)) (gfp run)"
    apply measurable
    apply (rule measurable_gfp[OF cont_run])
    apply (auto simp: run_def)
    done

  have "emeasure (T x) {ω  space (T x). alw (HLD Y) ω} 
    emeasure (T x) {ω  space (T x). ((alw (HLD Y)) aand (alw (λ ω. HLD Y ω  ev (HLD X) ω))) ω}"
    apply (rule emeasure_mono_AE)
    subgoal using ae by eventually_elim auto
    by measurable
  also have "  emeasure (T x) {ω  space (T x). gfp run ω}"
    apply (rule emeasure_mono)
    subgoal using le_gfp by auto
    by measurable
  also have "  r ^ n" for n
  proof (induction n arbitrary: x)
    case 0 then show ?case by (simp add: T.emeasure_le_1)
  next
    case (Suc n)
    { fix x 
      have "(+ t. + t'. emeasure (T t') {xspace S. tX  tY  t'Y  gfp run x} K t K x) 
        (+ t. indicator (X  Y) t * + t'. indicator Y t' * ennreal (r ^ n) K t K x)"
        using Suc by (auto intro!: nn_integral_mono split: split_indicator)
      also have "  (+ t. indicator (X  Y) t * r K x) * ennreal (r^n)"
        by (auto intro!: nn_integral_mono mult_right_mono r ennreal_leI split: split_indicator
                 simp: nn_integral_multc mult.assoc[symmetric] measure_pmf.emeasure_eq_measure)
      also have " = emeasure (K x) (X  Y) * r^(Suc n)"
        by (simp add: ennreal_mult 0  r nn_integral_multc ennreal_indicator mult.assoc)
      finally have *: "(+ t. + t'. emeasure (T t') {xspace S. t  X  t  Y  t'  Y  gfp run x} K t K x) 
        emeasure (K x) (X  Y) * r^Suc n" .
  
      have "(+ t. + t'. emeasure (T t') {x  space S. t  X  t  Y  t'  Y  gfp run x} K t K x) +
           ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X) 
        emeasure (K x) (X  Y) * ennreal (r^Suc n) + ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X)"
        by (intro add_mono_left *)
      also have " = emeasure (K x) ((X  Y)  (Y - X)) * ennreal (r^Suc n)"
        by (subst plus_emeasure[symmetric]) (auto simp: field_simps)
      also have "  1 * ennreal (r^Suc n)"
        by (intro mult_right_mono measure_pmf.emeasure_le_1) simp
      finally have "(+ t. + t'. emeasure (T t') {x  space MC_syntax.S. t  X  t  Y  t'  Y  gfp run x} K t K x) +
           ennreal (r^Suc n) * emeasure (measure_pmf (K x)) (Y - X)  1 * ennreal (r^Suc n)" by simp }
    note * = this
    
    show ?case
      apply (subst gfp_unfold[OF inf_continuous_mono[OF cont_run]])
      apply (subst run_def)
      apply (subst emeasure_suntil_disj)
        apply measurable []
      subgoal for s
        by (rule AE_I2) (auto simp: HLD_iff)
      apply (rule le_funD[of _ _ x])
      apply (rule lfp_lowerbound)
      apply (rule le_funI)
      apply (subst emeasure_Collect_T)
       apply measurable []
      apply (subst emeasure_Collect_T)
      apply simp
      apply (simp add: nn_integral_cmult)
      using * by simp
  qed
  finally have "emeasure (T x) {ω  space (T x). alw (HLD Y) ω}  r^n" for n .
  then have "emeasure (T x) {ω  space (T x). alw (HLD Y) ω}  ennreal 0"
    using 0  r r < 1
    by (intro LIMSEQ_le_const[OF tendsto_ennrealI[OF LIMSEQ_power_zero[of r]]]) auto
  then have *: "emeasure (T x) {ω  space (T x). alw (HLD Y) ω} = 0"
    by simp
  show ?thesis
    by (rule AE_I[OF _ *]) (auto simp: not_ev_iff not_HLD[symmetric])
qed

end

context Markov_Decision_Process
begin

lemma cfg_on_inv:
  "pred_stream (λ cfg. cfg  cfg_on (state cfg)) ω" if
  "MC.enabled cfg ω" "cfg  cfg_on s"
  using that proof (coinduction arbitrary: ω cfg s)
  case prems: stream_pred
  note [simp] = _ = ω[symmetric]
  from prems(2) have "a  set_pmf (K_cfg cfg)" "MC.enabled a w"
    by (auto simp: MC.enabled_Stream)
  moreover from a  _ have "a  cont cfg ` set_pmf (action cfg)"
    by (simp add: set_K_cfg)
  ultimately show ?case
    using cfg  _ by auto
qed

lemma MC_T_not_sconst_strong:
  assumes
    " l.  cfg  ( x  f -` {u}. cfg_on x)  Y  X. measure_pmf (action cfg) (f -` {u})  r"
    "r < 1" "cfg  cfg_on x"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
    "AE ω in MC.T cfg. alw (λ ω. HLD (f -` {u}) (smap state ω)  ev (HLD Y) ω) ω"
  shows "AE ω in MC.T cfg. smap (f o state) ω  sconst u"
proof -
  let ?U = "f -` {u}"
  let ?S = "( x  f -` {u}. cfg_on x)  X"
  let ?T = "Y  (( x  f -` {u}. cfg_on x)  X)"
  have *: "emeasure (K_cfg cfg) ?S  r" if "cfg  ?T" for cfg
  proof -
    have "emeasure (K_cfg cfg) ?S  emeasure (measure_pmf (action cfg)) ?U"
      unfolding K_cfg_def by (auto dest: cfg_onD_state intro!: emeasure_mono)
    also from assms(1) cfg  ?T have "  r"
      by auto
    finally show ?thesis .
  qed
  have "AE ω in MC.T cfg. ev (HLD (- ?S)) ω"
    apply (rule MC.AE_T_ev_HLD_infinite_strong'[where r = "enn2real r" and ?X = Y])
    apply (simp; fail)
    subgoal
      using r < 1
      by (metis ennreal_enn2real_if ennreal_less_one_iff zero_less_one)
    subgoal for x
     by (drule *)
        (metis Sigma_Algebra.measure_def assms(2) enn2real_mono ennreal_one_less_top less_trans)
    subgoal
      using assms(5)
      by (rule AE_mp) (rule AE_I2, intro impI, auto simp: HLD_iff elim: alw_mono)
    done
  then show ?thesis
    apply (rule AE_mp)
  proof (rule AE_mp[OF assms(4)], rule AE_mp[OF MC.AE_T_enabled], rule AE_I2, safe)
    fix ω assume
      "ω  space (MC.T cfg)" "pred_stream (λω. ω  X) ω"
      "MC.enabled cfg ω" "ev (HLD (- ?S)) ω" "smap (f  state) ω = sconst u"
    from this(2,3) cfg  _
    have "pred_stream (λ x. x  cfg_on (state x)) ω"
      by (auto dest: cfg_onD_state intro!: cfg_on_inv)
    from smap _ ω = _ have "pred_stream (λ y. y  ( x  ?U. cfg_on x)) ω"
    proof -
      have "(f o state) cfg = u" if "cfg  sset ω" for cfg
        using stream.set_map[of "f o state" ω] that smap _ ω = _ by fastforce
      with pred_stream (λ x. x  cfg_on (state x)) ω show ?thesis
        by (auto elim!: stream.pred_mono_strong)
    qed
    with pred_stream (λω. ω  X) ω have "pred_stream (λ x. x  ?S) ω"
      by (coinduction arbitrary: ω) auto
    then have "alw (HLD ?S) ω"
      by (simp add: alw_holds_pred_stream_iff HLD_def)
    with ev (HLD (- ?S)) ω show False
      unfolding not_ev_not[symmetric] not_HLD by simp
  qed
qed

lemma MC_T_not_sconst:
  assumes
    " l.  cfg  ( x  f -` {u}. cfg_on x)  X. measure_pmf (action cfg) (f -` {u})  r"
    "r < 1" "cfg  cfg_on x"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
  shows "AE ω in MC.T cfg. smap (f o state) ω  sconst u"
proof -
  let ?U = "f -` {u}"
  let ?S = "( x  f -` {u}. cfg_on x)  X"
  have *: "emeasure (K_cfg cfg) ?S  r" if "cfg  ?S" for cfg
  proof -
    have "emeasure (K_cfg cfg) ?S  emeasure (measure_pmf (action cfg)) ?U"
      unfolding K_cfg_def by (auto dest: cfg_onD_state intro!: emeasure_mono)
    also from assms(1) cfg  ?S have "  r"
      by auto
    finally show ?thesis .
  qed
  have "AE ω in MC.T cfg. ev (HLD (- ?S)) ω"
    apply (rule MC.AE_T_ev_HLD_infinite[where r = "enn2real r"])
    subgoal
      using r < 1
      by (metis ennreal_enn2real_if ennreal_less_one_iff zero_less_one)
    apply (drule *)
    by (metis Sigma_Algebra.measure_def assms(2) enn2real_mono ennreal_one_less_top less_trans)
  then show ?thesis
    apply (rule AE_mp)
  proof (rule AE_mp[OF assms(4)], rule AE_mp[OF MC.AE_T_enabled], rule AE_I2, safe)
    fix ω assume
      "ω  space (MC.T cfg)" "pred_stream (λω. ω  X) ω"
      "MC.enabled cfg ω" "ev (HLD (- ?S)) ω" "smap (f  state) ω = sconst u"
    from this(2,3) cfg  _
    have "pred_stream (λ x. x  cfg_on (state x)) ω"
      by (auto dest: cfg_onD_state intro!: cfg_on_inv)
    from smap _ ω = _ have "pred_stream (λ y. y  ( x  ?U. cfg_on x)) ω"
    proof -
      have "(f o state) cfg = u" if "cfg  sset ω" for cfg
        using stream.set_map[of "f o state" ω] that smap _ ω = _ by fastforce
      with pred_stream (λ x. x  cfg_on (state x)) ω show ?thesis
        by (auto elim!: stream.pred_mono_strong)
    qed
    with pred_stream (λω. ω  X) ω have "pred_stream (λ x. x  ?S) ω"
      by (coinduction arbitrary: ω) auto
    then have "alw (HLD ?S) ω"
      by (simp add: alw_holds_pred_stream_iff HLD_def)
    with ev (HLD (- ?S)) ω show False
      unfolding not_ev_not[symmetric] not_HLD by simp
  qed
qed

lemma MC_T_not_sconst':
  assumes
    " cfg  cfg_on x  X. measure_pmf (action cfg) {x}  r" "r < 1" "cfg  cfg_on x'"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
  shows "AE ω in MC.T cfg. smap state ω  sconst x"
  using assms by (rule MC_T_not_sconst[where f = id, simplified])

lemma K_cfg_cfg_onI:
  "cfg'  cfg_on (state cfg')" if "cfg  cfg_on x" "cfg'  K_cfg cfg"
  using that by (force simp: set_K_cfg)

lemma MC_acc_cfg_onI:
  "cfg'  cfg_on (state cfg')" if "(cfg, cfg')  MC.acc" "cfg  cfg_on x"
proof -
  from that(1) obtain n where "((λ a b. b  K_cfg a) ^^ n) cfg cfg'"
    by (erule MC.acc_relfunD)
  with cfg  cfg_on x show ?thesis
    by (induction n arbitrary: cfg') (auto intro: K_cfg_cfg_onI)
qed

lemma non_loop_tail_strong:
  assumes
    " l.  cfg  ( x  f -` {u}. cfg_on x)  Y  X. measure_pmf (action cfg) (f -` {u})  r"
    "r < 1" "cfg  cfg_on x"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
    "AE ω in MC.T cfg. alw (λ ω. HLD (f -` {u}) (smap state ω)  ev (HLD Y) ω) ω"
  shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = u))) (smap (f o state) ω)"
    (is "AE ω in ?M. ?P ω")
proof -
  have *: "?P ω  alw (λ xs. smap (f o state) xs  sconst u) ω" for ω
    apply (simp add: not_ev_iff)
    apply (rule arg_cong2[where f = alw])
     apply (rule ext)
    subgoal for xs
      using MC.alw_HLD_iff_sconst[of u "smap (f o state) xs"] by (simp add: HLD_iff comp_def)
    by (rule HOL.refl)
  have "AE ω in ?M. alw (λ xs. smap (f o state) xs  sconst u) ω"
    apply (rule MC.AE_T_alw)
    subgoal by (intro pred_intros_logic measurable_eq_stream_space) measurable
    using assms
    by - (erule MC_T_not_sconst_strong,
        auto intro: MC.AE_all_accD MC.AE_alw_accD elim: MC_acc_cfg_onI
        )
  with * show ?thesis
    by simp
qed

lemma non_loop_tail:
  assumes
    " l.  cfg  ( x  f -` {u}. cfg_on x)  X. measure_pmf (action cfg) (f -` {u})  r"
    "r < 1" "cfg  cfg_on x"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
  shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = u))) (smap (f o state) ω)"
    (is "AE ω in ?M. ?P ω")
proof -
  have *: "?P ω  alw (λ xs. smap (f o state) xs  sconst u) ω" for ω
    apply (simp add: not_ev_iff)
    apply (rule arg_cong2[where f = alw])
     apply (rule ext)
    subgoal for xs
      using MC.alw_HLD_iff_sconst[of u "smap (f o state) xs"] by (simp add: HLD_iff comp_def)
    by (rule HOL.refl)
  have "AE ω in ?M. alw (λ xs. smap (f o state) xs  sconst u) ω"
    apply (rule MC.AE_T_alw)
    subgoal by (intro pred_intros_logic measurable_eq_stream_space) measurable
    using assms by - (erule MC_T_not_sconst, auto intro: MC.AE_all_accD elim: MC_acc_cfg_onI)
  with * show ?thesis
    by simp
qed

lemma non_loop_tail':
  assumes
    " cfg  cfg_on x  X. measure_pmf (action cfg) {x}  r" "r < 1"
    "cfg  cfg_on y"
    "AE ω in MC.T cfg. pred_stream (λ x. x  X) ω"
  shows "AE ω in MC.T cfg. ¬ (ev (alw (λ xs. shd xs = x))) (smap state ω)"
  using assms by simp (erule non_loop_tail[where f = id, simplified])

end

lemma (in Regions) intv_const_mono:
  assumes "u  region X I r" "c1  X" "c2  X" "u c1  u c2" "¬ isGreater (I c2)"
  shows "intv_const (I c1)  intv_const (I c2)"
proof -
  from assms have "intv_elem c1 u (I c1)" "intv_elem c2 u (I c2)" by auto
  with u c1  u c2 ¬ _ show ?thesis by (cases "I c1"; cases "I c2"; auto)
qed

lemma sset_sdrop:
  assumes "x  sset (sdrop i xs)"
  shows "x  sset xs"
using assms by (auto simp: sset_range)

lemma holds_untilD:
  assumes "(holds P until holds Q) xs" " i  j. ¬ Q (xs !! i)"
  shows "P (xs !! j)"
using assms
proof (induction j arbitrary: xs)
  case 0
  then show ?case by cases auto
next
  case (Suc j)
  from Suc.prems show ?case by cases (auto dest!: Suc.IH)
qed

(* TODO: Move *)
lemma frac_le_self:
  assumes "x  0"
  shows "frac x  x"
  using assms less_trans [of "frac x" 1 x]
  by (auto simp add: le_less frac_eq not_less frac_lt_1)

lemma frac_le_1I:
  assumes "0  x" "x  1" "x  y"
  shows "frac x  y"
  using assms dual_order.trans frac_le_self by auto

lemma frac_le_1I':
  assumes "0  x" "x  y" "y < 1"
  shows "frac x  frac y"
proof -
  from assms have "frac y = y" by (simp add: frac_eq)
  moreover from assms have "frac x  y" by (auto intro: frac_le_1I)
  ultimately show ?thesis by simp
qed

(* XXX Move *)
lemmas [intro] = order.strict_implies_order[OF frac_lt_1]

lemma nat_eventually_critical:
  assumes "P i" "¬ P j" "i < j"
  shows " k  i. P k  ¬ P (Suc k)"
using assms by (metis dec_induct less_le)

lemma nat_eventually_critical_path:
  fixes i :: nat
  assumes "P i" "¬ P j" "i < j"
  shows " k > i. k  j  ¬ P k  ( m  i. m < k  P m)"
proof -
  let ?S = "{k. i < k  k  j  ¬ P k}"
  let ?k = "Min ?S"
  from assms have "j  ?S" by auto
  moreover have "finite ?S" by auto
  ultimately have "i < ?k" "?k  j" "¬ P ?k" using Min_in[of ?S] by blast+
  moreover have "P m" if "i  m" "m < ?k" for m
  proof (cases "i = m")
    case True with P i show ?thesis by simp
  next
    case False
    with i  m have "i < m" by simp
    with Min_le[OF finite _] m < ?k ?k  j show ?thesis by fastforce
  qed
  ultimately show ?thesis using P i by - (rule exI[where x = ?k]; blast)
qed

subsection ‹MDP Invariant›

locale Markov_Decision_Process_Invariant =
  Markov_Decision_Process K for K :: "'s  's pmf set"+
fixes S :: "'s set"
assumes invariant: " s D. s  S  D  K s  (s'  D. s'  S)"
begin

lemma E_invariant:
  "{s'. (s, s')  E}  S" if "s  S"
  using that by (auto dest: invariant simp: E_def)

definition "valid_cfg = (sS. cfg_on s)"

lemma valid_cfgI: "s  S  cfg  cfg_on s  cfg  valid_cfg"
  by (auto simp: valid_cfg_def)

lemma valid_cfgD: "cfg  valid_cfg  cfg  cfg_on (state cfg)"
  by (auto simp: valid_cfg_def)

lemma action_closed: "s  S  cfg  cfg_on s  t  action cfg  t  S"
  using cfg_onD_action[of cfg s] invariant[of s] by auto

lemma
  shows valid_cfg_state_in_S: "cfg  valid_cfg  state cfg  S"
    and valid_cfg_action: "cfg  valid_cfg  s  action cfg  s  S"
    and valid_cfg_cont: "cfg  valid_cfg  s  action cfg  cont cfg s  valid_cfg"
  by (auto simp: valid_cfg_def intro!: bexI[of _ s] intro: action_closed)

lemma valid_K_cfg[intro]: "cfg  valid_cfg  cfg'  K_cfg cfg  cfg'  valid_cfg"
  by (auto simp add: K_cfg_def valid_cfg_cont)

lemma pred_stream_valid_cfg:
  assumes valid: "cfg  valid_cfg"
  assumes enabled: "MC.enabled cfg xs"
  shows "pred_stream (λ cfg. cfg  valid_cfg) xs"
  using assms by (coinduction arbitrary: cfg xs) (subst (asm) MC.enabled_iff; auto)

lemma pred_stream_cfg_on:
  assumes valid: "cfg  valid_cfg"
  assumes enabled: "MC.enabled cfg xs"
  shows "pred_stream (λ cfg. state cfg  S  cfg  cfg_on (state cfg)) xs"
  using valid pred_stream_valid_cfg[OF _ enabled] unfolding stream.pred_set
  by (auto intro: valid_cfgI dest: valid_cfgD valid_cfg_state_in_S)

lemma alw_S: "almost_everywhere (T cfg) (pred_stream (λs. s  S))" if "cfg  valid_cfg"
  unfolding T_def using pred_stream_cfg_on cfg  valid_cfg
  by (subst AE_distr_iff) (measurable, auto simp: stream.pred_set intro: AE_mp[OF MC.AE_T_enabled])

end

context Finite_Markov_Decision_Process
begin

sublocale Invariant: Markov_Decision_Process_Invariant
  rewrites "Invariant.valid_cfg = valid_cfg"
proof -
  show "Markov_Decision_Process_Invariant K S"
    by standard (auto dest: set_pmf_closed)
  then show "Markov_Decision_Process_Invariant.valid_cfg K S = valid_cfg"
    by (subst Markov_Decision_Process_Invariant.valid_cfg_def; simp add: valid_cfg_def)
qed

lemmas pred_stream_cfg_on = Invariant.pred_stream_cfg_on
   and pred_stream_valid_cfg = Invariant.pred_stream_valid_cfg
   and alw_S = Invariant.alw_S
   and valid_cfg_state_in_S = Invariant.valid_cfg_state_in_S

end

end