Theory Indexed_PQueue_Impl

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

section ‹Implementation of the indexed priority queue›

theory Indexed_PQueue_Impl
  imports DynamicArray "../Functional/Indexed_PQueue"
begin

text ‹
  Imperative implementation of indexed priority queue. The data structure
  is also verified in \<^cite>‹"Refine_Imperative_HOL-AFP"› by Peter Lammich.
›

datatype 'a indexed_pqueue =
  Indexed_PQueue (pqueue: "(nat × 'a) dynamic_array") (index: "nat option array")
setup ‹add_simple_datatype "indexed_pqueue"›

fun idx_pqueue :: "'a::heap idx_pqueue ⇒ 'a indexed_pqueue ⇒ assn" where
  "idx_pqueue (xs, m) (Indexed_PQueue pq idx) = (dyn_array xs pq * idx ↦⇩a m)"
setup ‹add_rewrite_ent_rule @{thm idx_pqueue.simps}›

subsection ‹Basic operations›

definition idx_pqueue_empty :: "nat ⇒ 'a::heap indexed_pqueue Heap" where
  "idx_pqueue_empty k = do {
    pq ← dyn_array_new;
    idx ← Array.new k None;
    return (Indexed_PQueue pq idx) }"

lemma idx_pqueue_empty_rule [hoare_triple]:
  "<emp>
   idx_pqueue_empty n
   <idx_pqueue ([], replicate n None)>" by auto2

definition idx_pqueue_nth :: "'a::heap indexed_pqueue ⇒ nat ⇒ (nat × 'a) Heap" where
  "idx_pqueue_nth p i = array_nth (pqueue p) i"

lemma idx_pqueue_nth_rule [hoare_triple]:
  "<idx_pqueue (xs, m) p * ↑(i < length xs)>
   idx_pqueue_nth p i
   <λr. idx_pqueue (xs, m) p * ↑(r = xs ! i)>" by auto2

definition idx_nth :: "'a::heap indexed_pqueue ⇒ nat ⇒ nat option Heap" where
  "idx_nth p i = Array.nth (index p) i"

lemma idx_nth_rule [hoare_triple]:
  "<idx_pqueue (xs, m) p * ↑(i < length m)>
   idx_nth p i
   <λr. idx_pqueue (xs, m) p * ↑(r = m ! i)>" by auto2

definition idx_pqueue_length :: "'a indexed_pqueue ⇒ nat Heap" where
  "idx_pqueue_length a = array_length (pqueue a)"

lemma idx_pqueue_length_rule [hoare_triple]:
  "<idx_pqueue (xs, m) p>
   idx_pqueue_length p
   <λr. idx_pqueue (xs, m) p * ↑(r = length xs)>" by auto2

definition idx_pqueue_swap ::
  "'a::{heap,linorder} indexed_pqueue ⇒ nat ⇒ nat ⇒ unit Heap" where
  "idx_pqueue_swap p i j = do {
     pr_i ← array_nth (pqueue p) i;
     pr_j ← array_nth (pqueue p) j;
     Array.upd (fst pr_i) (Some j) (index p);
     Array.upd (fst pr_j) (Some i) (index p);
     array_swap (pqueue p) i j
   }"

lemma idx_pqueue_swap_rule [hoare_triple]:
  "i < length xs ⟹ j < length xs ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   idx_pqueue_swap p i j
   <λ_. idx_pqueue (idx_pqueue_swap_fun (xs, m) i j) p>"
@proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed

definition idx_pqueue_push :: "nat ⇒ 'a::heap ⇒ 'a indexed_pqueue ⇒ 'a indexed_pqueue Heap" where
  "idx_pqueue_push k v p = do {
     len ← array_length (pqueue p);
     d' ← push_array (k, v) (pqueue p);
     Array.upd k (Some len) (index p);
     return (Indexed_PQueue d' (index p))
   }"

lemma idx_pqueue_push_rule [hoare_triple]:
  "k < length m ⟹ ¬has_key_alist xs k ⟹
   <idx_pqueue (xs, m) p>
   idx_pqueue_push k v p
   <idx_pqueue (idx_pqueue_push_fun k v (xs, m))>⇩t"
@proof @unfold "idx_pqueue_push_fun k v (xs, m)" @qed

