# 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
```