author Peter Lammich Thu, 17 Dec 2020 13:51:22 +0000 changeset 73182 8b92a2ab5370 parent 73177 686c7ee213e9 child 73183 b945880827ff
tuned running time functions
```--- 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"