[STATEMENT]
lemma monadic_nfoldli_refine[refine]:
  assumes L: "(li, l) \<in> \<langle>S\<rangle>list_rel"
    and  [simp]: "(si, s) \<in> R"
    and CR[refine]: "\<And>si s. (si,s)\<in>R \<Longrightarrow> ci si \<le>\<Down>bool_rel (c s)"
    and [refine]: "\<And>xi x si s. \<lbrakk> (xi,x)\<in>S; x\<in>set l; (si,s)\<in>R; inres (c s) True \<rbrakk> \<Longrightarrow> fi xi si \<le> \<Down>R (f x s)"
  shows "monadic_nfoldli li ci fi si \<le> \<Down> R (monadic_nfoldli l c f s)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli li ci fi si \<le> \<Down> R (monadic_nfoldli l c f s)
[PROOF STEP]
supply RELATESI[of "S\<inter>(set li\<times>set l)", refine_dref_RELATES]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli li ci fi si \<le> \<Down> R (monadic_nfoldli l c f s)
[PROOF STEP]
supply RELATESI[of R, refine_dref_RELATES]
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli li ci fi si \<le> \<Down> R (monadic_nfoldli l c f s)
[PROOF STEP]
unfolding monadic_nfoldli_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. REC\<^sub>T (\<lambda>D (l, s). case l of [] \<Rightarrow> RETURN s | x # ls \<Rightarrow> ci s \<bind> (\<lambda>b. if b then fi x s \<bind> (\<lambda>s'. D (ls, s')) else RETURN s)) (li, si) \<le> \<Down> R (REC\<^sub>T (\<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)) (l, s))
[PROOF STEP]
apply (refine_rcg bind_refine')
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. ((li, si), l, s) \<in> ?R
 2. \<And>D Da x x' x1 x2 x1a x2a. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a)\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel
 3. \<And>D Da x x' x1 x2 x1a x2a. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a)\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 4. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 5. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2)\<rbrakk> \<Longrightarrow> b = ba
 6. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> (xa, xb) \<in> S
 7. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> xb \<in> set l
 8. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 9. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> inres (c x2) True
 10. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba s' s'a. \<lbrakk>\<And>x x'. (x, x') \<in> ?R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> ?R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> ?S15 D Da x x' x1 x2 x1a x2a; (ls, lsa) \<in> \<langle>?S15 D Da x x' x1 x2 x1a x2a\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba; (s', s'a) \<in> R; inres (fi xa x2a) s'; inres (f xb x2) s'a; nofail (fi xa x2a); nofail (f xb x2)\<rbrakk> \<Longrightarrow> D (ls, s') \<le> \<Down> R (Da (lsa, s'a))
A total of 11 subgoals...
[PROOF STEP]
apply refine_dref_type
[PROOF STATE]
proof (prove)
goal (11 subgoals):
 1. ((li, si), l, s) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R
 2. \<And>D Da x x' x1 x2 x1a x2a. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a)\<rbrakk> \<Longrightarrow> (x1a, x1) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel
 3. \<And>D Da x x' x1 x2 x1a x2a. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a)\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 4. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 5. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2)\<rbrakk> \<Longrightarrow> b = ba
 6. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> (xa, xb) \<in> S
 7. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> xb \<in> set l
 8. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> (x2a, x2) \<in> R
 9. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba\<rbrakk> \<Longrightarrow> inres (c x2) True
 10. \<And>D Da x x' x1 x2 x1a x2a xa xb ls lsa b ba s' s'a. \<lbrakk>\<And>x x'. (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R \<Longrightarrow> D x \<le> \<Down> R (Da x'); (x, x') \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel \<times>\<^sub>r R; x' = (x1, x2); x = (x1a, x2a); (xa, xb) \<in> S \<inter> set li \<times> set l; (ls, lsa) \<in> \<langle>S \<inter> set li \<times> set l\<rangle>list_rel; x1a = xa # ls; x1 = xb # lsa; (b, ba) \<in> bool_rel; inres (ci x2a) b; inres (c x2) ba; nofail (ci x2a); nofail (c x2); b; ba; (s', s'a) \<in> R; inres (fi xa x2a) s'; inres (f xb x2) s'a; nofail (fi xa x2a); nofail (f xb x2)\<rbrakk> \<Longrightarrow> D (ls, s') \<le> \<Down> R (Da (lsa, s'a))
A total of 11 subgoals...
[PROOF STEP]
apply (vc_solve simp: list_rel_congD[OF L])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma monadic_FOREACH_itsl:
  fixes R I tsl
  shows
    "do { l \<leftarrow> it_to_sorted_list R s; monadic_nfoldli l c f \<sigma> }
     \<le> monadic_FOREACH R I s c f \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R s \<bind> (\<lambda>l. monadic_nfoldli l c f \<sigma>) \<le> monadic_FOREACH R I s c f \<sigma>
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R s \<bind> (\<lambda>l. monadic_nfoldli l c f \<sigma>) \<le> \<Down> Id (monadic_FOREACH R I s c f \<sigma>)
[PROOF STEP]
unfolding monadic_FOREACH_def it_to_sorted_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>l. distinct l \<and> s = set l \<and> sorted_wrt R l) \<bind> (\<lambda>l. monadic_nfoldli l c f \<sigma>) \<le> \<Down> Id (ASSERT (finite s) \<bind> (\<lambda>_. SPEC (\<lambda>l. distinct l \<and> s = set l \<and> sorted_wrt R l) \<bind> (\<lambda>xs0. REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs \<noteq> [] then c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)) else RETURN (xs, \<sigma>))) (xs0, \<sigma>) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))))
[PROOF STEP]
apply (refine_rcg)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l xs0. \<lbrakk>finite s; (l, xs0) \<in> Id; l \<in> {l. distinct l \<and> s = set l \<and> sorted_wrt R l}; xs0 \<in> {l. distinct l \<and> s = set l \<and> sorted_wrt R l}\<rbrakk> \<Longrightarrow> monadic_nfoldli l c f \<sigma> \<le> \<Down> Id (REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv xs0 I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs \<noteq> [] then c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)) else RETURN (xs, \<sigma>))) (xs0, \<sigma>) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. distinct l \<and> s = set l \<and> sorted_wrt R l \<Longrightarrow> monadic_nfoldli l c f \<sigma> \<le> REC\<^sub>T (\<lambda>W (xs, \<sigma>). ASSERT (FOREACH_inv l I (xs, \<sigma>)) \<bind> (\<lambda>_. if xs = [] then RETURN (xs, \<sigma>) else c \<sigma> \<bind> (\<lambda>b. if b then FOREACH_body f (xs, \<sigma>) \<bind> W else RETURN (xs, \<sigma>)))) (l, \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)
[PROOF STEP]
apply (rule monadic_nfoldli_rec[simplified])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma FOREACHoci_itsl:
  fixes R I tsl
  shows
    "do { l \<leftarrow> it_to_sorted_list R s; nfoldli l c f \<sigma> }
     \<le> FOREACHoci R I s c f \<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R s \<bind> (\<lambda>l. nfoldli l c f \<sigma>) \<le> FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup> s c f \<sigma>
