src/HOL/Library/State_Monad.thy

 context begin
 
 qualified definition return :: "'a \<Rightarrow> ('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 \<Rightarrow> 'b) state \<Rightarrow> ('s, 'a) state \<Rightarrow> ('s, 'b) state" where
 "ap f x = State (\<lambda>s. case run_state f s of (g, s') \<Rightarrow> case run_state x s' of (y, s'') \<Rightarrow> (g y, s''))"
 
 qualified definition bind :: "('s, 'a) state \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state) \<Rightarrow> ('s, 'b) state" where
 "bind x f = State (\<lambda>s. case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"

 unfolding bind_def get_def set_def return_def
 by simp
 
 lemma set_set[simp]: "bind (set s) (\<lambda>_. set s') = set s'"
 unfolding bind_def set_def
+by simp
+
+lemma get_bind_set[simp]: "bind get (\<lambda>s. bind (set s) (f s)) = bind get (\<lambda>s. f s ())"
+unfolding bind_def get_def set_def
+by simp
+
+lemma get_const[simp]: "bind get (\<lambda>_. m) = m"
+unfolding get_def bind_def
 by simp
 
 fun traverse_list :: "('a \<Rightarrow> ('b, 'c) state) \<Rightarrow> 'a list \<Rightarrow> ('b, 'c list) state" where
 "traverse_list _ [] = return []" |
 "traverse_list f (x # xs) = do {

 
 lemma update_comp[simp]: "bind (update f) (\<lambda>_. update g) = update (g \<circ> f)"
 unfolding update_def return_def get_def set_def bind_def
 by auto
 
+lemma set_update[simp]: "bind (set s) (\<lambda>_. 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) (\<lambda>_. 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 "\<And>x. x \<le> f x"
   shows "mono_state (update f)"
 using assms unfolding update_def get_def set_def bind_def
 by (auto intro!: state_io_relI)