# HG changeset patch
# User nipkow
# Date 1485966984 -3600
# Node ID 96b66d5c0fc116fd364e8d7d30d901aa6afa80aa
# Parent  d0e55f85fd8a1b42a61d907b9a3c9a7b5e445289
added is_empty

diff -r d0e55f85fd8a -r 96b66d5c0fc1 src/HOL/Data_Structures/Leftist_Heap.thy
--- a/src/HOL/Data_Structures/Leftist_Heap.thy	Mon Jan 30 16:47:20 2017 +0100
+++ b/src/HOL/Data_Structures/Leftist_Heap.thy	Wed Feb 01 17:36:24 2017 +0100
@@ -83,12 +83,14 @@
 
 locale Priority_Queue =
 fixes empty :: "'q"
+and is_empty :: "'q \<Rightarrow> bool"
 and insert :: "'a::linorder \<Rightarrow> 'q \<Rightarrow> 'q"
 and get_min :: "'q \<Rightarrow> 'a"
 and del_min :: "'q \<Rightarrow> 'q"
 and invar :: "'q \<Rightarrow> bool"
 and mset :: "'q \<Rightarrow> 'a multiset"
 assumes mset_empty: "mset empty = {#}"
+and is_empty: "invar q \<Longrightarrow> is_empty q = (mset q = {#})"
 and mset_insert: "invar q \<Longrightarrow> mset (insert x q) = mset q + {#x#}"
 and mset_del_min: "invar q \<Longrightarrow> mset (del_min q) = mset q - {#get_min q#}"
 and get_min: "invar q \<Longrightarrow> q \<noteq> empty \<Longrightarrow>
@@ -147,21 +149,24 @@
 
 
 interpretation lheap: Priority_Queue
-where empty = Leaf and insert = insert and del_min = del_min
+where empty = Leaf and is_empty = "\<lambda>h. h = Leaf"
+and insert = insert and del_min = del_min
 and get_min = get_min and invar = "\<lambda>h. heap h \<and> ltree h"
 and mset = mset_tree
 proof(standard, goal_cases)
   case 1 show ?case by simp
 next
-  case 2 show ?case by(rule mset_insert)
+  case (2 q) show ?case by (cases q) auto
 next
-  case 3 show ?case by(rule mset_del_min)
+  case 3 show ?case by(rule mset_insert)
+next
+  case 4 show ?case by(rule mset_del_min)
 next
-  case 4 thus ?case by(simp add: get_min)
+  case 5 thus ?case by(simp add: get_min)
 next
-  case 5 thus ?case by(simp add: heap_insert ltree_insert)
+  case 6 thus ?case by(simp add: heap_insert ltree_insert)
 next
-  case 6 thus ?case by(simp add: heap_del_min ltree_del_min)
+  case 7 thus ?case by(simp add: heap_del_min ltree_del_min)
 qed