Theory MDP_RP

section ‹Value Iteration for Reachability Probabilities of MDPs›

theory MDP_RP
  imports "../Markov_Models"
begin

subsection ‹Auxiliary Theorems›

lemma INF_Union_eq: "(INF xA. f x) = (INF aA. INF xa. f x)" for f :: "_  'a::complete_lattice"
  by (auto intro!: antisym INF_greatest intro: INF_lower2)

lemma lift_option_eq_None: "lift_option f A B = None  (A  None  B = None)"
  by (cases A; cases B; auto)

lemma lift_option_eq_Some: "lift_option f A B = Some y  (a b. A = Some a  B = Some b  y = f a b)"
  by (cases A; cases B; auto)

lemma ord_option_Some1_iff: "ord_option R (Some a) y  (b. y = Some b  R a b)"
  by (cases y; auto)

lemma ord_option_Some2_iff: "ord_option R x (Some b)  (a. x = Some a  R a b)"
  by (cases x; auto)

lemma sym_Restr: "sym A  sym (Restr A S)"
  by (auto simp: sym_def)

lemma trans_Restr: "trans A  trans (Restr A S)"
  by (auto simp: trans_def)

lemma image_eq_singleton_iff: "inj_on f S  f ` S = {y}  (x. S = {x}  y = f x)"
  by (auto elim: inj_img_insertE)

lemma quotient_eq_singleton: "equiv A r  A // r = {B}  B = A"
  using Union_quotient[of A r] by auto

lemma UN_singleton_image: "(xA. {f x}) = f ` A"
  by auto

lemma image_eq_singeltonD: "f ` A = {x}  aA. f a = x"
  by auto

lemma fun_ord_refl: "reflp ord   reflp (fun_ord ord)"
  by (auto simp: fun_ord_def reflp_def)

lemma fun_ord_trans: "transp ord   transp (fun_ord ord)"
  by (fastforce simp: fun_ord_def transp_def)

lemma fun_ord_antisym: "antisymp ord   antisymp (fun_ord ord)"
  by (fastforce simp: fun_ord_def antisymp_def)

lemma fun_ord_combine:
  "fun_ord ord a b  fun_ord ord c d  (s. ord (a s) (b s)  ord (c s) (d s)  ord (e s) (f s))  fun_ord ord e f"
  by (auto simp: fun_ord_def)

lemma not_all_eq: "~ (y. x  y)"
  by auto

lemma ball_vimage_iff: "(xf -` X. P x)  (x. f x  X  P x)"
  by auto

lemma UN_If_cases: "(xX. if P x then A x else B x) = (x{xX. P x}. A x)  (x{xX. ¬ P x}. B x)"
  by (auto split: if_splits)

lemma (in Reachability_Problem) n_eq_0_closed:
  assumes s: "s  S'" and S': "S'  S" "S'  S2 = {}" and closed: "s. s  S'  DK s. D  S'"
  shows "n s = 0"
