uniform do notation for monads

--- a/src/HOL/IsaMakefile	Tue Jul 13 00:15:37 2010 +0200
+++ b/src/HOL/IsaMakefile	Tue Jul 13 00:15:37 2010 +0200
@@ -414,8 +414,8 @@
   Library/LaTeXsugar.thy Library/Lattice_Algebras.thy			\
   Library/Lattice_Syntax.thy Library/Library.thy			\
   Library/List_Prefix.thy Library/List_lexord.thy Library/Mapping.thy	\
-  Library/More_List.thy Library/More_Set.thy Library/Multiset.thy	\
-  Library/Nat_Bijection.thy Library/Nat_Infinity.thy			\
+  Library/Monad_Syntax.thy Library/More_List.thy Library/More_Set.thy	\
+  Library/Multiset.thy Library/Nat_Bijection.thy Library/Nat_Infinity.thy	\
   Library/Nested_Environment.thy Library/Numeral_Type.thy		\
   Library/OptionalSugar.thy Library/Order_Relation.thy			\
   Library/Permutation.thy Library/Permutations.thy			\

--- a/src/HOL/Library/Library.thy	Tue Jul 13 00:15:37 2010 +0200
+++ b/src/HOL/Library/Library.thy	Tue Jul 13 00:15:37 2010 +0200
@@ -32,6 +32,7 @@
   ListVector
   Kleene_Algebra
   Mapping
+  Monad_Syntax
   More_List
   Multiset
   Nat_Infinity

--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Library/Monad_Syntax.thy	Tue Jul 13 00:15:37 2010 +0200
@@ -0,0 +1,60 @@
+(* Author: Alexander Krauss, TU Muenchen
+   Author: Christian Sternagel, University of Innsbruck
+*)
+
+header {* Monad notation for arbitrary types *}
+
+theory Monad_Syntax
+imports Adhoc_Overloading
+begin
+
+consts
+  bindM :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
+
+notation (xsymbols)
+  bindM (infixr "\<guillemotright>=" 54)
+
+abbreviation (do_notation)
+  bindM_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
+where
+  "bindM_do \<equiv> bindM"
+
+notation (output)
+  bindM_do (infixr ">>=" 54)
+
+notation (xsymbols output)
+  bindM_do (infixr "\<guillemotright>=" 54)
+
+nonterminals
+  do_binds do_bind
+
+syntax
+  "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
+  "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
+  "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
+  "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
+  "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
+  "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
+
+syntax (xsymbols)
+  "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
+  "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
+
+translations
+  "_do_block (_do_cons (_do_then t) (_do_final e))"
+    == "CONST bindM_do t (\<lambda>_. e)"
+  "_do_block (_do_cons (_do_bind p t) (_do_final e))"
+    == "CONST bindM_do t (\<lambda>p. e)"
+  "_do_block (_do_cons (_do_let p t) bs)"
+    == "let p = t in _do_block bs"
+  "_do_block (_do_cons b (_do_cons c cs))"
+    == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
+  "_do_cons (_do_let p t) (_do_final s)"
+    == "_do_final (let p = t in s)"
+  "_do_block (_do_final e)" => "e"
+  "(m >> n)" => "(m >>= (\<lambda>_. n))"
+
+setup {* Adhoc_Overloading.add_overloaded @{const_name bindM} *}
+
+end