# HG changeset patch
# User nipkow
# Date 1606157875 -3600
# Node ID 8cb82e7f1743365d7f3eba9ff013d4116170e960
# Parent  8e5428ff35af9d99a82e83e6c190b10818c0de31
proper defn of a heap

diff -r 8e5428ff35af -r 8cb82e7f1743 src/HOL/Data_Structures/Heaps.thy
--- /dev/null	Thu Jan 01 00:00:00 1970 +0000
+++ b/src/HOL/Data_Structures/Heaps.thy	Mon Nov 23 19:57:55 2020 +0100
@@ -0,0 +1,87 @@
+(* 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
diff -r 8e5428ff35af -r 8cb82e7f1743 src/HOL/ROOT
--- a/src/HOL/ROOT	Sun Nov 22 18:26:54 2020 +0000
+++ b/src/HOL/ROOT	Mon Nov 23 19:57:55 2020 +0100
@@ -285,6 +285,7 @@
     Trie_Map
     Tries_Binary
     Queue_2Lists
+    Heaps
     Leftist_Heap
     Binomial_Heap
   document_files "root.tex" "root.bib"