Theory Refine_Default

theory Refine_Default

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: "Xdefault_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 (Rdefault_rel d)"
  by (auto simp: default_rel_def intro!: relator_props) (auto simp: single_valued_def)

  assumes "a = None  b = d"
  assumes "x. a = Some x  (x, b)  R"
  shows "(a, b)  Rdefault_rel d"
  using assms image_iff
  by (force simp: default_rel_def)

lemma Some_mem_default_rel: "(Some x, y)  Xdefault_rel d (x, y)  X"
  by (auto simp: default_rel_def)

lemma option_rel_inverse[simp]: "(Roption_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 Anres_rel"
  shows "(λxs.
    case xs of None  SUCCEED
    | Some x  do {(r, s)  split_impl x; RETURN (r, Some s)},
    Adefault_rel d  B ×r Adefault_rel dnres_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)
    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)
  then show ?thesis
    by (auto simp: split_spec_def default_rel_def
        intro!: nres_relI)

lemma br_Some_O_default_rel_eq: "br Some top O Adefault_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)  Adefault_rel dlist_wset_rel"
  assumes Union_A: "(concat, Union)  Alist_wset_rel  A"
  shows "(map_option concat (those xs), op_Union_default $ X)  Adefault_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)[]
    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])

definition [simp]: "op_empty_default = {}"
lemma default_rel_empty[autoref_rules]:
  assumes "GEN_OP ei {} A"
  shows "(Some ei, op_empty_default)  Adefault_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  Rdefault_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))  Roption_relnres_rel"
  by (force simp: default_rep_def nres_rel_def default_rel_def
      split: option.splits intro!: RETURN_SPEC_refine )