Theory Pairing_Heap.Pairing_Heap_List1

(* Author: Tobias Nipkow *)

section ‹Pairing Heap According to Okasaki›

theory Pairing_Heap_List1
imports
  "HOL-Library.Multiset"
  "HOL-Library.Pattern_Aliases"
  "HOL-Data_Structures.Priority_Queue_Specs"
begin

subsection ‹Definitions›

text
‹This implementation follows Okasaki \<^cite>‹"Okasaki"›.
It satisfies the invariant that ‹Empty› only occurs
at the root of a pairing heap. The functional correctness proof does not
require the invariant but the amortized analysis (elsewhere) makes use of it.›

datatype 'a heap = Empty | Hp 'a "'a heap list"

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

hide_const (open) insert

context includes pattern_aliases
begin

fun merge :: "('a::linorder) heap ⇒ 'a heap ⇒ 'a heap" where
"merge h Empty = h" |
"merge Empty h = h" |
"merge (Hp x hsx =: hx) (Hp y hsy =: hy) = 
    (if x < y then Hp x (hy # hsx) else Hp y (hx # hsy))"

end

fun insert :: "('a::linorder) ⇒ 'a heap ⇒ 'a heap" where
"insert x h = merge (Hp x []) h"

fun pass⇩1 :: "('a::linorder) heap list ⇒ 'a heap list" where
"pass⇩1 (h1#h2#hs) = merge h1 h2 # pass⇩1 hs" |
"pass⇩1 hs = hs"

fun pass⇩2 :: "('a::linorder) heap list ⇒ 'a heap" where
  "pass⇩2 [] = Empty"
| "pass⇩2 (h#hs) = merge h (pass⇩2 hs)"

fun merge_pairs :: "('a::linorder)  heap list ⇒ 'a heap" where
  "merge_pairs [] = Empty"
| "merge_pairs [h] = h" 
| "merge_pairs (h1 # h2 # hs) = merge (merge h1 h2) (merge_pairs hs)"

fun del_min :: "('a::linorder) heap ⇒ 'a heap" where
  "del_min Empty = Empty"
| "del_min (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 mset_heap :: "'a heap ⇒'a multiset" where
"mset_heap Empty = {#}" |
"mset_heap (Hp x hs) = {#x#} + sum_mset(mset(map mset_heap hs))"

fun pheap :: "('a :: linorder) heap ⇒ bool" where
"pheap Empty = True" |
"pheap (Hp x hs) = (∀h ∈ set hs. (∀y ∈# mset_heap h. x ≤ y) ∧ pheap h)"

lemma pheap_merge: "pheap h1 ⟹ pheap h2 ⟹ pheap (merge h1 h2)"
by (induction h1 h2 rule: merge.induct) fastforce+

lemma pheap_merge_pairs: "∀h ∈ set hs. pheap h ⟹ pheap (merge_pairs hs)"
by (induction hs rule: merge_pairs.induct)(auto simp: pheap_merge)

lemma pheap_insert: "pheap h ⟹ pheap (insert x h)"
by (auto simp: pheap_merge)
(*
lemma pheap_pass1: "∀h ∈ set hs. pheap h ⟹ ∀h ∈ set (pass⇩1 hs). pheap h"
by(induction hs rule: pass⇩1.induct) (auto simp: pheap_merge)

lemma pheap_pass2: "∀h ∈ set hs. pheap h ⟹ pheap (pass⇩2 hs)"
by (induction hs)(auto simp: pheap_merge)
*)
lemma pheap_del_min: "pheap h ⟹ pheap (del_min h)"
by(cases h) (auto simp: pass12_merge_pairs pheap_merge_pairs)


subsubsection ‹Functional Correctness›

lemma mset_heap_empty_iff: "mset_heap h = {#} ⟷ h = Empty"
by (cases h) auto

lemma get_min_in: "h ≠ Empty ⟹ get_min h ∈# mset_heap(h)"
by(induction rule: get_min.induct)(auto)

lemma get_min_min: "⟦ h ≠ Empty; pheap h; x ∈# mset_heap(h) ⟧ ⟹ get_min h ≤ x"
by(induction h rule: get_min.induct)(auto)

lemma get_min: "⟦ pheap h;  h ≠ Empty ⟧ ⟹ get_min h = Min_mset (mset_heap h)"
by (metis Min_eqI finite_set_mset get_min_in get_min_min )

lemma mset_merge: "mset_heap (merge h1 h2) = mset_heap h1 + mset_heap h2"
by(induction h1 h2 rule: merge.induct)(auto simp: add_ac)

lemma mset_insert: "mset_heap (insert a h) = {#a#} + mset_heap h"
by(cases h) (auto simp add: mset_merge insert_def add_ac)

lemma mset_merge_pairs: "mset_heap (merge_pairs hs) = sum_mset(image_mset mset_heap(mset hs))"
by(induction hs rule: merge_pairs.induct)(auto simp: mset_merge)

lemma mset_del_min: "h ≠ Empty ⟹
  mset_heap (del_min h) = mset_heap h - {#get_min h#}"
by(cases h) (auto simp: pass12_merge_pairs mset_merge_pairs)


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

interpretation pairing: Priority_Queue_Merge
where empty = Empty and is_empty = "λh. h = Empty"
and merge = merge and insert = insert
and del_min = del_min and get_min = get_min
and invar = pheap and mset = mset_heap
proof(standard, goal_cases)
  case 1 show ?case by simp
next
  case (2 q) show ?case by (cases q) auto
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_iff)
next
  case 5 thus ?case using get_min mset_heap.simps(1) by blast
next
  case 6 thus ?case by(simp)
next
  case 7 thus ?case by(rule pheap_insert)
next
  case 8 thus ?case by (simp add: pheap_del_min)
next
  case 9 thus ?case by (simp add: mset_merge)
next
  case 10 thus ?case by (simp add: pheap_merge)
qed

end