Theory Separation_Logic_Imperative_HOL.Array_Map_Impl

theory Array_Map_Impl
imports 
  "../Sep_Main" Imp_Map_Spec Array_Blit
  "HOL-Library.Code_Target_Numeral"
begin
  subsection "Array Map"

  type_synonym 'v array_map = "'v option array"
  definition "iam_initial_size ≡ 8::nat"

  definition "iam_of_list l i ≡ if i<length l then l!i else None"

  definition is_iam :: "(nat⇀'a) ⇒ ('a::heap) array_map ⇒ assn" where
    "is_iam m a ≡ ∃⇩Al. a↦⇩al * ↑(m=iam_of_list l)"

  definition iam_new_sz :: "nat ⇒ ('v::heap) array_map Heap"
    where "iam_new_sz sz ≡ Array.new sz None"

  definition iam_new :: "('v::heap) array_map Heap"
    where "iam_new ≡ iam_new_sz iam_initial_size"

  definition iam_lookup 
    :: "nat ⇒ ('v::heap) array_map ⇒ 'v option Heap"
    where "iam_lookup k a = do {
      l←Array.len a;
      if k < l then Array.nth a k else return None
    }"

  lemma [code]: "iam_lookup k a ≡ nth_oo None a k"
    unfolding nth_oo_def iam_lookup_def .

  definition iam_delete
    :: "nat ⇒ ('v::heap) array_map ⇒ ('v::heap) array_map Heap"
  where "iam_delete k a = do {
      l←Array.len a;
      if k < l then Array.upd k None a else return a
    }"

  lemma [code]: "iam_delete k a ≡ upd_oo (return a) k None a"
    unfolding upd_oo_def iam_delete_def .

  definition iam_update
    :: "nat ⇒ 'v::heap ⇒ 'v array_map ⇒ 'v array_map Heap"
    where "iam_update k v a = do {
      l←Array.len a;
      a←if k>=l then do {
          let newsz = max (k+1) (2 * l + 3);
          array_grow a newsz None
        } else return a;

      Array.upd k (Some v) a
    }"

  lemma [code]: "iam_update k v a = upd_oo 
    (do {
      l←Array.len a;
      let newsz = max (k+1) (2 * l + 3);
      a←array_grow a newsz None;
      Array.upd k (Some v) a
    })
    k (Some v) a"
  proof -
    have [simp]: 
      "⋀x t e. do {
        l←Array.len a;
        if x l then 
          t l 
        else do {
          l'←Array.len a;
          e l l'
        } 
      }
      =
      do {
        l←Array.len a;
        if x l then t l else e l l
      }"
      apply (auto 
        simp: bind_def execute_len 
        split: option.split
        intro!: ext
      )
      done
  
    show ?thesis
      unfolding upd_oo_def iam_update_def
      apply simp
      apply (rule cong[OF arg_cong, where f1=bind])
      apply simp
      apply (rule ext)
      apply auto
      done
  qed

  lemma precise_iam: "precise is_iam"
    apply rule
    by (auto simp add: is_iam_def dest: preciseD[OF snga_prec])

  lemma iam_new_abs: "iam_of_list (replicate n None) = Map.empty"
    unfolding iam_of_list_def[abs_def]
    by auto

  lemma iam_new_sz_rule: "<emp> iam_new_sz n < is_iam Map.empty >"
    unfolding iam_new_sz_def is_iam_def[abs_def]
    by (sep_auto simp: iam_new_abs)

  lemma iam_new_rule: "<emp> iam_new < is_iam Map.empty >"
    unfolding iam_new_def by (sep_auto heap: iam_new_sz_rule)

  lemma iam_lookup_abs1: "k<length l ⟹ iam_of_list l k = l!k"
    by (simp add: iam_of_list_def)
  lemma iam_lookup_abs2: "¬k<length l ⟹ iam_of_list l k = None"
    by (simp add: iam_of_list_def)

  lemma iam_lookup_rule: "< is_iam m p > 
    iam_lookup k p 
    <λr. is_iam m p * ↑(r=m k) >"
    unfolding iam_lookup_def is_iam_def
    by (sep_auto simp: iam_lookup_abs1 iam_lookup_abs2)

  lemma iam_delete_abs1: "k<length l 
    ⟹ iam_of_list (l[k := None]) = iam_of_list l |` (- {k})"
    unfolding iam_of_list_def[abs_def]
    by (auto intro!: ext simp: restrict_map_def)

  lemma iam_delete_abs2: "¬k<length l 
    ⟹ iam_of_list l |` (- {k}) = iam_of_list l"
    unfolding iam_of_list_def[abs_def]
    by (auto intro!: ext simp: restrict_map_def)

  lemma iam_delete_rule: "< is_iam m p >
    iam_delete k p
    <λr. is_iam (m|`(-{k})) r>"
    unfolding is_iam_def iam_delete_def
    by (sep_auto simp: iam_delete_abs1 iam_delete_abs2)
    

  lemma iam_update_abs1: "iam_of_list (l@replicate n None) = iam_of_list l"
    unfolding iam_of_list_def[abs_def]
    by (auto intro!: ext simp: nth_append)

  lemma iam_update_abs2: "¬ length l ≤ k 
    ⟹ iam_of_list (l[k := Some v]) = (iam_of_list l)(k ↦ v)"
    unfolding iam_of_list_def[abs_def]
    by auto

  lemma iam_update_rule:
    "< is_iam m p > iam_update k v p <λr. is_iam (m(k↦v)) r>⇩t"
    unfolding is_iam_def iam_update_def
    by (sep_auto 
      decon: decon_if_split 
      simp: iam_update_abs1 iam_update_abs2)
  
  interpretation iam: imp_map is_iam
    apply unfold_locales
    by (rule precise_iam)
  interpretation iam: imp_map_empty is_iam iam_new
    apply unfold_locales
    by (sep_auto heap: iam_new_rule)
  interpretation iam_sz: imp_map_empty is_iam "iam_new_sz sz"
    apply unfold_locales
    by (sep_auto heap: iam_new_sz_rule)
 
  interpretation iam: imp_map_lookup is_iam iam_lookup
    apply unfold_locales
    by (sep_auto heap: iam_lookup_rule)
  interpretation iam: imp_map_delete is_iam iam_delete
    apply unfold_locales
    by (sep_auto heap: iam_delete_rule)
  interpretation iam: imp_map_update is_iam iam_update
    apply unfold_locales
    by (sep_auto heap: iam_update_rule)

end