src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 36078 59f6773a7d1d
parent 36057 ca6610908ae9
child 36176 3fe7e97ccca8
equal deleted inserted replaced
36077:13f0e77128f8 36078:59f6773a7d1d
    80 
    80 
    81 definition
    81 definition
    82   raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
    82   raise :: "string \<Rightarrow> 'a Heap" where -- {* the string is just decoration *}
    83   [code del]: "raise s = Heap (Pair (Inr Exn))"
    83   [code del]: "raise s = Heap (Pair (Inr Exn))"
    84 
    84 
    85 notation (latex output)
       
    86   "raise" ("\<^raw:{\textsf{raise}}>")
       
    87 
       
    88 lemma execute_raise [simp]:
    85 lemma execute_raise [simp]:
    89   "execute (raise s) h = (Inr Exn, h)"
    86   "execute (raise s) h = (Inr Exn, h)"
    90   by (simp add: raise_def)
    87   by (simp add: raise_def)
    91 
    88 
    92 
    89 
   113     ("_" [12] 12)
   110     ("_" [12] 12)
   114 
   111 
   115 syntax (xsymbols)
   112 syntax (xsymbols)
   116   "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   113   "_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
   117     ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
   114     ("_ \<leftarrow> _;//_" [1000, 13, 12] 12)
   118 syntax (latex output)
       
   119   "_do" :: "do_expr \<Rightarrow> 'a"
       
   120     ("(\<^raw:{\textsf{do}}> (_))" [12] 100)
       
   121   "_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"
       
   122     ("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)
       
   123 notation (latex output)
       
   124   "return" ("\<^raw:{\textsf{return}}>")
       
   125 
   115 
   126 translations
   116 translations
   127   "_do f" => "f"
   117   "_do f" => "f"
   128   "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   118   "_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"
   129   "_chainM f g" => "f \<guillemotright> g"
   119   "_chainM f g" => "f \<guillemotright> g"