# HG changeset patch
# User nipkow
# Date 1724705547 -7200
# Node ID 3a9e570c916d34f44b16a8581dbea982f24215e7
# Parent  de95c82eb31ac76c95185725bbb4a84758a1d729
more precise bound

diff -r de95c82eb31a -r 3a9e570c916d src/HOL/Data_Structures/Leftist_Heap_List.thy
--- a/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Aug 26 18:26:06 2024 +0200
+++ b/src/HOL/Data_Structures/Leftist_Heap_List.thy	Mon Aug 26 22:52:27 2024 +0200
@@ -155,7 +155,7 @@
 qed
 
 lemma T_lheap_list: assumes "length xs = 2 ^ k"
-shows "T_lheap_list xs \<le> 5 * length xs"
+shows "T_lheap_list xs \<le> 5 * length xs - 2 * log 2 (length xs)"
 proof -
   let ?ts = "map (\<lambda>x. Node Leaf (x,1) Leaf) xs"
   have "T_lheap_list xs = T_merge_all ?ts" by simp
@@ -172,10 +172,8 @@
     by (simp add:log_nat_power algebra_simps)
   also have "\<dots> = 5*(2::real)^k - (2::real)*k - 5"
     using summation by (simp)
-  also have "\<dots> \<le> 5*(2::real)^k"
-    by linarith
   finally show ?thesis
-    using assms of_nat_le_iff by fastforce
+    using assms of_nat_le_iff by simp
 qed
 
 end
\ No newline at end of file