changeset 37878 d016aaead7a2 parent 37845 b70d7a347964 child 37947 844977c7abeb
equal inserted replaced
`   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 *}`