src/HOL/Library/State_Monad.thy
changeset 26141 e1b3a6953cdc
parent 25765 49580bd58a21
child 26260 23ce0d32de11
     1.1 --- a/src/HOL/Library/State_Monad.thy	Tue Feb 26 07:59:57 2008 +0100
     1.2 +++ b/src/HOL/Library/State_Monad.thy	Tue Feb 26 07:59:58 2008 +0100
     1.3 @@ -268,12 +268,17 @@
     1.4    list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
     1.5    "list_yield f [] = return []"
     1.6  | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
     1.7 -  
     1.8 +
     1.9 +definition
    1.10 +  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
    1.11 +  where
    1.12 +  "collapse f = (do g \<leftarrow> f; g done)"
    1.13 +
    1.14  text {* combinator properties *}
    1.15  
    1.16  lemma list_append [simp]:
    1.17    "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
    1.18 -  by (induct xs) (simp_all del: id_apply) (*FIXME*)
    1.19 +  by (induct xs) (simp_all del: id_apply)
    1.20  
    1.21  lemma list_cong [fundef_cong, recdef_cong]:
    1.22    "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
    1.23 @@ -304,10 +309,6 @@
    1.24  qed
    1.25  
    1.26  text {*
    1.27 -  still waiting for extensions@{text "\<dots>"}
    1.28 -*}
    1.29 -
    1.30 -text {*
    1.31    For an example, see HOL/ex/Random.thy.
    1.32  *}
    1.33