Theory Indexed_PQueue

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

section ‹Indexed priority queues›

theory Indexed_PQueue
  imports Arrays_Ex Mapping_Str
begin

text ‹
  Verification of indexed priority queue: functional part. The data
  structure is also verified by Lammich in
  \<^cite>‹"Refine_Imperative_HOL-AFP"›.
›

subsection ‹Successor functions, eq-pred predicate›

fun s1 :: "nat ⇒ nat" where "s1 m = 2 * m + 1"
fun s2 :: "nat ⇒ nat" where "s2 m = 2 * m + 2"

lemma s_inj [forward]:
  "s1 m = s1 m' ⟹ m = m'" "s2 m = s2 m' ⟹ m = m'" by auto
lemma s_neq [resolve]:
  "s1 m ≠ s2 m'" "s1 m > m" "s2 m > m" "s2 m > s1 m" using s1.simps s2.simps by presburger+
setup ‹add_forward_prfstep_cond @{thm s_neq(2)} [with_term "s1 ?m"]›
setup ‹add_forward_prfstep_cond @{thm s_neq(3)} [with_term "s2 ?m"]›
setup ‹add_forward_prfstep_cond @{thm s_neq(4)} [with_term "s2 ?m", with_term "s1 ?m"]›

inductive eq_pred :: "nat ⇒ nat ⇒ bool" where
  "eq_pred n n"
| "eq_pred n m ⟹ eq_pred n (s1 m)"
| "eq_pred n m ⟹ eq_pred n (s2 m)"
setup ‹add_case_induct_rule @{thm eq_pred.cases}›
setup ‹add_prop_induct_rule @{thm eq_pred.induct}›
setup ‹add_resolve_prfstep @{thm eq_pred.intros(1)}›
setup ‹fold add_backward_prfstep @{thms eq_pred.intros(2,3)}›

lemma eq_pred_parent1 [forward]:
  "eq_pred i (s1 k) ⟹ i ≠ s1 k ⟹ eq_pred i k"
@proof @let "v = s1 k" @prop_induct "eq_pred i v" @qed

lemma eq_pred_parent2 [forward]:
  "eq_pred i (s2 k) ⟹ i ≠ s2 k ⟹ eq_pred i k"
@proof @let "v = s2 k" @prop_induct "eq_pred i v" @qed

lemma eq_pred_cases:
  "eq_pred i j ⟹ eq_pred (s1 i) j ∨ eq_pred (s2 i) j ∨ j = i ∨ j = s1 i ∨ j = s2 i"
@proof @prop_induct "eq_pred i j" @qed
setup ‹add_forward_prfstep_cond @{thm eq_pred_cases} [with_cond "?i ≠ s1 ?k", with_cond "?i ≠ s2 ?k"]›

lemma eq_pred_le [forward]: "eq_pred i j ⟹ i ≤ j"
@proof @prop_induct "eq_pred i j" @qed

subsection ‹Heap property›

text ‹The corresponding tree is a heap›
definition is_heap :: "('a × 'b::linorder) list ⇒ bool" where [rewrite]:
  "is_heap xs = (∀i j. eq_pred i j ⟶ j < length xs ⟶ snd (xs ! i) ≤ snd (xs ! j))"

lemma is_heapD:
  "is_heap xs ⟹ j < length xs ⟹ eq_pred i j ⟹ snd (xs ! i) ≤ snd (xs ! j)" by auto2
setup ‹add_forward_prfstep_cond @{thm is_heapD} [with_term "?xs ! ?j"]›
setup ‹del_prfstep_thm_eqforward @{thm is_heap_def}›

subsection ‹Bubble-down›

text ‹The corresponding tree is a heap, except k is not necessarily smaller than its descendents.›
definition is_heap_partial1 :: "('a × 'b::linorder) list ⇒ nat ⇒ bool" where [rewrite]:
  "is_heap_partial1 xs k = (∀i j. eq_pred i j ⟶ i ≠ k ⟶ j < length xs ⟶ snd (xs ! i) ≤ snd (xs ! j))"

