# Theory Separation_Logic_Imperative_HOL.Imp_Set_Spec

```section ‹Interface for Sets›
theory Imp_Set_Spec
imports "../Sep_Main"
begin
text ‹
This file specifies an abstract interface for set data structures. It can
be implemented by concrete set data structures, as demonstrated in the
hash set example.
›

locale imp_set =
fixes is_set :: "'a set ⇒ 's ⇒ assn"
assumes precise: "precise is_set"

locale imp_set_empty = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes empty :: "'s Heap"
assumes empty_rule[sep_heap_rules]: "<emp> empty <is_set {}>⇩t"

locale imp_set_is_empty = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes is_empty :: "'s ⇒ bool Heap"
assumes is_empty_rule[sep_heap_rules]:
"<is_set s p> is_empty p <λr. is_set s p * ↑(r ⟷ s={})>⇩t"

locale imp_set_memb = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes memb :: "'a ⇒ 's ⇒ bool Heap"
assumes memb_rule[sep_heap_rules]:
"<is_set s p> memb a p <λr. is_set s p * ↑(r ⟷ a ∈ s)>⇩t"

locale imp_set_ins = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes ins :: "'a ⇒ 's ⇒ 's Heap"
assumes ins_rule[sep_heap_rules]:
"<is_set s p> ins a p <is_set (Set.insert a s)>⇩t"

locale imp_set_delete = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes delete :: "'a ⇒ 's ⇒ 's Heap"
assumes delete_rule[sep_heap_rules]:
"<is_set s p> delete a p <is_set (s - {a})>⇩t"

locale imp_set_size = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes size :: "'s ⇒ nat Heap"
assumes size_rule[sep_heap_rules]:
"<is_set s p> size p <λr. is_set s p * ↑(r = card s)>⇩t"

locale imp_set_iterate = imp_set +
constrains is_set :: "'a set ⇒ 's ⇒ assn"
fixes is_it :: "'a set ⇒ 's ⇒ 'a set ⇒ 'it ⇒ assn"
fixes it_init :: "'s ⇒ ('it) Heap"
fixes it_has_next :: "'it ⇒ bool Heap"
fixes it_next :: "'it ⇒ ('a×'it) Heap"
assumes it_init_rule[sep_heap_rules]:
"<is_set s p> it_init p <is_it s p s>⇩t"
assumes it_next_rule[sep_heap_rules]: "s'≠{} ⟹
<is_it s p s' it>
it_next it
<λ(a,it'). is_it s p (s' - {a}) it' * ↑(a ∈ s')>⇩t"
assumes it_has_next_rule[sep_heap_rules]:
"<is_it s p s' it> it_has_next it <λr. is_it s p s' it * ↑(r⟷s'≠{})>⇩t"
assumes quit_iteration:
"is_it s p s' it ⟹⇩A is_set s p * true"

locale imp_set_union = imp_set_iterate +
fixes union :: "'s ⇒ 's ⇒ 's Heap"
assumes union_rule[sep_heap_rules]:
"finite se ⟹ <(is_set s p) * (is_set se q)> union p q <λr.
∃⇩As'. is_set s' r * (is_set se q)* true *  ↑ (s' = s ∪ se)>"

(* TODO: Move Generic implementation*)

partial_function (heap) set_it_union
where [code]: "set_it_union
it_has_next it_next set_ins it a = do {
co ← it_has_next it;
if co then do {
(x,it') ← it_next it;
insx <- set_ins x a;
set_it_union it_has_next it_next set_ins it' (insx)
} else return a
}"

lemma set_it_union_rule:
assumes "imp_set_iterate is_set is_it it_init it_has_next it_next"
assumes "imp_set_ins is_set set_ins"
assumes FIN: "finite it"
shows "
< is_it b q it iti * is_set a p>
set_it_union it_has_next it_next set_ins iti p
< λr. ∃⇩As'. is_set s' r *  is_set b q  * true * ↑ (s' = a ∪ it) >"
proof -
interpret imp_set_iterate is_set is_it it_init it_has_next it_next
+ imp_set_ins is_set set_ins
by fact+

from FIN show ?thesis
proof (induction  arbitrary: a p iti rule: finite_psubset_induct)
case (psubset it)
show ?case
apply (subst set_it_union.simps)
using imp_set_iterate_axioms
apply (sep_auto heap: psubset.IH)
by (metis ent_refl_true ent_star_mono_true quit_iteration star_aci(2))
qed
qed

definition union_loop_ins  where
"union_loop_ins it_init it_has_next it_next set_ins a b ≡ do {
it <- (it_init b);
set_it_union it_has_next it_next set_ins it a
}"

lemma set_union_rule:
assumes IT: "imp_set_iterate is_set is_it it_init it_has_next it_next"
assumes INS: "imp_set_ins is_set set_ins"
assumes finb: "finite b"
shows "
<is_set a p * is_set b q>
union_loop_ins it_init  it_has_next it_next set_ins p q
<λr.  ∃⇩As'. is_set s' r * true * is_set b q * ↑ (s' = a ∪ b)>"
proof -
interpret
imp_set_iterate is_set is_it it_init it_has_next it_next
+ imp_set_ins is_set set_ins
by fact+

note it_aux[sep_heap_rules] = set_it_union_rule[OF IT INS finb]
show ?thesis
unfolding union_loop_ins_def
apply (sep_auto)
done
qed

end
```