Theory DynamicArray

(*
  File: DynamicArray.thy
  Author: Bohua Zhan
*)

section ‹Implementation of dynamic arrays›

theory DynamicArray
  imports Arrays_Impl
begin

text ‹Dynamically allocated arrays.›

datatype 'a dynamic_array = Dyn_Array (alen: nat) (aref: "'a array")
setup ‹add_simple_datatype "dynamic_array"›

subsection ‹Raw assertion›

fun dyn_array_raw :: "'a::heap list × nat ⇒ 'a dynamic_array ⇒ assn" where
  "dyn_array_raw (xs, n) (Dyn_Array m a) = (a ↦⇩a xs * ↑(m = n))"
setup ‹add_rewrite_ent_rule @{thm dyn_array_raw.simps}›

definition dyn_array_new :: "'a::heap dynamic_array Heap" where
  "dyn_array_new = do {
     p ← Array.new 5 undefined;
     return (Dyn_Array 0 p)
   }"

lemma dyn_array_new_rule' [hoare_triple]:
  "<emp>
   dyn_array_new
   <dyn_array_raw (replicate 5 undefined, 0)>" by auto2

fun double_length :: "'a::heap dynamic_array ⇒ 'a dynamic_array Heap" where
  "double_length (Dyn_Array al ar) = do {
      am ← Array.len ar;
      p ← Array.new (2 * am + 1) undefined;
      array_copy ar p am;
      return (Dyn_Array am p)
    }"

fun double_length_fun :: "'a::heap list × nat ⇒ 'a list × nat" where
  "double_length_fun (xs, n) =
    (Arrays_Ex.array_copy xs (replicate (2 * n + 1) undefined) n, n)"
setup ‹add_rewrite_rule @{thm double_length_fun.simps}›

lemma double_length_rule' [hoare_triple]:
  "length xs = n ⟹
   <dyn_array_raw (xs, n) p>
   double_length p
   <dyn_array_raw (double_length_fun (xs, n))>⇩t" by auto2

fun push_array_basic :: "'a ⇒ 'a::heap dynamic_array ⇒ 'a dynamic_array Heap" where
  "push_array_basic x (Dyn_Array al ar) = do {
    Array.upd al x ar;
    return (Dyn_Array (al + 1) ar)
   }"

fun push_array_basic_fun :: "'a ⇒ 'a::heap list × nat ⇒ 'a list × nat" where
  "push_array_basic_fun x (xs, n) = (list_update xs n x, n + 1)"
setup ‹add_rewrite_rule @{thm push_array_basic_fun.simps}›

lemma push_array_basic_rule' [hoare_triple]:
  "n < length xs ⟹
   <dyn_array_raw (xs, n) p>
   push_array_basic x p
   <dyn_array_raw (push_array_basic_fun x (xs, n))>" by auto2

definition array_length :: "'a dynamic_array ⇒ nat Heap" where
  "array_length d = return (alen d)"

lemma array_length_rule' [hoare_triple]:
  "<dyn_array_raw (xs, n) p>
   array_length p
   <λr. dyn_array_raw (xs, n) p * ↑(r = n)>" by auto2

definition array_max :: "'a::heap dynamic_array ⇒ nat Heap" where
  "array_max d = Array.len (aref d)"

lemma array_max_rule' [hoare_triple]:
  "<dyn_array_raw (xs, n) p>
   array_max p
   <λr. dyn_array_raw (xs, n) p * ↑(r = length xs)>" by auto2

definition array_nth :: "'a::heap dynamic_array ⇒ nat ⇒ 'a Heap" where
  "array_nth d i = Array.nth (aref d) i"

lemma array_nth_rule' [hoare_triple]:
  "i < n ⟹ n ≤ length xs ⟹
   <dyn_array_raw (xs, n) p>
   array_nth p i
   <λr. dyn_array_raw (xs, n) p * ↑(r = xs ! i)>" by auto2

definition array_upd :: "nat ⇒ 'a ⇒ 'a::heap dynamic_array ⇒ unit Heap" where
  "array_upd i x d = do { Array.upd i x (aref d); return () }"

lemma array_upd_rule' [hoare_triple]:
  "i < n ⟹ n ≤ length xs ⟹
   <dyn_array_raw (xs, n) p>
   array_upd i x p
   <λ_. dyn_array_raw (list_update xs i x, n) p>" by auto2

