Theory Separation_Logic_Imperative_HOL.Hash_Set_Impl

section "Hash-Sets"
theory Hash_Set_Impl
imports Imp_Set_Spec Hash_Map_Impl
begin

subsection ‹Auxiliary Definitions›
definition map_of_set:: "'a set ⇒ 'a⇀unit" 
  where "map_of_set S x ≡ if x∈S then Some () else None"

lemma ne_some_unit_eq: "x≠Some () ⟷ x=None" 
  by (cases x) auto

lemma map_of_set_simps[simp]:
  "dom (map_of_set s) = s"
  "map_of_set (dom m) = m"
  "map_of_set {} = Map.empty"
  "map_of_set s x = None ⟷ x∉s"
  "map_of_set s x = Some u ⟷ x∈s"
  "(map_of_set s) (x↦()) = map_of_set (insert x s)"
  "(map_of_set s) |` (-{x}) = map_of_set (s -{x})"
  apply (auto simp: map_of_set_def 
    dom_def ne_some_unit_eq restrict_map_def 
    intro!: ext)
  done

lemma map_of_set_eq':
  "map_of_set a = map_of_set b ⟷ a=b"
  apply (auto simp: map_of_set_def[abs_def])
  apply (metis option.simps(3))+
  done

lemma map_of_set_eq[simp]:
  "map_of_set s = m ⟷ dom m=s"
  apply (auto 
    simp: dom_def map_of_set_def[abs_def] ne_some_unit_eq 
    intro!: ext)
  apply (metis option.simps(3))
  done

subsection ‹Main Definitions›
type_synonym 'a hashset = "('a,unit) hashtable"
definition "is_hashset s ht ≡ is_hashmap (map_of_set s) ht"

lemma hs_set_impl: "imp_set is_hashset"
  apply unfold_locales
  apply rule
  unfolding is_hashset_def
  apply (subst map_of_set_eq'[symmetric])
  by (metis preciseD[OF is_hashmap_prec])
interpretation hs: imp_set is_hashset by (rule hs_set_impl)

definition hs_new :: "'a::{heap,hashable} hashset Heap" 
  where "hs_new = hm_new"

lemma hs_new_impl: "imp_set_empty is_hashset hs_new"
  apply unfold_locales
  apply (sep_auto heap: hm_new_rule simp: is_hashset_def hs_new_def)
  done
interpretation hs: imp_set_empty is_hashset hs_new by (rule hs_new_impl)

definition hs_memb:: "'a::{heap,hashable} ⇒ 'a hashset ⇒ bool Heap" 
  where "hs_memb x s ≡ do { 
  r←hm_lookup x s; 
  return (case r of Some _ ⇒ True | None ⇒ False)  
}"

lemma hs_memb_impl: "imp_set_memb is_hashset hs_memb"
  apply unfold_locales
  unfolding hs_memb_def
  apply (sep_auto 
    heap: hm_lookup_rule 
    simp: is_hashset_def split: option.split)
  done
interpretation hs: imp_set_memb is_hashset hs_memb by (rule hs_memb_impl)

definition hs_ins:: "'a::{heap,hashable} ⇒ 'a hashset ⇒ 'a hashset Heap"
  where "hs_ins x ht ≡ hm_update x () ht"

lemma hs_ins_impl: "imp_set_ins is_hashset hs_ins"
  apply unfold_locales
  apply (sep_auto heap: hm_update_rule simp: hs_ins_def is_hashset_def)
  done
interpretation hs: imp_set_ins is_hashset hs_ins by (rule hs_ins_impl)

definition hs_delete
  :: "'a::{heap,hashable} ⇒ 'a hashset ⇒ 'a hashset Heap"
  where "hs_delete x ht ≡ hm_delete x ht"

lemma hs_delete_impl: "imp_set_delete is_hashset hs_delete"
  apply unfold_locales
  apply (sep_auto heap: hm_delete_rule simp: is_hashset_def hs_delete_def)
  done
interpretation hs: imp_set_delete is_hashset hs_delete
  by (rule hs_delete_impl)

definition "hs_isEmpty == hm_isEmpty"

lemma hs_is_empty_impl: "imp_set_is_empty is_hashset hs_isEmpty"
  apply unfold_locales
  apply (sep_auto heap: hm_isEmpty_rule simp: is_hashset_def hs_isEmpty_def)
  done
interpretation hs: imp_set_is_empty is_hashset hs_isEmpty
  by (rule hs_is_empty_impl)

definition "hs_size == hm_size"

lemma hs_size_impl: "imp_set_size is_hashset hs_size"
  apply unfold_locales
  apply (sep_auto heap: hm_size_rule simp: is_hashset_def hs_size_def)
  done
interpretation hs: imp_set_size is_hashset hs_size by (rule hs_size_impl)

type_synonym ('a) hs_it = "('a,unit) hm_it"

definition "hs_is_it s hs its it 
  ≡ hm_is_it (map_of_set s) hs (map_of_set its) it"

definition hs_it_init :: "('a::{heap,hashable}) hashset ⇒ 'a hs_it Heap"
  where "hs_it_init ≡ hm_it_init"

definition hs_it_has_next :: "('a::{heap,hashable}) hs_it ⇒ bool Heap"
  where "hs_it_has_next ≡ hm_it_has_next"

definition hs_it_next 
  :: "('a::{heap,hashable}) hs_it ⇒ ('a×'a hs_it) Heap"
  where 
  "hs_it_next it ≡ do {
    ((x,_),it) ← hm_it_next it;
    return (x,it)
  }"

lemma hs_iterate_impl: "imp_set_iterate 
  is_hashset hs_is_it hs_it_init hs_it_has_next hs_it_next"
  apply unfold_locales
  unfolding hs_it_init_def hs_it_next_def hs_it_has_next_def 
    hs_is_it_def is_hashset_def
  apply sep_auto
  apply sep_auto
  apply sep_auto
  apply (sep_auto eintros: hm.quit_iteration)
  done

interpretation hs: imp_set_iterate 
  is_hashset hs_is_it hs_it_init hs_it_has_next hs_it_next
  by (rule hs_iterate_impl)

definition "hs_union 
    ≡ union_loop_ins hs_it_init hs_it_has_next hs_it_next hs_ins"

lemmas hs_union_rule[sep_heap_rules] =
    set_union_rule[OF hs_iterate_impl hs_ins_impl,
    folded hs_union_def] 

lemma hs_union_impl: "imp_set_union 
is_hashset hs_is_it hs_it_init hs_it_has_next hs_it_next hs_union"
  apply (unfold_locales)
  by (sep_auto)

interpretation hs: imp_set_union 
  is_hashset hs_is_it hs_it_init hs_it_has_next hs_it_next hs_union
  by (rule hs_union_impl)




export_code hs_new hs_memb hs_ins hs_delete hs_isEmpty hs_size 
  hs_it_init hs_it_has_next hs_it_next hs_union
  checking SML_imp

end