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
    This implements a datastructure that efficiently supports two operations: appending an element and looking up the nth element. 
  The implementation is straightforward.
    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 ← 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))