definition idx_pqueue_pop :: "'a::heap indexed_pqueue ⇒ ((nat × 'a) × 'a indexed_pqueue) Heap" where
  "idx_pqueue_pop p = do {
     (x, d') ← pop_array (pqueue p);
     Array.upd (fst x) None (index p);
     return (x, Indexed_PQueue d' (index p))
   }"

lemma idx_pqueue_pop_rule [hoare_triple]:
  "xs ≠ [] ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   idx_pqueue_pop p
   <λ(x, r). idx_pqueue (idx_pqueue_pop_fun (xs, m)) r * ↑(x = last xs)>"
@proof @unfold "idx_pqueue_pop_fun (xs, m)" @qed

definition idx_pqueue_array_upd :: "nat ⇒ 'a ⇒ 'a::heap dynamic_array ⇒ unit Heap" where
  "idx_pqueue_array_upd i x d = array_upd i x d"

lemma array_upd_idx_pqueue_rule [hoare_triple]:
  "i < length xs ⟹ k = fst (xs ! i) ⟹
   <idx_pqueue (xs, m) p>
   idx_pqueue_array_upd i (k, v) (pqueue p)
   <λ_. idx_pqueue (list_update xs i (k, v), m) p>" by auto2

definition has_key_idx_pqueue :: "nat ⇒ 'a::{heap,linorder} indexed_pqueue ⇒ bool Heap" where
  "has_key_idx_pqueue k p = do {
    i_opt ← Array.nth (index p) k;
    return (i_opt ≠ None) }"

lemma has_key_idx_pqueue_rule [hoare_triple]:
  "k < length m ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   has_key_idx_pqueue k p
   <λr. idx_pqueue (xs, m) p * ↑(r ⟷ has_key_alist xs k)>" by auto2

setup ‹del_prfstep_thm @{thm idx_pqueue.simps}›
setup ‹del_simple_datatype "indexed_pqueue"›

subsection ‹Bubble up and down›

partial_function (heap) idx_bubble_down :: "'a::{heap,linorder} indexed_pqueue ⇒ nat ⇒ unit Heap" where
  "idx_bubble_down a k = do {
    len ← idx_pqueue_length a;
    (if s2 k < len then do {
      vk ← idx_pqueue_nth a k;
      vs1k ← idx_pqueue_nth a (s1 k);
      vs2k ← idx_pqueue_nth a (s2 k);
      (if snd vs1k ≤ snd vs2k then
         if snd vk > snd vs1k then
           do { idx_pqueue_swap a k (s1 k); idx_bubble_down a (s1 k) }
         else return ()
       else
         if snd vk > snd vs2k then
           do { idx_pqueue_swap a k (s2 k); idx_bubble_down a (s2 k) }
         else return ()) }
     else if s1 k < len then do {
       vk ← idx_pqueue_nth a k;
       vs1k ← idx_pqueue_nth a (s1 k);
       (if snd vk > snd vs1k then
          do { idx_pqueue_swap a k (s1 k); idx_bubble_down a (s1 k) }
        else return ()) }
     else return ()) }"

lemma idx_bubble_down_rule [hoare_triple]:
  "index_of_pqueue x ⟹
   <idx_pqueue x a>
   idx_bubble_down a k
   <λ_. idx_pqueue (idx_bubble_down_fun x k) a>"
@proof @fun_induct "idx_bubble_down_fun x k" @with
  @subgoal "(x = (xs, m), k = k)"
  @unfold "idx_bubble_down_fun (xs, m) k"
  @case "s2 k < length xs" @with
    @case "snd (xs ! s1 k) ≤ snd (xs ! s2 k)"
  @end
  @case "s1 k < length xs" @end
@qed

partial_function (heap) idx_bubble_up :: "'a::{heap,linorder} indexed_pqueue ⇒ nat ⇒ unit Heap" where
  "idx_bubble_up a k =
    (if k = 0 then return () else do {
       len ← idx_pqueue_length a;
       (if k < len then do {
          vk ← idx_pqueue_nth a k;
          vpk ← idx_pqueue_nth a (par k);
          (if snd vk < snd vpk then
             do { idx_pqueue_swap a k (par k); idx_bubble_up a (par k) }
           else return ()) }
        else return ())})"

lemma idx_bubble_up_rule [hoare_triple]:
  "index_of_pqueue x ⟹
   <idx_pqueue x a>
   idx_bubble_up a k
   <λ_. idx_pqueue (idx_bubble_up_fun x k) a>"
@proof @fun_induct "idx_bubble_up_fun x k" @with
  @subgoal "(x = (xs, m), k = k)"
  @unfold "idx_bubble_up_fun (xs, m) k" @end
@qed

subsection ‹Main operations›

