Theory Refine_Phantom

theory Refine_Phantom
imports
  Autoref_Misc
  Refine_Unions
begin
consts i_phantom :: "interface ⇒ interface"

context includes autoref_syntax begin


definition pphantom_rel_internal:
  "phantom_rel A = {(Some x, y)|x y. (x, y) ∈ A} ∪ {(None, y)|x y. (x, y) ∈ A}"
lemma phantom_rel_def: "⟨A⟩phantom_rel = {(Some x, y)|x y. (x, y) ∈ A} ∪ {(None, y)|x y. (x, y) ∈ A}"
  by (auto simp: relAPP_def pphantom_rel_internal)
lemmas [autoref_rel_intf] = REL_INTFI[of phantom_rel i_phantom]

definition [simp]: "mk_phantom x = x"

lemma phantom_rel_const[autoref_rules(overloaded)]:
  shows "(Some, mk_phantom) ∈ A → ⟨A⟩phantom_rel"
  by (auto simp: phantom_rel_def)

definition [simp]: "op_union_phantom = (∪)"
lemma [autoref_op_pat]: "(∪) ≡ OP op_union_phantom"
  by simp
lemma phantom_rel_union[autoref_rules]:
  assumes [THEN GEN_OP_D, autoref_rules(overloaded)]: "GEN_OP un (∪) (A → A → A)"
  shows "(λa b. do {a ← a; b ← b; Some (un a b)}, op_union_phantom) ∈ ⟨A⟩phantom_rel → ⟨A⟩phantom_rel → ⟨A⟩phantom_rel"
  using assms
  by (fastforce simp: phantom_rel_def dest: fun_relD)

definition [simp]: "op_empty_phantom b = {}"

lemma phantom_rel_empty_coll[autoref_rules]:
  shows "(λb. (if b then None else Some []), op_empty_phantom) ∈ bool_rel → ⟨clw_rel A⟩phantom_rel"
  apply (auto simp: phantom_rel_def br_def lw_rel_def Union_rel_def)
    apply (rule relcompI)
     apply force
    apply (rule relcompI)
     defer
  by (force dest!: spec[where x="[]"])+


lemma mem_phantom_rel_Some[simp]:
  "(Some x, y) ∈ ⟨A⟩phantom_rel ⟷ (x, y) ∈ A"
  by (auto simp: phantom_rel_def)

lemma RETURN_None_ph_relI: "(RETURN y, x) ∈ ⟨B⟩nres_rel ⟹ (RETURN None, x) ∈ ⟨⟨B⟩phantom_rel⟩nres_rel"
  by (auto simp: phantom_rel_def nres_rel_def pw_le_iff refine_pw_simps)
lemma RETURN_Some_ph_relI: "(RETURN y, x) ∈ ⟨B⟩nres_rel ⟹ (RETURN (Some y), x) ∈ ⟨⟨B⟩phantom_rel⟩nres_rel"
  by (auto simp: phantom_rel_def nres_rel_def pw_le_iff refine_pw_simps)

lemma None_ph_relI: "(x, X) ∈ B ⟹ (None, X) ∈ ⟨B⟩phantom_rel"
  by (auto simp: phantom_rel_def)

definition "phantom_rel_unop fid x = (case x of None ⇒ None | Some x ⇒ (Some (fid x)))"
lemma phantom_rel_unop:
  assumes f[THEN GEN_OP_D]: "GEN_OP fi f (A → ⟨B⟩nres_rel)"
  assumes fi[unfolded autoref_tag_defs]: "⋀x. TRANSFER (RETURN (fid x) ≤ fi x)"
  shows "(λx. RETURN (phantom_rel_unop fid x), f) ∈ ⟨A⟩phantom_rel → ⟨⟨B⟩phantom_rel⟩nres_rel"
proof (rule fun_relI)
  fix x a assume x: "(x, a) ∈ ⟨A⟩phantom_rel"
  with assms obtain b where "(b, a) ∈ A" by (auto simp: phantom_rel_def)
  show "(RETURN (phantom_rel_unop fid x), f a) ∈ ⟨⟨B⟩phantom_rel⟩nres_rel"
    using x
    by (auto split: option.splits intro!: x ‹(b, a) ∈ A› f[param_fo]
        RETURN_Some_ph_relI RETURN_None_ph_relI nres_rel_trans1[OF fi]
        simp: phantom_rel_unop_def)
qed

lemma phantom_rel_union_coll[autoref_rules]:
  assumes [THEN GEN_OP_D, autoref_rules(overloaded)]: "GEN_OP un op_union_coll (clw_rel A → clw_rel A → clw_rel A)"
  shows "(λa b. do {a ← a; b ← b; Some (un a b)}, op_union_phantom) ∈ ⟨clw_rel A⟩phantom_rel → ⟨clw_rel A⟩phantom_rel → ⟨clw_rel A⟩phantom_rel"
  using assms
  by (fastforce simp: phantom_rel_def dest: fun_relD)

definition [refine_vcg_def]: "get_phantom X = SPEC (λR. R = X)"

lemma get_phantom_impl[autoref_rules]:
  "(λx. nres_of (case x of None ⇒ dSUCCEED | Some y ⇒ dRETURN y), get_phantom) ∈ ⟨A⟩phantom_rel → ⟨A⟩nres_rel"
  by (auto simp: get_phantom_def phantom_rel_def nres_rel_def RETURN_RES_refine_iff)

end

end