Theory Refine_Iterator

theory Refine_Iterator
  imports Refine_Monadic.Refine_Monadic
begin

subsection ‹Misc›

abbreviation FORCE_id where
  "FORCE_id ≡ PREFER REL_FORCE_ID"

lemma PREFER_id:
  "PREFER_id R ⟹ (x, x) ∈ R" by simp

lemma FORCE_id:
  "FORCE_id R ⟹ (x, x) ∈ R" by simp

subsection ‹Iterators›

text ‹Iterators enumerate a set, allowing duplicate elements. We define a corresponding relator.›

definition it_set_rel_def': "it_set_rel R ≡ ⟨R⟩list_rel O br set (λ_. True)"

lemma it_set_rel_def [refine_rel_defs]:
  "⟨R⟩it_set_rel ≡ ⟨R⟩list_rel O br set (λ_. True)"
  by (auto simp: relAPP_def it_set_rel_def')

lemma list_set_rel_sub_it_set_rel:
  "⟨R⟩list_set_rel ⊆ ⟨R⟩it_set_rel"
  by (auto simp: br_def list_set_rel_def it_set_rel_def)

lemmas list_set_rel_imp_it_set_rel = subsetD[OF list_set_rel_sub_it_set_rel]

definition op_set_to_it where
  "op_set_to_it X = SPEC (λxs. set xs = X)"

lemma op_set_to_it_ref [autoref_rules]:
  shows "(RETURN, op_set_to_it) ∈ ⟨R⟩it_set_rel → ⟨⟨R⟩list_rel⟩nres_rel"
  by (force simp: op_set_to_it_def nres_rel_def it_set_rel_def br_def intro!: RETURN_SPEC_refine)

lemma it_set_rel_Id_implies_finite [simp]:
  shows "(X', X) ∈ ⟨Id⟩it_set_rel ⟹ finite X"
  by (auto simp: it_set_rel_def br_def)

(*
lemma list_set_rel_Id_implies_finite [simp]:
  shows "(X', X) ∈ ⟨Id⟩list_set_rel ⟹ finite X"
  by (auto simp: list_set_rel_def br_def)

lemma list_set_rel_Id_implies_set_eq [simp]:
  shows "(X', X) ∈ ⟨Id⟩list_set_rel ⟹ set X' = X"
  by (auto simp: list_set_rel_def br_def fun_rel_def)

lemma op_set_to_it_ref [autoref_rules]:
  shows "(RETURN, op_set_to_it) ∈ ⟨R⟩list_set_rel → ⟨⟨R⟩list_rel⟩nres_rel"
  by (force simp: op_set_to_it_def nres_rel_def list_set_rel_def intro!: RETURN_SPEC_refine)
*)

lemma union_it_set_rel:
  assumes "(A', A) ∈ ⟨R⟩it_set_rel"
  assumes "(B', B) ∈ ⟨R⟩it_set_rel"
  shows "(A' @ B', A ∪ B) ∈ ⟨R⟩it_set_rel"
  using param_append[THEN fun_relD, THEN fun_relD, of A' _ R B'] assms
  by (fastforce simp: it_set_rel_def br_def)

subsection ‹Iteration›

definition FOREACH_it :: "'b set ⇒ ('b ⇒ 'a ⇒ 'a nres) ⇒ 'a ⇒ 'a nres" where
  "FOREACH_it X f s = LIST_FOREACH (λ_ _. True) (op_set_to_it X) (λ_. True) f s"

lemma FOREACH_it_rule:
  fixes I :: "'a set ⇒ 'b ⇒ bool" and X :: "'a set" and s :: 'b
  assumes I0: "I X s"
  assumes I1: "⋀x X' s'. finite X ⟹ x ∈ X ⟹ X' ⊆ X ⟹ I (insert x X') s' ⟹ f x s' ≤ SPEC (I X')"
  assumes F: "⋀s. finite X ⟹ I {} s ⟹ Φ s"
  shows "FOREACH_it X f s ≤ SPEC Φ"
  unfolding FOREACH_it_def LIST_FOREACH_def FOREACH_cond_def FOREACH_body_def op_set_to_it_def
  apply (refine_vcg order.trans[OF WHILEIT_weaken WHILEIT_rule[where
    I = "λ(it, B'). ∃xs'. xs = xs' @ it ∧ I (set it) B'" and s = "(xs, _)" for xs]]
    wf_measure[of "λ(xs, _). length xs"])
  subgoal by simp
  subgoal using I0 by (auto simp: hd_def split: list.splits)
  subgoal for xs s it B' using I1[of "hd it" "set (tl it)" B'] by (force simp: hd_def split: list.splits)
  subgoal by (auto intro: F)
  done

end