author huffman Fri Mar 30 12:32:35 2012 +0200 (2012-03-30) changeset 47220 52426c62b5d0 parent 46143 c932c80d3eae child 52622 e0ff1625e96d permissions -rw-r--r--
replace lemmas eval_nat_numeral with a simpler reformulation
```     1 (* Author: Alexander Krauss, TU Muenchen
```
```     2    Author: Christian Sternagel, University of Innsbruck
```
```     3 *)
```
```     4
```
```     5 header {* Monad notation for arbitrary types *}
```
```     6
```
```     7 theory Monad_Syntax
```
```     8 imports Main "~~/src/Tools/Adhoc_Overloading"
```
```     9 begin
```
```    10
```
```    11 text {*
```
```    12   We provide a convenient do-notation for monadic expressions
```
```    13   well-known from Haskell.  @{const Let} is printed
```
```    14   specially in do-expressions.
```
```    15 *}
```
```    16
```
```    17 consts
```
```    18   bind :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c" (infixr ">>=" 54)
```
```    19
```
```    20 notation (xsymbols)
```
```    21   bind (infixr "\<guillemotright>=" 54)
```
```    22
```
```    23 notation (latex output)
```
```    24   bind (infixr "\<bind>" 54)
```
```    25
```
```    26 abbreviation (do_notation)
```
```    27   bind_do :: "['a, 'b \<Rightarrow> 'c] \<Rightarrow> 'c"
```
```    28 where
```
```    29   "bind_do \<equiv> bind"
```
```    30
```
```    31 notation (output)
```
```    32   bind_do (infixr ">>=" 54)
```
```    33
```
```    34 notation (xsymbols output)
```
```    35   bind_do (infixr "\<guillemotright>=" 54)
```
```    36
```
```    37 notation (latex output)
```
```    38   bind_do (infixr "\<bind>" 54)
```
```    39
```
```    40 nonterminal do_binds and do_bind
```
```    41
```
```    42 syntax
```
```    43   "_do_block" :: "do_binds \<Rightarrow> 'a" ("do {//(2  _)//}" [12] 62)
```
```    44   "_do_bind" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ <-/ _)" 13)
```
```    45   "_do_let" :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(2let _ =/ _)" [1000, 13] 13)
```
```    46   "_do_then" :: "'a \<Rightarrow> do_bind" ("_" [14] 13)
```
```    47   "_do_final" :: "'a \<Rightarrow> do_binds" ("_")
```
```    48   "_do_cons" :: "[do_bind, do_binds] \<Rightarrow> do_binds" ("_;//_" [13, 12] 12)
```
```    49   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr ">>" 54)
```
```    50
```
```    51 syntax (xsymbols)
```
```    52   "_do_bind"  :: "[pttrn, 'a] \<Rightarrow> do_bind" ("(_ \<leftarrow>/ _)" 13)
```
```    53   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<guillemotright>" 54)
```
```    54
```
```    55 syntax (latex output)
```
```    56   "_thenM" :: "['a, 'b] \<Rightarrow> 'b" (infixr "\<then>" 54)
```
```    57
```
```    58 translations
```
```    59   "_do_block (_do_cons (_do_then t) (_do_final e))"
```
```    60     == "CONST bind_do t (\<lambda>_. e)"
```
```    61   "_do_block (_do_cons (_do_bind p t) (_do_final e))"
```
```    62     == "CONST bind_do t (\<lambda>p. e)"
```
```    63   "_do_block (_do_cons (_do_let p t) bs)"
```
```    64     == "let p = t in _do_block bs"
```
```    65   "_do_block (_do_cons b (_do_cons c cs))"
```
```    66     == "_do_block (_do_cons b (_do_final (_do_block (_do_cons c cs))))"
```
```    67   "_do_cons (_do_let p t) (_do_final s)"
```
```    68     == "_do_final (let p = t in s)"
```
```    69   "_do_block (_do_final e)" => "e"
```
```    70   "(m >> n)" => "(m >>= (\<lambda>_. n))"
```
```    71
```
```    72 setup {*
```
```    73   Adhoc_Overloading.add_overloaded @{const_name bind}
```
```    74   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Set.bind}
```
```    75   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Predicate.bind}
```
```    76   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name Option.bind}
```
```    77   #> Adhoc_Overloading.add_variant @{const_name bind} @{const_name List.bind}
```
```    78 *}
```
```    79
```
```    80 end
```