[STATEMENT]
lemma imp_nfoldli_simps[simp,code]:
  "imp_nfoldli [] c f s = return s"
  "imp_nfoldli (x#ls) c f s = (do {
    b \<leftarrow> c s;
    if b then do { 
      s'\<leftarrow>f x s; 
      imp_nfoldli ls c f s'
    } else return s
  })"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. imp_nfoldli [] c f s = return s &&& imp_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> imp_nfoldli ls c f else return s)
[PROOF STEP]
apply -
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. imp_nfoldli [] c f s = return s
 2. imp_nfoldli (x # ls) c f s = c s \<bind> (\<lambda>b. if b then f x s \<bind> imp_nfoldli ls c f else return s)
[PROOF STEP]
unfolding imp_nfoldli_def
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) ([], s) = return s
 2. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply (subst heap.mono_body_fixp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x. monotone heap.le_fun Heap_ord (\<lambda>fa. case x of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. fa (ls, s')) else return s))
 2. (case ([], s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = return s
 3. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply pf_mono
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. (case ([], s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = return s
 2. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (x # ls, s) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply (subst heap.mono_body_fixp)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x. monotone heap.le_fun Heap_ord (\<lambda>fa. case x of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. fa (ls, s')) else return s))
 2. (case (x # ls, s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply pf_mono
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. (case (x # ls, s) of ([], s) \<Rightarrow> return s | (x # ls, s) \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)) = c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | x # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (ls, s')) else return s)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done