# HG changeset patch
# User haftmann
# Date 1204009198 -3600
# Node ID e1b3a6953cdc5ccd70e30a34f06e57380f5ba767
# Parent  e453751350528d2ef6187530c7e8e58fd7a57139
operation collapse

diff -r e45375135052 -r e1b3a6953cdc src/HOL/Library/State_Monad.thy
--- a/src/HOL/Library/State_Monad.thy	Tue Feb 26 07:59:57 2008 +0100
+++ b/src/HOL/Library/State_Monad.thy	Tue Feb 26 07:59:58 2008 +0100
@@ -268,12 +268,17 @@
   list_yield :: "('a \<Rightarrow> 'b \<Rightarrow> 'c \<times> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'c list \<times> 'b" where
   "list_yield f [] = return []"
 | "list_yield f (x#xs) = (do y \<leftarrow> f x; ys \<leftarrow> list_yield f xs; return (y#ys) done)"
-  
+
+definition
+  collapse :: "('a \<Rightarrow> ('a \<Rightarrow> 'b \<times> 'a) \<times> 'a) \<Rightarrow> 'a \<Rightarrow> 'b \<times> 'a"
+  where
+  "collapse f = (do g \<leftarrow> f; g done)"
+
 text {* combinator properties *}
 
 lemma list_append [simp]:
   "list f (xs @ ys) = list f xs \<guillemotright> list f ys"
-  by (induct xs) (simp_all del: id_apply) (*FIXME*)
+  by (induct xs) (simp_all del: id_apply)
 
 lemma list_cong [fundef_cong, recdef_cong]:
   "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
@@ -304,10 +309,6 @@
 qed
 
 text {*
-  still waiting for extensions@{text "\<dots>"}
-*}
-
-text {*
   For an example, see HOL/ex/Random.thy.
 *}