isabelle: src/HOL/Library/Monad_Syntax.thy@b8aeeedf7e68 (annotated)

68061 81d90f830f99 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); wenzelm parents: 66608 diff changeset	1	(* Title: HOL/Library/Monad_Syntax.thy
81d90f830f99 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); wenzelm parents: 66608 diff changeset	2	Author: Alexander Krauss, TU Muenchen
81d90f830f99 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); wenzelm parents: 66608 diff changeset	3	Author: Christian Sternagel, University of Innsbruck
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	4	*)
7fea92005066 uniform do notation for monads krauss parents: diff changeset	5
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 59359 diff changeset	6	section \<open>Monad notation for arbitrary types\<close>
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	7
7fea92005066 uniform do notation for monads krauss parents: diff changeset	8	theory Monad_Syntax
68061 81d90f830f99 clarified theory location and imports: avoid surprises due to Pure instead of Main (e.g. simpset operations); wenzelm parents: 66608 diff changeset	9	imports Adhoc_Overloading
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	10	begin
7fea92005066 uniform do notation for monads krauss parents: diff changeset	11
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 59359 diff changeset	12	text \<open>
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	13	We provide a convenient do-notation for monadic expressions well-known from Haskell.
2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	14	const>\<open>Let\<close> is printed specially in do-expressions.
60500 903bb1495239 isabelle update_cartouches; wenzelm parents: 59359 diff changeset	15	\<close>
37791 0d6b64060543 State_Monad uses Monad_Syntax krauss parents: 37790 diff changeset	16
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	17	consts
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	18	bind :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd" (infixl "\<bind>" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	19
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	20	notation (ASCII)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	21	bind (infixl ">>=" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	22
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	23
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	24	abbreviation (do_notation)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	25	bind_do :: "'a \<Rightarrow> ('b \<Rightarrow> 'c) \<Rightarrow> 'd"
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	26	where "bind_do \<equiv> bind"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	27
7fea92005066 uniform do notation for monads krauss parents: diff changeset	28	notation (output)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	29	bind_do (infixl "\<bind>" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	30
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	31	notation (ASCII output)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	32	bind_do (infixl ">>=" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	33
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	34
41229 d797baa3d57c replaced command 'nonterminals' by slightly modernized version 'nonterminal'; wenzelm parents: 39151 diff changeset	35	nonterminal do_binds and do_bind
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	36	syntax
7fea92005066 uniform do notation for monads krauss parents: diff changeset	37	"_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2 _)//}" [12] 62)
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	38	"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ \<leftarrow>/ _)" 13)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	39	"_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
7fea92005066 uniform do notation for monads krauss parents: diff changeset	40	"_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
7fea92005066 uniform do notation for monads krauss parents: diff changeset	41	"_do_final" :: "'a \<Rightarrow> do_binds" ("_")
7fea92005066 uniform do notation for monads krauss parents: diff changeset	42	"_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	43	"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl "\<then>" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	44
61955 e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	45	syntax (ASCII)
e96292f32c3c former "xsymbols" syntax is used by default, and ASCII replacement syntax with print mode "ASCII"; wenzelm parents: 60500 diff changeset	46	"_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2_ <-/ _)" 13)
70433 2137db107788 Monadic bind is now infixl as is the norm nipkow parents: 69593 diff changeset	47	"_thenM" :: "['a, 'b] \<Rightarrow> 'c" (infixl ">>" 54)
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	48
7fea92005066 uniform do notation for monads krauss parents: diff changeset	49	translations
7fea92005066 uniform do notation for monads krauss parents: diff changeset	50	"_do_block (_do_cons (_do_then t) (_do_final e))"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	51	\<rightleftharpoons> "CONST bind_do t (\<lambda>_. e)"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	52	"_do_block (_do_cons (_do_bind p t) (_do_final e))"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	53	\<rightleftharpoons> "CONST bind_do t (\<lambda>p. e)"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	54	"_do_block (_do_cons (_do_let p t) bs)"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	55	\<rightleftharpoons> "let p = t in _do_block bs"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	56	"_do_block (_do_cons b (_do_cons c cs))"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	57	\<rightleftharpoons> "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	58	"_do_cons (_do_let p t) (_do_final s)"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	59	\<rightleftharpoons> "_do_final (let p = t in s)"
62189 116f41763b2b more symbols; wenzelm parents: 62035 diff changeset	60	"_do_block (_do_final e)" \<rightharpoonup> "e"
62035 b3cda398a5b1 more symbols; wenzelm parents: 62026 diff changeset	61	"(m \<then> n)" \<rightharpoonup> "(m \<bind> (\<lambda>_. n))"
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	62
52622 e0ff1625e96d localized and modernized adhoc-overloading (patch by Christian Sternagel); wenzelm parents: 46143 diff changeset	63	adhoc_overloading
66608 f3e7a1418979 avoid depedency on FSet; wenzelm parents: 66263 diff changeset	64	bind Set.bind Predicate.bind Option.bind List.bind
37790 7fea92005066 uniform do notation for monads krauss parents: diff changeset	65
66608 f3e7a1418979 avoid depedency on FSet; wenzelm parents: 66263 diff changeset	66	end

author	wenzelm
	Tue, 05 Nov 2019 14:16:16 +0100
changeset 71046	b8aeeedf7e68
parent 70433	2137db107788
child 77107	4c4d40913900
permissions	-rw-r--r--