```(*  Title:      HOL/Library/State_Monad.thy
Author:     Lars Hupel, TU München
*)

begin

datatype ('s, 'a) state = State (run_state: "'s ⇒ ('a × 's)")

lemma set_state_iff: "x ∈ set_state m ⟷ (∃s s'. run_state m s = (x, s'))"
by (cases m) (simp add: prod_set_defs eq_fst_iff)

lemma pred_stateI[intro]:
assumes "⋀a s s'. run_state m s = (a, s') ⟹ P a"
shows "pred_state P m"
proof (subst state.pred_set, rule)
fix x
assume "x ∈ set_state m"
then obtain s s' where "run_state m s = (x, s')"
by (auto simp: set_state_iff)
with assms show "P x" .
qed

lemma pred_stateD[dest]:
assumes "pred_state P m" "run_state m s = (a, s')"
shows "P a"
proof (rule state.exhaust[of m])
fix f
assume "m = State f"
with assms have "pred_fun (λ_. True) (pred_prod P top) f"
by (metis state.pred_inject)
moreover have "f s = (a, s')"
using assms unfolding ‹m = _› by auto
ultimately show "P a"
unfolding pred_prod_beta pred_fun_def
by (metis fst_conv)
qed

lemma pred_state_run_state: "pred_state P m ⟹ P (fst (run_state m s))"
by (meson pred_stateD prod.exhaust_sel)

definition state_io_rel :: "('s ⇒ 's ⇒ bool) ⇒ ('s, 'a) state ⇒ bool" where
"state_io_rel P m = (∀s. P s (snd (run_state m s)))"

lemma state_io_relI[intro]:
assumes "⋀a s s'. run_state m s = (a, s') ⟹ P s s'"
shows "state_io_rel P m"
using assms unfolding state_io_rel_def
by (metis prod.collapse)

lemma state_io_relD[dest]:
assumes "state_io_rel P m" "run_state m s = (a, s')"
shows "P s s'"
using assms unfolding state_io_rel_def
by (metis snd_conv)

lemma state_io_rel_mono[mono]: "P ≤ Q ⟹ state_io_rel P ≤ state_io_rel Q"
by blast

lemma state_ext:
assumes "⋀s. run_state m s = run_state n s"
shows "m = n"
using assms
by (cases m; cases n) auto

context begin

qualified definition return :: "'a ⇒ ('s, 'a) state" where
"return a = State (Pair a)"

lemma run_state_return[simp]: "run_state (return x) s = (x, s)"
unfolding return_def
by simp

qualified definition ap :: "('s, 'a ⇒ 'b) state ⇒ ('s, 'a) state ⇒ ('s, 'b) state" where
"ap f x = State (λs. case run_state f s of (g, s') ⇒ case run_state x s' of (y, s'') ⇒ (g y, s''))"

lemma run_state_ap[simp]:
"run_state (ap f x) s = (case run_state f s of (g, s') ⇒ case run_state x s' of (y, s'') ⇒ (g y, s''))"
unfolding ap_def by auto

qualified definition bind :: "('s, 'a) state ⇒ ('a ⇒ ('s, 'b) state) ⇒ ('s, 'b) state" where
"bind x f = State (λs. case run_state x s of (a, s') ⇒ run_state (f a) s')"

lemma run_state_bind[simp]:
"run_state (bind x f) s = (case run_state x s of (a, s') ⇒ run_state (f a) s')"
unfolding bind_def by auto

lemma bind_left_identity[simp]: "bind (return a) f = f a"
unfolding return_def bind_def by simp

lemma bind_right_identity[simp]: "bind m return = m"
unfolding return_def bind_def by simp

lemma bind_assoc[simp]: "bind (bind m f) g = bind m (λx. bind (f x) g)"
unfolding bind_def by (auto split: prod.splits)

lemma bind_predI[intro]:
assumes "pred_state (λx. pred_state P (f x)) m"
shows "pred_state P (bind m f)"
apply (rule pred_stateI)
unfolding bind_def
using assms by (auto split: prod.splits)

qualified definition get :: "('s, 's) state" where
"get = State (λs. (s, s))"

lemma run_state_get[simp]: "run_state get s = (s, s)"
unfolding get_def by simp

qualified definition set :: "'s ⇒ ('s, unit) state" where
"set s' = State (λ_. ((), s'))"

lemma run_state_set[simp]: "run_state (set s') s = ((), s')"
unfolding set_def by simp

lemma get_set[simp]: "bind get set = return ()"
unfolding bind_def get_def set_def return_def
by simp

lemma set_set[simp]: "bind (set s) (λ_. set s') = set s'"
unfolding bind_def set_def
by simp

lemma get_bind_set[simp]: "bind get (λs. bind (set s) (f s)) = bind get (λs. f s ())"
unfolding bind_def get_def set_def
by simp

lemma get_const[simp]: "bind get (λ_. m) = m"
unfolding get_def bind_def
by simp

fun traverse_list :: "('a ⇒ ('b, 'c) state) ⇒ 'a list ⇒ ('b, 'c list) state" where
"traverse_list _ [] = return []" |
"traverse_list f (x # xs) = do {
x ← f x;
xs ← traverse_list f xs;
return (x # xs)
}"

lemma traverse_list_app[simp]: "traverse_list f (xs @ ys) = do {
xs ← traverse_list f xs;
ys ← traverse_list f ys;
return (xs @ ys)
}"
by (induction xs) auto

lemma traverse_comp[simp]: "traverse_list (g ∘ f) xs = traverse_list g (map f xs)"
by (induction xs) auto

abbreviation mono_state :: "('s::preorder, 'a) state ⇒ bool" where
"mono_state ≡ state_io_rel (≤)"

abbreviation strict_mono_state :: "('s::preorder, 'a) state ⇒ bool" where
"strict_mono_state ≡ state_io_rel (<)"

corollary strict_mono_implies_mono: "strict_mono_state m ⟹ mono_state m"
unfolding state_io_rel_def

lemma return_mono[simp, intro]: "mono_state (return x)"
unfolding return_def by auto

lemma get_mono[simp, intro]: "mono_state get"
unfolding get_def by auto

lemma put_mono:
assumes "⋀x. s' ≥ x"
shows "mono_state (set s')"
using assms unfolding set_def
by auto

lemma map_mono[intro]: "mono_state m ⟹ mono_state (map_state f m)"
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)

lemma map_strict_mono[intro]: "strict_mono_state m ⟹ strict_mono_state (map_state f m)"
by (auto intro!: state_io_relI split: prod.splits simp: map_prod_def state.map_sel)

lemma bind_mono_strong:
assumes "mono_state m"
assumes "⋀x s s'. run_state m s = (x, s') ⟹ mono_state (f x)"
shows "mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: order_trans)

lemma bind_strict_mono_strong1:
assumes "mono_state m"
assumes "⋀x s s'. run_state m s = (x, s') ⟹ strict_mono_state (f x)"
shows "strict_mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: le_less_trans)

lemma bind_strict_mono_strong2:
assumes "strict_mono_state m"
assumes "⋀x s s'. run_state m s = (x, s') ⟹ mono_state (f x)"
shows "strict_mono_state (bind m f)"
unfolding bind_def
apply (rule state_io_relI)
using assms by (auto split: prod.splits dest!: state_io_relD intro: less_le_trans)

corollary bind_strict_mono_strong:
assumes "strict_mono_state m"
assumes "⋀x s s'. run_state m s = (x, s') ⟹ strict_mono_state (f x)"
shows "strict_mono_state (bind m f)"
using assms by (auto intro: bind_strict_mono_strong1 strict_mono_implies_mono)

qualified definition update :: "('s ⇒ 's) ⇒ ('s, unit) state" where
"update f = bind get (set ∘ f)"

lemma update_id[simp]: "update (λx. x) = return ()"
unfolding update_def return_def get_def set_def bind_def
by auto

lemma update_comp[simp]: "bind (update f) (λ_. update g) = update (g ∘ f)"
unfolding update_def return_def get_def set_def bind_def
by auto

lemma set_update[simp]: "bind (set s) (λ_. update f) = set (f s)"
unfolding set_def update_def bind_def get_def set_def
by simp

lemma set_bind_update[simp]: "bind (set s) (λ_. bind (update f) g) = bind (set (f s)) g"
unfolding set_def update_def bind_def get_def set_def
by simp

lemma update_mono:
assumes "⋀x. x ≤ f x"
shows "mono_state (update f)"
using assms unfolding update_def get_def set_def bind_def
by (auto intro!: state_io_relI)

lemma update_strict_mono:
assumes "⋀x. x < f x"
shows "strict_mono_state (update f)"
using assms unfolding update_def get_def set_def bind_def
by (auto intro!: state_io_relI)

end

end```