# HG changeset patch
# User Peter Lammich
# Date 1608213082 0
# Node ID 8b92a2ab53703e4fef79a2ba39c49e3cd473a477
# Parent  686c7ee213e9ee1fda327df44bb145e5fa22083b
tuned running time functions

diff -r 686c7ee213e9 -r 8b92a2ab5370 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Dec 16 17:48:06 2020 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Dec 17 13:51:22 2020 +0000
@@ -478,6 +478,9 @@
 definition T_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
 [simp]: "T_link _ _ = 1"
 
+text \<open>This function is non-canonical: we omitted a \<open>+1\<close> in the \<open>else\<close>-part,
+  to keep the following analysis simpler and more to the point.
+\<close>
 fun T_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
   "T_ins_tree t [] = 1"
 | "T_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
@@ -603,13 +606,13 @@
 definition T_del_min :: "'a::linorder heap \<Rightarrow> nat" where
   "T_del_min ts = T_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
                     \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
-  )"
+  ) + 1"
 
 lemma T_del_min_bound:
   fixes ts
   defines "n \<equiv> size (mset_heap ts)"
   assumes "invar ts" and "ts\<noteq>[]"
-  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2"
+  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
 proof -
   obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
     by (metis surj_pair tree.exhaust_sel)
@@ -625,7 +628,7 @@
     using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
     by (auto simp: mset_heap_def)
 
-  have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)"
+  have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2) + 1"
     unfolding T_del_min_def GM
     by simp
   also have "T_get_min_rest ts \<le> log 2 (n+1)" 
@@ -634,7 +637,7 @@
     unfolding T_rev_def n\<^sub>1_def using size_mset_heap[OF I1] by simp
   also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
     unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
-  finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 2"
+  finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 3"
     by (simp add: algebra_simps)
   also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close>
   also note \<open>n\<^sub>1 \<le> n\<close>