(* Author: Tobias Nipkow *)

section ‹Heaps›

theory Heaps
imports
  "HOL-Library.Tree_Multiset"
  Priority_Queue_Specs
begin

text ‹Heap = priority queue on trees:›
    
locale Heap =
fixes insert :: "('a::linorder) → 'a tree → 'a tree"
and  del_min :: "'a tree → 'a tree"
assumes mset_insert: "heap q ==> mset_tree (insert x q) = {#x#} + mset_tree q"
and    mset_del_min: "[ heap q; q ≠ Leaf ] ==> mset_tree (del_min q) = mset_tree q - {#value q#}"
and     heap_insert: "heap q ==> heap(insert x q)"
and    heap_del_min: "heap q ==> heap(del_min q)"
begin

definition empty :: "'a tree" where
"empty = Leaf"

fun is_empty :: "'a tree → bool" where
"is_empty t = (t = Leaf)"

fun get_min :: "'a tree → 'a" where
"get_min (Node l a r) = a"

sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert
and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree
proof (standard, goal_cases)
  case 1 thus ?case by (simp add: empty_def)
next
  case 2 thus ?case by(auto)
next
  case 3 thus ?case by(simp add: mset_insert)
next
  case 4 thus ?case by(auto simp add: mset_del_min neq_Leaf_iff)
next
  case 5 thus ?case by(auto simp: neq_Leaf_iff Min_insert2 simp del: Un_iff)
next
  case 6 thus ?case by(simp add: empty_def)
next
  case 7 thus ?case by(simp add: heap_insert)
next
  case 8 thus ?case by(simp add: heap_del_min)
qed

end


text ‹Once you have ‹merge›, ‹insert› and ‹del_min› are easy:›

locale Heap_Merge =
fixes merge :: "'a::linorder tree → 'a tree → 'a tree"
assumes mset_merge: "[ heap q1; heap q2 ] ==> mset_tree (merge q1 q2) = mset_tree q1 + mset_tree q2"
and invar_merge: "[ heap q1; heap q2 ] ==> heap (merge q1 q2)"
begin

fun insert :: "'a → 'a tree → 'a tree" where
"insert x t = merge (Node Leaf x Leaf) t"

fun del_min :: "'a tree → 'a tree" where
"del_min Leaf = Leaf" |
"del_min (Node l x r) = merge l r"

interpretation Heap insert del_min
proof(standard, goal_cases)
  case 1 thus ?case by(simp add:mset_merge)
next
  case (2 q) thus ?case by(cases q)(auto simp: mset_merge)
next
  case 3 thus ?case by (simp add: invar_merge)
next
  case (4 q) thus ?case by (cases q)(auto simp: invar_merge)
qed

lemmas local_empty_def = local.empty_def
lemmas local_get_min_def = local.get_min.simps

sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert
and get_min = get_min and del_min = del_min and invar = heap and mset = mset_tree and merge = merge
proof(standard, goal_cases)
  case 1 thus ?case by (simp add: mset_merge)
next
  case 2 thus ?case by (simp add: invar_merge)
qed

end

end