src/HOL/Imperative_HOL/Heap_Monad.thy
changeset 37878 d016aaead7a2
parent 37845 b70d7a347964
child 37947 844977c7abeb
equal deleted inserted replaced
37877:d4a30d210220 37878:d016aaead7a2
   122   runs with the heap @{text h} will result in return value @{text r}
   122   runs with the heap @{text h} will result in return value @{text r}
   123   and a heap @{text "h'"}, i.e.~no exception occurs.
   123   and a heap @{text "h'"}, i.e.~no exception occurs.
   124 *}  
   124 *}  
   125 
   125 
   126 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
   126 definition crel :: "'a Heap \<Rightarrow> heap \<Rightarrow> heap \<Rightarrow> 'a \<Rightarrow> bool" where
   127   crel_def: "crel c h h' r \<longleftrightarrow> Heap_Monad.execute c h = Some (r, h')"
   127   crel_def: "crel c h h' r \<longleftrightarrow> execute c h = Some (r, h')"
   128 
   128 
   129 lemma crelI:
   129 lemma crelI:
   130   "Heap_Monad.execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
   130   "execute c h = Some (r, h') \<Longrightarrow> crel c h h' r"
   131   by (simp add: crel_def)
   131   by (simp add: crel_def)
   132 
   132 
   133 lemma crelE:
   133 lemma crelE:
   134   assumes "crel c h h' r"
   134   assumes "crel c h h' r"
   135   obtains "r = fst (the (execute c h))"
   135   obtains "r = fst (the (execute c h))"
   298   assumes "crel (f \<guillemotright>= g) h h'' r'"
   298   assumes "crel (f \<guillemotright>= g) h h'' r'"
   299   obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   299   obtains h' r where "crel f h h' r" "crel (g r) h' h'' r'"
   300   using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   300   using assms by (auto simp add: crel_def bind_def split: option.split_asm)
   301 
   301 
   302 lemma execute_bind_eq_SomeI:
   302 lemma execute_bind_eq_SomeI:
   303   assumes "Heap_Monad.execute f h = Some (x, h')"
   303   assumes "execute f h = Some (x, h')"
   304     and "Heap_Monad.execute (g x) h' = Some (y, h'')"
   304     and "execute (g x) h' = Some (y, h'')"
   305   shows "Heap_Monad.execute (f \<guillemotright>= g) h = Some (y, h'')"
   305   shows "execute (f \<guillemotright>= g) h = Some (y, h'')"
   306   using assms by (simp add: bind_def)
   306   using assms by (simp add: bind_def)
   307 
   307 
   308 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   308 lemma return_bind [simp]: "return x \<guillemotright>= f = f x"
   309   by (rule Heap_eqI) (simp add: execute_bind execute_simps)
   309   by (rule Heap_eqI) (simp add: execute_bind execute_simps)
   310 
   310 
   485 def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
   485 def update[A](r: Ref[A], x: A): Unit = { r.value = x }*}
   486 
   486 
   487 code_reserved Scala Heap
   487 code_reserved Scala Heap
   488 
   488 
   489 code_type Heap (Scala "Unit/ =>/ _")
   489 code_type Heap (Scala "Unit/ =>/ _")
   490 code_const bind (Scala "!Heap.bind((_), (_))")
   490 code_const bind (Scala "bind")
   491 code_const return (Scala "('_: Unit)/ =>/ _")
   491 code_const return (Scala "('_: Unit)/ =>/ _")
   492 code_const Heap_Monad.raise' (Scala "!error((_))")
   492 code_const Heap_Monad.raise' (Scala "!error((_))")
   493 
   493 
   494 
   494 
   495 subsubsection {* Target variants with less units *}
   495 subsubsection {* Target variants with less units *}