text ‹Two cases of switching with s1 k.›
lemma bubble_down1:
  "s1 k < length xs ⟹ is_heap_partial1 xs k ⟹ snd (xs ! k) > snd (xs ! s1 k) ⟹
   snd (xs ! s1 k) ≤ snd (xs ! s2 k) ⟹ is_heap_partial1 (list_swap xs k (s1 k)) (s1 k)" by auto2
setup ‹add_forward_prfstep_cond @{thm bubble_down1} [with_term "list_swap ?xs ?k (s1 ?k)"]›

lemma bubble_down2:
  "s1 k < length xs ⟹ is_heap_partial1 xs k ⟹ snd (xs ! k) > snd (xs ! s1 k) ⟹
   s2 k ≥ length xs ⟹ is_heap_partial1 (list_swap xs k (s1 k)) (s1 k)" by auto2
setup ‹add_forward_prfstep_cond @{thm bubble_down2} [with_term "list_swap ?xs ?k (s1 ?k)"]›

text ‹One case of switching with s2 k.›
lemma bubble_down3:
  "s2 k < length xs ⟹ is_heap_partial1 xs k ⟹ snd (xs ! s1 k) > snd (xs ! s2 k) ⟹
   snd (xs ! k) > snd (xs ! s2 k) ⟹ xs' = list_swap xs k (s2 k) ⟹ is_heap_partial1 xs' (s2 k)" by auto2
setup ‹add_forward_prfstep_cond @{thm bubble_down3} [with_term "?xs'"]›

subsection ‹Bubble-up›

fun par :: "nat ⇒ nat" where
  "par m = (m - 1) div 2"
setup ‹register_wellform_data ("par m", ["m ≠ 0"])›

lemma ps_inverse [rewrite]: "par (s1 k) = k" "par (s2 k) = k" by simp+

lemma p_basic: "m ≠ 0 ⟹ par m < m" by auto
setup ‹add_forward_prfstep_cond @{thm p_basic} [with_term "par ?m"]›

lemma p_cases: "m ≠ 0 ⟹ m = s1 (par m) ∨ m = s2 (par m)" by auto
setup ‹add_forward_prfstep_cond @{thm p_cases} [with_term "par ?m"]›

lemma eq_pred_p_next:
  "i ≠ 0 ⟹ eq_pred i j ⟹ eq_pred (par i) j"
@proof @prop_induct "eq_pred i j" @qed
setup ‹add_forward_prfstep_cond @{thm eq_pred_p_next} [with_term "par ?i"]›

lemma heap_implies_hd_min [resolve]:
  "is_heap xs ⟹ i < length xs ⟹ xs ≠ [] ⟹ snd (hd xs) ≤ snd (xs ! i)"
@proof
  @strong_induct i
  @case "i = 0" @apply_induct_hyp "par i"
  @have "eq_pred (par i) i"
@qed

text ‹The corresponding tree is a heap, except k is not necessarily greater than its ancestors.›
definition is_heap_partial2 :: "('a × 'b::linorder) list ⇒ nat ⇒ bool" where [rewrite]:
  "is_heap_partial2 xs k = (∀i j. eq_pred i j ⟶ j < length xs ⟶ j ≠ k ⟶ snd (xs ! i) ≤ snd (xs ! j))"

lemma bubble_up1 [forward]:
  "k < length xs ⟹ is_heap_partial2 xs k ⟹ snd (xs ! k) < snd (xs ! par k) ⟹ k ≠ 0 ⟹
   is_heap_partial2 (list_swap xs k (par k)) (par k)" by auto2

lemma bubble_up2 [forward]:
  "k < length xs ⟹ is_heap_partial2 xs k ⟹ snd (xs ! k) ≥ snd (xs ! par k) ⟹ k ≠ 0 ⟹
   is_heap xs" by auto2
setup ‹del_prfstep_thm @{thm p_cases}›

subsection ‹Indexed priority queue›

type_synonym 'a idx_pqueue = "(nat × 'a) list × nat option list"

fun index_of_pqueue :: "'a idx_pqueue ⇒ bool" where
  "index_of_pqueue (xs, m) = (
    (∀i<length xs. fst (xs ! i) < length m ∧ m ! (fst (xs ! i)) = Some i) ∧
    (∀i. ∀k<length m. m ! k = Some i ⟶ i < length xs ∧ fst (xs ! i) = k))"
setup ‹add_rewrite_rule @{thm index_of_pqueue.simps}›

