# HG changeset patch
# User Lars Hupel <lars.hupel@mytum.de>
# Date 1499877752 -7200
# Node ID 2c1d223c5417a8eb506d9bf79b789d1a770773d1
# Parent  be8d3819c21cfd4537e651cfce27bc088f31324a
additional lemmas for State_Monad, courtesy of Andreas Lochbihler

diff -r be8d3819c21c -r 2c1d223c5417 src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Wed Jul 12 11:33:32 2017 +0200
+++ b/src/HOL/Library/State_Monad.thy	Wed Jul 12 18:42:32 2017 +0200
@@ -71,6 +71,10 @@
 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''))"
 
@@ -109,6 +113,14 @@
 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 {
@@ -196,6 +208,14 @@
 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)"