[STATEMENT]
lemma bind_cong [fundef_cong]:
  fixes f1 f2 :: "('heap, 'e, 'result) prog"
    and g1 g2 :: "'result \<Rightarrow> ('heap, 'e, 'result2) prog"
  assumes "h \<turnstile> f1 = h \<turnstile> f2"
    and "\<And>y h'. h \<turnstile> f1 \<rightarrow>\<^sub>r y \<Longrightarrow> h \<turnstile> f1 \<rightarrow>\<^sub>h h' \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y"
  shows "h \<turnstile> (f1 \<bind> g1) = h \<turnstile> (f2 \<bind> g2)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
[PROOF STEP]
apply(insert assms, cases "h \<turnstile> f1")
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a. \<lbrakk>h \<turnstile> f1 = h \<turnstile> f2; \<And>y h'. \<lbrakk>h \<turnstile> f1 \<rightarrow>\<^sub>r y; h \<turnstile> f1 \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y; h \<turnstile> f1 = Inl a\<rbrakk> \<Longrightarrow> h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
 2. \<And>b. \<lbrakk>h \<turnstile> f1 = h \<turnstile> f2; \<And>y h'. \<lbrakk>h \<turnstile> f1 \<rightarrow>\<^sub>r y; h \<turnstile> f1 \<rightarrow>\<^sub>h h'\<rbrakk> \<Longrightarrow> h' \<turnstile> g1 y = h' \<turnstile> g2 y; h \<turnstile> f1 = Inr b\<rbrakk> \<Longrightarrow> h \<turnstile> f1 \<bind> g1 = h \<turnstile> f2 \<bind> g2
[PROOF STEP]
by(auto simp add: bind_def returns_result_def returns_heap_def execute_def 
      split: sum.splits)