[STATEMENT]
lemma memo_lookup:
  "bind (memo f x) (\<lambda>i. bind (lookup x) (g i)) = bind (memo f x) (\<lambda>i. g i i)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. bind (memo f x) (\<lambda>i. bind (lookup x) (g i)) = bind (memo f x) (\<lambda>i. g i i)
[PROOF STEP]
apply(simp cong del: option.case_cong_weak add: lookup_def memo_def bind_get option.case_distrib[where h="\<lambda>x. bind x _"] bind_assoc bind_update return_bind update_get o_def get_const)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some xa \<Rightarrow> get (\<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(subst (3) get_const[symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. case s x of None \<Rightarrow> get (\<lambda>_. bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y))) | Some xa \<Rightarrow> get (\<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(subst option.case_distrib[where h=get, symmetric])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. get (\<lambda>s. get (case s x of None \<Rightarrow> \<lambda>_. bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some xa \<Rightarrow> \<lambda>s. case s x of None \<Rightarrow> bind fail (g xa) | Some x \<Rightarrow> g xa x)) = get (\<lambda>s. case s x of None \<Rightarrow> bind (f x) (\<lambda>y. update (\<lambda>m. m(x \<mapsto> y)) (g y y)) | Some x \<Rightarrow> g x x)
[PROOF STEP]
apply(simp add: get_get case_option_apply cong: option.case_cong)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done