# Theory Separation_Logic_Imperative_HOL.Array_Set_Impl

```theory Array_Set_Impl
imports
"../Sep_Main" Imp_Set_Spec Array_Blit
"HOL-Library.Code_Target_Numeral"
begin
subsection "Array Set"

type_synonym array_set = "bool array"
definition "ias_initial_size ≡ 8::nat"

definition "ias_of_list l ≡ {i. i<length l ∧ l!i}"

definition is_ias :: "(nat set) ⇒ array_set ⇒ assn" where
"is_ias m a ≡ ∃⇩Al. a↦⇩al * ↑(m=ias_of_list l)"

definition ias_new_sz :: "nat ⇒ array_set Heap"
where "ias_new_sz sz ≡ Array.new sz False"

definition ias_new :: "array_set Heap"
where "ias_new ≡ ias_new_sz ias_initial_size"

definition ias_memb
:: "nat ⇒ array_set ⇒ bool Heap"
where "ias_memb k a = do {
l←Array.len a;
if k < l then Array.nth a k else return False
}"

lemma [code]: "ias_memb k a ≡ nth_oo False a k"
unfolding ias_memb_def nth_oo_def .

definition ias_delete
:: "nat ⇒ array_set ⇒ array_set Heap"
where "ias_delete k a = do {
l←Array.len a;
if k < l then Array.upd k False a else return a
}"

lemma [code]: "ias_delete k a ≡ upd_oo (return a) k False a"
unfolding ias_delete_def upd_oo_def .

definition ias_ins
:: "nat ⇒ array_set ⇒ array_set Heap"
where "ias_ins k a = do {
l←Array.len a;
a←if k>=l then do {
let newsz = max (k+1) (2 * l + 3);
array_grow a newsz False
} else return a;

Array.upd k True a
}"

lemma [code]: "ias_ins k a ≡ upd_oo (do {
l←Array.len a;
let newsz = max (k+1) (2 * l + 3);
a←array_grow a newsz False;
Array.upd k True a
})
k True a"
unfolding ias_ins_def upd_oo_def
apply (rule eq_reflection)
apply (auto simp add: bind_def execute_len execute_return)
done

lemma precise_ias: "precise is_ias"
apply rule
by (auto simp add: is_ias_def dest: preciseD[OF snga_prec])

lemma ias_new_abs: "ias_of_list (replicate n False) = {}"
unfolding ias_of_list_def[abs_def]
by auto

lemma ias_new_sz_rule: "<emp> ias_new_sz n < is_ias {} >"
unfolding ias_new_sz_def is_ias_def[abs_def]
by (sep_auto simp: ias_new_abs)

lemma ias_new_rule: "<emp> ias_new < is_ias {} >"
unfolding ias_new_def by (sep_auto heap: ias_new_sz_rule)

lemma ias_memb_abs1: "k<length l ⟹ k∈ias_of_list l ⟷ l!k"
by (simp add: ias_of_list_def)
lemma ias_memb_abs2: "¬k<length l ⟹ k∉ias_of_list l"
by (simp add: ias_of_list_def)

lemma ias_memb_rule: "< is_ias m p >
ias_memb k p
<λr. is_ias m p * ↑(r⟷k∈m) >"
unfolding ias_memb_def is_ias_def
by (sep_auto simp: ias_memb_abs1 ias_memb_abs2)

lemma ias_delete_abs1: "k<length l
⟹ ias_of_list (l[k := False]) = ias_of_list l - {k}"
unfolding ias_of_list_def[abs_def]
by (auto simp: nth_list_update)

lemma ias_delete_abs2: "¬k<length l
⟹ ias_of_list l - {k} = ias_of_list l"
unfolding ias_of_list_def[abs_def]
by (auto)

lemma ias_delete_rule: "< is_ias m p >
ias_delete k p
<λr. is_ias (m-{k}) r>"
unfolding is_ias_def ias_delete_def
by (sep_auto simp: ias_delete_abs1 ias_delete_abs2)

lemma ias_ins_abs1: "ias_of_list (l@replicate n False) = ias_of_list l"
unfolding ias_of_list_def[abs_def]
apply rule
apply rule
apply simp
apply (elim conjE)
apply (case_tac "x<length l")
apply (simp_all add: nth_append) [2]
apply rule
apply (simp add: nth_append)
done

lemma ias_ins_abs2: "¬ length l ≤ k
⟹ ias_of_list (l[k := True]) = insert k (ias_of_list l)"
unfolding ias_of_list_def[abs_def]
by (auto simp: nth_list_update)

lemma ias_ins_rule:
"< is_ias m p > ias_ins k p <λr. is_ias (insert k m) r>⇩t"
unfolding is_ias_def ias_ins_def
by (sep_auto
decon: decon_if_split
simp: ias_ins_abs1 ias_ins_abs2)

lemma ias_set_impl: "imp_set is_ias"
apply unfold_locales
by (rule precise_ias)
interpretation ias: imp_set is_ias using ias_set_impl .

lemma ias_empty_impl: "imp_set_empty is_ias ias_new"
apply unfold_locales
by (sep_auto heap: ias_new_rule)
interpretation ias: imp_set_empty is_ias ias_new using ias_empty_impl .

lemma ias_empty_sz_impl: "imp_set_empty is_ias (ias_new_sz sz)"
apply unfold_locales
by (sep_auto heap: ias_new_sz_rule)
interpretation ias_sz: imp_set_empty is_ias "ias_new_sz sz"
using ias_empty_sz_impl .

lemma ias_memb_impl: "imp_set_memb is_ias ias_memb"
apply unfold_locales
by (sep_auto heap: ias_memb_rule)
interpretation ias: imp_set_memb is_ias ias_memb
using ias_memb_impl .

lemma ias_delete_impl: "imp_set_delete is_ias ias_delete"
apply unfold_locales
by (sep_auto heap: ias_delete_rule)
interpretation ias: imp_set_delete is_ias ias_delete
using ias_delete_impl .

(* Self - contained proof, for paper *)
context begin
interpretation ias: imp_set_ins is_ias ias_ins proof
fix s p a
show "<is_ias s p> ias_ins a p <is_ias (insert a s)>⇩t"
unfolding is_ias_def ias_ins_def
by (sep_auto decon: decon_if_split simp: ias_ins_abs1 ias_ins_abs2)
qed

end

lemma "imp_set_ins is_ias ias_ins"
apply unfold_locales
by (sep_auto heap: ias_ins_rule)

lemma ias_ins_impl: "imp_set_ins is_ias ias_ins"
apply unfold_locales
by (sep_auto heap: ias_ins_rule)
interpretation ias: imp_set_ins is_ias ias_ins
using ias_ins_impl .

end
```