```section ‹\isaheader{Refine-Monadci setup for ICF}›
imports ICF_Impl
begin
text ‹
This theory sets up some lemmas that automate refinement proofs using
the Isabelle Collection Framework (ICF).
›

subsection ‹General Setup›

lemma (in set) drh[refine_dref_RELATES]:
"RELATES (build_rel α invar)" by (simp add: RELATES_def)
lemma (in map) drh[refine_dref_RELATES]:
"RELATES (build_rel α invar)" by (simp add: RELATES_def)

lemma (in uprio) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)"
lemma (in prio) drh[refine_dref_RELATES]: "RELATES (build_rel α invar)"

lemmas (in StdSet) [refine_hsimp] = correct
lemmas (in StdMap) [refine_hsimp] = correct

lemma (in set_sel') pick_ref[refine_hsimp]:
"⟦ invar s; α s ≠ {}⟧ ⟹ the (sel' s (λ_. True)) ∈ α s"
by (auto elim!: sel'E)

(*text {* Wrapper to prevent higher-order unification problems *}
definition [simp, code_unfold]: "IT_tag x ≡ x"

lemma (in set_iteratei) it_is_iterator[refine_transfer]:
"invar s ⟹ set_iterator (IT_tag iteratei s) (α s)"
unfolding IT_tag_def by (rule iteratei_rule)

lemma (in map_iteratei) it_is_iterator[refine_transfer]:
"invar m ⟹ set_iterator (IT_tag iteratei m) (map_to_set (α m))"
unfolding IT_tag_def by (rule iteratei_rule)
*)

text ‹
This definition is handy to be used on the abstract level.
›
definition "prio_pop_min q ≡ do {
ASSERT (dom q ≠ {});
SPEC (λ(e,w,q').
q'=q(e:=None) ∧
q e = Some w ∧
(∀ e' w'. q e' = Some w' ⟶ w≤w')
)
}"

lemma (in uprio_pop) prio_pop_min_refine[refine]:
"(q,q')∈build_rel α invar ⟹ RETURN (pop q)
≤ ⇓ (⟨Id,⟨Id,br α invar⟩prod_rel⟩prod_rel) (prio_pop_min q')"
unfolding prio_pop_min_def
apply refine_rcg
apply (clarsimp simp: prod_rel_def br_def)
apply (erule (1) popE)
apply (rule pw_leI)
apply (auto simp: refine_pw_simps intro: ranI)
done

subsection "Iterators"
lemmas (in poly_map_iteratei) [refine_transfer] = iteratei_correct
lemmas (in poly_map_iterateoi) [refine_transfer] = iterateoi_correct
lemmas (in map_no_invar) [refine_transfer] = invar

lemmas (in poly_set_iteratei) [refine_transfer] = iteratei_correct
lemmas (in poly_set_iterateoi) [refine_transfer] = iterateoi_correct
lemmas (in set_no_invar) [refine_transfer] = invar

lemma (in poly_set_iteratei) dres_ne_bot_iterate[refine_transfer]:
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
unfolding iteratei_def it_to_list_def it_to_it_def
apply (rule dres_foldli_ne_bot)
lemma (in poly_set_iterateoi) dres_ne_bot_iterateo[refine_transfer]:
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "iterateoi r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
unfolding iterateoi_def it_to_list_def it_to_it_def
apply (rule dres_foldli_ne_bot)

lemma (in poly_map_iteratei) dres_ne_bot_map_iterate[refine_transfer]:
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
unfolding iteratei_def it_to_list_def it_to_it_def
apply (rule dres_foldli_ne_bot)
lemma (in poly_set_iterateoi) dres_ne_bot_map_iterateo[refine_transfer]:
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "iterateoi r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
unfolding iterateoi_def it_to_list_def it_to_it_def
apply (rule dres_foldli_ne_bot)

subsection "Alternative FOREACH-transfer"
text ‹Required for manual refinements›
lemma transfer_FOREACHoci_plain[refine_transfer]:
assumes A: "set_iterator_genord iterate s ordR"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate c fi σ) ≤ FOREACHoci ordR I s c f σ"
proof -
from A obtain l where [simp]:
"distinct l"
"s = set l"
"sorted_wrt ordR l"
"iterate = foldli l"
unfolding set_iterator_genord_def by blast

have "RETURN (foldli l c fi σ) ≤ nfoldli l c f σ"
by (rule nfoldli_transfer_plain[OF R])
also have "… = do { l ← RETURN l; nfoldli l c f σ }" by simp
also have "… ≤ FOREACHoci ordR I s c f σ"
apply (rule refine_IdD)
unfolding FOREACHoci_def
apply refine_rcg
apply simp
apply simp
apply (rule nfoldli_while)
done
finally show ?thesis by simp
qed

lemma transfer_FOREACHoi_plain[refine_transfer]:
assumes A: "set_iterator_genord iterate s ordR"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACHoi ordR I s f σ"
using assms unfolding FOREACHoi_def by (rule transfer_FOREACHoci_plain)

lemma transfer_FOREACHci_plain[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate c fi σ) ≤ FOREACHci I s c f σ"
using assms unfolding FOREACHci_def set_iterator_def
by (rule transfer_FOREACHoci_plain)

lemma transfer_FOREACHi_plain[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACHi I s f σ"
using assms unfolding FOREACHi_def
by (rule transfer_FOREACHci_plain)

lemma transfer_FOREACHc_plain[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate c fi σ) ≤ FOREACHc s c f σ"
using assms unfolding FOREACHc_def
by (rule transfer_FOREACHci_plain)

lemma transfer_FOREACH_plain[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. RETURN (fi x σ) ≤ f x σ"
shows "RETURN (iterate (λ_. True) fi σ) ≤ FOREACH s f σ"
using assms unfolding FOREACH_def
by (rule transfer_FOREACHc_plain)

abbreviation "dres_it iterate c (fi::'a ⇒ 'b ⇒ 'b dres) σ ≡
iterate (case_dres False False c) (λx s. s⤜fi x) (dRETURN σ)"

lemma transfer_FOREACHoci_nres[refine_transfer]:
assumes A: "set_iterator_genord iterate s ordR"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHoci ordR I s c f σ"
proof -
from A obtain l where [simp]:
"distinct l"
"s = set l"
"sorted_wrt ordR l"
"iterate = foldli l"
unfolding set_iterator_genord_def by blast

have "nres_of (dres_it (foldli l) c fi σ) ≤ nfoldli l c f σ"
by (rule nfoldli_transfer_dres[OF R])
also have "… = do { l ← RETURN l; nfoldli l c f σ }" by simp
also have "… ≤ FOREACHoci ordR I s c f σ"
apply (rule refine_IdD)
unfolding FOREACHoci_def
apply refine_rcg
apply simp
apply simp
apply (rule nfoldli_while)
done
finally show ?thesis by simp
qed

lemma transfer_FOREACHoi_nres[refine_transfer]:
assumes A: "set_iterator_genord iterate s ordR"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACHoi ordR I s f σ"
using assms unfolding FOREACHoi_def by (rule transfer_FOREACHoci_nres)

lemma transfer_FOREACHci_nres[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHci I s c f σ"
using assms unfolding FOREACHci_def set_iterator_def
by (rule transfer_FOREACHoci_nres)

lemma transfer_FOREACHi_nres[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACHi I s f σ"
using assms unfolding FOREACHi_def
by (rule transfer_FOREACHci_nres)

lemma transfer_FOREACHc_nres[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate c fi σ) ≤ FOREACHc s c f σ"
using assms unfolding FOREACHc_def
by (rule transfer_FOREACHci_nres)

lemma transfer_FOREACH_nres[refine_transfer]:
assumes A: "set_iterator iterate s"
assumes R: "⋀x σ. nres_of (fi x σ) ≤ f x σ"
shows "nres_of (dres_it iterate (λ_. True) fi σ) ≤ FOREACH s f σ"
using assms unfolding FOREACH_def
by (rule transfer_FOREACHc_nres)

(*
lemma dres_ne_bot_iterate[refine_transfer]:
assumes B: "set_iterator (IT_tag it r) S"
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "IT_tag it r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
apply (rule_tac I="λ_ s. s≠dSUCCEED" in set_iterator_rule_P[OF B])
apply (rule dres_ne_bot_basic A | assumption)+
done
*)

(*
subsubsection {* Monotonicity for Iterators *}

lemma it_mono_aux:
assumes COND: "⋀σ σ'. σ≤σ' ⟹ c σ ≠ c σ' ⟹ σ=bot ∨ σ'=top "
assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
assumes B: "σ≤σ'"
assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
shows "foldli l c f σ ≤ foldli l c f' σ'"
proof -
{ fix l
have "foldli l c f bot = bot" by (induct l) (auto simp: STRICT)
} note [simp] = this
{ fix l
have "foldli l c f' top = top" by (induct l) (auto simp: STRICT)
} note [simp] = this

show ?thesis
using B
apply (induct l arbitrary: σ σ')
apply simp_all
apply (metis assms foldli_not_cond)
done
qed

lemma it_mono_aux_dres':
assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
shows "foldli l (case_dres True True c) f σ
≤ foldli l (case_dres True True c) f' σ"
apply (rule it_mono_aux)
apply (simp_all split: dres.split_asm add: STRICT A)
done

lemma it_mono_aux_dres:
assumes A: "⋀a x. f a x ≤ f' a x"
shows "foldli l (case_dres True True c) (λx s. dbind s (f x)) σ
≤ foldli l (case_dres True True c) (λx s. dbind s (f' x)) σ"
apply (rule it_mono_aux_dres')
apply (simp_all)
apply (rule dbind_mono)
done

lemma iteratei_mono':
assumes L: "set_iteratei α invar it"
assumes STRICT: "⋀x. f x bot = bot" "⋀x. f' x top = top"
assumes A: "⋀a x x'. x≤x' ⟹ f a x ≤ f' a x'"
assumes I: "invar s"
shows "IT_tag it s (case_dres True True c) f σ
≤ IT_tag it s (case_dres True True c) f' σ"
proof -
from set_iteratei.iteratei_rule[OF L, OF I, unfolded set_iterator_foldli_conv]
obtain l0 where l0_props: "distinct l0" "α s = set l0" "it s = foldli l0" by blast

from it_mono_aux_dres' [of f f' l0 c σ]
show ?thesis
unfolding IT_tag_def l0_props(3)
qed

lemma iteratei_mono:
assumes L: "set_iteratei α invar it"
assumes A: "⋀a x. f a x ≤ f' a x"
assumes I: "invar s"
shows "IT_tag it s (case_dres True True c) (λx s. dbind s (f x)) σ
≤ IT_tag it s (case_dres True True c) (λx s. dbind s (f' x)) σ"
proof -
from set_iteratei.iteratei_rule[OF L, OF I, unfolded set_iterator_foldli_conv]
obtain l0 where l0_props: "distinct l0" "α s = set l0" "it s = foldli l0" by blast

from it_mono_aux_dres [of f f' l0 c σ]
show ?thesis
unfolding IT_tag_def l0_props(3)
qed

lemmas [refine_mono] = iteratei_mono[OF ls_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF lsi_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF rs_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ahs_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ias_iteratei_impl]
lemmas [refine_mono] = iteratei_mono[OF ts_iteratei_impl]
*)
(* Do not require the invariant for lsi_iteratei.

This is kind of a hack -- the real fix comes with the new Collection/Refinement-Framework. *)
(*
lemma dres_ne_bot_iterate_lsi[refine_transfer]:
fixes s :: "'a"
assumes A: "⋀x s. f x s ≠ dSUCCEED"
shows "IT_tag lsi_iteratei r c (λx s. dbind s (f x)) (dRETURN s) ≠ dSUCCEED"
proof -
{
fix l and s :: "'a dres"
assume "s≠dSUCCEED"
hence "foldli l c (λx s. s⤜f x) s ≠ dSUCCEED"
apply (induct l arbitrary: s)
using A
apply simp_all
apply (intro impI)
apply (metis dres_ne_bot_basic)
done
} note R=this
with A show ?thesis
unfolding lsi_iteratei_def
by simp
qed

lemma iteratei_mono_lsi[refine_mono]:
assumes A: "⋀a x. f a x ≤ f' a x"
shows "IT_tag lsi_iteratei s (case_dres True True c) (λx s. dbind s (f x)) σ
≤ IT_tag lsi_iteratei s (case_dres True True c) (λx s. dbind s (f' x)) σ"
proof -
from it_mono_aux_dres [of f f' s c σ]
show ?thesis
unfolding IT_tag_def lsi_iteratei_def