src/HOL/Library/State_Monad.thy
changeset 66275 2c1d223c5417
parent 66271 d157195a468a
child 67399 eab6ce8368fa
equal deleted inserted replaced
66274:be8d3819c21c 66275:2c1d223c5417
    69 context begin
    69 context begin
    70 
    70 
    71 qualified definition return :: "'a \<Rightarrow> ('s, 'a) state" where
    71 qualified definition return :: "'a \<Rightarrow> ('s, 'a) state" where
    72 "return a = State (Pair a)"
    72 "return a = State (Pair a)"
    73 
    73 
       
    74 lemma run_state_return[simp]: "run_state (return x) s = (x, s)"
       
    75 unfolding return_def
       
    76 by simp
       
    77 
    74 qualified definition ap :: "('s, 'a \<Rightarrow> 'b) state \<Rightarrow> ('s, 'a) state \<Rightarrow> ('s, 'b) state" where
    78 qualified definition ap :: "('s, 'a \<Rightarrow> 'b) state \<Rightarrow> ('s, 'a) state \<Rightarrow> ('s, 'b) state" where
    75 "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''))"
    79 "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''))"
    76 
    80 
    77 qualified definition bind :: "('s, 'a) state \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state) \<Rightarrow> ('s, 'b) state" where
    81 qualified definition bind :: "('s, 'a) state \<Rightarrow> ('a \<Rightarrow> ('s, 'b) state) \<Rightarrow> ('s, 'b) state" where
    78 "bind x f = State (\<lambda>s. case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
    82 "bind x f = State (\<lambda>s. case run_state x s of (a, s') \<Rightarrow> run_state (f a) s')"
   105 unfolding bind_def get_def set_def return_def
   109 unfolding bind_def get_def set_def return_def
   106 by simp
   110 by simp
   107 
   111 
   108 lemma set_set[simp]: "bind (set s) (\<lambda>_. set s') = set s'"
   112 lemma set_set[simp]: "bind (set s) (\<lambda>_. set s') = set s'"
   109 unfolding bind_def set_def
   113 unfolding bind_def set_def
       
   114 by simp
       
   115 
       
   116 lemma get_bind_set[simp]: "bind get (\<lambda>s. bind (set s) (f s)) = bind get (\<lambda>s. f s ())"
       
   117 unfolding bind_def get_def set_def
       
   118 by simp
       
   119 
       
   120 lemma get_const[simp]: "bind get (\<lambda>_. m) = m"
       
   121 unfolding get_def bind_def
   110 by simp
   122 by simp
   111 
   123 
   112 fun traverse_list :: "('a \<Rightarrow> ('b, 'c) state) \<Rightarrow> 'a list \<Rightarrow> ('b, 'c list) state" where
   124 fun traverse_list :: "('a \<Rightarrow> ('b, 'c) state) \<Rightarrow> 'a list \<Rightarrow> ('b, 'c list) state" where
   113 "traverse_list _ [] = return []" |
   125 "traverse_list _ [] = return []" |
   114 "traverse_list f (x # xs) = do {
   126 "traverse_list f (x # xs) = do {
   194 
   206 
   195 lemma update_comp[simp]: "bind (update f) (\<lambda>_. update g) = update (g \<circ> f)"
   207 lemma update_comp[simp]: "bind (update f) (\<lambda>_. update g) = update (g \<circ> f)"
   196 unfolding update_def return_def get_def set_def bind_def
   208 unfolding update_def return_def get_def set_def bind_def
   197 by auto
   209 by auto
   198 
   210 
       
   211 lemma set_update[simp]: "bind (set s) (\<lambda>_. update f) = set (f s)"
       
   212 unfolding set_def update_def bind_def get_def set_def
       
   213 by simp
       
   214 
       
   215 lemma set_bind_update[simp]: "bind (set s) (\<lambda>_. bind (update f) g) = bind (set (f s)) g"
       
   216 unfolding set_def update_def bind_def get_def set_def
       
   217 by simp
       
   218 
   199 lemma update_mono:
   219 lemma update_mono:
   200   assumes "\<And>x. x \<le> f x"
   220   assumes "\<And>x. x \<le> f x"
   201   shows "mono_state (update f)"
   221   shows "mono_state (update f)"
   202 using assms unfolding update_def get_def set_def bind_def
   222 using assms unfolding update_def get_def set_def bind_def
   203 by (auto intro!: state_io_relI)
   223 by (auto intro!: state_io_relI)