26170

1 
(* Title: HOL/Library/Heap_Monad.thy


2 
ID: $Id$


3 
Author: John Matthews, Galois Connections; Alexander Krauss, Lukas Bulwahn & Florian Haftmann, TU Muenchen


4 
*)


5 


6 
header {* A monad with a polymorphic heap *}


7 


8 
theory Heap_Monad


9 
imports Heap


10 
begin


11 


12 
subsection {* The monad *}


13 


14 
subsubsection {* Monad combinators *}


15 


16 
datatype exception = Exn


17 


18 
text {* Monadic heap actions either produce values


19 
and transform the heap, or fail *}


20 
datatype 'a Heap = Heap "heap \<Rightarrow> ('a + exception) \<times> heap"


21 


22 
primrec


23 
execute :: "'a Heap \<Rightarrow> heap \<Rightarrow> ('a + exception) \<times> heap" where


24 
"execute (Heap f) = f"


25 
lemmas [code del] = execute.simps


26 


27 
lemma Heap_execute [simp]:


28 
"Heap (execute f) = f" by (cases f) simp_all


29 


30 
lemma Heap_eqI:


31 
"(\<And>h. execute f h = execute g h) \<Longrightarrow> f = g"


32 
by (cases f, cases g) (auto simp: expand_fun_eq)


33 


34 
lemma Heap_eqI':


35 
"(\<And>h. (\<lambda>x. execute (f x) h) = (\<lambda>y. execute (g y) h)) \<Longrightarrow> f = g"


36 
by (auto simp: expand_fun_eq intro: Heap_eqI)


37 


38 
lemma Heap_strip: "(\<And>f. PROP P f) \<equiv> (\<And>g. PROP P (Heap g))"


39 
proof


40 
fix g :: "heap \<Rightarrow> ('a + exception) \<times> heap"


41 
assume "\<And>f. PROP P f"


42 
then show "PROP P (Heap g)" .


43 
next


44 
fix f :: "'a Heap"


45 
assume assm: "\<And>g. PROP P (Heap g)"


46 
then have "PROP P (Heap (execute f))" .


47 
then show "PROP P f" by simp


48 
qed


49 


50 
definition


51 
heap :: "(heap \<Rightarrow> 'a \<times> heap) \<Rightarrow> 'a Heap" where


52 
[code del]: "heap f = Heap (\<lambda>h. apfst Inl (f h))"


53 


54 
lemma execute_heap [simp]:


55 
"execute (heap f) h = apfst Inl (f h)"


56 
by (simp add: heap_def)


57 


58 
definition


59 
run :: "'a Heap \<Rightarrow> 'a Heap" where


60 
run_drop [code del]: "run f = f"


61 


62 
definition


63 
bindM :: "'a Heap \<Rightarrow> ('a \<Rightarrow> 'b Heap) \<Rightarrow> 'b Heap" (infixl ">>=" 54) where


64 
[code del]: "f >>= g = Heap (\<lambda>h. case execute f h of


65 
(Inl x, h') \<Rightarrow> execute (g x) h'


66 
 r \<Rightarrow> r)"


67 


68 
notation


69 
bindM (infixl "\<guillemotright>=" 54)


70 


71 
abbreviation


72 
chainM :: "'a Heap \<Rightarrow> 'b Heap \<Rightarrow> 'b Heap" (infixl ">>" 54) where


73 
"f >> g \<equiv> f >>= (\<lambda>_. g)"


74 


75 
notation


76 
chainM (infixl "\<guillemotright>" 54)


77 


78 
definition


79 
return :: "'a \<Rightarrow> 'a Heap" where


80 
[code del]: "return x = heap (Pair x)"


81 


82 
lemma execute_return [simp]:


83 
"execute (return x) h = apfst Inl (x, h)"


84 
by (simp add: return_def)


85 


86 
definition


87 
raise :: "string \<Rightarrow> 'a Heap" where  {* the string is just decoration *}


88 
[code del]: "raise s = Heap (Pair (Inr Exn))"


89 


90 
notation (latex output)


91 
"raise" ("\<^raw:{\textsf{raise}}>")


92 


93 
lemma execute_raise [simp]:


94 
"execute (raise s) h = (Inr Exn, h)"


95 
by (simp add: raise_def)


96 


