# HG changeset patch
# User Peter Lammich
# Date 1608052947 0
# Node ID c145be662fbd57aa33e5583c98571f6e4b0563fd
# Parent  3883f536d84dfc2733256c08c5df4c90baf66842
removed redundant T_xxx_bound_aux lemmas

diff -r 3883f536d84d -r c145be662fbd src/HOL/Data_Structures/Binomial_Heap.thy
--- 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