definition push_array :: "'a ⇒ 'a::heap dynamic_array ⇒ 'a dynamic_array Heap" where
  "push_array x p = do {
    m ← array_max p;
    l ← array_length p;
    if l < m then push_array_basic x p
    else do {
      u ← double_length p;
      push_array_basic x u
    }
  }"

definition pop_array :: "'a::heap dynamic_array ⇒ ('a × 'a dynamic_array) Heap" where
  "pop_array d = do {
    x ← Array.nth (aref d) (alen d - 1);
    return (x, Dyn_Array (alen d - 1) (aref d))
   }"

lemma pop_array_rule' [hoare_triple]:
  "n > 0 ⟹ n ≤ length xs ⟹
   <dyn_array_raw (xs, n) p>
   pop_array p
   <λ(x, r). dyn_array_raw (xs, n - 1) r * ↑(x = xs ! (n - 1))>" by auto2

setup ‹del_prfstep_thm @{thm dyn_array_raw.simps}›
setup ‹del_simple_datatype "dynamic_array"›

fun push_array_fun :: "'a ⇒ 'a::heap list × nat ⇒ 'a list × nat" where
  "push_array_fun x (xs, n) = (
     if n < length xs then push_array_basic_fun x (xs, n)
     else push_array_basic_fun x (double_length_fun (xs, n)))"
setup ‹add_rewrite_rule @{thm push_array_fun.simps}›

lemma push_array_rule' [hoare_triple]:
  "n ≤ length xs ⟹
   <dyn_array_raw (xs, n) p>
   push_array x p
   <dyn_array_raw (push_array_fun x (xs, n))>⇩t" by auto2

subsection ‹Abstract assertion›

fun abs_array :: "'a::heap list × nat ⇒ 'a list" where
  "abs_array (xs, n) = take n xs"
setup ‹add_rewrite_rule @{thm abs_array.simps}›

lemma double_length_abs [rewrite]:
  "length xs = n ⟹ abs_array (double_length_fun (xs, n)) = abs_array (xs, n)" by auto2

lemma push_array_basic_abs [rewrite]:
  "n < length xs ⟹ abs_array (push_array_basic_fun x (xs, n)) = abs_array (xs, n) @ [x]"
@proof @have "length (take n xs @ [x]) = n + 1" @qed

lemma push_array_fun_abs [rewrite]:
  "n ≤ length xs ⟹ abs_array (push_array_fun x (xs, n)) = abs_array (xs, n) @ [x]" by auto2

definition dyn_array :: "'a::heap list ⇒ 'a dynamic_array ⇒ assn" where [rewrite_ent]:
  "dyn_array xs a = (∃⇩Ap. dyn_array_raw p a * ↑(xs = abs_array p) * ↑(snd p ≤ length (fst p)))"

lemma dyn_array_new_rule [hoare_triple]:
  "<emp> dyn_array_new <dyn_array []>" by auto2

lemma array_length_rule [hoare_triple]:
  "<dyn_array xs p>
   array_length p
   <λr. dyn_array xs p * ↑(r = length xs)>" by auto2

lemma array_nth_rule [hoare_triple]:
  "i < length xs ⟹
   <dyn_array xs p>
    array_nth p i
   <λr. dyn_array xs p * ↑(r = xs ! i)>" by auto2

lemma array_upd_rule [hoare_triple]:
  "i < length xs ⟹
   <dyn_array xs p>
    array_upd i x p
   <λ_. dyn_array (list_update xs i x) p>" by auto2

lemma push_array_rule [hoare_triple]:
  "<dyn_array xs p>
    push_array x p
   <dyn_array (xs @ [x])>⇩t" by auto2

lemma pop_array_rule [hoare_triple]:
  "xs ≠ [] ⟹
   <dyn_array xs p>
   pop_array p
   <λ(x, r). dyn_array (butlast xs) r * ↑(x = last xs)>"
@proof @have "last xs = xs ! (length xs - 1)" @qed

setup ‹del_prfstep_thm @{thm dyn_array_def}›

subsection ‹Derived operations›

definition array_swap :: "'a::heap dynamic_array ⇒ nat ⇒ nat ⇒ unit Heap" where
  "array_swap d i j = do {
    x ← array_nth d i;
    y ← array_nth d j;
    array_upd i y d;
    array_upd j x d;
    return ()
   }"

lemma array_swap_rule [hoare_triple]:
  "i < length xs ⟹ j < length xs ⟹
   <dyn_array xs p>
   array_swap p i j
   <λ_. dyn_array (list_swap xs i j) p>" by auto2

end