lemma index_of_pqueueD1:
  "i < length xs ⟹ index_of_pqueue (xs, m) ⟹
   fst (xs ! i) < length m ∧ m ! (fst (xs ! i)) = Some i" by auto2
setup ‹add_forward_prfstep_cond @{thm index_of_pqueueD1} [with_term "?xs ! ?i"]›

lemma index_of_pqueueD2 [forward]:
  "k < length m ⟹ index_of_pqueue (xs, m) ⟹
   m ! k = Some i ⟹ i < length xs ∧ fst (xs ! i) = k" by auto2

lemma index_of_pqueueD3 [forward]:
  "index_of_pqueue (xs, m) ⟹ p ∈ set xs ⟹ fst p < length m"
@proof @obtain i where "i < length xs" "xs ! i = p" @qed
setup ‹del_prfstep_thm_eqforward @{thm index_of_pqueue.simps}›

lemma has_index_unique_key [forward]:
  "index_of_pqueue (xs, m) ⟹ unique_keys_set (set xs)"
@proof
  @have "∀a x y. (a, x) ∈ set xs ⟶ (a, y) ∈ set xs ⟶ x = y" @with
    @obtain i where "i < length xs" "xs ! i = (a, x)"
    @obtain j where "j < length xs" "xs ! j = (a, y)"
  @end
@qed

lemma has_index_keys_of [rewrite]:
  "index_of_pqueue (xs, m) ⟹ has_key_alist xs k ⟷ (k < length m ∧ m ! k ≠ None)"
@proof
  @case "has_key_alist xs k" @with
    @obtain v' where "(k, v') ∈ set xs"
    @obtain i where "i < length xs ∧ xs ! i = (k, v')"
  @end
@qed

lemma has_index_distinct [forward]:
  "index_of_pqueue (xs, m) ⟹ distinct xs"
@proof
  @have "∀i<length xs. ∀j<length xs. i ≠ j ⟶ xs ! i ≠ xs ! j"
@qed

subsection ‹Basic operations on indexed\_queue›

fun idx_pqueue_swap_fun :: "(nat × 'a) list × nat option list ⇒ nat ⇒ nat ⇒ (nat × 'a) list × nat option list" where
  "idx_pqueue_swap_fun (xs, m) i j = (
    list_swap xs i j, ((m [fst (xs ! i) := Some j]) [fst (xs ! j) := Some i]))"

lemma index_of_pqueue_swap [forward_arg]:
  "i < length xs ⟹ j < length xs ⟹ index_of_pqueue (xs, m) ⟹
   index_of_pqueue (idx_pqueue_swap_fun (xs, m) i j)"
@proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed

lemma fst_idx_pqueue_swap [rewrite]:
  "fst (idx_pqueue_swap_fun (xs, m) i j) = list_swap xs i j"
@proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed

lemma snd_idx_pqueue_swap [rewrite]:
  "length (snd (idx_pqueue_swap_fun (xs, m) i j)) = length m"
@proof @unfold "idx_pqueue_swap_fun (xs, m) i j" @qed

fun idx_pqueue_push_fun :: "nat ⇒ 'a ⇒ 'a idx_pqueue ⇒ 'a idx_pqueue" where
  "idx_pqueue_push_fun k v (xs, m) = (xs @ [(k, v)], list_update m k (Some (length xs)))"

lemma idx_pqueue_push_correct [forward_arg]:
  "index_of_pqueue (xs, m) ⟹ k < length m ⟹ ¬has_key_alist xs k ⟹
   r = idx_pqueue_push_fun k v (xs, m) ⟹
   index_of_pqueue r ∧ fst r = xs @ [(k, v)] ∧ length (snd r) = length m"
@proof @unfold "idx_pqueue_push_fun k v (xs, m)" @qed

fun idx_pqueue_pop_fun :: "'a idx_pqueue ⇒ 'a idx_pqueue" where
  "idx_pqueue_pop_fun (xs, m) = (butlast xs, list_update m (fst (last xs)) None)"

lemma idx_pqueue_pop_correct [forward_arg]:
  "index_of_pqueue (xs, m) ⟹ xs ≠ [] ⟹ r = idx_pqueue_pop_fun (xs, m) ⟹
   index_of_pqueue r ∧ fst r = butlast xs ∧ length (snd r) = length m"
