Theory Array_List

theory Array_List
imports Array_Blit
```section‹Array List›
text‹Most of this has been contributed by Peter Lammich.›
theory Array_List
imports
Separation_Logic_Imperative_HOL.Array_Blit
begin
text‹
This implements a datastructure that efficiently supports two operations: appending an element and looking up the nth element.
The implementation is straightforward.
›
text‹
As underlying data structure an array is used.
Since changing the length of an array requires copying, we double the size whenever the array needs to be expanded.
We use a counter for the current length to track which elements are used and which are spares.
›
type_synonym 'a array_list = "'a array × nat"

definition "is_array_list l ≡ λ(a,n). ∃⇩Al'. a ↦⇩a l' * ↑(n ≤ length l' ∧ l = take n l' ∧ length l'>0)"

definition "initial_capacity ≡ 16::nat"

definition "arl_empty ≡ do {
a ← Array.new initial_capacity default;
return (a,0)
}"

lemma [sep_heap_rules]: "< emp > arl_empty <is_array_list []>"
by (sep_auto simp: arl_empty_def is_array_list_def initial_capacity_def)

definition "arl_nth ≡ λ(a,n) i. do {
Array.nth a i
}"

lemma [sep_heap_rules]: "i<length l ⟹ < is_array_list l a > arl_nth a i <λx. is_array_list l a * ↑(x = l!i) >"
by (sep_auto simp: arl_nth_def is_array_list_def split: prod.splits)

definition "arl_append ≡ λ(a,n) x. do {
len ← Array.len a;

if n<len then do {
a ← Array.upd n x a;
return (a,n+1)
} else do {
let newcap = 2 * len;
a ← array_grow a newcap default;
a ← Array.upd n x a;
return (a,n+1)
}
}"

lemma [sep_heap_rules]: "
< is_array_list l a >
arl_append a x
<λa. is_array_list (l@[x]) a >⇩t"
by (sep_auto
simp: arl_append_def is_array_list_def take_update_last neq_Nil_conv
split: prod.splits nat.split)

lemma is_array_list_prec: "precise is_array_list"
unfolding is_array_list_def[abs_def]
apply(rule preciseI)
apply(simp split: prod.splits)
using preciseD snga_prec by fastforce

lemma is_array_list_lengthIA: "is_array_list l li ⟹⇩A ↑(snd li = length l) * true"
by(sep_auto simp: is_array_list_def split: prod.splits)
find_consts "assn ⇒ bool"
lemma is_array_list_lengthI: "x ⊨ is_array_list l li ⟹ snd li = length l"
using is_array_list_lengthIA by (metis (full_types) ent_pure_post_iff star_aci(2))

end
```