[STATEMENT]
lemma bind_is_OK_E3 [elim]:
  assumes "h \<turnstile> ok (f \<bind> g)" and "pure f h"
  obtains x where "h \<turnstile> f \<rightarrow>\<^sub>r x"  and "h \<turnstile> ok (g x)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (\<And>x. \<lbrakk>h \<turnstile> f \<rightarrow>\<^sub>r x; h \<turnstile> ok g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
h \<turnstile> ok Heap_Error_Monad.bind f g
pure f h

goal (1 subgoal):
 1. (\<And>x. \<lbrakk>h \<turnstile> f \<rightarrow>\<^sub>r x; h \<turnstile> ok g x\<rbrakk> \<Longrightarrow> thesis) \<Longrightarrow> thesis
[PROOF STEP]
by(auto simp add: bind_def returns_result_def returns_heap_def is_OK_def execute_def pure_def
               split: sum.splits)