Theory Pairing_Heap.Pairing_Heap_List2

(* Author: Tobias Nipkow *)

section ‹Pairing Heap According to Oksaki (Modified)›

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

subsection ‹Definitions›

text ‹This version of pairing heaps is a modified version
of the one by Okasaki \<^cite>‹"Okasaki"› that avoids structural invariants.›

datatype 'a hp = Hp 'a (hps: "'a hp list")

type_synonym 'a heap = "'a hp option"

hide_const (open) insert

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


fun link :: "('a::linorder) hp ⇒ 'a hp ⇒ 'a hp" where
"link (Hp x lx) (Hp y ly) = 
    (if x < y then Hp x (Hp y ly # lx) else Hp y (Hp x lx # ly))"

fun merge :: "('a::linorder) heap ⇒ 'a heap ⇒ '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 :: "('a::linorder) ⇒ 'a heap ⇒ 'a heap" where
"insert x None = Some(Hp x [])" |
"insert x (Some h) = Some(link (Hp x []) h)"

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

fun pass⇩2 :: "('a::linorder) hp list ⇒ '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 :: "('a::linorder) hp list ⇒ '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 :: "('a::linorder) heap ⇒ 'a heap" where
  "del_min None = None"
| "del_min (Some(Hp x hs)) = pass⇩2 (pass⇩1 hs)"


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 php :: "('a::linorder) hp ⇒ bool" where
"php (Hp x hs) = (∀h ∈ set hs. (∀y ∈ set_hp h. x ≤ y) ∧ php h)"

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

lemma php_link: "php h1 ⟹ php h2 ⟹ php (link h1 h2)"
by (induction h1 h2 rule: link.induct) fastforce+

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 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)


subsubsection ‹Functional Correctness›

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

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

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

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

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

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

lemma 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) ⟧ ⟹ get_min h ≤ x"
by(induction h rule: get_min.induct)(auto simp: invar_def)


lemma 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 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 mset_insert: "mset_heap (insert a h) = {#a#} + mset_heap h"
by(cases h) (auto simp add: mset_link mset_heap_def insert_def)

lemma 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 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 ‹Last step: prove all axioms of the priority queue specification:›

interpretation pairing: Priority_Queue_Merge
where empty = None and is_empty = "λh. h = None"
and merge = merge and insert = insert
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