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)Aset_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" :: "Aset_rel  Aset_rel" where "A = Id" .
sepref_decl_op set_empty: "{}" :: "Aset_rel" .
sepref_decl_op (no_def) set_is_empty: op_set_is_empty :: "Aset_rel  bool_rel" .
sepref_decl_op set_member: "(∈)" :: "A  Aset_rel  bool_rel" where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_insert: Set.insert :: "A  Aset_rel  Aset_rel" where "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_delete: "λx s. s - {x}" :: "A  Aset_rel  Aset_rel" 
  where "IS_LEFT_UNIQUE A" "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_union: "(∪)" :: "Aset_rel  Aset_rel  Aset_rel" .
sepref_decl_op set_inter: "(∩)" :: "Aset_rel  Aset_rel  Aset_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_diff: "(-) ::_ set  _" :: "Aset_rel  Aset_rel  Aset_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subseteq: "(⊆)" :: "Aset_rel  Aset_rel  bool_rel" where "IS_LEFT_UNIQUE A"  "IS_RIGHT_UNIQUE A" .
sepref_decl_op set_subset: "(⊂)" :: "Aset_rel  Aset_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 Kset_rel  K" by auto

sepref_decl_op set_size: "(card)" :: "Aset_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