97 


98 
subsubsection {* dosyntax *}


99 


100 
text {*


101 
We provide a convenient donotation for monadic expressions


102 
wellknown from Haskell. @{const Let} is printed


103 
specially in doexpressions.


104 
*}


105 


106 
nonterminals do_expr


107 


108 
syntax


109 
"_do" :: "do_expr \<Rightarrow> 'a"


110 
("(do (_)//done)" [12] 100)


111 
"_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"


112 
("_ < _;//_" [1000, 13, 12] 12)


113 
"_chainM" :: "'a \<Rightarrow> do_expr \<Rightarrow> do_expr"


114 
("_;//_" [13, 12] 12)


115 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"


116 
("let _ = _;//_" [1000, 13, 12] 12)


117 
"_nil" :: "'a \<Rightarrow> do_expr"


118 
("_" [12] 12)


119 


120 
syntax (xsymbols)


121 
"_bindM" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"


122 
("_ \<leftarrow> _;//_" [1000, 13, 12] 12)


123 
syntax (latex output)


124 
"_do" :: "do_expr \<Rightarrow> 'a"


125 
("(\<^raw:{\textsf{do}}> (_))" [12] 100)


126 
"_let" :: "pttrn \<Rightarrow> 'a \<Rightarrow> do_expr \<Rightarrow> do_expr"


127 
("\<^raw:\textsf{let}> _ = _;//_" [1000, 13, 12] 12)


128 
notation (latex output)


129 
"return" ("\<^raw:{\textsf{return}}>")


130 


131 
translations


132 
"_do f" => "CONST run f"


133 
"_bindM x f g" => "f \<guillemotright>= (\<lambda>x. g)"


134 
"_chainM f g" => "f \<guillemotright> g"


135 
"_let x t f" => "CONST Let t (\<lambda>x. f)"


136 
"_nil f" => "f"


137 


