--- a/src/HOL/Library/State_Monad.thy Sat Nov 18 00:20:26 2006 +0100
+++ b/src/HOL/Library/State_Monad.thy Sat Nov 18 00:20:27 2006 +0100
@@ -144,7 +144,6 @@
"\<And>f. run f = f \<longleftrightarrow> True"
unfolding run_def by rule+
-
subsection {* Monad laws *}
text {*
@@ -161,6 +160,14 @@
unfolding mbind_def by (simp add: expand_fun_eq split_Pair)
lemma
+ id_fcomp [simp]: "id \<guillemotright> f = f"
+ unfolding fcomp_def by simp
+
+lemma
+ fcomp_id [simp]: "f \<guillemotright> id = f"
+ unfolding fcomp_def by simp
+
+lemma
mbind_mbind [simp]: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"
unfolding mbind_def by (simp add: split_def expand_fun_eq)
@@ -176,7 +183,7 @@
fcomp_fcomp [simp]: "(f \<guillemotright> g) \<guillemotright> h = f \<guillemotright> (g \<guillemotright> h)"
unfolding fcomp_def o_assoc ..
-lemmas monad_simp = run_simp return_mbind mbind_return
+lemmas monad_simp = run_simp return_mbind mbind_return id_fcomp fcomp_id
mbind_mbind mbind_fcomp fcomp_mbind fcomp_fcomp
text {*
@@ -246,6 +253,61 @@
] end;
*}
+subsection {* Combinators *}
+
+definition
+ lift :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'c \<Rightarrow> 'b \<times> 'c"
+ "lift f x = return (f x)"
+
+fun
+ list :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
+ "list f [] = id"
+ "list f (x#xs) = (do f x; list f xs done)"
+lemmas [code] = list.simps
+
+fun 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)"
+lemmas [code] = list_yield.simps
+
+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*)
+
+lemma list_cong [fundef_cong, recdef_cong]:
+ "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
+ \<Longrightarrow> list f xs = list g ys"
+proof (induct f xs arbitrary: g ys rule: list.induct)
+ case 1 then show ?case by simp
+next
+ case (2 f x xs g)
+ from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
+ then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
+ with 2 have "list f xs = list g xs" by auto
+ with 2 have "list f (x # xs) = list g (x # xs)" by auto
+ with 2 show "list f (x # xs) = list g ys" by auto
+qed
+
+lemma list_yield_cong [fundef_cong, recdef_cong]:
+ "\<lbrakk> \<And>x. x \<in> set xs \<Longrightarrow> f x = g x; xs = ys \<rbrakk>
+ \<Longrightarrow> list_yield f xs = list_yield g ys"
+proof (induct f xs arbitrary: g ys rule: list_yield.induct)
+ case 1 then show ?case by simp
+next
+ case (2 f x xs g)
+ from 2 have "\<And>y. y \<in> set (x # xs) \<Longrightarrow> f y = g y" by auto
+ then have "\<And>y. y \<in> set xs \<Longrightarrow> f y = g y" by auto
+ with 2 have "list_yield f xs = list_yield g xs" by auto
+ with 2 have "list_yield f (x # xs) = list_yield g (x # xs)" by auto
+ with 2 show "list_yield f (x # xs) = list_yield g ys" by auto
+qed
+
+text {*
+ still waiting for extensions@{text "\<dots>"}
+*}
+
text {*
For an example, see HOL/ex/CodeRandom.thy (more examples coming soon).
*}