Theory Refine_Imperative_HOL.IICF_Set

section ‹Set Interface›
theory IICF_Set
imports "../../Sepref"
begin

subsection ‹Operations›
definition [simp]: "op_set_is_empty s ≡ s={}"
lemma op_set_is_empty_param[param]: "(op_set_is_empty,op_set_is_empty)∈⟨A⟩set_rel → bool_rel" by auto

definition op_set_copy :: "'a set ⇒ 'a set" where [simp]:  "op_set_copy s ≡ s"


context 
  notes [simp] = IS_LEFT_UNIQUE_def (* Argh, the set parametricity lemmas use single_valued (K¯) here. *)
begin

sepref_decl_op (no_def) set_copy: "op_set_copy" :: "⟨A⟩set_rel → ⟨A⟩set_rel" where "A = Id" .
sepref_decl_op set_empty: "{}" :: "⟨A⟩set_rel" .
sepref_decl_op (no_def) set_is_empty: op_set_is_empty :: "⟨A⟩set_rel → bool_rel" .
sepref_decl_op set_member: "(∈)" :: "A → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_insert: Set.insert :: "A → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_delete: "λx s. s - {x}" :: "A → ⟨A⟩set_rel → ⟨A⟩set_rel" 
  where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_union: "(∪)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" .
sepref_decl_op set_inter: "(∩)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_diff: "(-) ::_ set ⇒ _" :: "⟨A⟩set_rel → ⟨A⟩set_rel → ⟨A⟩set_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subseteq: "(⊆)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subset: "(⊂)" :: "⟨A⟩set_rel → ⟨A⟩set_rel → bool_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .

(* TODO: We may want different operations here: pick with predicate returning option,
  pick with remove, ... *)    
sepref_decl_op set_pick: "RES" :: "[λs. s≠{}]⇩f ⟨K⟩set_rel → K" by auto

sepref_decl_op set_size: "(card)" :: "⟨A⟩set_rel → nat_rel"  where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .


end

(* TODO: Set-pick. Move from where it is already defined! *)

subsection ‹Patterns›
lemma pat_set[def_pat_rules]:
  "{} ≡ op_set_empty"
  "(∈) ≡ op_set_member"    
  "Set.insert ≡ op_set_insert"
  "(∪) ≡ op_set_union"
  "(∩) ≡ op_set_inter"
  "(-) ≡ op_set_diff"
  "(⊆) ≡ op_set_subseteq"
  "(⊂) ≡ op_set_subset"
  by (auto intro!: eq_reflection)
  
lemma pat_set2[pat_rules]: 
  "(=) $s${} ≡ op_set_is_empty$s"
  "(=) ${}$s ≡ op_set_is_empty$s"

  "(-) $s$(Set.insert$x${}) ≡ op_set_delete$x$s"
  "SPEC$(λ⇩2x. (∈) $x$s) ≡ op_set_pick s"
  "RES$s ≡ op_set_pick s"
  by (auto intro!: eq_reflection)


locale set_custom_empty = 
  fixes empty and op_custom_empty :: "'a set"
  assumes op_custom_empty_def: "op_custom_empty = op_set_empty"
begin
  sepref_register op_custom_empty :: "'ax set"

  lemma fold_custom_empty:
    "{} = op_custom_empty"
    "op_set_empty = op_custom_empty"
    "mop_set_empty = RETURN op_custom_empty"
    unfolding op_custom_empty_def by simp_all
end

end