# 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```