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 x∈⋃A. f x) = (INF a∈A. INF x∈a. 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: "(⋃x∈A. {f x}) = f ` A"
  by auto

lemma image_eq_singeltonD: "f ` A = {x} ⟹ ∀a∈A. 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: "(∀x∈f -` X. P x) ⟷ (∀x. f x ∈ X ⟶ P x)"
  by auto

lemma UN_If_cases: "(⋃x∈X. if P x then A x else B x) = (⋃x∈{x∈X. P x}. A x) ∪ (⋃x∈{x∈X. ¬ 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' ⟹ ∃D∈K 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 ≤ (∑t∈S. 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 ‹s∈S›])
    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 ‹s∈S› 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 ` (⋃t∈f -` {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 "(⋃x∈f -` {s}. actions M x) = (⋃x∈f -` {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 ∃m∈M. 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 ∃m∈M. 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) = (⋃a∈A. 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 = (⋃a∈A. 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) = (⋃a∈A. 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 ⟹ ∃c∈A. 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) ∈ (⋃x∈A. en x)⇧*"
    using rtrancl_mono[of "en c" "⋃a∈A. en a"] ‹c∈A› 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. {a∈A. set_pmf a ⊆ states φ}) φ"

lemma
  shows states_close[simp]: "states (close φ) = states φ"
    and actions_close[simp]: "actions (close φ) s = {a∈actions φ 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 ⟹ ∃c∈A. 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 ∧ (∀s∈states φ. 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 ⟹ (⋃D∈actions' 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 ⟹ (⋃D∈actions' 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 "∃x∈actions' 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