Theory Ordered_Pairing_Heap_List2

(* Original Author: Tobias Nipkow
   Modified in order to parametrize over the order
*)

section ‹Pairing Heap According to Oksaki (Modified)›

theory Ordered_Pairing_Heap_List2
imports
  "HOL-Library.Multiset"
  "HOL-Data_Structures.Priority_Queue_Specs"
begin

chapter ‹Pairing heaps›


text ‹
  To make it useful we simply parametrized the formalization by the order. We ruse the formalization
  of Tobias Nipkow, but make it ∗‹useful› for refinement by separating node and score. We also need
  to add way to increase the score.›

subsection ‹Definitions›

text ‹This version of pairing heaps is a modified version
of the one by Okasaki \cite{Okasaki} that avoids structural invariants.›

datatype ('b, 'a) hp = Hp (node: 'b) (score: 'a) (hps: "('b, 'a) hp list")

type_synonym ('a, 'b) heap = "('a, 'b) hp option"

hide_const (open) insert

fun get_min  :: "('b, 'a) heap ⇒ 'a" where
"get_min (Some(Hp _ x _)) = x"

text ‹This is basically the useful version:›
fun get_min2  :: "('b, 'a) heap ⇒ 'b" where
"get_min2 (Some(Hp n x _)) = n"


locale pairing_heap_assms =
  fixes lt :: ‹'a ⇒ 'a ⇒ bool› and
    le :: ‹'a ⇒ 'a ⇒ bool›
begin

