--- a/src/HOL/Data_Structures/Binomial_Heap.thy Tue Dec 15 17:22:40 2020 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Wed Dec 16 16:53:13 2020 +0000
@@ -485,7 +485,7 @@
)"
definition T_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
-"T_insert x ts = T_ins_tree (Node 0 x []) ts"
+"T_insert x ts = T_ins_tree (Node 0 x []) ts + 1"
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1"
by (induction t ts rule: T_ins_tree.induct) auto
@@ -494,21 +494,22 @@
lemma T_insert_bound:
assumes "invar ts"
- shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
+ shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 2"
proof -
- have 1: "T_insert x ts \<le> length ts + 1"
- unfolding T_insert_def by (rule T_ins_tree_simple_bound)
- also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
+ have 1: "T_insert x ts \<le> length ts + 2"
+ unfolding T_insert_def using T_ins_tree_simple_bound by auto
+ also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1)) + 1"
proof -
from size_mset_heap[of ts] assms
have "2 ^ length ts \<le> size (mset_heap ts) + 1"
unfolding invar_def by auto
hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
- thus ?thesis using le_log2_of_power by blast
+ hence "length ts + 1 \<le> log 2 (2 * (size (mset_heap ts) + 1))"
+ using le_log2_of_power by blast
+ thus ?thesis by simp
qed
- finally show ?thesis
- by (simp only: log_mult of_nat_mult) auto
+ finally show ?thesis by (simp only: log_mult of_nat_mult) auto
qed
subsubsection \<open>\<open>T_merge\<close>\<close>