@proof
  @unfold "idx_pqueue_pop_fun (xs, m)"
  @have "length xs = length (butlast xs) + 1"
  @have "fst (xs ! length (butlast xs)) < length m"  (* TODO: remove? *)
@qed

subsection ‹Bubble up and down›

function idx_bubble_down_fun :: "'a::linorder idx_pqueue ⇒ nat ⇒ 'a idx_pqueue" where
  "idx_bubble_down_fun (xs, m) k = (
    if s2 k < length xs then
      if snd (xs ! s1 k) ≤ snd (xs ! s2 k) then
        if snd (xs ! k) > snd (xs ! s1 k) then
          idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s1 k)) (s1 k)
        else (xs, m)
      else
        if snd (xs ! k) > snd (xs ! s2 k) then
          idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s2 k)) (s2 k)
        else (xs, m)
    else if s1 k < length xs then
      if snd (xs ! k) > snd (xs ! s1 k) then
        idx_bubble_down_fun (idx_pqueue_swap_fun (xs, m) k (s1 k)) (s1 k)
      else (xs, m)
    else (xs, m))"
  by pat_completeness auto
  termination by (relation "measure (λ((xs,_),k). (length xs - k))") (simp_all, auto2+)

lemma idx_bubble_down_fun_correct:
  "r = idx_bubble_down_fun x k ⟹ is_heap_partial1 (fst x) k ⟹
   is_heap (fst r) ∧ mset (fst r) = mset (fst x) ∧ length (snd r) = length (snd x)"
@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
setup ‹add_forward_prfstep_cond @{thm idx_bubble_down_fun_correct} [with_term "?r"]›

lemma idx_bubble_down_fun_correct2 [forward]:
  "index_of_pqueue x ⟹ index_of_pqueue (idx_bubble_down_fun x k)"
@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

fun idx_bubble_up_fun :: "'a::linorder idx_pqueue ⇒ nat ⇒ 'a idx_pqueue" where
  "idx_bubble_up_fun (xs, m) k = (
    if k = 0 then (xs, m)
    else if k < length xs then
      if snd (xs ! k) < snd (xs ! par k) then
        idx_bubble_up_fun (idx_pqueue_swap_fun (xs, m) k (par k)) (par k)
      else (xs, m)
    else (xs, m))"

lemma idx_bubble_up_fun_correct:
  "r = idx_bubble_up_fun x k ⟹ is_heap_partial2 (fst x) k ⟹
   is_heap (fst r) ∧ mset (fst r) = mset (fst x) ∧ length (snd r) = length (snd x)"
@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
setup ‹add_forward_prfstep_cond @{thm idx_bubble_up_fun_correct} [with_term "?r"]›

lemma idx_bubble_up_fun_correct2 [forward]:
  "index_of_pqueue x ⟹ index_of_pqueue (idx_bubble_up_fun x k)"
@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›

fun delete_min_idx_pqueue_fun :: "'a::linorder idx_pqueue ⇒ (nat × 'a) × 'a idx_pqueue" where
  "delete_min_idx_pqueue_fun (xs, m) = (
    let (xs', m') = idx_pqueue_swap_fun (xs, m) 0 (length xs - 1);
        a'' = idx_pqueue_pop_fun (xs', m')
     in (last xs', idx_bubble_down_fun a'' 0))"

lemma delete_min_idx_pqueue_correct:
  "index_of_pqueue (xs, m) ⟹ xs ≠ [] ⟹ res = delete_min_idx_pqueue_fun (xs, m) ⟹
   index_of_pqueue (snd res)"
@proof @unfold "delete_min_idx_pqueue_fun (xs, m)" @qed
setup ‹add_forward_prfstep_cond @{thm delete_min_idx_pqueue_correct} [with_term "?res"]›

lemma hd_last_swap_eval_last [rewrite]:
  "xs ≠ [] ⟹ last (list_swap xs 0 (length xs - 1)) = hd xs"
@proof
  @let "xs' = list_swap xs 0 (length xs - 1)"
  @have "last xs' = xs' ! (length xs - 1)"
@qed

text ‹Correctness of delete-min.›
theorem delete_min_idx_pqueue_correct2:
  "is_heap xs ⟹ xs ≠ [] ⟹ res = delete_min_idx_pqueue_fun (xs, m) ⟹ index_of_pqueue (xs, m) ⟹
   is_heap (fst (snd res)) ∧ fst res = hd xs ∧ length (snd (snd res)) = length m ∧
   map_of_alist (fst (snd res)) = delete_map (fst (fst res)) (map_of_alist xs)"
@proof @unfold "delete_min_idx_pqueue_fun (xs, m)"
  @let "xs' = list_swap xs 0 (length xs - 1)"
  @have "is_heap_partial1 (butlast xs') 0"
@qed
setup ‹add_forward_prfstep_cond @{thm delete_min_idx_pqueue_correct2} [with_term "?res"]›

fun insert_idx_pqueue_fun :: "nat ⇒ 'a::linorder ⇒ 'a idx_pqueue ⇒ 'a idx_pqueue" where
  "insert_idx_pqueue_fun k v x = (
    let x' = idx_pqueue_push_fun k v x in
      idx_bubble_up_fun x' (length (fst x') - 1))"