fun link :: "('b, 'a) hp ⇒ ('b, 'a) hp ⇒ ('b, 'a) hp" where
"link (Hp m x lx) (Hp n y ly) = 
    (if lt x y then Hp m x (Hp n y ly # lx) else Hp n y (Hp m x lx # ly))"

fun merge :: "('b, 'a) heap ⇒ ('b, 'a) heap ⇒ ('b, 'a) heap" where
"merge h None = h" |
"merge None h = h" |
"merge (Some h1) (Some h2) = Some(link h1 h2)"

lemma merge_None[simp]: "merge None h = h"
by(cases h)auto

fun insert :: "'b ⇒ ('a) ⇒ ('b, 'a) heap ⇒ ('b, 'a) heap" where
"insert n x None = Some(Hp n x [])" |
"insert n x (Some h) = Some(link (Hp n x []) h)"

fun pass⇩1 :: "('b, 'a) hp list ⇒ ('b, 'a) hp list" where
  "pass⇩1 [] = []"
| "pass⇩1 [h] = [h]" 
| "pass⇩1 (h1#h2#hs) = link h1 h2 # pass⇩1 hs"

fun pass⇩2 :: "('b, 'a) hp list ⇒ ('b, 'a) heap" where
  "pass⇩2 [] = None"
| "pass⇩2 (h#hs) = Some(case pass⇩2 hs of None ⇒ h | Some h' ⇒ link h h')"

fun merge_pairs :: "('b, 'a) hp list ⇒ ('b, 'a) heap" where
  "merge_pairs [] = None"
| "merge_pairs [h] = Some h" 
| "merge_pairs (h1 # h2 # hs) =
  Some(let h12 = link h1 h2 in case merge_pairs hs of None ⇒ h12 | Some h ⇒ link h12 h)"

fun del_min :: "('b, 'a) heap ⇒ ('b, 'a) heap" where
  "del_min None = None"
| "del_min (Some(Hp _ x hs)) = pass⇩2 (pass⇩1 hs)"

fun (in -)remove_key_children :: ‹'b ⇒ ('b, 'a) hp list ⇒ ('b, 'a) hp list› where
  ‹remove_key_children k [] = []› |
  ‹remove_key_children k ((Hp x n c) # xs) =
  (if k = x then remove_key_children k xs else ((Hp x n (remove_key_children k c)) # remove_key_children k xs))›

fun (in -)remove_key :: ‹'b ⇒ ('b, 'a) hp ⇒ ('b, 'a) heap› where
  ‹remove_key k (Hp x n c) = (if x = k then None else Some (Hp x n (remove_key_children k c)))›

fun (in -)find_key_children :: ‹'b ⇒ ('b, 'a) hp list ⇒ ('b, 'a) heap› where
  ‹find_key_children k [] = None› |
  ‹find_key_children k ((Hp x n c) # xs) =
  (if k = x then Some (Hp x n c) else
  (case find_key_children k c of Some a ⇒ Some a | _ ⇒ find_key_children k xs))›


fun (in -)find_key :: ‹'b ⇒ ('b, 'a) hp ⇒ ('b, 'a) heap› where
  ‹find_key k (Hp x n c) =
  (if k = x then Some (Hp x n c) else find_key_children k c)›

definition decrease_key :: ‹'b ⇒ 'a ⇒ ('b, 'a) hp ⇒ ('b, 'a) heap› where
  ‹decrease_key k s hp = (case find_key k hp of None ⇒ Some hp 
    | (Some (Hp _ _ c)) ⇒
      (case remove_key k hp of
          None ⇒ Some (Hp k s c)
        | Some x ⇒  merge_pairs [Hp k s c, x]))›


subsection ‹Correctness Proofs›

text ‹An optimization:›

lemma pass12_merge_pairs: "pass⇩2 (pass⇩1 hs) = merge_pairs hs"
by (induction hs rule: merge_pairs.induct) (auto split: option.split)

declare pass12_merge_pairs[code_unfold]


subsubsection ‹Invariants›

fun (in -) set_hp :: ‹('b, 'a) hp ⇒ 'a set› where
  ‹set_hp (Hp _ x hs) = ({x} ∪ ⋃(set_hp ` set hs))›


fun php :: "('b, 'a) hp ⇒ bool" where
"php (Hp _ x hs) = (∀h ∈ set hs. (∀y ∈ set_hp h. le x y) ∧ php h)"

definition invar :: "('b, 'a) heap ⇒ bool" where
"invar ho = (case ho of None ⇒ True | Some h ⇒ php h)"
end

locale pairing_heap = pairing_heap_assms lt le
  for lt :: ‹'a ⇒ 'a ⇒ bool› and
    le :: ‹'a ⇒ 'a ⇒ bool› +
  assumes le: ‹⋀a b. le a b ⟷ a = b ∨ lt a b› and
    trans: ‹transp le› and
    transt: ‹transp lt› and
    totalt: ‹totalp lt›
begin

lemma php_link: "php h1 ⟹ php h2 ⟹ php (link h1 h2)"
  apply (induction h1 h2 rule: link.induct)
  apply (auto 4 3 simp: le transt dest: transpD[OF transt] totalpD[OF totalt])
  by (metis totalpD totalt transpD transt)

lemma invar_None[simp]: ‹invar None›
  by (auto simp: invar_def)

lemma invar_merge:
  "⟦ invar h1; invar h2 ⟧ ⟹ invar (merge h1 h2)"
by (auto simp: php_link invar_def split: option.splits)

lemma invar_insert: "invar h ⟹ invar (insert n x h)"
by (auto simp: php_link invar_def split: option.splits)

lemma invar_pass1: "∀h ∈ set hs. php h ⟹ ∀h ∈ set (pass⇩1 hs). php h"
by(induction hs rule: pass⇩1.induct) (auto simp: php_link)

lemma invar_pass2: "∀h ∈ set hs. php h ⟹ invar (pass⇩2 hs)"
by (induction hs)(auto simp: php_link invar_def split: option.splits)

lemma invar_Some: "invar(Some h) = php h"
by(simp add: invar_def)

lemma invar_del_min: "invar h ⟹ invar (del_min h)"
by(induction h rule: del_min.induct)
  (auto simp: invar_Some intro!: invar_pass1 invar_pass2)

lemma (in -)in_remove_key_children_in_childrenD: ‹h ∈ set (remove_key_children k c) ⟹ xa ∈ set_hp h ⟹ xa ∈ ⋃(set_hp ` set c)›
  by (induction k c arbitrary: h rule: remove_key_children.induct)
   (auto split: if_splits)

lemma php_remove_key_children: ‹∀h∈set h1. php h  ⟹ h ∈ set (remove_key_children k h1) ⟹ php h›
  by (induction k h1 arbitrary: h rule: remove_key_children.induct; simp)
   (force simp: decrease_key_def invar_def split: option.splits hp.splits if_splits
    dest: in_remove_key_children_in_childrenD)

lemma php_remove_key: ‹php h1  ⟹ invar (remove_key k h1)›
  by (induction k h1 rule: remove_key.induct)
   (auto simp: decrease_key_def invar_def split: option.splits hp.splits
    dest: in_remove_key_children_in_childrenD
    intro: php_remove_key_children)

lemma invar_find_key_children: ‹∀h∈set c. php h ⟹  invar (find_key_children k c)›
  by (induction k c rule: find_key_children.induct)
   (auto simp: invar_def split: option.splits)

lemma invar_find_key: ‹php h1 ⟹ invar (find_key k h1)›
  by (induction k h1 rule: find_key.induct)
   (use invar_find_key_children[of _ ] in ‹force simp: invar_def›)

lemma (in -)remove_key_None_iff: ‹remove_key k h1 = None ⟷ node h1 = k›
  by (cases ‹(k,h1)› rule: remove_key.cases) auto

lemma php_decrease_key:
  ‹php h1  ⟹ (case (find_key k h1) of None ⇒ True | Some a ⇒ le s (score a)) ⟹ invar (decrease_key k s h1)›
  using invar_find_key[of h1 k, simplified] remove_key_None_iff[of k h1] php_remove_key[of h1 k]
  apply (auto simp: decrease_key_def invar_def php_remove_key php_link
    dest: transpD[OF transt, of _ ‹score (the (find_key k h1))›] totalpD[OF totalt]
    split: option.splits hp.splits)
  apply (meson le local.trans transpE)
  apply (rule php_link)
  apply (auto simp: decrease_key_def invar_def php_remove_key php_link
    split: option.splits hp.splits
    dest: transpD[OF transt, of _ ‹score (the (find_key k h1))›] totalpD[OF totalt])
  apply (meson le local.trans transpE)
  done


subsubsection ‹Functional Correctness›

fun (in -) mset_hp :: "('b, 'a) hp ⇒'a multiset" where
"mset_hp (Hp _ x hs) = {#x#} + sum_mset(mset(map mset_hp hs))"

definition (in -) mset_heap :: "('b, 'a) heap ⇒'a multiset" where
"mset_heap ho = (case ho of None ⇒ {#} | Some h ⇒ mset_hp h)"

lemma (in -) set_mset_mset_hp: "set_mset (mset_hp h) = set_hp h"
by(induction h) auto

lemma (in -) mset_hp_empty[simp]: "mset_hp hp ≠ {#}"
by (cases hp) auto

lemma (in -) mset_heap_Some: "mset_heap(Some hp) = mset_hp hp"
by(simp add: mset_heap_def)

lemma (in -) mset_heap_empty: "mset_heap h = {#} ⟷ h = None"
by (cases h) (auto simp add: mset_heap_def)

lemma (in -)get_min_in:
  "h ≠ None ⟹ get_min h ∈ set_hp(the h)"
by(induction rule: get_min.induct)(auto)

lemma get_min_min: "⟦ h ≠ None; invar h; x ∈ set_hp(the h) ⟧ ⟹ le (get_min h) x"
  by (induction h rule: get_min.induct) (auto simp: invar_def le)


lemma (in pairing_heap_assms) mset_link: "mset_hp (link h1 h2) = mset_hp h1 + mset_hp h2"
by(induction h1 h2 rule: link.induct)(auto simp: add_ac)

lemma (in pairing_heap_assms) mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
by (induction h1 h2 rule: merge.induct)
   (auto simp add: mset_heap_def mset_link ac_simps)

lemma (in pairing_heap_assms) mset_insert: "mset_heap (insert n a h) = {#a#} + mset_heap h"
by(cases h) (auto simp add: mset_link mset_heap_def insert_def)

lemma (in pairing_heap_assms) mset_merge_pairs: "mset_heap (merge_pairs hs) = sum_mset(image_mset mset_hp (mset hs))"
by(induction hs rule: merge_pairs.induct)
  (auto simp: mset_merge mset_link mset_heap_def Let_def split: option.split)

lemma (in pairing_heap_assms) mset_del_min: "h ≠ None ⟹
  mset_heap (del_min h) = mset_heap h - {#get_min h#}"
by(induction h rule: del_min.induct)
  (auto simp: mset_heap_Some pass12_merge_pairs mset_merge_pairs)

text ‹Some more lemmas to make the heaps easier to use:›
lemma invar_merge_pairs:
  "⟦∀h∈set h1. invar (Some h)⟧ ⟹ invar (merge_pairs h1)"
  by (metis invar_Some invar_pass1 invar_pass2 pass12_merge_pairs)

end

context pairing_heap_assms
begin

lemma merge_pairs_None_iff [iff]: "merge_pairs hs = None ⟷ hs = []"
  by (cases hs rule: merge_pairs.cases) auto


end



text ‹Last step: prove all axioms of the priority queue specification with the right sort:›


locale pairing_heap2 =
  fixes ltype :: ‹'a::linorder itself›
begin

sublocale pairing_heap where
    lt =‹(<) :: 'a ⇒ 'a ⇒ bool› and le = ‹(≤)›
  by unfold_locales
     (auto simp: antisymp_def totalp_on_def)

interpretation pairing: Priority_Queue_Merge
where empty = None and is_empty = "λh. h = None"
and merge = merge and insert = ‹insert default›
and del_min = del_min and get_min = get_min
and invar = invar and mset = mset_heap
proof(standard, goal_cases)
  case 1 show ?case by(simp add: mset_heap_def)
next
  case (2 q) thus ?case by(auto simp add: mset_heap_def split: option.split)
next
  case 3 show ?case by(simp add: mset_insert mset_merge)
next
  case 4 thus ?case by(simp add: mset_del_min mset_heap_empty)
next
  case (5 q) thus ?case using get_min_in[of q]
    by(auto simp add: eq_Min_iff get_min_min mset_heap_empty mset_heap_Some set_mset_mset_hp)
next
  case 6 thus ?case by (simp add: invar_def)
next
  case 7 thus ?case by(rule invar_insert)
next
  case 8 thus ?case by (simp add: invar_del_min)
next
  case 9 thus ?case by (simp add: mset_merge)
next
  case 10 thus ?case by (simp add: invar_merge)
qed

end

end