1.1 --- a/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 13 14:43:16 2010 +0200
     1.2 +++ b/src/HOL/Imperative_HOL/Heap_Monad.thy	Fri Aug 13 14:45:07 2010 +0200
     1.3 @@ -274,6 +274,11 @@
     1.4    "execute f h = None \<Longrightarrow> execute (f \<guillemotright>= g) h = None"
     1.5    by (simp_all add: bind_def)
     1.6  
     1.7 +lemma execute_bind_case:
     1.8 +  "execute (f \<guillemotright>= g) h = (case (execute f h) of
     1.9 +    Some (x, h') \<Rightarrow> execute (g x) h' | None \<Rightarrow> None)"
    1.10 +  by (simp add: bind_def)
    1.11 +
    1.12  lemma execute_bind_success:
    1.13    "success f h \<Longrightarrow> execute (f \<guillemotright>= g) h = execute (g (fst (the (execute f h)))) (snd (the (execute f h)))"
    1.14    by (cases f h rule: Heap_cases) (auto elim!: successE simp add: bind_def)