# HG changeset patch # User Lars Hupel # 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 \ ('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''))" @@ -109,6 +113,14 @@ 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 { @@ -196,6 +208,14 @@ 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)"