# Theory Refine_Folds

```theory Refine_Folds
imports
Autoref_Misc
begin

section ‹Fold binary predicate over finite nonempty set›

definition "FOLD_bin_ne b X = do {
ASSERT (X ≠ {});
x ← SPEC (λx. x ∈ X);
let X = X - {x};
FOREACH X (λx r. RETURN (b x r)) x
}"

lemma Fold_bin_spec:
assumes 1: "X ≠ {}"
assumes 2: "finite X"
assumes refl: "⋀x. c x x"
assumes idem1: "⋀x y. c (b x y) x"
assumes idem2: "⋀x y. c (b x y) y"
assumes trans: "⋀x y z. c x y ⟹ c y z ⟹ c x z"
shows "FOLD_bin_ne b X ≤ SPEC (λr. ∀x ∈ X. c r x)"
using 1 2
unfolding FOLD_bin_ne_def
apply refine_vcg
subgoal for x
apply (rule FOREACH_rule[where I = "λit r. (∀x ∈ (insert x (X - {x} - it)). c r x)"])
subgoal by simp
subgoal
using idem1 idem2 trans
by simp fast
subgoal by simp
done
done

subsection ‹@{term Inf}/@{term Sup}/@{term Max}/@{term Min}›

lemma inf_Inf_absorb[simp]:
fixes x::"'a::conditionally_complete_lattice"
shows "x ∈ X ⟹ finite X ⟹ inf x (Inf X) = Inf X"
by (subst cInf_insert[symmetric]) (auto simp: insert_absorb)

lemma sup_Sup_absorb[simp]:
fixes x::"'a::conditionally_complete_lattice"
shows "x ∈ X ⟹ finite X ⟹ sup x (Sup X) = Sup X"
by (subst cSup_insert[symmetric]) (auto simp: insert_absorb)

definition "Inf_ne X = FOLD_bin_ne inf X"
definition "Sup_ne X = FOLD_bin_ne sup X"
definition "Min_ne X = FOLD_bin_ne min X"
definition "Max_ne X = FOLD_bin_ne max X"
lemma [autoref_itype]:
"Inf_ne ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_nres"
"Sup_ne ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_nres"
"Min_ne ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_nres"
"Max_ne ::⇩i ⟨I⟩⇩ii_set →⇩i ⟨I⟩⇩ii_nres"
by simp_all

lemma Inf_ne_spec:
fixes X::"'a::conditionally_complete_lattice set"
assumes "X ≠ {}"
assumes "finite X"
shows "Inf_ne X ≤ SPEC (λr. r = Inf X)"
using assms
unfolding Inf_ne_def FOLD_bin_ne_def
apply refine_vcg
apply (rule_tac I = "λit r. r = (Inf (insert x (X - {x} - it)))" in FOREACH_rule)
apply (auto simp: assms it_step_insert_iff cInf_insert_If ac_simps)
done

lemma Sup_ne_spec:
fixes X::"'a::conditionally_complete_lattice set"
assumes "X ≠ {}"
assumes "finite X"
shows "Sup_ne X ≤ SPEC (λr. r = Sup X)"
using assms
unfolding Sup_ne_def  FOLD_bin_ne_def
apply (refine_rcg refine_vcg)
apply (rule_tac I = "λit r. r = (Sup (insert x (X - {x} - it)))" in FOREACH_rule)
apply (auto simp: assms it_step_insert_iff cSup_insert_If ac_simps)
done

lemma Min_ne_spec:
fixes X::"'a::linorder set"
assumes "X ≠ {}"
assumes "finite X"
shows "Min_ne X ≤ SPEC (λr. r = Min X)"
using assms
unfolding Min_ne_def  FOLD_bin_ne_def
apply refine_vcg
apply (rule_tac I = "λit r. r = (Min (insert x (X - {x} - it)))" in FOREACH_rule)
apply (auto simp: assms it_step_insert_iff Min.insert_remove ac_simps)
done

lemma Max_ne_spec:
fixes X::"'a::linorder set"
assumes "X ≠ {}"
assumes "finite X"
shows "Max_ne X ≤ SPEC (λr. r = Max X)"
using assms
unfolding Max_ne_def  FOLD_bin_ne_def
apply refine_vcg
apply (rule_tac I = "λit r. r = (Max (insert x (X - {x} - it)))" in FOREACH_rule)
apply (auto simp: assms it_step_insert_iff Max.insert_remove ac_simps Max.in_idem)
done

subsection ‹Implementations›
context includes autoref_syntax begin

schematic_goal FOLD_bin_ne_impl:
assumes [autoref_rules(overloaded)]: "(del_impl,op_set_delete) ∈ R → ⟨R⟩C → ⟨R⟩C"
assumes [autoref_rules(overloaded)]: "(pick_impl,op_set_pick) ∈ ⟨R⟩C → ⟨R⟩nres_rel"
assumes [autoref_ga_rules]: "is_set_to_list R C tsl"
assumes[unfolded comps, autoref_rules(overloaded)]: "(bi, b) ∈ R → R → R"
assumes[autoref_rules]: "(Xi, X) ∈ ⟨R⟩C"
shows "(?f, (OP FOLD_bin_ne ::: ((R → R → R) → ⟨R⟩C → ⟨R⟩nres_rel)) \$ b \$ X) ∈ ⟨R⟩nres_rel"
unfolding FOLD_bin_ne_def[abs_def] autoref_tag_defs comps
concrete_definition FOLD_bin_ne_impl uses FOLD_bin_ne_impl
lemmas [autoref_rules(overloaded)] = FOLD_bin_ne_impl.refine [OF GEN_OP_D GEN_OP_D SIDE_GEN_ALGO_D]

schematic_goal Inf_ne_impl:
assumes [autoref_rules(overloaded)]: "(del_impl,op_set_delete) ∈ R → ⟨R⟩C → ⟨R⟩C"
assumes [autoref_rules(overloaded)]: "(pick_impl,op_set_pick) ∈ ⟨R⟩C → ⟨R⟩nres_rel"
assumes [autoref_ga_rules]: "is_set_to_list R C tsl"
assumes[autoref_rules(overloaded)]: "(infi, inf) ∈ R → R → R"
assumes[autoref_rules]: "(Xi, X) ∈ ⟨R⟩C"
shows "(?f, (OP Inf_ne ::: (⟨R⟩C → ⟨R⟩nres_rel)) \$ X) ∈ ⟨R⟩nres_rel"
unfolding Inf_ne_def[abs_def] FOLD_bin_ne_def[abs_def] autoref_tag_defs
concrete_definition Inf_ne_impl uses Inf_ne_impl
lemmas [autoref_rules(overloaded)] = Inf_ne_impl.refine [OF GEN_OP_D GEN_OP_D SIDE_GEN_ALGO_D]

schematic_goal Sup_ne_impl:
assumes [autoref_rules(overloaded)]: "(del_impl,op_set_delete) ∈ R → ⟨R⟩C → ⟨R⟩C"
assumes [autoref_rules(overloaded)]: "(pick_impl,op_set_pick) ∈ ⟨R⟩C → ⟨R⟩nres_rel"
assumes [autoref_ga_rules]: "is_set_to_list R C tsl"
assumes[autoref_rules(overloaded)]: "(supi, sup) ∈ R → R → R"
assumes[autoref_rules]: "(Xi, X) ∈ ⟨R⟩C"
shows "(?f, (OP Sup_ne ::: (⟨R⟩C → ⟨R⟩nres_rel)) \$ X) ∈ ⟨R⟩nres_rel"
unfolding Sup_ne_def[abs_def] FOLD_bin_ne_def[abs_def] autoref_tag_defs
concrete_definition Sup_ne_impl uses Sup_ne_impl
lemmas [autoref_rules(overloaded)] = Sup_ne_impl.refine [OF GEN_OP_D GEN_OP_D SIDE_GEN_ALGO_D]

schematic_goal Min_ne_impl:
assumes [autoref_rules(overloaded)]: "(del_impl,op_set_delete) ∈ R → ⟨R⟩C → ⟨R⟩C"
assumes [autoref_rules(overloaded)]: "(pick_impl,op_set_pick) ∈ ⟨R⟩C → ⟨R⟩nres_rel"
assumes [autoref_ga_rules]: "is_set_to_list R C tsl"
assumes[autoref_rules(overloaded)]: "(mini, min) ∈ R → R → R"
assumes[autoref_rules]: "(Xi, X) ∈ ⟨R⟩C"
shows "(?f, (OP Min_ne ::: (⟨R⟩C → ⟨R⟩nres_rel)) \$ X) ∈ ⟨R⟩nres_rel"
unfolding Min_ne_def[abs_def] FOLD_bin_ne_def[abs_def] autoref_tag_defs
concrete_definition Min_ne_impl uses Min_ne_impl
lemmas [autoref_rules(overloaded)] = Min_ne_impl.refine [OF GEN_OP_D GEN_OP_D SIDE_GEN_ALGO_D]

schematic_goal Max_ne_impl:
assumes [autoref_rules(overloaded)]: "(del_impl,op_set_delete) ∈ R → ⟨R⟩C → ⟨R⟩C"
assumes [autoref_rules(overloaded)]: "(pick_impl,op_set_pick) ∈ ⟨R⟩C → ⟨R⟩nres_rel"
assumes [autoref_ga_rules]: "is_set_to_list R C tsl"
assumes[autoref_rules(overloaded)]: "(maxi, max) ∈ R → R → R"
assumes[autoref_rules]: "(Xi, X) ∈ ⟨R⟩C"
shows "(?f, (OP Max_ne ::: (⟨R⟩C → ⟨R⟩nres_rel)) \$ X) ∈ ⟨R⟩nres_rel"
unfolding Max_ne_def[abs_def] FOLD_bin_ne_def[abs_def] autoref_tag_defs