# HG changeset patch
# User nipkow
# Date 1735405421 -3600
# Node ID 88feb0047d7c640027b43878cc02f5ca65ea3517
# Parent  4219bb3951deceb9a1ccf2dde151c68df83ab4b7
tuned

diff -r 4219bb3951de -r 88feb0047d7c src/HOL/Data_Structures/Heaps.thy
--- a/src/HOL/Data_Structures/Heaps.thy	Sat Dec 28 16:38:57 2024 +0100
+++ b/src/HOL/Data_Structures/Heaps.thy	Sat Dec 28 18:03:41 2024 +0100
@@ -25,8 +25,11 @@
 fun is_empty :: "'a tree \<Rightarrow> bool" where
 "is_empty t = (t = Leaf)"
 
+fun get_min :: "'a tree \<Rightarrow> '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 = "value" and del_min = del_min and invar = heap and mset = mset_tree
+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
@@ -34,7 +37,7 @@
 next
   case 3 thus ?case by(simp add: mset_insert)
 next
-  case 4 thus ?case by(simp add: mset_del_min)
+  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
@@ -74,8 +77,11 @@
   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 = "value" and del_min = del_min and invar = heap and mset = mset_tree and merge = merge
+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