lemma insert_idx_pqueue_correct [forward_arg]:
  "index_of_pqueue (xs, m) ⟹ k < length m ⟹ ¬has_key_alist xs k ⟹
   index_of_pqueue (insert_idx_pqueue_fun k v (xs, m))"
@proof @unfold "insert_idx_pqueue_fun k v (xs, m)" @qed

text ‹Correctness of insertion.›
theorem insert_idx_pqueue_correct2:
  "index_of_pqueue (xs, m) ⟹ is_heap xs ⟹ k < length m ⟹ ¬has_key_alist xs k ⟹
   r = insert_idx_pqueue_fun k v (xs, m) ⟹
   is_heap (fst r) ∧ length (snd r) = length m ∧
   map_of_alist (fst r) = map_of_alist xs { k → v }"
@proof @unfold "insert_idx_pqueue_fun k v (xs, m)"
  @have "is_heap_partial2 (xs @ [(k, v)]) (length xs)"
@qed
setup ‹add_forward_prfstep_cond @{thm insert_idx_pqueue_correct2} [with_term "?r"]›

fun update_idx_pqueue_fun :: "nat ⇒ 'a::linorder ⇒ 'a idx_pqueue ⇒ 'a idx_pqueue" where
  "update_idx_pqueue_fun k v (xs, m) = (
    if m ! k = None then
      insert_idx_pqueue_fun k v (xs, m)
    else let
      i = the (m ! k);
      xs' = list_update xs i (k, v)
    in
      if snd (xs ! i) ≤ v then idx_bubble_down_fun (xs', m) i
      else idx_bubble_up_fun (xs', m) i)"

lemma update_idx_pqueue_correct [forward_arg]:
  "index_of_pqueue (xs, m) ⟹ k < length m ⟹
   index_of_pqueue (update_idx_pqueue_fun k v (xs, m))"
@proof @unfold "update_idx_pqueue_fun k v (xs, m)"
  @let "i' = the (m ! k)"
  @let "xs' = list_update xs i' (k, v)"
  @case "m ! k = None"
  @have "index_of_pqueue (xs', m)"
@qed

text ‹Correctness of update.›
theorem update_idx_pqueue_correct2:
  "index_of_pqueue (xs, m) ⟹ is_heap xs ⟹ k < length m ⟹
   r = update_idx_pqueue_fun k v (xs, m) ⟹
   is_heap (fst r) ∧ length (snd r) = length m ∧
   map_of_alist (fst r) = map_of_alist xs { k → v }"
@proof @unfold "update_idx_pqueue_fun k v (xs, m)"
  @let "i = the (m ! k)"
  @let "xs' = list_update xs i (k, v)"
  @have "xs' = fst (xs', m)" (* TODO: remove *)
  @case "m ! k = None"
  @case "snd (xs ! the (m ! k)) ≤ v" @with
    @have "is_heap_partial1 xs' i"
  @end
  @have "is_heap_partial2 xs' i"
@qed
setup ‹add_forward_prfstep_cond @{thm update_idx_pqueue_correct2} [with_term "?r"]›

end