[PROOF STEP]
apply (rule refine_IdD)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. it_to_sorted_list R s \<bind> (\<lambda>l. nfoldli l c f \<sigma>) \<le> \<Down> Id (FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup> s c f \<sigma>)
[PROOF STEP]
unfolding FOREACHoci_def it_to_sorted_list_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. SPEC (\<lambda>l. distinct l \<and> s = set l \<and> sorted_wrt R l) \<bind> (\<lambda>l. nfoldli l c f \<sigma>) \<le> \<Down> Id (ASSERT (finite s) \<bind> (\<lambda>_. SPEC (\<lambda>xs. distinct xs \<and> s = set xs \<and> sorted_wrt R xs) \<bind> (\<lambda>xs. WHILE\<^sub>T\<^bsup>\<lambda>(it, \<sigma>). \<exists>xs'. xs = xs' @ it \<and> I (set it) \<sigma>\<^esup> (FOREACH_cond c) (FOREACH_body f) (xs, \<sigma>) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))))
[PROOF STEP]
apply refine_rcg
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l xs. \<lbrakk>finite s; (l, xs) \<in> Id; l \<in> {l. distinct l \<and> s = set l \<and> sorted_wrt R l}; xs \<in> {xs. distinct xs \<and> s = set xs \<and> sorted_wrt R xs}\<rbrakk> \<Longrightarrow> nfoldli l c f \<sigma> \<le> \<Down> Id (WHILE\<^sub>T\<^bsup>\<lambda>(it, \<sigma>). \<exists>xs'. xs = xs' @ it \<and> I (set it) \<sigma>\<^esup> (FOREACH_cond c) (FOREACH_body f) (xs, \<sigma>) \<bind> (\<lambda>(uu_, \<sigma>). RETURN \<sigma>))
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>l. distinct l \<and> s = set l \<and> sorted_wrt R l \<Longrightarrow> nfoldli l c f \<sigma> \<le> WHILE\<^sub>T\<^bsup>\<lambda>(it, \<sigma>). (\<exists>xs'. l = xs' @ it) \<and> I (set it) \<sigma>\<^esup> (FOREACH_cond c) (FOREACH_body f) (l, \<sigma>) \<bind> (\<lambda>(uu_, y). RETURN y)
[PROOF STEP]
apply (rule nfoldli_while)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma [def_pat_rules]:
  "FOREACHc \<equiv> PR_CONST (FOREACHoci (\<lambda>_ _. True) (\<lambda>_ _. True))"
  "FOREACHci$I \<equiv> PR_CONST (FOREACHoci (\<lambda>_ _. True) I)"
  "FOREACHi$I \<equiv> \<lambda>\<^sub>2s. PR_CONST (FOREACHoci (\<lambda>_ _. True) I)$s$(\<lambda>\<^sub>2x. True)"
  "FOREACH \<equiv> FOREACHi$(\<lambda>\<^sub>2_ _. True)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. ((FOREACH\<^sub>C \<equiv> PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>\<lambda>_ _. True,\<lambda>_ _. True\<^esup>) &&& FOREACHci $ I \<equiv> PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>\<lambda>_ _. True,I\<^esup>) &&& (FOREACHi $ I \<equiv> \<lambda>x. (#PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>\<lambda>_ _. True,I\<^esup> $ x $ (\<lambda>x. (#True#))#)) &&& FOREACH \<equiv> FOREACHi $ (\<lambda>x. (#\<lambda>x. (#True#)#))
[PROOF STEP]
by (simp_all add:
    FOREACHci_def FOREACHi_def[abs_def] FOREACHc_def FOREACH_def[abs_def])


[STATEMENT]
lemma id_FOREACHoci[id_rules]: "PR_CONST (FOREACHoci R I) ::\<^sub>i
  TYPE('c set \<Rightarrow> ('d \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> 'd nres) \<Rightarrow> 'd \<Rightarrow> 'd nres)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup> ::\<^sub>i TYPE('c set \<Rightarrow> ('d \<Rightarrow> bool) \<Rightarrow> ('c \<Rightarrow> 'd \<Rightarrow> 'd nres) \<Rightarrow> 'd \<Rightarrow> 'd nres)
[PROOF STEP]
by simp


