--- a/src/HOL/Data_Structures/Binomial_Heap.thy Sun Dec 13 23:11:41 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy Tue Dec 15 17:22:27 2020 +0000
@@ -541,15 +541,17 @@
(auto simp: T_ins_tree_length algebra_simps)
text \<open>Finally, we get the desired logarithmic bound\<close>
-lemma T_merge_bound_aux:
+lemma T_merge_bound:
fixes ts\<^sub>1 ts\<^sub>2
defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
- assumes BINVARS: "invar ts\<^sub>1" "invar ts\<^sub>2"
+ assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
proof -
define n where "n = n\<^sub>1 + n\<^sub>2"
+ note BINVARS = \<open>invar ts\<^sub>1\<close> \<open>invar ts\<^sub>2\<close>
+
from T_merge_length[of ts\<^sub>1 ts\<^sub>2]
have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
hence "(2::nat)^T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)"
@@ -575,14 +577,6 @@
thus ?thesis unfolding n_def by (auto simp: algebra_simps)
qed
-lemma T_merge_bound:
- fixes ts\<^sub>1 ts\<^sub>2
- defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
- defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
- assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
- shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
-using assms T_merge_bound_aux unfolding invar_def by blast
-
subsubsection \<open>\<open>T_get_min\<close>\<close>
fun T_get_min :: "'a::linorder heap \<Rightarrow> nat" where
@@ -616,7 +610,7 @@
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts"
by (induction ts rule: T_get_min_rest.induct) auto
-lemma T_get_min_rest_bound_aux:
+lemma T_get_min_rest_bound:
assumes "invar ts"
assumes "ts\<noteq>[]"
shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
@@ -631,12 +625,6 @@
finally show ?thesis by auto
qed
-lemma T_get_min_rest_bound:
- assumes "invar ts"
- assumes "ts\<noteq>[]"
- shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
-using assms T_get_min_rest_bound_aux unfolding invar_def by blast
-
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
it can and is implemented (via suitable code lemmas) as a linear time function.
Thus the following definition is justified:\<close>
@@ -665,17 +653,17 @@
finally show ?thesis by (auto simp: algebra_simps)
qed
-lemma T_del_min_bound_aux:
+lemma T_del_min_bound:
fixes ts
defines "n \<equiv> size (mset_heap ts)"
- assumes BINVAR: "invar ts"
+ assumes "invar ts"
assumes "ts\<noteq>[]"
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)
- note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+ note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>]
hence BINVAR1: "invar (rev ts\<^sub>1)" by (blast intro: invar_children)
define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
@@ -694,11 +682,11 @@
have "T_del_min ts = T_get_min_rest ts + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
unfolding T_del_min_def by (simp add: GM)
also have "\<dots> \<le> log 2 (n+1) + T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2"
- using T_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
+ using T_get_min_rest_bound[OF assms(2-)] by (auto simp: n_def)
also have "\<dots> \<le> 2*log 2 (n+1) + T_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
using T_rev_ts1_bound by auto
also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
- using T_merge_bound_aux[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>]
+ using T_merge_bound[OF \<open>invar (rev ts\<^sub>1)\<close> \<open>invar ts\<^sub>2\<close>]
by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
also have "n\<^sub>1 + n\<^sub>2 \<le> n"
unfolding n\<^sub>1_def n\<^sub>2_def n_def
@@ -709,12 +697,4 @@
thus ?thesis by (simp add: algebra_simps)
qed
-lemma T_del_min_bound:
- fixes ts
- defines "n \<equiv> size (mset_heap ts)"
- assumes "invar ts"
- assumes "ts\<noteq>[]"
- shows "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
-using assms T_del_min_bound_aux unfolding invar_def by blast
-
end