src/HOL/Data_Structures/Binomial_Heap.thy

   estimations of their complexity.
 \<close>
 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) = (
     (if rank t\<^sub>1 < rank t\<^sub>2 then 1
      else T_link t\<^sub>1 t\<^sub>2 + T_ins_tree (link t\<^sub>1 t\<^sub>2) rest)

 definition "T_rev xs = length xs + 1"
 
 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)
 
   have I1: "invar (rev ts\<^sub>1)" and I2: "invar ts\<^sub>2"

 
   have "n\<^sub>1 \<le> n" "n\<^sub>1 + n\<^sub>2 \<le> n" unfolding n_def n\<^sub>1_def n\<^sub>2_def
     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)" 
     using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp
   also have "T_rev ts\<^sub>1 \<le> 1 + log 2 (n\<^sub>1 + 1)"
     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>
   finally show ?thesis by (simp add: algebra_simps)
 qed