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 pass1 :: "('a::linorder) tree  'a tree" where
"pass1 (Node hsx x (Node hsy y hs)) = link (Node hsx x (Node hsy y (pass1 hs)))" |
"pass1 hs = hs"

fun pass2 :: "('a::linorder) tree  'a tree" where
"pass2 (Node hsx x hs) = link(Node hsx x (pass2 hs))" |
"pass2 Leaf = Leaf"

fun del_min :: "('a::linorder) tree  'a tree" where
  "del_min Leaf = Leaf"
| "del_min (Node hs _ Leaf) = pass2 (pass1 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 pass1_struct: "l a r. pass1 (Node hs1 x hs) = Node l a r" 
by (cases hs) simp_all

lemma pass2_struct: "l a. pass2 (Node hs1 x hs) = Node l a Leaf" 
by(induction hs arbitrary: hs1 x rule: pass2.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 "pass1 lx = Node a la ra" 
      using pass1_struct by blast
    moreover obtain lb b where "pass2  = Node b lb Leaf"
      using pass2_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 (pass1 h)"
by(induction h rule: pass1.induct) (auto)

lemma pheap_pass2: "pheap h  pheap (pass2 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_pass1: "mset_tree (pass1 h) = mset_tree h"
by (induction h rule: pass1.induct) auto

lemma mset_pass2: "mset_tree (pass2 h) = mset_tree h"
by (induction h rule: pass2.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_pass1 mset_pass2)

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