# HG changeset patch
# User Peter Lammich
# Date 1608140870 0
# Node ID 1dc01c11aa86be45f2a3fde4ac5f5eec1cb4c9a3
# Parent  aa86651805e0d710e013c1c86942d65afd9e431b
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)

diff -r aa86651805e0 -r 1dc01c11aa86 src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Dec 16 16:53:13 2020 +0000
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Wed Dec 16 17:47:50 2020 +0000
@@ -448,7 +448,7 @@
 text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
 lemma size_mset_heap:
   assumes "invar ts"
-  shows "2^length ts \<le> size (mset_heap ts) + 1"
+  shows "length ts \<le> log 2 (size (mset_heap ts) + 1)"
 proof -
   from \<open>invar ts\<close> have
     ASC: "sorted_wrt (<) (map rank ts)" and
@@ -465,7 +465,8 @@
     by (auto cong: map_cong simp: size_mset_tree)
   also have "\<dots> = size (mset_heap ts) + 1"
     unfolding mset_heap_def by (induction ts) auto
-  finally show ?thesis .
+  finally have "2^length ts \<le> size (mset_heap ts) + 1" .
+  then show ?thesis using le_log2_of_power by blast
 qed
 
 subsubsection \<open>Timing Functions\<close>
@@ -496,20 +497,11 @@
   assumes "invar ts"
   shows "T_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 2"
 proof -
-
-  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
-    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
+  have "real (T_insert x ts) \<le> real (length ts) + 2"
+    unfolding T_insert_def using T_ins_tree_simple_bound 
+    using of_nat_mono by fastforce
+  also note size_mset_heap[OF \<open>invar ts\<close>]
+  finally show ?thesis by simp
 qed
 
 subsubsection \<open>\<open>T_merge\<close>\<close>
@@ -547,35 +539,21 @@
   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"
+  shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1"
 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>
+  note n_defs = assms(1,2)
 
-  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)"
-    by (rule power_increasing) auto
-  also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
-    by (auto simp: algebra_simps power_add power_mult)
-  also note BINVARS(1)[THEN size_mset_heap]
-  also note BINVARS(2)[THEN size_mset_heap]
-  finally have "2 ^ T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (n\<^sub>1 + 1)\<^sup>2 * (n\<^sub>2 + 1)\<^sup>2"
-    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
-  from le_log2_of_power[OF this] have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
-    by simp
-  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
-    by (simp add: log_mult log_nat_power)
-  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
-  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n + 1)"
-    by auto
-  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
-  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
-    by auto
-  also have "log 2 2 \<le> 2" by auto
-  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
-  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
+  have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * real (length ts\<^sub>1) + 2 * real (length ts\<^sub>2) + 1"
+    using T_merge_length[of ts\<^sub>1 ts\<^sub>2] by simp
+  also note size_mset_heap[OF \<open>invar ts\<^sub>1\<close>]
+  also note size_mset_heap[OF \<open>invar ts\<^sub>2\<close>]
+  finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * log 2 (n\<^sub>1 + 1) + 2 * log 2 (n\<^sub>2 + 1) + 1"
+    unfolding n_defs by (simp add: algebra_simps)
+  also have "log 2 (n\<^sub>1 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
+    unfolding n_defs by (simp add: algebra_simps)
+  also have "log 2 (n\<^sub>2 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" 
+    unfolding n_defs by (simp add: algebra_simps)
+  finally show ?thesis by (simp add: algebra_simps)
 qed
 
 subsubsection \<open>\<open>T_get_min\<close>\<close>
@@ -593,13 +571,8 @@
   shows "T_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
 proof -
   have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto
-  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
-  proof -
-    from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
-      unfolding invar_def by auto
-    thus ?thesis using le_log2_of_power by blast
-  qed
-  finally show ?thesis by auto
+  also note size_mset_heap[OF \<open>invar ts\<close>]
+  finally show ?thesis .
 qed
 
 subsubsection \<open>\<open>T_del_min\<close>\<close>
@@ -617,13 +590,8 @@
   shows "T_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
 proof -
   have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto
-  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
-  proof -
-    from size_mset_heap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
-      by auto
-    thus ?thesis using le_log2_of_power by blast
-  qed
-  finally show ?thesis by auto
+  also note size_mset_heap[OF \<open>invar ts\<close>]
+  finally show ?thesis .
 qed
 
 text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity,
@@ -637,65 +605,40 @@
                     \<Rightarrow> T_rev ts\<^sub>1 + T_merge (rev ts\<^sub>1) ts\<^sub>2
   )"
 
-lemma T_rev_ts1_bound_aux:
-  fixes ts
-  defines "n \<equiv> size (mset_heap ts)"
-  assumes BINVAR: "invar (rev ts)"
-  shows "T_rev ts \<le> 1 + log 2 (n+1)"
-proof -
-  have "T_rev ts = length ts + 1" by (auto simp: T_rev_def)
-  hence "2^T_rev ts = 2*2^length ts" by auto
-  also have "\<dots> \<le> 2*n+2" using size_mset_heap[OF BINVAR] by (auto simp: n_def)
-  finally have "2 ^ T_rev ts \<le> 2 * n + 2" .
-  from le_log2_of_power[OF this] have "T_rev ts \<le> log 2 (2 * (n + 1))"
-    by auto
-  also have "\<dots> = 1 + log 2 (n+1)"
-    by (simp only: of_nat_mult log_mult) auto
-  finally show ?thesis by (auto simp: 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"
+  assumes "invar ts" and "ts\<noteq>[]"
+  shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2"
 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> \<open>invar ts\<close>]
-  hence BINVAR1: "invar (rev ts\<^sub>1)" by (blast intro: invar_children)
+  have I1: "invar (rev ts\<^sub>1)" and I2: "invar ts\<^sub>2"
+    using invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>] invar_children
+    by auto
 
   define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
   define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
 
-  have T_rev_ts1_bound: "T_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
-  proof -
-    note T_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
-    also have "n\<^sub>1 \<le> n"
-      unfolding n\<^sub>1_def n_def
-      using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
-      by (auto simp: mset_heap_def)
-    finally show ?thesis by (auto simp: algebra_simps)
-  qed
-
-  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[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[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
+  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)
-  finally have "T_del_min ts \<le> 6 * log 2 (n+1) + 3"
-    by auto
-  thus ?thesis by (simp add: algebra_simps)
+
+  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)"
+    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"
+    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
 
 end