Theory Heaps

(* 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)"

sublocale Priority_Queue where empty = empty and is_empty = is_empty and insert = insert
and get_min = "value" 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(simp add: mset_del_min)
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

sublocale PQM: Priority_Queue_Merge where empty = empty and is_empty = is_empty and insert = insert
and get_min = "value" 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