# HG changeset patch
# User haftmann
# Date 1281703507 -7200
# Node ID 9ee71ec7db4e01d3520ae0eef033745902848c97
# Parent  721b4d6095b751363f98084de83f6e72a034796c
lemma execute_bind_case

diff -r 721b4d6095b7 -r 9ee71ec7db4e src/HOL/Imperative_HOL/Heap_Monad.thy
--- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 13 14:43:16 2010 +0200
+++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 13 14:45:07 2010 +0200
@@ -274,6 +274,11 @@
   "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
   by (simp_all add: bind_def)
 
+lemma execute_bind_case:
+  "execute (f \<guillemotright>= g) h = (case (execute f h) of
+    Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
+  by (simp add: bind_def)
+
 lemma execute_bind_success:
   "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
   by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)