--- a/src/HOL/Library/State_Monad.thy Fri Aug 17 20:44:45 2018 +0200
+++ b/src/HOL/Library/State_Monad.thy Fri Aug 17 21:34:12 2018 +0200
@@ -78,9 +78,17 @@
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''))"
+lemma run_state_ap[simp]:
+ "run_state (ap f x) s = (case run_state f s of (g, s') \<Rightarrow> case run_state x s' of (y, s'') \<Rightarrow> (g y, s''))"
+unfolding ap_def by auto
+
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')"
+lemma run_state_bind[simp]:
+ "run_state (bind x f) s = (case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
+unfolding bind_def by auto
+
adhoc_overloading Monad_Syntax.bind bind
lemma bind_left_identity[simp]: "bind (return a) f = f a"
@@ -102,9 +110,15 @@
qualified definition get :: "('s, 's) state" where
"get = State (\<lambda>s. (s, s))"
+lemma run_state_get[simp]: "run_state get s = (s, s)"
+unfolding get_def by simp
+
qualified definition set :: "'s \<Rightarrow> ('s, unit) state" where
"set s' = State (\<lambda>_. ((), 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
@@ -230,4 +244,4 @@
end
-end
+end
\ No newline at end of file