# HG changeset patch
# User haftmann
# Date 1318624976 -7200
# Node ID d5086da3c32d11c434b904665dd31e7487c9a03a
# Parent  97e81a8aa27739dec009f14db419af7ba00c49fd
monadic bind

diff -r 97e81a8aa277 -r d5086da3c32d src/HOL/Library/Monad_Syntax.thy
--- a/src/HOL/Library/Monad_Syntax.thy	Fri Oct 14 11:34:30 2011 +0200
+++ b/src/HOL/Library/Monad_Syntax.thy	Fri Oct 14 22:42:56 2011 +0200
@@ -5,7 +5,7 @@
 header {* Monad notation for arbitrary types *}
 
 theory Monad_Syntax
-imports Main "~~/src/Tools/Adhoc_Overloading"
+imports Main "~~/src/Tools/Adhoc_Overloading" "~~/src/HOL/Library/More_List"
 begin
 
 text {*
@@ -73,6 +73,7 @@
   Adhoc_Overloading.add_overloaded @{const_name bind}
   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
+  #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name More_List.bind}
 *}
 
 end
diff -r 97e81a8aa277 -r d5086da3c32d src/HOL/Library/More_List.thy
--- a/src/HOL/Library/More_List.thy	Fri Oct 14 11:34:30 2011 +0200
+++ b/src/HOL/Library/More_List.thy	Fri Oct 14 22:42:56 2011 +0200
@@ -17,6 +17,7 @@
 declare (in complete_lattice) Inf_set_fold [code_unfold del]
 declare (in complete_lattice) Sup_set_fold [code_unfold del]
 
+
 text {* Fold combinator with canonical argument order *}
 
 primrec fold :: "('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b" where
@@ -156,6 +157,7 @@
   "sort xs = fold insort xs []"
   by (rule sort_key_conv_fold) simp
 
+
 text {* @{const Finite_Set.fold} and @{const fold} *}
 
 lemma (in comp_fun_commute) fold_set_remdups:
@@ -268,6 +270,7 @@
   "SUPR (set xs) f = fold (sup \<circ> f) xs bot"
   unfolding SUP_def set_map [symmetric] Sup_set_fold fold_map ..
 
+
 text {* @{text nth_map} *}
 
 definition nth_map :: "nat \<Rightarrow> ('a \<Rightarrow> 'a) \<Rightarrow> 'a list \<Rightarrow> 'a list" where
@@ -295,4 +298,15 @@
   "nth_map (Suc n) f (x # xs) = x # nth_map n f xs"
   by (simp add: nth_map_def)
 
+
+text {* monad operation *}
+
+definition bind :: "'a list \<Rightarrow> ('a \<Rightarrow> 'b list) \<Rightarrow> 'b list" where
+  "bind xs f = concat (map f xs)"
+
+lemma bind_simps [simp]:
+  "bind [] f = []"
+  "bind (x # xs) f = f x @ bind xs f"
+  by (simp_all add: bind_def)
+
 end