proof -
  from closed obtain ct where ct: "s. s  S'  ct s  K s" "s. s  S'  ct s  S'"
    by metis

  define cfg where "cfg = memoryless_on (λs. if s  S' then ct s else arb_act s)"

  have cfg_on: "cfg s  cfg_on s" for s
    unfolding cfg_def using ct by (intro memoryless_on_cfg_onI) auto

  have state_cfg[simp]: "state (cfg s) = s" for s
    unfolding cfg_def by (intro state_memoryless_on)
  have action_cfg[simp]: "action (cfg s) = (if s  S' then ct s else arb_act s)" for s
    unfolding cfg_def by (intro action_memoryless_on)
  have cont_cfg[simp]: "s  S'  t  ct s  cont (cfg s) t = cfg t" for s t
    unfolding cfg_def by (intro cont_memoryless_on) auto

  from s have "v (cfg s) = 0"
  proof (coinduction arbitrary: s rule: v_eq_0_coinduct)
    case (valid cfg') with cfg_on s S' show ?case
      by (auto simp: valid_cfg_def)
  next
    case (nS2 cfg') with S' show ?case
      by auto
  next
    case (cont cfg') with S' ct show ?case
      by (force simp: set_K_cfg)
  qed
  show "n s = 0"
  proof (rule n_eq_0)
    show "s  S" using s S' by auto
  qed fact+
qed

lemma (in Reachability_Problem) n_lb_ennreal:
  fixes x
  assumes "s  S"
  assumes solution: "s D. s  S1  D  K s  x s  (tS. ennreal (pmf D t) * x t)"
  assumes solution_n0: "s. s  S  n s = 0  x s = 0"
  assumes solution_S2: "s. s  S2  x s = 1"
    and le_1:  "s. s  S  x s  1"
  shows "x s  n s" (is "_  ?y s")
proof -
  have x_less_top[simp]: "s  S  x s < top" for s
    using le_1[of s] by (auto simp: less_top[symmetric] top_unique)

  have "enn2real (x s)  enn2real (n s)"
    apply (rule n_lb[OF sS])
    subgoal for s D
      by (rule ennreal_le_iff[THEN iffD1])
          (use S1 in auto intro!: sum_nonneg simp add: subset_eq solution sum_ennreal[symmetric] ennreal_mult simp del: sum_ennreal)
    apply (auto simp: solution_n0 solution_S2)
    done
  with sS show ?thesis
    by (subst (asm) ennreal_le_iff[symmetric]) (simp_all add: real_n)
qed

lifting_forget pmf_as_function.pmf.lifting

text ‹
  Type to describe MDP components. The support (i.e. elements which are not mapped to an empty
set) is the set of states of the component.

Most of this is from:
  Formal verification of probabilistic systems
  Luca de Alfaro (PhD thesis, 1997)
and
  Reachability in MDPs: Refining Convergence of Value Iteration
  Serge Haddad and Benjamin Monmege (2014)
›

typedef 's mdpc = "UNIV :: ('s  's pmf set) set"
  by auto

setup_lifting type_definition_mdpc

lift_definition states :: "'s mdpc  's set"
  is dom .

declare [[coercion states]]

lift_definition actions :: "'s mdpc  's  's pmf set"
  is "λf s. case f s of None  {} | Some a  a" .

lemma in_states: "actions φ s  {}  s  states φ"
  by transfer auto

lemma mdpc_eqI: "states φ = states ψ  (s. s  states φ  actions φ s = actions ψ s)  φ = ψ"
  apply transfer
  apply (rule ext)
  subgoal premises prems for φ ψ x
    using prems(1) prems(2)[of x]
    by (cases "x  dom φ") (auto simp: fun_eq_iff split: option.splits)
  done

lift_definition map_mdpc :: "('s  't)  's mdpc  't mdpc"
  is "λm f s. if f ` (m -` {s})  {None} then None else Some {map_pmf m d | d A t. m t = s  f t = Some A  d  A}" .

lemma states_map_mdpc: "states (map_mdpc f M) = f ` (states M)"
  by (transfer fixing: f) (auto simp: subset_eq image_iff dom_def split: if_splits)

lemma actions_map_mdpc_eq_Collect: "actions (map_mdpc f M) s = {map_pmf f d | d t. f t = s  d  actions M t}"
  by transfer (force simp: subset_eq split: option.splits)

lemma actions_map_mdpc: "actions (map_mdpc f M) s = map_pmf f ` (tf -` {s}. actions M t)"
  by (auto simp: actions_map_mdpc_eq_Collect)

lemma map_mdpc_compose: "map_mdpc f (map_mdpc g M) = map_mdpc (f  g) M"
  by (intro mdpc_eqI)
     (auto simp add: states_map_mdpc image_comp actions_map_mdpc image_UN map_pmf_compose[symmetric]
                     vimage_comp[symmetric])

lemma map_mdpc_id: "map_mdpc id = id"
  by (auto simp: fun_eq_iff states_map_mdpc actions_map_mdpc intro!: mdpc_eqI)

lemma finite_states_map: "finite (states M)  finite (map_mdpc f M)"
  by (simp add: states_map_mdpc)

lemma finite_actions_map:
  assumes "finite (states M)" "s. finite (actions M s)" shows "finite (actions (map_mdpc f M) s)"
proof -
  have "(xf -` {s}. actions M x) = (xf -` {s}  states M. actions M x)"
    using in_states[of M] by auto
  with assms show ?thesis
    by (auto simp add: actions_map_mdpc)
qed

lift_definition fix_loop :: "'s  's mdpc  's mdpc"
  is "λs M t. if s = t then Some {return_pmf s} else M t" .

lemma states_fix_loop[simp]: "states (fix_loop s M) = insert s (states M)"
  by transfer (auto simp: subset_eq image_iff dom_def split: if_splits)

lemma actions_fix_loop[simp]: "actions (fix_loop s M) t = (if s = t then {return_pmf s} else actions M t)"
  by transfer auto

lemma fix_loop_idem: "fix_loop s (fix_loop s M) = fix_loop s M"
  by (auto intro!: mdpc_eqI)

lemma fix_loop_commute: "fix_loop s (fix_loop t M) = fix_loop t (fix_loop s M)"
  by (auto intro!: mdpc_eqI)

lemma map_fix_loop:
  assumes f_s: "t. f s = f t  t = s"
  shows "map_mdpc f (fix_loop s M) = fix_loop (f s) (map_mdpc f M)"
  by (auto simp: states_map_mdpc actions_map_mdpc_eq_Collect split: if_splits intro!: mdpc_eqI dest!: f_s f_s[OF sym]) force+

lift_definition map_actions :: "('s  's pmf set  's pmf set)  's mdpc  's mdpc"
  is "λm f s. map_option (m s) (f s)" .

lemma state_map_actions[simp]: "states (map_actions f φ) = states φ"
  by transfer auto

lemma actions_map_actions[simp]: "(s  states φ  f s {} = {})  actions (map_actions f φ) s = f s (actions φ s)"
  by transfer (auto split: option.splits)

lift_definition restrict_states :: "'s set  's mdpc  's mdpc"
  is "λS f s. if s  S then f s else None" .

lemma state_restrict_states[simp]: "states (restrict_states S φ) = states φ  S"
  by transfer (auto split: if_splits)

lemma actions_restrict_states[simp]: "actions (restrict_states S φ) s = (if s  S then actions φ s else {})"
  by transfer (auto split: if_splits)

lemma restrict_states_idem: "states φ  A  restrict_states A φ = φ"
  by transfer (force simp: fun_eq_iff subset_eq dom_def)

instantiation mdpc :: (type) lattice
begin

lift_definition less_eq_mdpc :: "'s mdpc  's mdpc  bool"
  is "fun_ord (ord_option (⊆))" .

definition less_mdpc :: "'s mdpc  's mdpc  bool"
  where "less_mdpc f g  (f  g  ¬ g  f)"

lift_definition inf_mdpc :: "'s mdpc  's mdpc  's mdpc"
  is "λf g s. lift_option (∩) (f s) (g s)" .

lift_definition sup_mdpc :: "'s mdpc  's mdpc  's mdpc"
  is "λf g s. combine_options (∪) (f s) (g s)" .

instance
proof
  fix x y z :: "'s mdpc"
  show "(x < y) = (x  y  ¬ y  x)"
    by (rule less_mdpc_def)
  note ord =
    fun_ord_refl[where 'b="'s", OF reflp_ord_option[where 'a="'s pmf set"], of "(⊆)"]
    fun_ord_trans[where 'b="'s", OF transp_ord_option[where 'a="'s pmf set"], of "(⊆)"]
    fun_ord_antisym[where 'b="'s", OF antisymp_ord_option[where 'a="'s pmf set"], of "(⊆)"]
  show  "x  x" "x  y  y  z  x  z" "x  y  y  x  x = y"
    by (transfer; insert ord; auto simp: transp_def antisymp_def reflp_def)+
  show "x  y  x" "x  y  y"
    by (transfer; auto simp: fun_ord_def ord_option.simps lift_option_def split: Option.bind_split)+
  show "x  y  x  z  x  y  z"
    apply transfer
    subgoal premises prems for a b c
      using prems by (rule fun_ord_combine) (auto simp: ord_option.simps)
    done
  show "x  x  y" "y  x  y"
    by (transfer; auto simp: fun_ord_def ord_option.simps combine_options_def not_all_eq split: option.splits)+
  show "y  x  z  x  y  z  x"
    apply transfer
    subgoal premises prems for a b c
      using prems by (rule fun_ord_combine) (auto simp: ord_option.simps)
    done
qed
end

instantiation mdpc :: (type) complete_lattice
begin

lift_definition bot_mdpc :: "'a mdpc" is "λ_. None" .

lift_definition top_mdpc :: "'a mdpc" is "λ_. Some UNIV" .

lift_definition Sup_mdpc :: "'a mdpc set  'a mdpc"
  is "λM s. if mM. m s  None then Some ({ d | m d. m  M  m s = Some d}) else None" .

lift_definition Inf_mdpc :: "'a mdpc set  'a mdpc"
  is "λM s. if mM. m s = None then None else Some ({ d | m d. m  M  m s = Some d})" .

instance
proof
  fix x :: "'a mdpc" and X :: "'a mdpc set"
  show "x  X  X  x" "x  X  x  X"
    by (transfer; force simp: fun_ord_def ord_option_Some1_iff ord_option_Some2_iff)+
  show "(y. y  X  x  y)  x  X"
    apply transfer
    apply (clarsimp simp: fun_ord_def ord_option.simps)
    subgoal premises P for X m x
      using P[rule_format, of _ x]
      by (cases "m x") fastforce+
    done
  show "(y. y  X  y  x)  X  x"
    apply transfer
    apply (clarsimp simp: fun_ord_def ord_option.simps)
    subgoal premises P for X m x y z
      using P(1)[rule_format, of _ x] P(1)[rule_format, of y x] P(2,3)
      by auto force
    done
qed (transfer; auto)+
end

lemma states_sup[simp]: "states (φ  ψ) = states φ  states ψ"
  by transfer (auto simp: combine_options_def split: option.splits)

lemma states_SUP[simp]: "states (A) = (aA. states a)"
  by transfer (auto simp: dom_def split: option.splits if_splits)

lemma states_inf[simp]: "states (φ  ψ) = states φ  states ψ"
  by transfer (auto simp: lift_option_eq_Some split: option.splits)

lemma states_mono: "φ  ψ  states φ  states ψ"
  using states_sup[of φ ψ] by (auto simp del: states_sup simp add: sup_absorb2)

lemma actions_sup[simp]: "actions (φ  ψ) = actions φ  actions ψ"
  by transfer (auto simp: combine_options_def split: option.splits)

lemma actions_SUP[simp]: "actions (A) s = (aA. actions a s)"
  by transfer (auto simp: dom_def split: option.splits if_splits, blast)

lemma actions_inf[simp]: "actions (φ  ψ) = actions φ  actions ψ"
  by transfer (auto simp: fun_eq_iff split: option.splits)

lemma actions_mono: assumes *: "φ  ψ" shows "actions φ  actions ψ"
proof -
  have "actions φ  actions φ  actions ψ"
    by auto
  also have " = actions ψ"
    using * actions_sup[of φ ψ] by (auto simp add: sup_absorb2)
  finally show ?thesis .
qed

lemma le_mdpcI: "states M  states N  (s. s  states M  actions M s  actions N s)  M  N"
  by transfer
     (force simp: fun_ord_def ord_option.simps subset_eq split: option.splits)

lemma le_mdpc_iff: "M  N  states M  states N  (s. actions M s  actions N s)"
  using states_mono[of M N] actions_mono[of M N] by (auto simp: le_fun_def intro!: le_mdpcI)

lemma map_actions_le: "(s A. s  states φ  f s A  A)  map_actions f φ  φ"
  apply (intro le_mdpcI)
  subgoal by auto
  subgoal premises p for s using p(1)[of s] p(1)[of s "{}"] p(2) actions_map_actions by auto
  done

lemma restrict_states_mono: "A  B  φ  ψ  restrict_states A φ  restrict_states B ψ"
  using states_mono[of φ ψ] actions_mono[of φ ψ] by (intro le_mdpcI) (auto simp: le_fun_def)

lemma restrict_states_le: "restrict_states A M  M"
  by (intro le_mdpcI) auto

lemma eq_bot_iff_states: "φ = bot  states φ = {}"
  by transfer auto

lemma fix_loop_neq_bot: "fix_loop s N  bot"
  unfolding eq_bot_iff_states by simp

lemma
  shows states_bot[simp]: "states bot = {}"
    and actions_bot[simp]: "actions bot = (λs. {})"
  unfolding fun_eq_iff by (transfer; auto)+

lemma inf_eq_bot_eq_disjnt_states: "A  B = bot  disjnt (states A) (states B)"
  unfolding disjnt_def by transfer  (auto simp: fun_eq_iff lift_option_eq_None)

text ‹Enabled States›
definition en :: "'s mdpc  's rel"
  where "en φ = {(s, t) | d s t. d  actions φ s  t  set_pmf d}"

lemma en_sup[simp]: "en (φ  ψ) = en φ  en ψ"
  by (auto simp: en_def)

lemma en_SUP[simp]: "en (Sup A) = (aA. en a)"
  by (auto simp: en_def)

lemma en_mono: "φ  ψ  en φ  en ψ"
  unfolding en_def
  apply transfer
  apply (auto simp: fun_ord_def split: option.splits)
  apply (auto simp add: ord_option.simps subset_iff)
  apply force
  done

lemma en_states: "(s, t)  en M  s  states M"
  using in_states[of M s] by (auto simp: en_def)

lemma en_bot[simp]: "en bot = {}"
  by (simp add: en_def)

lemma en_fix_loop[simp]: "en (fix_loop s M) = insert (s, s) (en M - {s} × UNIV)"
  by (force simp add: en_def )

lift_definition trivial :: "'s  's mdpc" is "λs. (λ_. None)(s := Some {})" .

lemma states_trivial[simp]: "states (trivial s) = {s}"
  by transfer auto

lemma actions_trivial[simp]: "actions (trivial s) = (λ_. {})"
  by transfer (auto simp: fun_eq_iff)

lemma en_trivial[simp]: "en (trivial s) = {}"
  by (simp add: en_def)

lemma trivial_le_iff: "trivial x  φ  x  states φ"
  by transfer (auto simp: ord_option.simps fun_ord_def)

lemma trivial_le: "x  states φ  trivial x  φ"
  unfolding trivial_le_iff .

lemma trivial_neq_bot: "trivial x  bot"
  by transfer auto

lift_definition loop :: "'s  's mdpc"
  is "λs. (λ_. None)(s := Some {return_pmf s})" .

lemma states_loop[simp]: "states (loop s) = {s}"
  by transfer auto

lemma actions_loop: "actions (loop s) = ((λ_. {})(s := {return_pmf s}))"
  by transfer (auto simp: fun_eq_iff)

lemma
  shows actions_loop_self[simp]: "actions (loop s) s = {return_pmf s}"
    and actions_loop_neq[simp]: "s  t  actions (loop s) t = {}"
  by (simp_all add: actions_loop)

lemma en_loop[simp]: "en (loop s) = {(s, s)}"
  by (auto simp: en_def actions_loop)

lemma loop_neq_bot: "loop s  bot"
  unfolding eq_bot_iff_states by simp

lemma loop_le: "loop x  M  (x  states M  return_pmf x  actions M x)"
  by (auto simp: le_mdpc_iff actions_loop)

lemma le_loop: "M  loop x  (states M  {x}  actions M x  {return_pmf x})"
  using in_states[of M] by (auto simp: le_mdpc_iff actions_loop)

text ‹Strongly Connected (SC)›
definition sc :: "'s mdpc  bool"
  where "sc φ  states φ × states φ  (en φ)*"

lemma scD: "sc φ  x  states φ  y  states φ  (x, y)  (en φ)*"
  by (auto simp: sc_def)

lemma scI: "(x y. x  states φ  y  states φ  (x, y)  (en φ)*)  sc φ"
  by (auto simp: sc_def)

lemma sc_trivial[simp]: "sc (trivial s)"
  by (simp add: sc_def)

lemma sc_loop[simp]: "sc (loop s)"
  by (auto simp: sc_def)

lemma sc_bot[simp]: "sc bot"
  by (simp add: sc_def)

lemma sc_SupI_directed:
  assumes A: "a. a  A  sc a"
    and directed: "a b. a  A  b  A  cA. a  c  b  c"
  shows "sc (Sup A)"
  unfolding sc_def
proof clarsimp
  fix x y a b assume "a  A" "b  A" and xy: "x  states a" "y  states b"
  with directed obtain c where "c  A" "a  c" "b  c"
    by auto
  with xy have "x  states c" "y  states c"
    using states_mono[of a c] states_mono[of b c] by auto
  with A[OF c  A] c  A
  have "(x, y)  (en c)*"
    by (auto simp: sc_def subset_eq)
  then show "(x, y)  (xA. en x)*"
    using rtrancl_mono[of "en c" "aA. en a"] cA by auto
qed

lemma sc_supI:
  assumes φ: "sc φ" and ψ: "sc ψ" and not_disjoint: "φ  ψ  bot"
  shows "sc (φ  ψ)"
  unfolding sc_def
proof safe
  fix x y assume "x  states (φ  ψ)" "y  states (φ  ψ)"
  moreover obtain z where "z  states φ" "z  states ψ"
    using not_disjoint by (auto simp: inf_eq_bot_eq_disjnt_states disjnt_def)
  moreover have "(en φ)*  (en ψ)*  (en (φ  ψ))*"
    by (metis rtrancl_Un_subset en_sup)
  ultimately have "(x, z)  (en (φ  ψ))*" "(z, y)  (en (φ  ψ))*"
    using φ ψ by (auto dest: scD)
  then show "(x, y)  (en (φ  ψ))*"
    by auto
qed

lemma sc_eq_loop:
  assumes M: "sc M" and s: "s  M" "actions M s = {return_pmf s}" shows "M = loop s"
proof -
  { fix t assume "t  M"
    then have "(s, t)  (en M)*"
      using M[THEN scD, OF s  M t  M] by simp
    from this have "t = s"
      by (induction rule: rtrancl_induct) (auto simp: en_def actions M s = {return_pmf s}) }
  then have "states M = {s}"
    using s  M by blast
  then show ?thesis
    by (intro mdpc_eqI) (auto simp: actions M s = {return_pmf s})
qed

lemma sc_eq_trivial:
  assumes M: "sc M" and s: "s  M" "actions M s = {}" shows "M = trivial s"
proof -
  { fix t assume "t  M" "t  s"
    then have "(s, t)  (en M)+"
      using M[THEN scD, OF s  M t  M] by (simp add: rtrancl_eq_or_trancl)
    from tranclD[OF this] actions M s = {} have False
      by (auto simp: en_def) }
  then have "states M = {s}"
    using s  M by auto
  then show ?thesis
    by (intro mdpc_eqI) (auto simp: actions M s = {})
qed

definition closed_mdpc :: "'s mdpc  bool"
  where "closed_mdpc φ  en φ  states φ × states φ"

lemma closed_mdpcD: "closed_mdpc φ  D  actions φ x  y  D  y  states φ"
  by (auto simp: closed_mdpc_def en_def)

lemma closed_mdpc_supI: "closed_mdpc φ  closed_mdpc ψ  closed_mdpc (φ  ψ)"
  by (auto simp: closed_mdpc_def)

lemma closed_mdpc_SupI: "(a. a  A  closed_mdpc a)  closed_mdpc (A)"
  by (auto simp: closed_mdpc_def)

lemma closed_mdpc_infI: "closed_mdpc φ  closed_mdpc ψ  closed_mdpc (φ  ψ)"
  using en_mono[of "φ  ψ" φ] en_mono[of "φ  ψ" ψ]
  by (auto simp: closed_mdpc_def lift_option_eq_Some)

lemma closed_mdpc_trivial[simp]: "closed_mdpc (trivial s)"
  by (simp add: closed_mdpc_def)

lemma closed_mdpc_bot[simp]: "closed_mdpc bot"
  by (simp add: closed_mdpc_def)

lemma closed_mdpc_loop[simp]: "closed_mdpc (loop s)"
  by (auto simp: closed_mdpc_def)

lemma closed_mdpc_fix_loop: "closed_mdpc M  closed_mdpc (fix_loop s M)"
  by (auto simp: closed_mdpc_def)

lemma closed_mdpc_map: assumes M: "closed_mdpc M" shows "closed_mdpc (map_mdpc f M)"
  using closed_mdpcD[OF M]
  by (auto simp: closed_mdpc_def en_def actions_map_mdpc states_map_mdpc intro!: imageI intro: in_states)

definition close :: "'s mdpc  's mdpc"
  where "close φ = map_actions (λs A. {aA. set_pmf a  states φ}) φ"

lemma
  shows states_close[simp]: "states (close φ) = states φ"
    and actions_close[simp]: "actions (close φ) s = {aactions φ s. a  states φ}"
  by (auto simp: close_def)

lemma closed_close: "closed_mdpc (close φ)"
  by (auto simp add: closed_mdpc_def en_def intro: in_states)

lemma close_closed: "closed_mdpc φ  close φ = φ"
  unfolding closed_mdpc_def by (intro mdpc_eqI) (auto simp: en_def)

lemma close_close: "close (close φ) = close φ"
  by (simp add: closed_close close_closed)

lemma close_le: "close M  M"
  unfolding close_def by (intro map_actions_le) auto

lemma close_mono: "φ  ψ  close φ  close ψ"
  using states_mono[of φ ψ] actions_mono[of φ ψ]
  unfolding close_def by (intro le_mdpcI) (auto simp: le_fun_def)

text ‹End Component (EC)›
definition ec :: "'s mdpc  bool"
  where "ec φ  sc φ  closed_mdpc φ"

lemma ec_trivial[simp]: "ec (trivial s)"
  by (auto simp: ec_def)

lemma ec_bot[simp]: "ec bot"
  by (auto simp: ec_def)

lemma ec_loop[simp]: "ec (loop s)"
  by (auto simp: ec_def)

lemma ec_sup: "ec φ  ec ψ  φ  ψ  bot  ec (φ  ψ)"
  by (simp add: ec_def sc_supI closed_mdpc_supI)

lemma ec_Sup_directed:
  "(a. a  A  ec a)  (a b. a  A  b  A  cA. a  c  b  c)  ec (A)"
  by (auto simp: ec_def closed_mdpc_SupI sc_SupI_directed)

text ‹Maximal End Component (MEC) relative to @{term M}
definition mec :: "'s mdpc  's mdpc  bool"
  where "mec M φ  ec φ  φ  M  (ψM. ec ψ  φ  ψ  φ = ψ)"

lemma mec_refl: "ec M  mec M M"
  by (auto simp: mec_def)

lemma mec_le: "mec M φ  φ  M"
  by (auto simp: mec_def)

lemma mec_ec: "mec M φ  ec φ"
  by (auto simp: mec_def)

lemma mec_least: "mec M φ  ψ  M  φ  ψ  ec ψ  φ  ψ"
  by (auto simp: mec_def)

lemma mec_bot_imp_bot: assumes "mec φ bot" shows "φ = bot"
proof (rule ccontr)
  assume "φ  bot"
  then obtain x where "x  states φ"
    unfolding eq_bot_iff_states by auto
  then have "ec (trivial x)" "trivial x  φ"
    by (auto intro: trivial_le)
  then have "trivial x = bot"
    using mec φ bot by (auto simp: mec_def)
  then show False
    by (simp add: trivial_neq_bot)
qed

lemma mec_imp_bot_eq_bot: "mec φ ψ  φ = bot  ψ = bot"
  using mec_bot_imp_bot[of φ] by (auto simp: mec_def)

lemma mec_unique: assumes φ: "mec M φ" and ψ: "mec M ψ" and "φ  ψ  bot" shows "φ = ψ"
proof -
  have "mec M (φ  ψ)"
    using assms
    by (auto intro!: mec_def[THEN iffD2] ec_sup antisym dest: mec_ec mec_le)
       (blast intro: le_supI1 mec_least[of M])
  with mec_least[OF φ, of "φ  ψ"] mec_least[OF ψ,  of "φ  ψ"] mec_le[OF this] mec_ec[OF this]
  show "φ = ψ"
    by auto
qed

lemma mec_exists: assumes φ: "φ  bot" "ec φ" and M: "φ  M" shows "ψφ. mec M ψ"
proof (intro exI conjI)
  show "φ  {ψ. φ  ψ  ψ  M  ec ψ}"
    using φ M by (intro Sup_upper) auto
  show "mec M ({ψ. φ  ψ  ψ  M  ec ψ})"
    unfolding mec_def
  proof safe
    show "ec ({ψ. φ  ψ  ψ  M  ec ψ})"
    proof (safe intro!: ec_Sup_directed)
      fix a b assume *: "φ  a" "φ  b" and "a  M" "b  M" "ec a" "ec b"
      moreover have "a  b  bot"
        using * φ bot_unique[of "φ"] le_inf_iff[of φ a b] by metis
      ultimately show "c{ψ. φ  ψ  ψ  M  ec ψ}. a  c  b  c"
        by (intro bexI[of _ "sup a b"]) (auto intro: le_supI1 intro!: ec_sup)
    qed
    fix ψ assume ψ: "ψ  M" "ec ψ" "{ψ. φ  ψ  ψ  M  ec ψ}  ψ"
    have "φ  {ψ. φ  ψ  ψ  M  ec ψ}"
      using assms by (auto intro!: Sup_upper)
    also have "  ψ" by fact
    finally show "{ψ. φ  ψ  ψ  M  ec ψ} = ψ"
      using ψ by (intro antisym Sup_upper) auto
  qed (auto intro!: Sup_least)
qed

lemma mec_exists': "x  states M  ψ. x  states ψ  mec M ψ"
  using mec_exists[of "trivial x"] by (auto simp: trivial_neq_bot trivial_le_iff)

lemma mec_loop: "x  states M  actions M x = {return_pmf x}  mec M (loop x)"
  apply (auto simp: mec_def loop_le ec_def)
  subgoal for φ
    using sc_eq_loop[of φ x] actions_mono[of φ M, THEN le_funD, of x] by auto
  done

lemma mec_fix_loop: "mec (fix_loop s M) (loop s)"
  by (intro mec_loop) auto

definition trivials :: "'s mdpc  's set"
  where "trivials M = {x. mec M (trivial x)}"

lemma trivials_subset_states: "trivials M  states M"
  by (auto simp: trivials_def mec_def trivial_le_iff)

text ‹Bottom MEC (BEMC) in @{term M}
definition bmec :: "'s mdpc  's mdpc  bool"
  where "bmec M φ  mec φ M  (sstates φ. actions φ s = actions M s)"

definition actions' :: "'s mdpc  's  's pmf set"
  where "actions' M s = (if s  states M then actions M s else {return_pmf s})"

lemma closed_mdpcD':
  "closed_mdpc M  s  states M  (Dactions' M s. set_pmf D)  states M"
  by (auto simp: actions'_def dest: closed_mdpcD)

locale Finite_MDP =
  fixes M :: "'s mdpc"
  assumes closed_M: "closed_mdpc M" and M_neq_bot: "M  bot"
    and actions_neq_empty_M: "s. s  states M  actions M s  {}"
    and finite_states_M: "finite M"
    and finite_actions_M: "s. finite (actions M s)"
begin

sublocale Finite_Markov_Decision_Process "actions' M" "states M"
proof
  show "actions' M s  {}" for s
    using actions_neq_empty_M by (auto simp: actions'_def )
  show "states M  {}" "finite M" "s. finite (actions' M s)"
    using M_neq_bot finite_states_M finite_actions_M by (auto simp: eq_bot_iff_states actions'_def)
  show "s  states M  (Dactions' M s. set_pmf D)  states M" for s
    using closed_M by (rule closed_mdpcD')
qed

lemma Finite_MDP_map_loop: "Finite_MDP (map_mdpc f M  loop s)"
proof
  show "closed_mdpc (map_mdpc f M  loop s)"
    by (intro closed_mdpc_supI closed_mdpc_map closed_M closed_mdpc_loop)
  show "finite (actions (map_mdpc f M  loop s) t)" for t
    by (auto simp: actions_loop intro!: finite_actions_map finite_states_M finite_actions_M)
  show "finite (map_mdpc f M  loop s)"
    by (auto intro!: finite_states_M finite_states_map)
qed (auto simp: loop_neq_bot states_map_mdpc actions_loop actions_map_mdpc dest: actions_neq_empty_M)

lemma Finite_MDP_map_fix_loop: "Finite_MDP (fix_loop s (map_mdpc f M))"
proof
  show "closed_mdpc (fix_loop s (map_mdpc f M))"
    by (intro closed_mdpc_supI closed_mdpc_map closed_M closed_mdpc_fix_loop)
  show "finite (actions (fix_loop s (map_mdpc f M)) t)" for t
    by (auto simp: actions_loop intro!: finite_actions_map finite_states_M finite_actions_M)
  show "finite (fix_loop s (map_mdpc f M))"
    by (auto intro!: finite_states_M finite_states_map)
qed (auto simp: fix_loop_neq_bot states_map_mdpc actions_map_mdpc dest: actions_neq_empty_M)

end

context
  fixes M :: "'s mdpc"
    and F :: "'s set"
  assumes M_neq_bot: "M  bot"
    and closed_M: "closed_mdpc M"
    and actions_neq_empty_M: "s. s  states M  actions M s  {}"
    and finite_states_M: "finite M"
    and finite_actions_M: "s. finite (actions M s)"
    and F_subset: "F  states M"
begin

lemma finite_F[simp]: "finite F"
  using F_subset finite_states_M by (auto dest: finite_subset)

interpretation M: Finite_MDP M
  proof qed fact+

interpretation M: Reachability_Problem "actions' M" "states M" "states M - F" F
  proof qed (insert F_subset, auto)

definition r :: "'s  's option"
  where "r s = (if s  F then None else Some s)"

lemma r_eq_None[simp]: "r s = None  s  F"
  by (simp add: r_def)

lemma r_eq_Some[simp]: "r s = Some t  (s  F  s = t)"
  by (simp add: r_def)

lemma r_in_Some_image: "r s  Some ` X  (s  F  s  X)"
  by (auto simp: r_def)

lemma r_inj: "s  F  t  F  r s = r t  s = t"
  by (auto simp: r_def)

lemma shows r_F: "s  F  r s = None" and r_nF: "s  F  r s = Some s"
  by auto

definition R :: "'s option mdpc"
  where "R = fix_loop None (map_mdpc r M)"

lemma closed_R: "closed_mdpc R"
  unfolding R_def by (intro closed_mdpc_map closed_M closed_mdpc_fix_loop)

lemma states_R[simp]: "states R = Some ` (states M - F)  {None}"
  by (auto simp add: R_def r_def[abs_def] states_map_mdpc)

lemma actions_R_None[simp]:
  "actions R None = {return_pmf None}"
  by (auto simp add: R_def)

lemma actions_R_Some[simp]:
  "actions R (Some s) = (if s  F then {} else map_pmf r ` actions M s)"
  by (auto simp add: R_def actions_map_mdpc split: if_splits intro!: imageI)

lemma mec_R_loop: "mec R (loop None)"
  unfolding R_def by (intro mec_fix_loop)

interpretation R: Finite_MDP R
  unfolding R_def by (rule M.Finite_MDP_map_fix_loop)

interpretation R: Reachability_Problem "actions' R" "states R" "{None}" "{}"
  proof qed auto

lemma F_not_trivial: "s  F  Some s  trivials R"
  by (auto simp: trivials_def mec_def trivial_le_iff)

primrec min_state :: "'s option  's + bool"
  where
    "min_state None = Inr True"
  | "min_state (Some s) = (if Some s  trivials R then Inl s else Inr False)"

lemma min_state_eq_Inl: "min_state s = Inl t  (Some t  trivials R  s = Some t)"
  by (cases s) auto

lemma min_state_eq_Inr: "min_state s = Inr b  (if b then s = None else s  None  s  trivials R)"
  by (cases s) auto

lemma map_min_state_R: "map_mdpc min_state R = fix_loop (Inr True) (map_mdpc (min_state  r) M)"
  unfolding R_def
  by (subst map_fix_loop)
     (auto simp: map_mdpc_compose min_state_eq_Inr eq_commute[of "Inr True"])

definition min_mdpc :: "('s + bool) mdpc"
  where "min_mdpc = fix_loop (Inr False) (map_mdpc min_state R)"

lemma states_min_mdpc: "states min_mdpc = {Inl t | t. Some t  trivials R}  {Inr True, Inr False}"
  using trivials_subset_states[of R] by (auto simp add: min_mdpc_def states_map_mdpc image_comp split: if_splits)

lemma actions_min_mdpc_Inl:
  "actions min_mdpc (Inl t) = (if Some t  trivials R then map_pmf (min_state  r) ` actions M t else {})"
proof -
  have eq: "min_state -` {Inl t} = (if Some t  trivials R then {Some t} else {})"
    by (auto simp: min_state_eq_Inl)
  show ?thesis using F_not_trivial[of t]
    by (simp add: min_mdpc_def actions_map_mdpc eq image_comp map_pmf_compose[symmetric])
qed

lemma actions_min_mdpc_Inr: "actions min_mdpc (Inr b) = {return_pmf (Inr b)}"
  by (simp add: min_mdpc_def map_min_state_R)

interpretation min: Finite_MDP min_mdpc
  unfolding min_mdpc_def by (rule R.Finite_MDP_map_fix_loop)

interpretation min: Reachability_Problem "actions' min_mdpc" "states min_mdpc" "states min_mdpc - {Inr True}" "{Inr True}"
  proof qed (auto simp: states_min_mdpc)

lemma M_n_eq_0_not_trivials:
  assumes "s  states M" "s  F" "Some s  trivials R"
  shows "M.n s = 0"
proof -
  have "Some s  states R"
    using assms by auto

  obtain φ where "mec R φ" "s  Some -` φ"
    using mec_exists'[OF Some s  states R] by auto
  then have action_φ: "Some t  φ  actions φ (Some t)  {}" for t
    using mec_ec[OF mec R φ] Some s  trivials R sc_eq_trivial[of φ "Some t"]
    by (auto simp: ec_def trivials_def)

  have None_notin_states: "None  states φ"
    using mec_R_loop mec R φ s  Some -` φ mec_unique[of R "loop None" φ]
    by (auto simp: inf_eq_bot_eq_disjnt_states disjnt_def)

  from s  Some -` φ show "M.n s = 0"
  proof (rule M.n_eq_0_closed)
    show "Some -` states φ  states M" "Some -` states φ  F = {}"
      using mec_le[OF mec R φ] by (auto simp: r_def le_mdpc_iff)
    fix s assume "s  Some -` φ"
    then have s: "s  states M" "s  F" "actions φ (Some s)  {}"
      using mec_le[OF mec R φ] by (auto simp: le_mdpc_iff action_φ)
    then obtain D where D: "D  actions φ (Some s)"
      by auto
    then have "D  actions R (Some s)"
      using mec_le[OF mec R φ, THEN actions_mono] s by (auto simp add: le_fun_def simp del: actions_R_Some)
    with s obtain D' where D_eq: "D = map_pmf r D'" and D': "D'  actions M s"
      by auto
    have "set_pmf D  states φ"
      using closed_mdpcD[OF _ D] mec_ec[OF mec R φ] by (auto simp: ec_def)
    then have "set_pmf D = Some ` set_pmf D'"
      using closed_mdpcD[of φ, OF _ D  actions φ (Some s)] None_notin_states
        mec_ec[OF mec R φ]
      unfolding D_eq by (auto intro!: image_cong simp: r_def ec_def)
    then show "xactions' M s. set_pmf x  Some -` states φ"
      using s  states M set_pmf D  states φ D'
      by (intro bexI[of _ D']) (auto simp: actions'_def)
  qed
qed

lemma min_state_r_in_min_mdpc[simp]: "s  M  min_state (r s)  min_mdpc"
  by (auto simp add: states_min_mdpc min_state_eq_Inr min_state_eq_Inl r_def)

end

end