# Theory Refine_Imperative_HOL.Sepref_Foreach

```section ‹Setup for Foreach Combinator›
theory Sepref_Foreach
begin

subsection "Foreach Loops"

text ‹
In a first step, we define a version of foreach where the continuation condition
is also monadic, and show that it is equal to the standard version for
continuation conditions of the form ‹λx. RETURN (c x)›
›

definition "FOREACH_inv xs Φ s ≡
case s of (it, σ) ⇒ ∃xs'. xs = xs' @ it ∧ Φ (set it) σ"

definition "monadic_FOREACH R Φ S c f σ0 ≡ do {
ASSERT (finite S);
xs0 ← it_to_sorted_list R S;
(_,σ) ← RECT (λW (xs,σ). do {
ASSERT (FOREACH_inv xs0 Φ (xs,σ));
if xs≠[] then do {
b ← c σ;
if b then
FOREACH_body f (xs,σ) ⤜ W
else
RETURN (xs,σ)
} else RETURN (xs,σ)
}) (xs0,σ0);
RETURN σ
}"

"FOREACHoci R Φ S c f σ0 = monadic_FOREACH R Φ S (λσ. RETURN (c σ)) f σ0"
unfolding it_to_sorted_list_def FOREACH_cond_def FOREACH_inv_def
apply simp
apply (fo_rule arg_cong[THEN cong] | rule refl ext)+
apply (simp split: prod.split)
apply (rule refl)+
done

text ‹Next, we define a characterization w.r.t. ‹nfoldli››
definition "monadic_nfoldli l c f s ≡ RECT (λD (l,s). case l of
[] ⇒ RETURN s
| x#ls ⇒ do {
b ← c s;
if b then do { s'←f x s; D (ls,s')} else RETURN s
}
) (l,s)"

"monadic_nfoldli l c f s = (
case l of
[] ⇒ RETURN s
| x#ls ⇒ do {
b←c s;
if b then f x s ⤜ monadic_nfoldli ls c f else RETURN s
}
)"
apply (subst RECT_unfold)
apply (tagged_solver)
apply simp
done

"monadic_nfoldli [] c f s = RETURN s"
"monadic_nfoldli (x#ls) c f s = do {
b←c s;
if b then f x s ⤜ monadic_nfoldli ls c f else RETURN s
}"
done

"nfoldli l c f = monadic_nfoldli l (λx. RETURN (c x)) f"
apply (induct l)
apply auto
done

definition "nfoldli_alt l c f s ≡ RECT (λD (l,s). case l of
[] ⇒ RETURN s
| x#ls ⇒ do {
let b = c s;
if b then do { s'←f x s; D (ls,s')} else RETURN s
}
) (l,s)"

lemma nfoldli_alt_eq:
"nfoldli_alt l c f s = (
case l of
[] ⇒ RETURN s
| x#ls ⇒ do {let b=c s; if b then f x s ⤜ nfoldli_alt ls c f else RETURN s}
)"
apply (subst nfoldli_alt_def)
apply (subst RECT_unfold)
apply (tagged_solver)
apply (subst nfoldli_alt_def[symmetric])
apply simp
done

lemma nfoldli_alt_simp[simp]:
"nfoldli_alt [] c f s = RETURN s"
"nfoldli_alt (x#ls) c f s = do {
let b = c s;
if b then f x s ⤜ nfoldli_alt ls c f else RETURN s
}"
apply (subst nfoldli_alt_eq, simp)
apply (subst nfoldli_alt_eq, simp)
done

lemma nfoldli_alt:
"(nfoldli::'a list ⇒ ('b ⇒ bool) ⇒ ('a ⇒ 'b ⇒ 'b nres) ⇒ 'b ⇒ 'b nres)
= nfoldli_alt"
proof (intro ext)
fix l::"'a list" and c::"'b ⇒ bool" and f::"'a ⇒ 'b ⇒ 'b nres" and s :: 'b
have "nfoldli l c f = nfoldli_alt l c f"
by (induct l) auto
thus "nfoldli l c f s = nfoldli_alt l c f s" by simp
qed

≤⇓Id (REC⇩T
(λW (xs, σ).
ASSERT (FOREACH_inv xs0 I (xs, σ)) ⤜
(λ_. if xs = [] then RETURN (xs, σ)
else c σ ⤜
(λb. if b then FOREACH_body f (xs, σ) ⤜ W
else RETURN (xs, σ))))
(x', σ) ⤜
(λ(_, y). RETURN y))"
apply (induct x' arbitrary: σ)

apply (subst RECT_unfold, refine_mono)
apply (simp)
apply (rule le_ASSERTI)
apply simp

apply (subst RECT_unfold, refine_mono)
apply (simp del: conc_Id cong: if_cong)
apply refine_rcg
apply simp
apply (rule_tac R="br (Pair x') (λ_. True)" in intro_prgR)
apply (simp add: pw_le_iff refine_pw_simps br_def)

apply (rule order_trans)
apply rprems
done

by (simp_all)

"⋀s c f σ. (monadic_nfoldli)\$s\$c\$f\$σ ≡
Refine_Basic.bind\$(EVAL\$s)\$(λ⇩2s. Refine_Basic.bind\$(EVAL\$σ)\$(λ⇩2σ.
))"
by (simp_all)

lemma list_rel_congD:
assumes A: "(li,l)∈⟨S⟩list_rel"
shows "(li,l)∈⟨S∩(set li×set l)⟩list_rel"
proof -
{
fix Si0 S0
assume "set li ⊆ Si0" "set l ⊆ S0"
with A have "(li,l)∈⟨S∩(Si0×S0)⟩list_rel"
by (induction rule: list_rel_induct) auto
} from this[OF order_refl order_refl] show ?thesis .
qed

assumes L: "(li, l) ∈ ⟨S⟩list_rel"
and  [simp]: "(si, s) ∈ R"
and CR[refine]: "⋀si s. (si,s)∈R ⟹ ci si ≤⇓bool_rel (c s)"
and [refine]: "⋀xi x si s. ⟦ (xi,x)∈S; x∈set l; (si,s)∈R; inres (c s) True ⟧ ⟹ fi xi si ≤ ⇓R (f x s)"
shows "monadic_nfoldli li ci fi si ≤ ⇓ R (monadic_nfoldli l c f s)"

supply RELATESI[of "S∩(set li×set l)", refine_dref_RELATES]
supply RELATESI[of R, refine_dref_RELATES]
apply (refine_rcg bind_refine')
apply refine_dref_type
apply (vc_solve simp: list_rel_congD[OF L])
done

fixes R I tsl
shows
"do { l ← it_to_sorted_list R s; monadic_nfoldli l c f σ }
≤ monadic_FOREACH R I s c f σ"
apply (rule refine_IdD)
apply (refine_rcg)
apply simp
done

lemma FOREACHoci_itsl:
fixes R I tsl
shows
"do { l ← it_to_sorted_list R s; nfoldli l c f σ }
≤ FOREACHoci R I s c f σ"
apply (rule refine_IdD)
unfolding FOREACHoci_def it_to_sorted_list_def
apply refine_rcg
apply simp
apply (rule nfoldli_while)
done

lemma [def_pat_rules]:
"FOREACHc ≡ PR_CONST (FOREACHoci (λ_ _. True) (λ_ _. True))"
"FOREACHci\$I ≡ PR_CONST (FOREACHoci (λ_ _. True) I)"
"FOREACHi\$I ≡ λ⇩2s. PR_CONST (FOREACHoci (λ_ _. True) I)\$s\$(λ⇩2x. True)"
"FOREACH ≡ FOREACHi\$(λ⇩2_ _. True)"
FOREACHci_def FOREACHi_def[abs_def] FOREACHc_def FOREACH_def[abs_def])

term "FOREACHoci R I"
lemma id_FOREACHoci[id_rules]: "PR_CONST (FOREACHoci R I) ::⇩i
TYPE('c set ⇒ ('d ⇒ bool) ⇒ ('c ⇒ 'd ⇒ 'd nres) ⇒ 'd ⇒ 'd nres)"
by simp

text ‹We set up the monadify-phase such that all FOREACH-loops get
rewritten to the monadic version of FOREACH›
(*"FOREACHc ≡ FOREACHoci\$(λ⇩2_ _. True)\$(λ⇩2_ _. True)"
"FOREACHci ≡ FOREACHoci\$(λ⇩2_ _. True)"
"FOREACHi ≡ λ⇩2I s. FOREACHci\$I\$s\$(λ⇩2x. True)"
"FOREACH ≡ FOREACHi\$(λ⇩2_ _. True)"*)
"PR_CONST (FOREACHoci R I) ≡ λ⇩2s c f σ. SP (PR_CONST (FOREACHoci R I))\$s\$(λ⇩2x. c\$x)\$(λ⇩2x σ. f\$x\$σ)\$σ"
by (simp_all)

"⋀s c f σ. (PR_CONST (FOREACHoci R I))\$s\$(λ⇩2x. c x)\$f\$σ ≡
Refine_Basic.bind\$(EVAL\$s)\$(λ⇩2s. Refine_Basic.bind\$(EVAL\$σ)\$(λ⇩2σ.
SP (PR_CONST (monadic_FOREACH R I))\$s\$(λ⇩2x. (EVAL\$(c x)))\$f\$σ
))"

subsubsection "Imperative Version of nfoldli"
text ‹We define an imperative version of ‹nfoldli›. It is the

definition "imp_nfoldli l c f s ≡ heap.fixp_fun (λD (l,s). case l of
[] ⇒ return s
| x#ls ⇒ do {
b←c s;
if b then do { s'←f x s; D (ls,s')} else return s
}
) (l,s)"

declare imp_nfoldli_def[code del]

lemma imp_nfoldli_simps[simp,code]:
"imp_nfoldli [] c f s = return s"
"imp_nfoldli (x#ls) c f s = (do {
b ← c s;
if b then do {
s'←f x s;
imp_nfoldli ls c f s'
} else return s
})"
apply -
unfolding imp_nfoldli_def
apply (subst heap.mono_body_fixp)
apply pf_mono
apply simp
apply (subst heap.mono_body_fixp)
apply pf_mono
apply simp
done

assumes c_ref: "⋀s s'. hn_refine
(Γ * hn_ctxt Rs s' s)
(c s)
(Γ * hn_ctxt Rs s' s)
bool_assn
(c' s')"
assumes f_ref: "⋀x x' s s'. hn_refine
(Γ * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
(f x s)
(Γ * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs
(f' x' s')"

shows "hn_refine
(Γ * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s)
(imp_nfoldli l c f s)
(Γ * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s) Rs
applyF (induct p≡Rl l' l
arbitrary: s s'
rule: list_assn.induct)

applyF simp
apply (rule hn_refine_cons_post)
apply (rule hn_refine_frame[OF hnr_RETURN_pass])
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
apply (simp add: hn_ctxt_def ent_true_drop invalid_assn_const)
solved

apply1 weaken_hnr_post
applyF (rule hnr_bind)
apply1 (rule hn_refine_frame[OF c_ref])
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)

applyF (rule hnr_If)
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
applyF (rule hnr_bind)
apply1 (rule hn_refine_frame[OF f_ref])

apply1 (rule ent_imp_entt)
apply1 (fr_rot 1, rule fr_refl)
apply1 (fr_rot 2, rule fr_refl)
apply1 (fr_rot 1, rule fr_refl)
applyS (rule ent_refl)

applyF (rule hn_refine_frame)
applyS rprems

apply1 (rule ent_imp_entt)
apply (rule fr_refl)
apply1 (fr_rot 3, rule fr_refl)
apply1 (fr_rot 3, rule fr_refl)
applyS (rule ent_refl)
solved

apply simp

applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
solved

apply1 (rule hn_refine_frame[OF hnr_RETURN_pass])
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)

applyS (tactic ‹Sepref_Frame.merge_tac (K (K no_tac)) @{context} 1›)
solved

apply (rule enttI)
apply (fr_rot_rhs 1)
apply (fr_rot 3, rule fr_refl)
applyS (fr_rot 3, rule ent_star_mono[rotated]; sep_auto simp: hn_ctxt_def)
solved

applyS (rule, sep_auto)
solved
done

assumes FR: "P ⟹⇩t Γ * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s"
assumes c_ref: "⋀s s'. hn_refine
(Γ * hn_ctxt Rs s' s)
(c s)
(Γ * hn_ctxt Rs s' s)
bool_assn
(c'\$s')"
assumes f_ref: "⋀x x' s s'. hn_refine
(Γ * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
(f x s)
(Γ * hn_invalid Rl x' x * hn_invalid Rs s' s) Rs
(f'\$x'\$s')"
shows "hn_refine
P
(imp_nfoldli l c f s)
(Γ * hn_invalid (list_assn Rl) l' l * hn_invalid Rs s' s)
Rs
"
apply (rule hn_refine_cons_pre[OF FR])
unfolding APP_def
apply (rule c_ref[unfolded APP_def])
apply (rule f_ref[unfolded APP_def])
done

definition
imp_foreach :: "('b ⇒ 'c list Heap) ⇒ 'b ⇒ ('a ⇒ bool Heap) ⇒ ('c ⇒ 'a ⇒ 'a Heap) ⇒ 'a ⇒ 'a Heap"
where
"imp_foreach tsl s c f σ ≡ do { l ← tsl s; imp_nfoldli l c f σ}"

lemma heap_fixp_mono[partial_function_mono]:
assumes [partial_function_mono]:
"⋀x d. mono_Heap (λxa. B x xa d)"
"⋀Z xa. mono_Heap (λa. B a Z xa)"
shows "mono_Heap (λx. heap.fixp_fun (λD σ. B x D σ) σ)"
apply rule
apply (rule ccpo.fixp_mono[OF heap.ccpo, THEN fun_ordD])
apply (rule mono_fun_fun_cnv, erule thin_rl, pf_mono)+
apply (rule fun_ordI)
apply (erule monotoneD[of "fun_ord Heap_ord" Heap_ord, rotated])
apply pf_mono
done

lemma imp_nfoldli_mono[partial_function_mono]:
assumes [partial_function_mono]: "⋀x σ. mono_Heap (λfa. f fa x σ)"
shows "mono_Heap (λx. imp_nfoldli l c (f x) σ)"
unfolding imp_nfoldli_def
by pf_mono

lemma imp_foreach_mono[partial_function_mono]:
assumes [partial_function_mono]: "⋀x σ. mono_Heap (λfa. f fa x σ)"
shows "mono_Heap (λx. imp_foreach tsl l c (f x) σ)"
unfolding imp_foreach_def
by pf_mono

(* Inline foreach and nfoldli as fixed-points *)
lemmas [sepref_opt_simps] = imp_foreach_def (*imp_nfoldli_def*)

definition
"IS_TO_SORTED_LIST Ω Rs Rk tsl ≡ (tsl,it_to_sorted_list Ω) ∈ (Rs)⇧k →⇩a list_assn Rk"

lemma IS_TO_SORTED_LISTI:
assumes "(tsl,PR_CONST (it_to_sorted_list Ω)) ∈ (Rs)⇧k →⇩a list_assn Rk"
shows "IS_TO_SORTED_LIST Ω Rs Rk tsl"
using assms unfolding IS_TO_SORTED_LIST_def PR_CONST_def .

assumes "INDEP Rk" "INDEP Rs" "INDEP Rσ"
assumes FR: "P ⟹⇩t Γ * hn_ctxt Rs s' s * hn_ctxt Rσ σ' σ"
assumes STL: "GEN_ALGO tsl (IS_TO_SORTED_LIST ordR Rs Rk)"
assumes c_ref: "⋀σ σ'. hn_refine
(Γ * hn_ctxt Rs s' s * hn_ctxt Rσ σ' σ)
(c σ)
(Γc σ' σ)
bool_assn
(c' σ')"
assumes C_FR:
Γc σ' σ ⟹⇩t Γ * hn_ctxt Rs s' s * hn_ctxt Rσ σ' σ"

assumes f_ref: "⋀x' x σ' σ. hn_refine
(Γ * hn_ctxt Rs s' s * hn_ctxt Rk x' x * hn_ctxt Rσ σ' σ)
(f x σ)
(Γf x' x σ' σ) Rσ
(f' x' σ')"
assumes F_FR: "⋀x' x σ' σ. TERM monadic_FOREACH ⟹ Γf x' x σ' σ ⟹⇩t
Γ * hn_ctxt Rs s' s * hn_ctxt Pfx x' x * hn_ctxt Pfσ σ' σ"

shows "hn_refine
P
(imp_foreach tsl s c f σ)
(Γ * hn_ctxt Rs s' s * hn_invalid Rσ σ' σ)
Rσ
\$s'\$(λ⇩2σ'. c' σ')\$(λ⇩2x' σ'. f' x' σ')\$σ'
)"
proof -
from STL have STL: "(tsl,it_to_sorted_list ordR) ∈ (Rs)⇧k →⇩a list_assn Rk"
unfolding GEN_ALGO_def IS_TO_SORTED_LIST_def by simp

show ?thesis
apply (rule hn_refine_cons_pre[OF FR])
apply weaken_hnr_post
unfolding APP_def PROTECT2_def PR_CONST_def imp_foreach_def
apply (rule hn_refine_guessI)
apply (rule hnr_bind)
apply (rule hn_refine_frame)
apply (rule STL[to_hnr, unfolded APP_def])
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
apply (rule hn_refine_cons_post)
apply (rule c_ref[unfolded APP_def])
apply (rule C_FR)
apply (rule TERMI)
apply weaken_hnr_post
apply (rule hn_refine_cons_post)
apply (rule f_ref[unfolded APP_def])
apply (rule entt_trans[OF F_FR])
apply (rule TERMI)
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)

apply simp
done

qed

assumes "set l ⊆ S"
shows "monadic_nfoldli l c (λx s. ASSERT (x∈S)⪢f x s) s = monadic_nfoldli l c f s"
using assms
apply (induction l arbitrary: s)
apply (auto simp: pw_eq_iff refine_pw_simps)
done

(* Refinement Setup for nfoldli  *)
"nfoldli ≡ λ⇩2s c f σ. SP (nfoldli)\$s\$(λ⇩2x. c\$x)\$(λ⇩2x σ. f\$x\$σ)\$σ"
by (simp_all)

"⋀s c f σ. (nfoldli)\$s\$(λ⇩2x. c x)\$f\$σ ≡
Refine_Basic.bind\$(EVAL\$s)\$(λ⇩2s. Refine_Basic.bind\$(EVAL\$σ)\$(λ⇩2σ.
))"

assumes SS: "set l' ⊆ S"
assumes c_ref: "⋀s s'. hn_refine
(Γ * hn_ctxt Rs s' s)
(c s)
(Γ * hn_ctxt Rs s' s)
bool_assn
(c' s')"
assumes f_ref: "⋀x x' s s'. ⟦x' ∈ S⟧ ⟹ hn_refine
(Γ * hn_ctxt Rl x' x * hn_ctxt Rs s' s)
(f x s)
(Γ * hn_ctxt Rl' x' x * hn_invalid Rs s' s) Rs
(f' x' s')"

assumes merge[sepref_frame_merge_rules]: "⋀x x'. hn_ctxt Rl' x' x ∨⇩A hn_ctxt Rl x' x ⟹⇩t hn_ctxt Rl'' x' x"
notes [sepref_frame_merge_rules] = merge_sat2[OF merge]

shows "hn_refine
(Γ * hn_ctxt (list_assn Rl) l' l * hn_ctxt Rs s' s)
(imp_nfoldli l c f s)
(Γ * hn_ctxt (list_assn Rl'') l' l * hn_invalid Rs s' s) Rs

applyF (induct p≡Rl l' l
arbitrary: s s'
rule: list_assn.induct)

applyF simp
apply (rule hn_refine_cons_post)
apply (rule hn_refine_frame[OF hnr_RETURN_pass])
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
solved

apply (rule hnr_bind)
apply (rule hn_refine_frame[OF c_ref])
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)

apply (rule hnr_If)
apply (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
apply (rule hnr_ASSERT)
apply (rule hnr_bind)
apply (rule hn_refine_frame[OF f_ref])
apply assumption
apply (rule ent_imp_entt)
apply (fr_rot_rhs 1)
apply (fr_rot 2)
apply (rule fr_refl)
apply (rule fr_refl)
apply (rule fr_refl)
apply (rule ent_refl)

applyF (rule hn_refine_frame)
applyS rprems

focus
apply (rule ent_imp_entt)

apply (fr_rot_rhs 1, rule fr_refl)
apply (fr_rot 2, rule fr_refl)
apply (fr_rot 1, rule fr_refl)
apply (rule ent_refl)
solved
solved

apply (rule ent_imp_entt)
apply (rule fr_refl)
apply (rule ent_refl)
solved

apply1 (rule hn_refine_frame[OF hnr_RETURN_pass])
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)

applyS (tactic ‹Sepref_Frame.merge_tac (K (K no_tac)) @{context} 1›)

apply simp
apply (rule ent_imp_entt)
apply solve_entails
apply (rule, sep_auto)
apply (rule, sep_auto)
solved
done

assumes "INDEP Rk" "INDEP Rσ"
assumes FR: "P ⟹⇩t Γ * hn_ctxt (list_assn Rk) s' s * hn_ctxt Rσ σ' σ"
assumes c_ref: "⋀σ σ'. hn_refine
(Γ * hn_ctxt Rσ σ' σ)
(c σ)
(Γc σ' σ)
bool_assn
(c' σ')"
assumes C_FR:
Γc σ' σ ⟹⇩t Γ * hn_ctxt Rσ σ' σ"

assumes f_ref: "⋀x' x σ' σ. ⟦x'∈set s'⟧ ⟹ hn_refine
(Γ * hn_ctxt Rk x' x * hn_ctxt Rσ σ' σ)
(f x σ)
(Γf x' x σ' σ) Rσ
(f' x' σ')"
assumes F_FR: "⋀x' x σ' σ. TERM monadic_nfoldli ⟹ Γf x' x σ' σ ⟹⇩t
Γ * hn_ctxt Rk' x' x * hn_ctxt Pfσ σ' σ"

assumes MERGE: "⋀x x'. hn_ctxt Rk' x' x ∨⇩A hn_ctxt Rk x' x ⟹⇩t hn_ctxt Rk'' x' x"

shows "hn_refine
P
(imp_nfoldli s c f σ)
(Γ * hn_ctxt (list_assn Rk'') s' s * hn_invalid Rσ σ' σ)
Rσ
\$s'\$(λ⇩2σ'. c' σ')\$(λ⇩2x' σ'. f' x' σ')\$σ'
)"
unfolding APP_def PROTECT2_def PR_CONST_def
apply1 (rule hn_refine_cons_pre[OF FR])
apply1 weaken_hnr_post
applyF (rule hn_refine_cons[rotated])
focus
apply (rule hn_refine_cons_post)
applyS (rule c_ref)
apply1 (rule entt_trans[OF C_FR[OF TERMI]])
applyS (rule entt_refl)
solved

apply1 weaken_hnr_post
applyF (rule hn_refine_cons_post)
applyS (rule f_ref; simp)

apply1 (rule entt_trans[OF F_FR[OF TERMI]])
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
solved

apply (rule MERGE)
solved

applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
applyS (tactic ‹Sepref_Frame.frame_tac (K (K no_tac)) @{context} 1›)
solved
done

lemma nfoldli_assert:
assumes "set l ⊆ S"
shows "nfoldli l c (λ x s. ASSERT (x ∈ S) ⪢ f x s) s = nfoldli l c f s"
using assms by (induction l arbitrary: s) (auto simp: pw_eq_iff refine_pw_simps)

lemmas nfoldli_assert' = nfoldli_assert[OF order.refl]

lemma fold_eq_nfoldli:
"RETURN (fold f l s) = nfoldli l (λ_. True) (λx s. RETURN (f x s)) s"
apply (induction l arbitrary: s) apply (auto) done

lemma fold_eq_nfoldli_assert:
"RETURN (fold f l s) = nfoldli l (λ_. True) (λx s. ASSERT (x∈set l) ⪢ RETURN (f x s)) s"

lemma fold_arity[sepref_monadify_arity]: "fold ≡ λ⇩2f l s. SP fold\$(λ⇩2x s. f\$x\$s)\$l\$s" by auto

"EVAL\$(fold\$(λ⇩2x s. f x s)\$l\$s) ≡ (⤜)\$(EVAL\$l)\$(λ⇩2l. (⤜)\$(EVAL\$s)\$(λ⇩2s. nfoldli\$l\$(λ⇩2_. True)\$(λ⇩2x s. EVAL\$(f x s))\$s))"

"EVAL\$(fold\$(λ⇩2x s. f x s)\$l\$s) ≡ (⤜)\$(EVAL\$l)\$(λ⇩2l. (⤜)\$(EVAL\$s)\$(λ⇩2s. nfoldli\$l\$(λ⇩2_. True)\$(λ⇩2x s. PR_CONST (op_ASSERT_bind (x∈set l))\$(EVAL\$(f x s)))\$s))"

text ‹foldli›

lemma foldli_eq_nfoldli:
"RETURN (foldli l c f s) = nfoldli l c (λx s. RETURN (f x s)) s"
by (induction l arbitrary: s) auto

"foldli ≡ λ⇩2s c f σ. SP (foldli)\$s\$(λ⇩2x. c\$x)\$(λ⇩2x σ. f\$x\$σ)\$σ"
by (simp_all)

"EVAL\$(foldli\$l\$c\$(λ⇩2x s. f x s)\$s) ≡
(⤜)\$(EVAL\$l)\$
(λ⇩2l. (⤜)\$(EVAL\$s)\$
(λ⇩2s. nfoldli\$l\$c\$(λ⇩2x s. (EVAL\$(f x s)))\$s))"

subsubsection ‹Deforestation›
lemma nfoldli_filter_deforestation:
"nfoldli (filter P xs) c f s = nfoldli xs c (λx s. if P x then f x s else RETURN s) s"
apply (induction xs arbitrary: s)
by (auto simp: pw_eq_iff refine_pw_simps)

lemma extend_list_of_filtered_set:
assumes [simp, intro!]: "finite S"
and A: "distinct xs'" "set xs' = {x ∈ S. P x}"
obtains xs where "xs' = filter P xs" "distinct xs" "set xs = S"
proof -
obtain xs2 where "{x∈S. ¬P x} = set xs2" "distinct xs2"
using finite_distinct_list[where A="{x∈S. ¬P x}"] by auto
with A have "xs' = filter P (xs'@xs2)" "distinct (xs'@xs2)" "set (xs'@xs2) = S"
by (auto simp: filter_empty_conv)
from that[OF this] show ?thesis .
qed

lemma FOREACHc_filter_deforestation:
assumes FIN[simp, intro!]: "finite S"
shows "(FOREACHc {x∈S. P x} c f s)
= FOREACHc S c (λx s. if P x then f x s else RETURN s) s"
unfolding FOREACHc_def FOREACHci_def FOREACHoci_by_LIST_FOREACH LIST_FOREACH'_eq
LIST_FOREACH'_def it_to_sorted_list_def
subgoal
proof (induction rule: antisym[consumes 0, case_names 1 2])
case 1
then show ?case
apply (rule le_ASSERTI)
apply (rule ASSERT_leI, simp)
apply (rule intro_spec_refine[where R=Id, simplified]; clarsimp)
apply (rule extend_list_of_filtered_set[OF FIN _ sym], assumption, assumption)
subgoal for xs' xs
apply (rule rhs_step_bind_SPEC[where R=Id and x'="xs", simplified])
applyS simp
done
done
next
case 2
then show ?case
apply (rule le_ASSERTI)
apply (rule ASSERT_leI, (simp; fail))
apply (rule intro_spec_refine[where R=Id, simplified]; clarsimp)
subgoal for xs
apply (rule rhs_step_bind_SPEC[where R=Id and x'="filter P xs", simplified])
apply simp
done
done
qed
done

lemma FOREACHc_filter_deforestation2:
assumes [simp]: "distinct xs"
shows "(FOREACHc (set (filter P xs)) c f s)
= FOREACHc (set xs) c (λx s. if P x then f x s else RETURN s) s"
using FOREACHc_filter_deforestation[of "set xs", simplified, folded set_filter]
.

subsection ‹For Loops›

partial_function (heap) imp_for :: "nat ⇒ nat ⇒ ('a ⇒ bool Heap) ⇒ (nat ⇒ 'a ⇒ 'a Heap) ⇒ 'a ⇒ 'a Heap" where
"imp_for i u c f s = (if i ≥ u then return s else do {ctn <- c s; if ctn then f i s ⤜ imp_for (i + 1) u c f else return s})"

declare imp_for.simps[code]

lemma [simp]:
"i ≥ u ⟹ imp_for i u c f s = return s"
"i < u ⟹ imp_for i u c f s = do {ctn <- c s; if ctn then f i s ⤜ imp_for (i + 1) u c f else return s}"
by (auto simp: imp_for.simps)

lemma imp_nfoldli_deforest[sepref_opt_simps]:
"imp_nfoldli [l..<u] c = imp_for l u c"
apply (intro ext)
subgoal for f s
apply (induction "u - l" arbitrary: l u s)
apply (fo_rule arg_cong)
by (auto cong: if_cong)
done

partial_function (heap) imp_for' :: "nat ⇒ nat ⇒ (nat ⇒ 'a ⇒ 'a Heap) ⇒ 'a ⇒ 'a Heap" where
"imp_for' i u f s = (if i ≥ u then return s else f i s ⤜ imp_for' (i + 1) u f)"

declare imp_for'.simps[code]

lemma [simp]:
"i ≥ u ⟹ imp_for' i u f s = return s"
"i < u ⟹ imp_for' i u f s = f i s ⤜ imp_for' (i + 1) u f"
by (auto simp: imp_for'.simps)

lemma imp_for_imp_for'[sepref_opt_simps]:
"imp_for i u (λ _. return True) = imp_for' i u"
apply (intro ext)
subgoal for f s
apply (induction "u - i" arbitrary: i u s)
apply (simp; fail)
apply simp
apply (fo_rule arg_cong)
by auto
done

partial_function (heap) imp_for_down :: "nat ⇒ nat ⇒ ('a ⇒ bool Heap) ⇒ (nat ⇒ 'a ⇒ 'a Heap) ⇒ 'a ⇒ 'a Heap" where
"imp_for_down l i c f s = do {
let i = i - 1;
ctn ← c s;
if ctn then do {
s ← f i s;
if i>l then imp_for_down l i c f s else return s
} else return s
}"

declare imp_for_down.simps[code]

lemma imp_nfoldli_deforest_down[sepref_opt_simps]:
"imp_nfoldli (rev [l..<u]) c =
(λf s. if u≤l then return s else imp_for_down l u c f s)"
proof (intro ext)
fix f s
show "imp_nfoldli (rev [l..<u]) c f s =
(if l ≥ u then return s else imp_for_down l u c f s)"
proof cases
assume "l≥u" thus ?thesis by auto
next
assume "¬(l≥u)" hence "l<u" by auto
thus ?thesis
apply simp
proof (induction "u - l" arbitrary: u s)
case 0 thus ?case by auto
next
case (Suc u')
from Suc.prems Suc.hyps(2) have [simp]: "rev [l..<u] = (u-1)#rev [l..<u-1]"
apply simp
apply (subst upt_Suc_append[symmetric])
apply auto
done
show ?case using Suc.hyps(1)[of "u-1"] Suc.hyps(2) Suc.prems
apply (subst imp_for_down.simps)
apply (cases "l < u - Suc 0")
apply (auto simp: Let_def cong: if_cong)
done
qed
qed
qed

context begin

private fun imp_for_down_induction_scheme :: "nat ⇒ nat ⇒ unit" where
"imp_for_down_induction_scheme l i = (
let i=i-1 in
if i>l then
imp_for_down_induction_scheme l i
else ()
)"

partial_function (heap) imp_for_down' :: "nat ⇒ nat ⇒ (nat ⇒ 'a ⇒ 'a Heap) ⇒ 'a ⇒ 'a Heap" where
"imp_for_down' l i f s = do {
let i = i - 1;
s ← f i s;
if i>l then imp_for_down' l i f s else return s
}"
declare imp_for_down'.simps[code]

lemma imp_for_down_no_cond[sepref_opt_simps]:
"imp_for_down l u (λ_. return True) = imp_for_down' l u"
apply (induction l u rule: imp_for_down_induction_scheme.induct)
apply (intro ext)
apply (subst imp_for_down.simps)
apply (subst imp_for_down'.simps)
apply (simp cong: if_cong)
done

end

(* TODO: Move. Add rule for imp_for! *)
lemma imp_for'_rule:
assumes LESS: "l≤u"
assumes PRE: "P ⟹⇩A I l s"
assumes STEP: "⋀i s. ⟦ l≤i; i<u ⟧ ⟹ <I i s> f i s <I (i+1)>"
shows "<P> imp_for' l u f s <I u>"
apply (rule Hoare_Triple.cons_pre_rule[OF PRE])
using LESS
proof (induction arbitrary: s rule: inc_induct)
case base thus ?case by sep_auto
next
case (step k)
show ?case using step.hyps
by (sep_auto heap: STEP step.IH)
qed

text ‹This lemma is used to manually convert a fold to a loop over indices. ›
lemma fold_idx_conv: "fold f l s = fold (λi. f (l!i)) [0..<length l] s"
proof (induction l arbitrary: s rule: rev_induct)
case Nil thus ?case by simp
next
case (snoc x l)
{ fix x s
have "fold (λa. f ((l @ [x]) ! a)) [0..<length l] s = fold (λa. f (l ! a)) [0..<length l] s"
by (rule fold_cong) (simp_all add: nth_append)
}
with snoc show ?case by simp
qed

end

```