Theory Refine_Imperative_HOL.Sepref_Foreach
section ‹Setup for Foreach Combinator›
theory Sepref_Foreach
imports Sepref_HOL_Bindings "Lib/Pf_Add" "HOL-Library.Rewrite"
begin
subsection "Foreach Loops"
subsubsection "Monadic Version of Foreach"
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 σ
}"
lemma FOREACH_oci_to_monadic:
"FOREACHoci R Φ S c f σ0 = monadic_FOREACH R Φ S (λσ. RETURN (c σ)) f σ0"
unfolding FOREACHoci_def monadic_FOREACH_def WHILEIT_def WHILEI_body_def
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)"
lemma monadic_nfoldli_eq:
"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 monadic_nfoldli_def)
apply (subst RECT_unfold)
apply (tagged_solver)
apply (subst monadic_nfoldli_def[symmetric])
apply simp
done
lemma monadic_nfoldli_simp[simp]:
"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
}"
apply (subst monadic_nfoldli_eq, simp)
apply (subst monadic_nfoldli_eq, simp)
done
lemma nfoldli_to_monadic:
"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
lemma monadic_nfoldli_rec:
"monadic_nfoldli x' c f σ
≤⇓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 (subst monadic_nfoldli_simp)
apply (simp del: conc_Id cong: if_cong)
apply refine_rcg
apply simp
apply (clarsimp simp add: FOREACH_body_def)
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
apply (simp add: br_def)
done
lemma monadic_nfoldli_arities[sepref_monadify_arity]:
"monadic_nfoldli ≡ λ⇩2s c f σ. SP (monadic_nfoldli)$s$(λ⇩2x. c$x)$(λ⇩2x σ. f$x$σ)$σ"
by (simp_all)
lemma monadic_nfoldli_comb[sepref_monadify_comb]:
"⋀s c f σ. (monadic_nfoldli)$s$c$f$σ ≡
Refine_Basic.bind$(EVAL$s)$(λ⇩2s. Refine_Basic.bind$(EVAL$σ)$(λ⇩2σ.
SP (monadic_nfoldli)$s$c$f$σ
))"
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
lemma monadic_nfoldli_refine[refine]:
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]
unfolding monadic_nfoldli_def
apply (refine_rcg bind_refine')
apply refine_dref_type
apply (vc_solve simp: list_rel_congD[OF L])
done
lemma monadic_FOREACH_itsl:
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)
unfolding monadic_FOREACH_def it_to_sorted_list_def
apply (refine_rcg)
apply simp
apply (rule monadic_nfoldli_rec[simplified])
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)"
by (simp_all add:
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›
lemma FOREACH_arities[sepref_monadify_arity]:
"PR_CONST (FOREACHoci R I) ≡ λ⇩2s c f σ. SP (PR_CONST (FOREACHoci R I))$s$(λ⇩2x. c$x)$(λ⇩2x σ. f$x$σ)$σ"
by (simp_all)
lemma FOREACHoci_comb[sepref_monadify_comb]:
"⋀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$σ
))"
by (simp_all add: FOREACH_oci_to_monadic)
subsubsection "Imperative Version of nfoldli"
text ‹We define an imperative version of ‹nfoldli›. It is the
equivalent to the monadic version in the nres-monad›
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)"
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
lemma monadic_nfoldli_refine_aux:
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
(monadic_nfoldli l' c' f' s')"
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
apply1 (simp only: imp_nfoldli_simps monadic_nfoldli_simp)
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 (simp add: assn_assoc)
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 (simp add: assn_assoc)
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›)
apply1 (simp add: assn_assoc)
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 (simp add: hn_ctxt_def invalid_assn_def)
applyS (rule, sep_auto)
solved
done
lemma hn_monadic_nfoldli:
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
(monadic_nfoldli$l'$c'$f'$s')
"
apply (rule hn_refine_cons_pre[OF FR])
unfolding APP_def
apply (rule monadic_nfoldli_refine_aux)
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
lemmas [sepref_opt_simps] = imp_foreach_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 .
lemma hn_monadic_FOREACH[sepref_comb_rules]:
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:
"⋀σ' σ. TERM monadic_FOREACH ⟹
Γ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σ
((PR_CONST (monadic_FOREACH ordR I))
$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_ref[OF monadic_FOREACH_itsl])
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 (rule hn_monadic_nfoldli[unfolded APP_def])
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
lemma monadic_nfoldli_assert_aux:
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
lemmas monadic_nfoldli_assert = monadic_nfoldli_assert_aux[OF order_refl]
lemma nfoldli_arities[sepref_monadify_arity]:
"nfoldli ≡ λ⇩2s c f σ. SP (nfoldli)$s$(λ⇩2x. c$x)$(λ⇩2x σ. f$x$σ)$σ"
by (simp_all)
lemma nfoldli_comb[sepref_monadify_comb]:
"⋀s c f σ. (nfoldli)$s$(λ⇩2x. c x)$f$σ ≡
Refine_Basic.bind$(EVAL$s)$(λ⇩2s. Refine_Basic.bind$(EVAL$σ)$(λ⇩2σ.
SP (monadic_nfoldli)$s$(λ⇩2x. (EVAL$(c x)))$f$σ
))"
by (simp_all add: nfoldli_to_monadic)
lemma monadic_nfoldli_refine_aux':
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
(monadic_nfoldli l' c' f' s')"
apply1 (subst monadic_nfoldli_assert_aux[OF SS,symmetric])
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)
solved
apply (simp only: imp_nfoldli_simps monadic_nfoldli_simp)
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 (simp only: nres_monad_laws)
apply (rule hnr_ASSERT)
apply (rule hnr_bind)
apply (rule hn_refine_frame[OF f_ref])
apply assumption
apply (simp add: assn_aci)
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 (simp add: assn_aci)
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
focus (simp add: assn_assoc)
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›)
apply1 (simp add: assn_assoc)
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
lemma hn_monadic_nfoldli_rl'[sepref_comb_rules]:
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:
"⋀σ' σ. TERM monadic_nfoldli ⟹
Γ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σ
((monadic_nfoldli)
$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])
applyF (rule monadic_nfoldli_refine_aux'[OF order_refl])
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"
by (simp add: nfoldli_assert' fold_eq_nfoldli)
lemma fold_arity[sepref_monadify_arity]: "fold ≡ λ⇩2f l s. SP fold$(λ⇩2x s. f$x$s)$l$s" by auto
lemma monadify_plain_fold[sepref_monadify_comb]:
"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))"
by (simp add: fold_eq_nfoldli)
lemma monadify_plain_fold_old_rl:
"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))"
by (simp add: fold_eq_nfoldli_assert)
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
lemma foldli_arities[sepref_monadify_arity]:
"foldli ≡ λ⇩2s c f σ. SP (foldli)$s$(λ⇩2x. c$x)$(λ⇩2x σ. f$x$σ)$σ"
by (simp_all)
lemma monadify_plain_foldli[sepref_monadify_comb]:
"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))"
by (simp add: foldli_eq_nfoldli)
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
applyS (simp add: nfoldli_filter_deforestation)
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
apply (simp add: nfoldli_filter_deforestation)
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 (simp add: upt_conv_Cons; fail)
apply (simp add: upt_conv_Cons)
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
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