Theory Pairing_Heap.Pairing_Heap_Tree

(* Author: Hauke Brinkop and Tobias Nipkow *)

section ‹Pairing Heap in Binary Tree Representation›

theory Pairing_Heap_Tree
imports  
  "HOL-Library.Tree_Multiset"
  "HOL-Data_Structures.Priority_Queue_Specs"
begin

subsection ‹Definitions›

text ‹Pairing heaps \<^cite>‹"FredmanSST86"›
in their original representation as binary trees.›

fun get_min  :: "'a :: linorder tree ⇒ 'a" where
"get_min (Node _ x _) = x"

fun link :: "('a::linorder) tree ⇒ 'a tree" where
"link (Node hsx x (Node hsy y hs)) = 
   (if x < y then Node (Node hsy y hsx) x hs else Node (Node hsx x hsy) y hs)" |
"link t = t"

fun pass⇩1 :: "('a::linorder) tree ⇒ 'a tree" where
"pass⇩1 (Node hsx x (Node hsy y hs)) = link (Node hsx x (Node hsy y (pass⇩1 hs)))" |
"pass⇩1 hs = hs"

fun pass⇩2 :: "('a::linorder) tree ⇒ 'a tree" where
"pass⇩2 (Node hsx x hs) = link(Node hsx x (pass⇩2 hs))" |
"pass⇩2 Leaf = Leaf"

fun del_min :: "('a::linorder) tree ⇒ 'a tree" where
  "del_min Leaf = Leaf"
| "del_min (Node hs _ Leaf) = pass⇩2 (pass⇩1 hs)"

fun merge :: "('a::linorder) tree ⇒ 'a tree ⇒ 'a tree" where
  "merge Leaf hp = hp"
| "merge hp Leaf = hp"
| "merge (Node hsx x Leaf) (Node hsy y Leaf) = link (Node hsx x (Node hsy y Leaf))"

fun insert :: "('a::linorder) ⇒ 'a tree ⇒ 'a tree" where
"insert x hp = merge (Node Leaf x Leaf) hp"

text ‹The invariant is the conjunction of ‹is_root› and ‹pheap›:›

fun is_root :: "'a tree ⇒ bool" where
  "is_root hp = (case hp of Leaf ⇒ True | Node l x r ⇒ r = Leaf)"

fun pheap :: "('a :: linorder) tree ⇒ bool" where
"pheap Leaf = True" |
"pheap (Node l x r) = ((∀y ∈ set_tree l. x ≤ y) ∧ pheap l ∧ pheap r)"


subsection ‹Correctness Proofs›

subsubsection ‹Invariants›

lemma link_struct: "∃l a. link (Node hsx x (Node hsy y hs)) = Node l a hs" 
by simp

lemma pass⇩1_struct: "∃l a r. pass⇩1 (Node hs1 x hs) = Node l a r" 
by (cases hs) simp_all

lemma pass⇩2_struct: "∃l a. pass⇩2 (Node hs1 x hs) = Node l a Leaf" 
by(induction hs arbitrary: hs1 x rule: pass⇩2.induct) (auto, metis link_struct)

lemma is_root_merge:
  "is_root h1 ⟹ is_root h2 ⟹ is_root (merge h1 h2)"
by (simp split: tree.splits)

lemma is_root_insert: "is_root h ⟹ is_root (insert x h)"
by (simp split: tree.splits)

lemma is_root_del_min:
  assumes "is_root h" shows "is_root (del_min h)"
proof (cases h)
  case [simp]: (Node lx x rx)
  have "rx = Leaf" using assms by simp
  thus ?thesis 
  proof (cases lx)
    case (Node ly y ry)
    then obtain la a ra where "pass⇩1 lx = Node a la ra" 
      using pass⇩1_struct by blast
    moreover obtain lb b where "pass⇩2 … = Node b lb Leaf"
      using pass⇩2_struct by blast
    ultimately show ?thesis using assms by simp
  qed simp
qed simp

lemma pheap_merge:
  "⟦ is_root h1; is_root h2; pheap h1; pheap h2 ⟧ ⟹ pheap (merge h1 h2)"
by (auto split: tree.splits)

lemma pheap_insert: "is_root h ⟹ pheap h ⟹ pheap (insert x h)"
by (auto split: tree.splits)

lemma pheap_link: "t ≠ Leaf ⟹ pheap t ⟹ pheap (link t)"
by(induction t rule: link.induct)(auto)

lemma pheap_pass1: "pheap h ⟹ pheap (pass⇩1 h)"
by(induction h rule: pass⇩1.induct) (auto)

lemma pheap_pass2: "pheap h ⟹ pheap (pass⇩2 h)"
by (induction h)(auto simp: pheap_link)

lemma pheap_del_min: "is_root h ⟹ pheap h ⟹ pheap (del_min h)"
by (auto simp: pheap_pass1 pheap_pass2 split: tree.splits)


subsubsection ‹Functional Correctness›

lemma get_min_in:
  "h ≠ Leaf ⟹ get_min h ∈ set_tree h"
by(auto simp add: neq_Leaf_iff)

lemma get_min_min: "⟦ is_root h; pheap h; x ∈ set_tree h ⟧ ⟹ get_min h ≤ x"
by(auto split: tree.splits)


lemma mset_link: "mset_tree (link t) = mset_tree t"
by(cases t rule: link.cases)(auto simp: add_ac)

lemma mset_pass⇩1: "mset_tree (pass⇩1 h) = mset_tree h"
by (induction h rule: pass⇩1.induct) auto

lemma mset_pass⇩2: "mset_tree (pass⇩2 h) = mset_tree h"
by (induction h rule: pass⇩2.induct) (auto simp: mset_link)

lemma mset_merge: "⟦ is_root h1; is_root h2 ⟧
 ⟹  mset_tree (merge h1 h2) = mset_tree h1 + mset_tree h2"
by (induction h1 h2 rule: merge.induct) (auto simp add: ac_simps)
(*
lemma mset_merge_pairs: "mset_tree (merge_pairs h) = mset_tree h"
by(induction h rule: merge_pairs.induct)(auto simp: mset_link add_ac)
*)
lemma mset_del_min: "⟦ is_root h; t ≠ Leaf ⟧ ⟹
  mset_tree (del_min h) = mset_tree h - {#get_min h#}"
by(induction h rule: del_min.induct)(auto simp: mset_pass⇩1 mset_pass⇩2)

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

interpretation pairing: Priority_Queue_Merge
where empty = Leaf and is_empty = "λh. h = Leaf"
and merge = merge and insert = insert
and del_min = del_min and get_min = get_min
and invar = "λh. is_root h ∧ pheap h" and mset = mset_tree
proof(standard, goal_cases)
  case 1 show ?case by simp
next
  case (2 q) show ?case by (cases q) auto
next
  case 3 thus ?case by(simp add: mset_merge)
next
  case 4 thus ?case by(simp add: mset_del_min)
next
  case 5 thus ?case by(simp add: eq_Min_iff get_min_in get_min_min)
next
  case 6 thus ?case by(simp)
next
  case 7 thus ?case using is_root_insert pheap_insert by blast
next
  case 8 thus ?case using is_root_del_min pheap_del_min by blast
next
  case 9 thus ?case by (simp add: mset_merge)
next
  case 10 thus ?case using is_root_merge pheap_merge by blast
qed

end