# 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
›

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)"

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
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 = {}"

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) = {}"

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 = {}"

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)"

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

lemma sc_bot[simp]: "sc bot"

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)"

lemma closed_mdpc_bot[simp]: "closed_mdpc bot"

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 φ"

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
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"

lemma r_eq_Some[simp]: "r s = Some t ⟷ (s ∉ F ∧ s = t)"

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}"

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)}"

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
```