# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1534534452 -7200
# Node ID 7066e83dfe46a3acef19c4669505578bdc7f7df5
# Parent  67d6f1708ea47be14501e81c2d42e1cc37ddf555
State_Monad: more simp lemmas

diff -r 67d6f1708ea4 -r 7066e83dfe46 src/HOL/Library/State_Monad.thy
--- 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