[STATEMENT]
lemma FOREACH_arities[sepref_monadify_arity]:
  (*"FOREACHc \<equiv> FOREACHoci$(\<lambda>\<^sub>2_ _. True)$(\<lambda>\<^sub>2_ _. True)"
  "FOREACHci \<equiv> FOREACHoci$(\<lambda>\<^sub>2_ _. True)"
  "FOREACHi \<equiv> \<lambda>\<^sub>2I s. FOREACHci$I$s$(\<lambda>\<^sub>2x. True)"
  "FOREACH \<equiv> FOREACHi$(\<lambda>\<^sub>2_ _. True)"*)
  "PR_CONST (FOREACHoci R I) \<equiv> \<lambda>\<^sub>2s c f \<sigma>. SP (PR_CONST (FOREACHoci R I))$s$(\<lambda>\<^sub>2x. c$x)$(\<lambda>\<^sub>2x \<sigma>. f$x$\<sigma>)$\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup> \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#\<lambda>xc. (#SP (PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup>) $ x $ (\<lambda>x. (#xa $ x#)) $ (\<lambda>x. (#\<lambda>xa. (#xb $ x $ xa#)#)) $ xc#)#)#)#)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma FOREACHoci_comb[sepref_monadify_comb]:
  "\<And>s c f \<sigma>. (PR_CONST (FOREACHoci R I))$s$(\<lambda>\<^sub>2x. c x)$f$\<sigma> \<equiv>
    Refine_Basic.bind$(EVAL$s)$(\<lambda>\<^sub>2s. Refine_Basic.bind$(EVAL$\<sigma>)$(\<lambda>\<^sub>2\<sigma>.
      SP (PR_CONST (monadic_FOREACH R I))$s$(\<lambda>\<^sub>2x. (EVAL$(c x)))$f$\<sigma>
    ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s c f \<sigma>. PR_CONST FOREACH\<^sub>O\<^sub>C\<^bsup>R,I\<^esup> $ s $ (\<lambda>x. (#c x#)) $ f $ \<sigma> \<equiv> (\<bind>) $ (EVAL $ s) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ \<sigma>) $ (\<lambda>xa. (#SP (PR_CONST (monadic_FOREACH R I)) $ x $ (\<lambda>x. (#EVAL $ c x#)) $ f $ xa#))#))
[PROOF STEP]
by (simp_all add: FOREACH_oci_to_monadic)


[STATEMENT]
lemma monadic_nfoldli_refine_aux:
  assumes c_ref: "\<And>s s'. hn_refine
    (\<Gamma> * hn_ctxt Rs s' s)
    (c s)
    (\<Gamma> * hn_ctxt Rs s' s)
    bool_assn
    (c' s')"
  assumes f_ref: "\<And>x x' s s'. hn_refine
    (\<Gamma> * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
    (f x s)
    (\<Gamma> * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs
    (f' x' s')"

  shows "hn_refine
    (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s)
    (imp_nfoldli l c f s)
    (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs
    (monadic_nfoldli l' c' f' s')"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s) (imp_nfoldli l c f s) (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli l' c' f' s')
[PROOF STEP]
applyF (induct p\<equiv>Rl l' l
    arbitrary: s s'
    rule: list_assn.induct)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] [] * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
 2. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (imp_nfoldli (ca # cs) c f s) (\<Gamma> * hn_invalid (list_assn Rl) (a # as) (ca # cs) * hn_invalid Rs s' s) Rs (monadic_nfoldli (a # as) c' f' s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' f' s')
 4. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
applyF simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s) (return s) (\<Gamma> * hn_invalid (list_assn Rl) [] [] * hn_invalid Rs s' s) Rs (RETURN s')
[PROOF STEP]
apply (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s) (return s) (?Q5 s s') Rs (RETURN s')
 2. \<And>s s'. ?Q5 s s' \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid (list_assn Rl) [] [] * hn_invalid Rs s' s
[PROOF STEP]
apply (rule hn_refine_frame[OF hnr_RETURN_pass])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. \<Gamma> * hn_ctxt Rs s' s \<Longrightarrow>\<^sub>t ?F8 s s' * hn_ctxt Rs s' s
 2. \<And>s s'. ?F8 s s' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid (list_assn Rl) [] [] * hn_invalid Rs s' s
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s s'. \<Gamma> * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t \<Gamma> * hn_invalid (list_assn Rl) [] [] * hn_invalid Rs s' s
[PROOF STEP]
apply (simp add: hn_ctxt_def ent_true_drop invalid_assn_const)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (imp_nfoldli (ca # cs) c f s) (\<Gamma> * hn_invalid (list_assn Rl) (a # as) (ca # cs) * hn_invalid Rs s' s) Rs (monadic_nfoldli (a # as) c' f' s')
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' f' s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
apply1 weaken_hnr_post
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (imp_nfoldli (ca # cs) c f s) (\<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s) Rs (monadic_nfoldli (a # as) c' f' s')
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' f' s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
apply1 (simp only: imp_nfoldli_simps monadic_nfoldli_simp)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (c s \<bind> (\<lambda>b. if b then f ca s \<bind> imp_nfoldli cs c f else return s)) (\<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s) Rs (c' s' \<bind> (\<lambda>b. if b then f' a s' \<bind> monadic_nfoldli as c' f' else RETURN s'))
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' f' s')
 3. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
applyF (rule hnr_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s) (c s) (?\<Gamma>1.28 a as ca cs s s') (?Rh28 a as ca cs s s') (c' s')
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.28 a as ca cs s s' * hn_ctxt (?Rh28 a as ca cs s s') x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.28 a as ca cs s s' x x') Rs (if x then f' a s' \<bind> monadic_nfoldli as c' f' else RETURN s')
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> ?\<Gamma>2.28 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x'
[PROOF STEP]
apply1 (rule hn_refine_frame[OF c_ref])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> \<Gamma> * hn_ctxt (list_assn Rl) (a # as) (ca # cs) * hn_ctxt Rs s' s \<Longrightarrow>\<^sub>t ?F33 a as ca cs s s' * (\<Gamma> * hn_ctxt Rs s' s)
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (?F33 a as ca cs s s' * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.28 a as ca cs s s' x x') Rs (if x then f' a s' \<bind> monadic_nfoldli as c' f' else RETURN s')
 3. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> ?\<Gamma>2.28 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x'
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x') (if x' then f ca s \<bind> imp_nfoldli cs c f else return s) (?\<Gamma>2.28 a as ca cs s s' x x') Rs (if x then f' a s' \<bind> monadic_nfoldli as c' f' else RETURN s')
 2. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> ?\<Gamma>2.28 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x'
[PROOF STEP]
applyF (rule hnr_If)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * (\<Gamma> * hn_ctxt Rs s' s) * hn_val bool_rel x x' \<Longrightarrow>\<^sub>t ?\<Gamma>1.43 a as ca cs s s' x x' * hn_val bool_rel x x'
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.43 a as ca cs s s' x x' * hn_val bool_rel x x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b43 a as ca cs s s' x x') Rs (f' a s' \<bind> monadic_nfoldli as c' f')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.43 a as ca cs s s' x x' * hn_val bool_rel x x') (return s) (?\<Gamma>2c43 a as ca cs s s' x x') Rs (RETURN s')
 4. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b43 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c43 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (f ca s \<bind> imp_nfoldli cs c f) (?\<Gamma>2b43 a as ca cs s s' x x') Rs (f' a s' \<bind> monadic_nfoldli as c' f')
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c43 a as ca cs s s' x x') Rs (RETURN s')
 3. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> ?\<Gamma>2b43 a as ca cs s s' x x' \<or>\<^sub>A ?\<Gamma>2c43 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
applyF (rule hnr_bind)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (f ca s) (?\<Gamma>1.54 a as ca cs s s' x x') (?Rh54 a as ca cs s s' x x') (f' a s')
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?\<Gamma>1.54 a as ca cs s s' x x' * hn_ctxt (?Rh54 a as ca cs s s' x x') xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (rule hn_refine_frame[OF f_ref])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x' \<Longrightarrow>\<^sub>t ?F59 a as ca cs s s' x x' * (\<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (simp add: assn_assoc)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_ctxt Rl a ca * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>t ?F59 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_ctxt Rl a ca * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F59 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (fr_rot 1, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt Rl a ca * hn_ctxt (list_assn Rl) as cs * \<Gamma> \<Longrightarrow>\<^sub>A ?F59 a as ca cs s s' True x' * \<Gamma> * hn_ctxt Rl a ca
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (fr_rot 2, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F59 a as ca cs s s' True x' * \<Gamma>
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply1 (fr_rot 1, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs \<Longrightarrow>\<^sub>A ?F59 a as ca cs s s' True x'
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?F59 a as ca cs s s' x x' * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 3. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
applyS (rule ent_refl)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a) (imp_nfoldli cs c f x'a) (?\<Gamma>2.54 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> ?\<Gamma>2.54 a as ca cs s s' x x' xa x'a \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
applyF (rule hn_refine_frame)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_refine (?P'90 a as ca cs s s' x x' xa x'a) (imp_nfoldli cs c f x'a) (?Q'90 a as ca cs s s' x x' xa x'a) Rs (monadic_nfoldli as c' f' xa)
 2. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F90 a as ca cs s s' x x' xa x'a * ?P'90 a as ca cs s s' x x' xa x'a
[PROOF STEP]
applyS rprems
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel x x' * hn_ctxt (list_assn Rl) as cs * (\<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s) * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F90 a as ca cs s s' x x' xa x'a * (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs xa x'a)
[PROOF STEP]
apply1 (simp add: assn_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>t ?F90 a as ca cs s s' True x' xa x'a * \<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs xa x'a
[PROOF STEP]
apply1 (rule ent_imp_entt)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s * hn_ctxt Rs xa x'a \<Longrightarrow>\<^sub>A ?F90 a as ca cs s s' True x' xa x'a * \<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs xa x'a
[PROOF STEP]
apply (rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_val bool_rel True x' * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s \<Longrightarrow>\<^sub>A ?F90 a as ca cs s s' True x' xa x'a * \<Gamma> * hn_ctxt (list_assn Rl) as cs
[PROOF STEP]
apply1 (fr_rot 3, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> \<Gamma> * hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F90 a as ca cs s s' True x' xa x'a * \<Gamma>
[PROOF STEP]
apply1 (fr_rot 3, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x; RETURN xa \<le> f' a s'\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel True x' \<Longrightarrow>\<^sub>A ?F90 a as ca cs s s' True x' xa x'a
[PROOF STEP]
applyS (rule ent_refl)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs xa x'a) \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' x x' * hn_ctxt (?Rx54 a as ca cs s s' x x') xa x'a
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x' xa x'a. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN True \<le> c' s'; x\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel True x' * (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs xa x'a) \<Longrightarrow>\<^sub>t ?\<Gamma>2b43 a as ca cs s s' True x' * hn_ctxt (?Rx54 a as ca cs s s' True x') xa x'a
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_refine (hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x') (return s) (?\<Gamma>2c43 a as ca cs s s' x x') Rs (RETURN s')
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_invalid (list_assn Rl) as cs \<or>\<^sub>A ?\<Gamma>2c43 a as ca cs s s' x x' \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
apply1 (rule hn_refine_frame[OF hnr_RETURN_pass])
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'; \<not> x\<rbrakk> \<Longrightarrow> hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_ctxt Rs s' s * hn_val bool_rel x x' \<Longrightarrow>\<^sub>t ?F230 a as ca cs s s' x x' * hn_ctxt Rs s' s
 2. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_invalid (list_assn Rl) as cs \<or>\<^sub>A ?F230 a as ca cs s s' x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_invalid (list_assn Rl) as cs \<or>\<^sub>A hn_ctxt (list_assn Rl) (a # as) (ca # cs) * \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
apply1 (simp add: assn_assoc)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. \<lbrakk>\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s'); RETURN x \<le> c' s'\<rbrakk> \<Longrightarrow> hn_invalid Rl a ca * hn_invalid Rs s' s * hn_val bool_rel x x' * \<Gamma> * hn_invalid (list_assn Rl) as cs \<or>\<^sub>A hn_ctxt Rl a ca * hn_ctxt (list_assn Rl) as cs * \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s \<Longrightarrow>\<^sub>t ?\<Gamma>2.28 a as ca cs s s' x x'
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.merge_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_invalid (list_assn Rl) as cs * hn_invalid Rl a ca \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x'
[PROOF STEP]
apply (rule enttI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_invalid (list_assn Rl) as cs * hn_invalid Rl a ca \<Longrightarrow>\<^sub>A \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x' * true
[PROOF STEP]
apply (fr_rot_rhs 1)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> \<Gamma> * hn_val bool_rel x x' * hn_invalid Rs s' s * hn_invalid (list_assn Rl) as cs * hn_invalid Rl a ca \<Longrightarrow>\<^sub>A true * \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s * hn_ctxt (?Rx28 a as ca cs s s') x x'
[PROOF STEP]
apply (fr_rot 3, rule fr_refl)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>a as ca cs s s' x x'. (\<And>s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) as cs * hn_ctxt Rs s' s) (imp_nfoldli cs c f s) (\<Gamma> * hn_invalid (list_assn Rl) as cs * hn_invalid Rs s' s) Rs (monadic_nfoldli as c' f' s')) \<Longrightarrow> hn_invalid Rs s' s * hn_invalid (list_assn Rl) as cs * hn_invalid Rl a ca * \<Gamma> \<Longrightarrow>\<^sub>A true * \<Gamma> * hn_ctxt (\<lambda>_ _. true) (a # as) (ca # cs) * hn_ctxt (\<lambda>_ _. true) s' s
[PROOF STEP]
applyS (fr_rot 3, rule ent_star_mono[rotated]; sep_auto simp: hn_ctxt_def)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) (v # va) [] * hn_ctxt Rs s' s) (imp_nfoldli [] c f s) (\<Gamma> * hn_invalid (list_assn Rl) (v # va) [] * hn_invalid Rs s' s) Rs (monadic_nfoldli (v # va) c' f' s')
 2. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
applyS (simp add: hn_ctxt_def invalid_assn_def)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>v va s s'. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) [] (v # va) * hn_ctxt Rs s' s) (imp_nfoldli (v # va) c f s) (\<Gamma> * hn_invalid (list_assn Rl) [] (v # va) * hn_invalid Rs s' s) Rs (monadic_nfoldli [] c' f' s')
[PROOF STEP]
applyS (rule, sep_auto)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
solved
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma hn_monadic_nfoldli:
  assumes FR: "P \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s"
  assumes c_ref: "\<And>s s'. hn_refine
    (\<Gamma> * hn_ctxt Rs s' s)
    (c s)
    (\<Gamma> * hn_ctxt Rs s' s)
    bool_assn
    (c'$s')"
  assumes f_ref: "\<And>x x' s s'. hn_refine
    (\<Gamma> * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
    (f x s)
    (\<Gamma> * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs
    (f'$x'$s')"
  shows "hn_refine
    P
    (imp_nfoldli l c f s)
    (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s)
    Rs
    (monadic_nfoldli$l'$c'$f'$s')
    "
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine P (imp_nfoldli l c f s) (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli $ l' $ c' $ f' $ s')
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s) (imp_nfoldli l c f s) (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli $ l' $ c' $ f' $ s')
[PROOF STEP]
unfolding APP_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s) (imp_nfoldli l c f s) (\<Gamma> * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs (monadic_nfoldli l' c' f' s')
[PROOF STEP]
apply (rule monadic_nfoldli_refine_aux)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s s'. hn_refine (\<Gamma> * hn_ctxt Rs s' s) (c s) (\<Gamma> * hn_ctxt Rs s' s) bool_assn (c' s')
 2. \<And>x x' s s'. hn_refine (\<Gamma> * hn_ctxt Rl x' x * hn_ctxt Rs s' s) (f x s) (\<Gamma> * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs (f' x' s')
[PROOF STEP]
apply (rule c_ref[unfolded APP_def])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x x' s s'. hn_refine (\<Gamma> * hn_ctxt Rl x' x * hn_ctxt Rs s' s) (f x s) (\<Gamma> * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs (f' x' s')
[PROOF STEP]
apply (rule f_ref[unfolded APP_def])
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma heap_fixp_mono[partial_function_mono]:
  assumes [partial_function_mono]:
    "\<And>x d. mono_Heap (\<lambda>xa. B x xa d)"
    "\<And>Z xa. mono_Heap (\<lambda>a. B a Z xa)"
  shows "mono_Heap (\<lambda>x. heap.fixp_fun (\<lambda>D \<sigma>. B x D \<sigma>) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>x. heap.fixp_fun (B x) \<sigma>)
[PROOF STEP]
apply rule
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> Heap_ord (heap.fixp_fun (B x) \<sigma>) (heap.fixp_fun (B y) \<sigma>)
[PROOF STEP]
apply (rule ccpo.fixp_mono[OF heap.ccpo, THEN fun_ordD])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x y. heap.le_fun x y \<Longrightarrow> monotone heap.le_fun heap.le_fun (B x)
 2. \<And>x y. heap.le_fun x y \<Longrightarrow> monotone heap.le_fun heap.le_fun (B y)
 3. \<And>x y Z. heap.le_fun x y \<Longrightarrow> heap.le_fun (B x Z) (B y Z)
[PROOF STEP]
apply (rule mono_fun_fun_cnv, erule thin_rl, pf_mono)+
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y Z. heap.le_fun x y \<Longrightarrow> heap.le_fun (B x Z) (B y Z)
[PROOF STEP]
apply (rule fun_ordI)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y Z xa. heap.le_fun x y \<Longrightarrow> Heap_ord (B x Z xa) (B y Z xa)
[PROOF STEP]
apply (erule monotoneD[of "fun_ord Heap_ord" Heap_ord, rotated])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>x y Z xa. monotone heap.le_fun Heap_ord (\<lambda>a. B a Z xa)
[PROOF STEP]
apply pf_mono
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma imp_nfoldli_mono[partial_function_mono]:
  assumes [partial_function_mono]: "\<And>x \<sigma>. mono_Heap (\<lambda>fa. f fa x \<sigma>)"
  shows "mono_Heap (\<lambda>x. imp_nfoldli l c (f x) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>x. imp_nfoldli l c (f x) \<sigma>)
[PROOF STEP]
unfolding imp_nfoldli_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>x. heap.fixp_fun (\<lambda>D (l, s). case l of [] \<Rightarrow> return s | xa # ls \<Rightarrow> c s \<bind> (\<lambda>b. if b then f x xa s \<bind> (\<lambda>s'. D (ls, s')) else return s)) (l, \<sigma>))
[PROOF STEP]
by pf_mono


[STATEMENT]
lemma imp_foreach_mono[partial_function_mono]:
  assumes [partial_function_mono]: "\<And>x \<sigma>. mono_Heap (\<lambda>fa. f fa x \<sigma>)"
  shows "mono_Heap (\<lambda>x. imp_foreach tsl l c (f x) \<sigma>)"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>x. imp_foreach tsl l c (f x) \<sigma>)
[PROOF STEP]
unfolding imp_foreach_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monotone heap.le_fun Heap_ord (\<lambda>x. tsl l \<bind> (\<lambda>l. imp_nfoldli l c (f x) \<sigma>))
[PROOF STEP]
by pf_mono


[STATEMENT]
lemma IS_TO_SORTED_LISTI:
  assumes "(tsl,PR_CONST (it_to_sorted_list \<Omega>)) \<in> (Rs)\<^sup>k \<rightarrow>\<^sub>a list_assn Rk"
  shows "IS_TO_SORTED_LIST \<Omega> Rs Rk tsl"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. IS_TO_SORTED_LIST \<Omega> Rs Rk tsl
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
(tsl, PR_CONST (it_to_sorted_list \<Omega>)) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk

goal (1 subgoal):
 1. IS_TO_SORTED_LIST \<Omega> Rs Rk tsl
[PROOF STEP]
unfolding IS_TO_SORTED_LIST_def PR_CONST_def
[PROOF STATE]
proof (prove)
using this:
(tsl, it_to_sorted_list \<Omega>) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk

goal (1 subgoal):
 1. (tsl, it_to_sorted_list \<Omega>) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk
[PROOF STEP]
.


[STATEMENT]
lemma hn_monadic_FOREACH[sepref_comb_rules]:
  assumes "INDEP Rk" "INDEP Rs" "INDEP R\<sigma>"
  assumes FR: "P \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>"
  assumes STL: "GEN_ALGO tsl (IS_TO_SORTED_LIST ordR Rs Rk)"
  assumes c_ref: "\<And>\<sigma> \<sigma>'. hn_refine
    (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>)
    (c \<sigma>)
    (\<Gamma>c \<sigma>' \<sigma>)
    bool_assn
    (c' \<sigma>')"
  assumes C_FR:
    "\<And>\<sigma>' \<sigma>. TERM monadic_FOREACH \<Longrightarrow>
      \<Gamma>c \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>"

  assumes f_ref: "\<And>x' x \<sigma>' \<sigma>. hn_refine
    (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x' x * hn_ctxt R\<sigma> \<sigma>' \<sigma>)
    (f x \<sigma>)
    (\<Gamma>f x' x \<sigma>' \<sigma>) R\<sigma>
    (f' x' \<sigma>')"
  assumes F_FR: "\<And>x' x \<sigma>' \<sigma>. TERM monadic_FOREACH \<Longrightarrow> \<Gamma>f x' x \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t
    \<Gamma> * hn_ctxt Rs s' s * hn_ctxt Pfx x' x * hn_ctxt Pf\<sigma> \<sigma>' \<sigma>"

  shows "hn_refine
    P
    (imp_foreach tsl s c f \<sigma>)
    (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>)
    R\<sigma>
    ((PR_CONST (monadic_FOREACH ordR I))
      $s'$(\<lambda>\<^sub>2\<sigma>'. c' \<sigma>')$(\<lambda>\<^sub>2x' \<sigma>'. f' x' \<sigma>')$\<sigma>'
    )"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine P (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
proof -
[PROOF STATE]
proof (state)
goal (1 subgoal):
 1. hn_refine P (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
from STL
[PROOF STATE]
proof (chain)
picking this:
GEN_ALGO tsl (IS_TO_SORTED_LIST ordR Rs Rk)
[PROOF STEP]
have STL: "(tsl,it_to_sorted_list ordR) \<in> (Rs)\<^sup>k \<rightarrow>\<^sub>a list_assn Rk"
[PROOF STATE]
proof (prove)
using this:
GEN_ALGO tsl (IS_TO_SORTED_LIST ordR Rs Rk)

goal (1 subgoal):
 1. (tsl, it_to_sorted_list ordR) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk
[PROOF STEP]
unfolding GEN_ALGO_def IS_TO_SORTED_LIST_def
[PROOF STATE]
proof (prove)
using this:
(tsl, it_to_sorted_list ordR) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk

goal (1 subgoal):
 1. (tsl, it_to_sorted_list ordR) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk
[PROOF STEP]
by simp
[PROOF STATE]
proof (state)
this:
(tsl, it_to_sorted_list ordR) \<in> Rs\<^sup>k \<rightarrow>\<^sub>a list_assn Rk

goal (1 subgoal):
 1. hn_refine P (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
show ?thesis
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine P (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
apply (rule hn_refine_cons_pre[OF FR])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
apply weaken_hnr_post
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')
[PROOF STEP]
unfolding APP_def PROTECT2_def PR_CONST_def imp_foreach_def
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)) (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>) R\<sigma> (monadic_FOREACH ordR I s' c' f' \<sigma>')
[PROOF STEP]
apply (rule hn_refine_ref[OF monadic_FOREACH_itsl])
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) (tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)) (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>) R\<sigma> (it_to_sorted_list ordR s' \<bind> (\<lambda>l. monadic_nfoldli l c' f' \<sigma>'))
[PROOF STEP]
apply (rule hn_refine_guessI)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) ?f11 (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma>) R\<sigma> (it_to_sorted_list ordR s' \<bind> (\<lambda>l. monadic_nfoldli l c' f' \<sigma>'))
 2. ?f11 = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule hnr_bind)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma>) ?m'14 ?\<Gamma>1.14 ?Rh14 (it_to_sorted_list ordR s')
 2. \<And>x x'. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (?\<Gamma>1.14 * hn_ctxt ?Rh14 x x') (?f'14 x') (?\<Gamma>2.14 x x') R\<sigma> (monadic_nfoldli x c' f' \<sigma>')
 3. \<And>x x'. ?\<Gamma>2.14 x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 4. ?m'14 \<bind> ?f'14 = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule hn_refine_frame)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. hn_refine ?P'18 ?m'14 ?Q'18 ?Rh14 (it_to_sorted_list ordR s')
 2. \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t ?F18 * ?P'18
 3. \<And>x x'. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (?F18 * ?Q'18 * hn_ctxt ?Rh14 x x') (?f'14 x') (?\<Gamma>2.14 x x') R\<sigma> (monadic_nfoldli x c' f' \<sigma>')
 4. \<And>x x'. ?\<Gamma>2.14 x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 5. ?m'14 \<bind> ?f'14 = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule STL[to_hnr, unfolded APP_def])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t ?F18 * hn_ctxt Rs s' ?xi21
 2. \<And>x x'. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (?F18 * hn_ctxt Rs s' ?xi21 * hn_ctxt (list_assn Rk) x x') (?f'14 x') (?\<Gamma>2.14 x x') R\<sigma> (monadic_nfoldli x c' f' \<sigma>')
 3. \<And>x x'. ?\<Gamma>2.14 x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 4. tsl ?xi21 \<bind> ?f'14 = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x'. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt R\<sigma> \<sigma>' \<sigma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rk) x x') (?f'14 x') (?\<Gamma>2.14 x x') R\<sigma> (monadic_nfoldli x c' f' \<sigma>')
 2. \<And>x x'. ?\<Gamma>2.14 x x' \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 3. tsl s \<bind> ?f'14 = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule hn_monadic_nfoldli[unfolded APP_def])
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x x'. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> \<Gamma> * hn_ctxt R\<sigma> \<sigma>' \<sigma> * hn_ctxt Rs s' s * hn_ctxt (list_assn Rk) x x' \<Longrightarrow>\<^sub>t ?\<Gamma>29 x x' * hn_ctxt (list_assn (?Rl29 x x')) x (?l30 x') * hn_ctxt R\<sigma> \<sigma>' (?s33 x')
 2. \<And>x x' s s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (?\<Gamma>29 x x' * hn_ctxt R\<sigma> s'a s) (?c31 x' s) (?\<Gamma>29 x x' * hn_ctxt R\<sigma> s'a s) bool_assn (c' s'a)
 3. \<And>x x' xa x'a s s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (?\<Gamma>29 x x' * hn_ctxt (?Rl29 x x') x'a xa * hn_ctxt R\<sigma> s'a s) (?f32 x' xa s) (?\<Gamma>29 x x' * hn_invalid (?Rl29 x x') x'a xa * hn_invalid R\<sigma> s'a s) R\<sigma> (f' x'a s'a)
 4. \<And>x x'. ?\<Gamma>29 x x' * hn_invalid (list_assn (?Rl29 x x')) x (?l30 x') * hn_invalid R\<sigma> \<sigma>' (?s33 x') \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 5. tsl s \<bind> (\<lambda>x'. imp_nfoldli (?l30 x') (?c31 x') (?f32 x') (?s33 x')) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x' sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> s'a sa) (?c31 x' sa) (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> s'a sa) bool_assn (c' s'a)
 2. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?f32 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid Rk x'a xa * hn_invalid R\<sigma> s'a sa) R\<sigma> (f' x'a s'a)
 3. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 4. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' (?c31 x') (?f32 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (5 subgoals):
 1. \<And>x x' sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> s'a sa) (?c31 x' sa) (?Q41 x x' sa s'a) bool_assn (c' s'a)
 2. \<And>x x' sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> ?Q41 x x' sa s'a \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> s'a sa
 3. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?f32 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid Rk x'a xa * hn_invalid R\<sigma> s'a sa) R\<sigma> (f' x'a s'a)
 4. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 5. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' (?c31 x') (?f32 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule c_ref[unfolded APP_def])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x' sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> \<Gamma>c s'a sa \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt R\<sigma> s'a sa
 2. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?f32 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid Rk x'a xa * hn_invalid R\<sigma> s'a sa) R\<sigma> (f' x'a s'a)
 3. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 4. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c (?f32 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule C_FR)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x' s s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> TERM monadic_FOREACH
 2. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?f32 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid Rk x'a xa * hn_invalid R\<sigma> s'a sa) R\<sigma> (f' x'a s'a)
 3. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 4. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c (?f32 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule TERMI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?f32 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid Rk x'a xa * hn_invalid R\<sigma> s'a sa) R\<sigma> (f' x'a s'a)
 2. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx14 x x'
 3. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c (?f32 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply weaken_hnr_post
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?fa10 x' xa sa) (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) x'a xa * hn_ctxt (\<lambda>_ _. true) s'a sa) R\<sigma> (f' x'a s'a)
 2. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 3. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c (?fa10 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule hn_refine_cons_post)
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> hn_refine (\<Gamma> * hn_ctxt Rs s' s * hn_ctxt Rk x'a xa * hn_ctxt R\<sigma> s'a sa) (?fa10 x' xa sa) (?Q11 x x' xa x'a sa s'a) R\<sigma> (f' x'a s'a)
 2. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> ?Q11 x x' xa x'a sa s'a \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) x'a xa * hn_ctxt (\<lambda>_ _. true) s'a sa
 3. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 4. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c (?fa10 x') \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule f_ref[unfolded APP_def])
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> \<Gamma>f x'a xa s'a sa \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) x'a xa * hn_ctxt (\<lambda>_ _. true) s'a sa
 2. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 3. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c f \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule entt_trans[OF F_FR])
[PROOF STATE]
proof (prove)
goal (4 subgoals):
 1. \<And>x x' xa x'a s s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> TERM monadic_FOREACH
 2. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> \<Gamma> * hn_ctxt Rs s' s * hn_ctxt Pfx x'a xa * hn_ctxt Pf\<sigma> s'a sa \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) x'a xa * hn_ctxt (\<lambda>_ _. true) s'a sa
 3. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 4. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c f \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply (rule TERMI)
[PROOF STATE]
proof (prove)
goal (3 subgoals):
 1. \<And>x x' xa x'a sa s'a. RETURN x \<le> it_to_sorted_list ordR s' \<Longrightarrow> \<Gamma> * hn_ctxt Rs s' s * hn_ctxt Pfx x'a xa * hn_ctxt Pf\<sigma> s'a sa \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) x'a xa * hn_ctxt (\<lambda>_ _. true) s'a sa
 2. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 3. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c f \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>x x'. \<Gamma> * hn_ctxt Rs s' s * hn_invalid (list_assn Rk) x x' * hn_invalid R\<sigma> \<sigma>' \<sigma> \<Longrightarrow>\<^sub>t \<Gamma> * hn_ctxt Rs s' s * hn_ctxt (\<lambda>_ _. true) \<sigma>' \<sigma> * hn_ctxt ?Rx10 x x'
 2. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c f \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
applyS (tactic \<open>Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1\<close>)
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. tsl s \<bind> (\<lambda>x'. imp_nfoldli x' c f \<sigma>) = tsl s \<bind> (\<lambda>l. imp_nfoldli l c f \<sigma>)
[PROOF STEP]
apply simp
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done
[PROOF STATE]
proof (state)
this:
hn_refine P (imp_foreach tsl s c f \<sigma>) (\<Gamma> * hn_ctxt Rs s' s * hn_invalid R\<sigma> \<sigma>' \<sigma>) R\<sigma> (PR_CONST (monadic_FOREACH ordR I) $ s' $ (\<lambda>x. (#c' x#)) $ (\<lambda>x. (#\<lambda>xa. (#f' x xa#)#)) $ \<sigma>')

goal:
No subgoals!
[PROOF STEP]
qed


[STATEMENT]
lemma monadic_nfoldli_assert_aux:
  assumes "set l \<subseteq> S"
  shows "monadic_nfoldli l c (\<lambda>x s. ASSERT (x\<in>S)\<then>f x s) s = monadic_nfoldli l c f s"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. monadic_nfoldli l c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = monadic_nfoldli l c f s
[PROOF STEP]
using assms
[PROOF STATE]
proof (prove)
using this:
set l \<subseteq> S

goal (1 subgoal):
 1. monadic_nfoldli l c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = monadic_nfoldli l c f s
[PROOF STEP]
apply (induction l arbitrary: s)
[PROOF STATE]
proof (prove)
goal (2 subgoals):
 1. \<And>s. set [] \<subseteq> S \<Longrightarrow> monadic_nfoldli [] c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = monadic_nfoldli [] c f s
 2. \<And>a l s. \<lbrakk>\<And>s. set l \<subseteq> S \<Longrightarrow> monadic_nfoldli l c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = monadic_nfoldli l c f s; set (a # l) \<subseteq> S\<rbrakk> \<Longrightarrow> monadic_nfoldli (a # l) c (\<lambda>x s. ASSERT (x \<in> S) \<bind> (\<lambda>_. f x s)) s = monadic_nfoldli (a # l) c f s
[PROOF STEP]
apply (auto simp: pw_eq_iff refine_pw_simps)
[PROOF STATE]
proof (prove)
goal:
No subgoals!
[PROOF STEP]
done


[STATEMENT]
lemma nfoldli_arities[sepref_monadify_arity]:
  "nfoldli \<equiv> \<lambda>\<^sub>2s c f \<sigma>. SP (nfoldli)$s$(\<lambda>\<^sub>2x. c$x)$(\<lambda>\<^sub>2x \<sigma>. f$x$\<sigma>)$\<sigma>"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. nfoldli \<equiv> \<lambda>x. (#\<lambda>xa. (#\<lambda>xb. (#\<lambda>xc. (#SP nfoldli $ x $ (\<lambda>x. (#xa $ x#)) $ (\<lambda>x. (#\<lambda>xa. (#xb $ x $ xa#)#)) $ xc#)#)#)#)
[PROOF STEP]
by (simp_all)


[STATEMENT]
lemma nfoldli_comb[sepref_monadify_comb]:
  "\<And>s c f \<sigma>. (nfoldli)$s$(\<lambda>\<^sub>2x. c x)$f$\<sigma> \<equiv>
    Refine_Basic.bind$(EVAL$s)$(\<lambda>\<^sub>2s. Refine_Basic.bind$(EVAL$\<sigma>)$(\<lambda>\<^sub>2\<sigma>.
      SP (monadic_nfoldli)$s$(\<lambda>\<^sub>2x. (EVAL$(c x)))$f$\<sigma>
    ))"
[PROOF STATE]
proof (prove)
goal (1 subgoal):
 1. \<And>s c f \<sigma>. nfoldli $ s $ (\<lambda>x. (#c x#)) $ f $ \<sigma> \<equiv> (\<bind>) $ (EVAL $ s) $ (\<lambda>x. (#(\<bind>) $ (EVAL $ \<sigma>) $ (\<lambda>xa. (#SP monadic_nfoldli $ x $ (\<lambda>x. (#EVAL $ c x#)) $ f $ xa#))#))
[PROOF STEP]
by (simp_all add: nfoldli_to_monadic)