Theory Refine_Default

theory Refine_Default
  imports
    Enclosure_Operations
    Weak_Set
begin

consts i_default::"interface ⇒ interface"

definition default_rel_internal: "default_rel d X = insert (None, d) ((λ(x, y). (Some x, y)) ` X)"
lemma default_rel_def: "⟨X⟩default_rel d = insert (None, d) ((λ(x, y). (Some x, y)) ` X)"
  by (auto simp: relAPP_def default_rel_internal)
lemmas [autoref_rel_intf] = REL_INTFI[of "default_rel d" i_default for d]

lemma single_valued_default_rel[relator_props]:
  "single_valued R ⟹ single_valued (⟨R⟩default_rel d)"
  by (auto simp: default_rel_def intro!: relator_props) (auto simp: single_valued_def)

lemma
  mem_default_relI:
  assumes "a = None ⟹ b = d"
  assumes "⋀x. a = Some x ⟹ (x, b) ∈ R"
  shows "(a, b) ∈ ⟨R⟩default_rel d"
  using assms image_iff
  by (force simp: default_rel_def)

lemma Some_mem_default_rel: "(Some x, y) ∈ ⟨X⟩default_rel d⟷ (x, y) ∈ X"
  by (auto simp: default_rel_def)

lemma option_rel_inverse[simp]: "(⟨R⟩option_rel)¯ = ⟨R¯⟩option_rel"
  by (auto simp: option_rel_def)

lemma default_rel_split[autoref_rules]:
  assumes split_impl: "(split_impl, split_spec) ∈ A → ⟨B ×⇩r A⟩nres_rel"
  shows "(λxs.
    case xs of None ⇒ SUCCEED
    | Some x ⇒ do {(r, s) ← split_impl x; RETURN (r, Some s)},
    split_spec) ∈
    ⟨A⟩default_rel d → ⟨B ×⇩r ⟨A⟩default_rel d⟩nres_rel"
proof -
  have "split_impl a ⤜ (λ(r, s). RETURN (r, Some s))
    ≤ ⇓ (B ×⇩r insert (None, d) ((λ(x, y). (Some x, y)) ` A)) (SPEC (λ(A, B). b ⊆ A ∪ B))"
    if "(a, b) ∈ A"
    for a b
  proof -
    have split_inresD:
      "∃a. (c, a) ∈ B ∧ (∃bb. (Some d, bb) ∈ (λ(x, y). (Some x, y)) ` A ∧ b ⊆ a ∪ bb)"
      if "inres (split_impl a) (c, d)"
      for c d
    proof -
      have "RETURN (c, d) ≤ ⇓ (B ×⇩r A) (split_spec b)"
        using ‹(a, b) ∈ A› that split_impl
        by (auto simp: inres_def nres_rel_def dest!: fun_relD)
      then show ?thesis
        using ‹(a, b) ∈ A› that split_impl
        by (fastforce simp: split_spec_def elim!: RETURN_ref_SPECD)
    qed
    have "nofail (split_impl a)"
      using split_impl[param_fo, OF ‹(a, b) ∈ A›] le_RES_nofailI
      by (auto simp: split_spec_def nres_rel_def conc_fun_def)
    then show ?thesis
      using that split_impl
      by (fastforce simp: refine_pw_simps dest!: split_inresD intro!: pw_leI)
  qed
  then show ?thesis
    by (auto simp: split_spec_def default_rel_def
        intro!: nres_relI)
qed

lemma br_Some_O_default_rel_eq: "br Some top O ⟨A⟩default_rel d = A"
  by (auto simp: br_def default_rel_def)

definition [simp]: "op_Union_default = Union"

context includes autoref_syntax begin
lemma [autoref_op_pat]: "Union ≡ OP op_Union_default"
  by simp

lemma default_rel_Union[autoref_rules]:
  assumes sv: "PREFER single_valued A"
  assumes safe: "SIDE_PRECOND (∀x ∈ X. x ⊆ d)"
  assumes xs: "(xs, X) ∈ ⟨⟨A⟩default_rel d⟩list_wset_rel"
  assumes Union_A: "(concat, Union) ∈ ⟨A⟩list_wset_rel → A"
  shows "(map_option concat (those xs), op_Union_default $ X) ∈ ⟨A⟩default_rel d"
  using xs
  apply (safe dest!: list_wset_relD intro!: mem_default_relI)
  subgoal using safe by (auto simp: default_rel_def)
  subgoal by (auto simp: default_rel_def those_eq_None_set_iff dest!: set_relD)[]
  subgoal
    by (auto simp: those_eq_Some_map_Some_iff image_mem_set_rel_iff br_Some_O_default_rel_eq list_wset_rel_def
        intro!: relcompI brI Union_A[param_fo])
  done

definition [simp]: "op_empty_default = {}"
lemma default_rel_empty[autoref_rules]:
  assumes "GEN_OP ei {} A"
  shows "(Some ei, op_empty_default) ∈ ⟨A⟩default_rel d"
  using assms by (auto simp: default_rel_def)

definition mk_default::"'a set ⇒ 'a set" where [refine_vcg_def, simp]: "mk_default x = x"

lemma mk_default[autoref_rules]:
  "(Some, mk_default) ∈ R → ⟨R⟩default_rel d"
  by (auto simp: default_rel_def)

definition [refine_vcg_def]: "default_rep d X = SPEC (λx. case x of None ⇒ X = d | Some r ⇒ X = r)"

lemma default_rep_op_pat[autoref_op_pat_def]: "default_rep d ≡ OP (default_rep d)"
  by auto

lemma default_rep[autoref_rules]:
  "(λx. RETURN x, default_rep d) ∈ (⟨R⟩(default_rel d)) → ⟨⟨R⟩option_rel⟩nres_rel"
  by (force simp: default_rep_def nres_rel_def default_rel_def
      split: option.splits intro!: RETURN_SPEC_refine )

end

end