138 
print_translation {*


139 
let


140 
fun dest_abs_eta (Abs (abs as (_, ty, _))) =


141 
let


142 
val (v, t) = Syntax.variant_abs abs;


143 
in ((v, ty), t) end


144 
 dest_abs_eta t =


145 
let


146 
val (v, t) = Syntax.variant_abs ("", dummyT, t $ Bound 0);


147 
in ((v, dummyT), t) end


148 
fun unfold_monad (Const (@{const_syntax bindM}, _) $ f $ g) =


149 
let


150 
val ((v, ty), g') = dest_abs_eta g;


151 
val v_used = fold_aterms


152 
(fn Free (w, _) => (fn s => s orelse v = w)  _ => I) g' false;


153 
in if v_used then


154 
Const ("_bindM", dummyT) $ Free (v, ty) $ f $ unfold_monad g'


155 
else


156 
Const ("_chainM", dummyT) $ f $ unfold_monad g'


157 
end


158 
 unfold_monad (Const (@{const_syntax chainM}, _) $ f $ g) =


159 
Const ("_chainM", dummyT) $ f $ unfold_monad g


160 
 unfold_monad (Const (@{const_syntax Let}, _) $ f $ g) =


161 
let


162 
val ((v, ty), g') = dest_abs_eta g;


163 
in Const ("_let", dummyT) $ Free (v, ty) $ f $ unfold_monad g' end


164 
 unfold_monad (Const (@{const_syntax Pair}, _) $ f) =


165 
Const ("return", dummyT) $ f


166 
 unfold_monad f = f;


167 
fun tr' (f::ts) =


168 
list_comb (Const ("_do", dummyT) $ unfold_monad f, ts)


169 
in [(@{const_syntax "run"}, tr')] end;


170 
*}


171 


172 
subsubsection {* Plain evaluation *}


173 


174 
definition


175 
evaluate :: "'a Heap \<Rightarrow> 'a"


176 
where


177 
[code del]: "evaluate f = (case execute f Heap.empty


178 
of (Inl x, _) \<Rightarrow> x)"


179 


180 


181 
subsection {* Monad properties *}


182 


183 
subsubsection {* Superfluous runs *}


184 


185 
text {* @{term run} is just a doodle *}


186 


187 
lemma run_simp [simp]:


188 
"\<And>f. run (run f) = run f"


189 
"\<And>f g. run f \<guillemotright>= g = f \<guillemotright>= g"


190 
"\<And>f g. run f \<guillemotright> g = f \<guillemotright> g"


191 
"\<And>f g. f \<guillemotright>= (\<lambda>x. run g) = f \<guillemotright>= (\<lambda>x. g)"


192 
"\<And>f g. f \<guillemotright> run g = f \<guillemotright> g"


193 
"\<And>f. f = run g \<longleftrightarrow> f = g"


194 
"\<And>f. run f = g \<longleftrightarrow> f = g"


195 
unfolding run_drop by rule+


196 


197 
subsubsection {* Monad laws *}


198 


199 
lemma return_bind: "return x \<guillemotright>= f = f x"


200 
by (simp add: bindM_def return_def)


201 


202 
lemma bind_return: "f \<guillemotright>= return = f"


203 
proof (rule Heap_eqI)


204 
fix h


205 
show "execute (f \<guillemotright>= return) h = execute f h"


206 
by (auto simp add: bindM_def return_def split: sum.splits prod.splits)


207 
qed


208 


209 
lemma bind_bind: "(f \<guillemotright>= g) \<guillemotright>= h = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h)"


210 
by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)


211 


212 
lemma bind_bind': "f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= h x) = f \<guillemotright>= (\<lambda>x. g x \<guillemotright>= (\<lambda>y. return (x, y))) \<guillemotright>= (\<lambda>(x, y). h x y)"


213 
by (rule Heap_eqI) (auto simp add: bindM_def split: split: sum.splits prod.splits)


214 


215 
lemma raise_bind: "raise e \<guillemotright>= f = raise e"


216 
by (simp add: raise_def bindM_def)


217 


218 


219 
lemmas monad_simp = return_bind bind_return bind_bind raise_bind


220 


221 


222 
subsection {* Generic combinators *}


223 


224 
definition


225 
liftM :: "('a \<Rightarrow> 'b) \<Rightarrow> 'a \<Rightarrow> 'b Heap"


226 
where


227 
"liftM f = return o f"


228 


229 
definition


230 
compM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> ('b \<Rightarrow> 'c Heap) \<Rightarrow> 'a \<Rightarrow> 'c Heap" (infixl ">>==" 54)


231 
where


232 
"(f >>== g) = (\<lambda>x. f x \<guillemotright>= g)"


233 


234 
notation


235 
compM (infixl "\<guillemotright>==" 54)


236 


237 
lemma liftM_collapse: "liftM f x = return (f x)"


238 
by (simp add: liftM_def)


239 


240 
lemma liftM_compM: "liftM f \<guillemotright>== g = g o f"


241 
by (auto intro: Heap_eqI' simp add: expand_fun_eq liftM_def compM_def bindM_def)


242 


243 
lemma compM_return: "f \<guillemotright>== return = f"


244 
by (simp add: compM_def monad_simp)


245 


246 
lemma compM_compM: "(f \<guillemotright>== g) \<guillemotright>== h = f \<guillemotright>== (g \<guillemotright>== h)"


247 
by (simp add: compM_def monad_simp)


248 


249 
lemma liftM_bind:


250 
"(\<lambda>x. liftM f x \<guillemotright>= liftM g) = liftM (\<lambda>x. g (f x))"


251 
by (rule Heap_eqI') (simp add: monad_simp liftM_def bindM_def)


252 


253 
lemma liftM_comp:


254 
"liftM f o g = liftM (f o g)"


255 
by (rule Heap_eqI') (simp add: liftM_def)


256 


257 
lemmas monad_simp' = monad_simp liftM_compM compM_return


258 
compM_compM liftM_bind liftM_comp


259 


260 
primrec


261 
mapM :: "('a \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b list Heap"


262 
where


263 
"mapM f [] = return []"


264 
 "mapM f (x#xs) = do y \<leftarrow> f x;


265 
ys \<leftarrow> mapM f xs;


266 
return (y # ys)


267 
done"


268 


269 
primrec


270 
foldM :: "('a \<Rightarrow> 'b \<Rightarrow> 'b Heap) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> 'b Heap"


271 
where


272 
"foldM f [] s = return s"


273 
 "foldM f (x#xs) s = f x s \<guillemotright>= foldM f xs"


274 


275 
hide (open) const heap execute


276 


277 
end
