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 by (simp add: refl)
    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
  by (autoref_monadic (plain))
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]
  ― ‹TODO: really? overloaded here?›

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
  by (autoref_monadic (plain))
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
  by (autoref_monadic (plain))
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
  by (autoref_monadic (plain))
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
  by (autoref_monadic (plain))
concrete_definition Max_ne_impl uses Max_ne_impl
lemmas [autoref_rules(overloaded)] = Max_ne_impl.refine [OF GEN_OP_D GEN_OP_D SIDE_GEN_ALGO_D]

end

end