definition delete_min_idx_pqueue :: "'a::{heap,linorder} indexed_pqueue ⇒ ((nat × 'a) × 'a indexed_pqueue) Heap" where
  "delete_min_idx_pqueue p = do {
     len ← idx_pqueue_length p;
     if len = 0 then raise STR ''delete_min''
     else do {
       idx_pqueue_swap p 0 (len - 1);
       (x', r) ← idx_pqueue_pop p;
       idx_bubble_down r 0;
       return (x', r)
     }
   }"

lemma delete_min_idx_pqueue_rule [hoare_triple]:
  "xs ≠ [] ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   delete_min_idx_pqueue p
   <λ(x, r). idx_pqueue (snd (delete_min_idx_pqueue_fun (xs, m))) r *
       ↑(x = fst (delete_min_idx_pqueue_fun (xs, m)))>"
@proof @unfold "delete_min_idx_pqueue_fun (xs, m)" @qed

definition insert_idx_pqueue :: "nat ⇒ 'a::{heap,linorder} ⇒ 'a indexed_pqueue ⇒ 'a indexed_pqueue Heap" where
  "insert_idx_pqueue k v p = do {
     p' ← idx_pqueue_push k v p;
     len ← idx_pqueue_length p';
     idx_bubble_up p' (len - 1);
     return p'
   }"

lemma insert_idx_pqueue_rule [hoare_triple]:
  "k < length m ⟹ ¬has_key_alist xs k ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   insert_idx_pqueue k v p
   <idx_pqueue (insert_idx_pqueue_fun k v (xs, m))>⇩t"
@proof @unfold "insert_idx_pqueue_fun k v (xs, m)" @qed

definition update_idx_pqueue ::
  "nat ⇒ 'a::{heap,linorder} ⇒ 'a indexed_pqueue ⇒ 'a indexed_pqueue Heap" where
  "update_idx_pqueue k v p = do {
    i_opt ← idx_nth p k;
    case i_opt of
      None ⇒ insert_idx_pqueue k v p
    | Some i ⇒ do {
      x ← idx_pqueue_nth p i;
      idx_pqueue_array_upd i (k, v) (pqueue p);
      (if snd x ≤ v then do {idx_bubble_down p i; return p}
       else do {idx_bubble_up p i; return p}) }}"

lemma update_idx_pqueue_rule [hoare_triple]:
  "k < length m ⟹ index_of_pqueue (xs, m) ⟹
   <idx_pqueue (xs, m) p>
   update_idx_pqueue k v p
   <idx_pqueue (update_idx_pqueue_fun k v (xs, m))>⇩t"
@proof @unfold "update_idx_pqueue_fun k v (xs, m)" @qed

subsection ‹Outer interface›

text ‹Express Hoare triples for indexed priority queue operations in terms of
  the mapping represented by the queue.›
definition idx_pqueue_map :: "(nat, 'a::{heap,linorder}) map ⇒ nat ⇒ 'a indexed_pqueue ⇒ assn" where
  "idx_pqueue_map M n p = (∃⇩Axs m. idx_pqueue (xs, m) p *
      ↑(index_of_pqueue (xs, m)) * ↑(is_heap xs) * ↑(M = map_of_alist xs) * ↑(n = length m))"
setup ‹add_rewrite_ent_rule @{thm idx_pqueue_map_def}›

lemma heap_implies_hd_min2 [resolve]:
  "is_heap xs ⟹ xs ≠ [] ⟹ (map_of_alist xs)⟨k⟩ = Some v ⟹ snd (hd xs) ≤ v"
@proof
  @obtain i where "i < length xs" "xs ! i = (k, v)"
  @have "snd (hd xs) ≤ snd (xs ! i)"
@qed

theorem idx_pqueue_empty_map [hoare_triple]:
  "<emp>
   idx_pqueue_empty n
   <idx_pqueue_map empty_map n>" by auto2

theorem delete_min_idx_pqueue_map [hoare_triple]:
  "<idx_pqueue_map M n p * ↑(M ≠ empty_map)>
   delete_min_idx_pqueue p
   <λ(x, r). idx_pqueue_map (delete_map (fst x) M) n r * ↑(fst x < n) *
                ↑(is_heap_min (fst x) M) * ↑(M⟨fst x⟩ = Some (snd x))>" by auto2

theorem insert_idx_pqueue_map [hoare_triple]:
  "k < n ⟹ k ∉ keys_of M ⟹
   <idx_pqueue_map M n p>
   insert_idx_pqueue k v p
   <idx_pqueue_map (M {k → v}) n>⇩t" by auto2

theorem has_key_idx_pqueue_map [hoare_triple]:
  "k < n ⟹
   <idx_pqueue_map M n p>
   has_key_idx_pqueue k p
   <λr. idx_pqueue_map M n p * ↑(r ⟷ k ∈ keys_of M)>" by auto2

theorem update_idx_pqueue_map [hoare_triple]:
  "k < n ⟹
   <idx_pqueue_map M n p>
   update_idx_pqueue k v p
   <idx_pqueue_map (M {k → v}) n>⇩t" by auto2

setup ‹del_prfstep_thm @{thm idx_pqueue_map_def}›

end