src/HOL/Data_Structures/Heaps.thy

tuned;

(* Author: Tobias Nipkow *)

section \<open>Heaps\<close>

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

text \<open>Heap = priority queue on trees:\<close>
    
locale Heap =
fixes insert :: "('a::linorder) \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
and  del_min :: "'a tree \<Rightarrow> 'a tree"
assumes mset_insert: "heap q \<Longrightarrow> mset_tree (insert x q) = {#x#} + mset_tree q"
and    mset_del_min: "\<lbrakk> heap q;  q \<noteq> Leaf \<rbrakk> \<Longrightarrow> mset_tree (del_min q) = mset_tree q - {#value q#}"
and     heap_insert: "heap q \<Longrightarrow> heap(insert x q)"
and    heap_del_min: "heap q \<Longrightarrow> heap(del_min q)"
begin

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

fun is_empty :: "'a tree \<Rightarrow> 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 \<open>Once you have \<open>merge\<close>, \<open>insert\<close> and \<open>del_min\<close> are easy:\<close>

locale Heap_Merge =
fixes merge :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree"
assumes mset_merge: "\<lbrakk> heap q1; heap q2 \<rbrakk> \<Longrightarrow> mset_tree (merge q1 q2) = mset_tree q1 + mset_tree q2"
and invar_merge: "\<lbrakk> heap q1; heap q2 \<rbrakk> \<Longrightarrow> heap (merge q1 q2)"
begin

fun insert :: "'a \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
"insert x t = merge (Node Leaf x Leaf) t"

fun del_min :: "'a tree \<Rightarrow> '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