# HG changeset patch
# User Peter Lammich
# Date 1607102441 0
# Node ID ba65dc3e35af7693f5711428a3e30a891c9e8cf4
# Parent  d7393c35aa5dc290b97cd341250c954295d4e3f2
summarized structural and ordering invariant for trees

diff -r d7393c35aa5d -r ba65dc3e35af src/HOL/Data_Structures/Binomial_Heap.thy
--- a/src/HOL/Data_Structures/Binomial_Heap.thy	Thu Dec 03 23:00:23 2020 +0100
+++ b/src/HOL/Data_Structures/Binomial_Heap.thy	Fri Dec 04 17:20:41 2020 +0000
@@ -8,7 +8,7 @@
 imports
   "HOL-Library.Pattern_Aliases"
   Complex_Main
-  Priority_Queue_Specs
+  "HOL-Data_Structures.Priority_Queue_Specs"
 begin
 
 text \<open>
@@ -59,33 +59,25 @@
 
 subsubsection \<open>Invariants\<close>
 
-text \<open>Binomial invariant\<close>
+text \<open>Binomial tree\<close>
 fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
 "invar_btree (Node r x ts) \<longleftrightarrow>
    (\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
 
-definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
-"invar_bheap ts
-  \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (<) (map rank ts))"
-
 text \<open>Ordering (heap) invariant\<close>
 fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
 "invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
 
-definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
-"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
+definition "invar_tree t \<longleftrightarrow> invar_btree t \<and> invar_otree t"
 
-definition invar :: "'a::linorder heap \<Rightarrow> bool" where
-"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
+text \<open>Binomial Heap invariant\<close>
+definition "invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_tree t) \<and> (sorted_wrt (<) (map rank ts))"
+
 
 text \<open>The children of a node are a valid heap\<close>
-lemma invar_oheap_children:
-  "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"
-by (auto simp: invar_oheap_def)
-
-lemma invar_bheap_children:
-  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
-by (auto simp: invar_bheap_def rev_map[symmetric])
+lemma invar_children:
+  "invar_tree (Node r v ts) \<Longrightarrow> invar (rev ts)"
+  by (auto simp: invar_tree_def invar_def rev_map[symmetric])
 
 
 subsection \<open>Operations and Their Functional Correctness\<close>
@@ -102,19 +94,12 @@
 
 end
 
-lemma invar_btree_link:
-  assumes "invar_btree t\<^sub>1"
-  assumes "invar_btree t\<^sub>2"
+lemma invar_link:
+  assumes "invar_tree t\<^sub>1"
+  assumes "invar_tree t\<^sub>2"
   assumes "rank t\<^sub>1 = rank t\<^sub>2"
-  shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
-using assms
-by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
-
-lemma invar_otree_link:
-  assumes "invar_otree t\<^sub>1"
-  assumes "invar_otree t\<^sub>2"
-  shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
-using assms
+  shows "invar_tree (link t\<^sub>1 t\<^sub>2)"
+using assms unfolding invar_tree_def
 by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
 
 lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
@@ -130,29 +115,21 @@
 | "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
   (if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1#t\<^sub>2#ts else ins_tree (link t\<^sub>1 t\<^sub>2) ts)"
 
-lemma invar_bheap_Cons[simp]:
-  "invar_bheap (t#ts)
-  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
-by (auto simp: invar_bheap_def)
+lemma invar_tree0[simp]: "invar_tree (Node 0 x [])"
+unfolding invar_tree_def by auto
 
-lemma invar_btree_ins_tree:
-  assumes "invar_btree t"
-  assumes "invar_bheap ts"
+lemma invar_Cons[simp]:
+  "invar (t#ts)
+  \<longleftrightarrow> invar_tree t \<and> invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
+by (auto simp: invar_def)
+
+lemma invar_ins_tree:
+  assumes "invar_tree t"
+  assumes "invar ts"
   assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
-  shows "invar_bheap (ins_tree t ts)"
+  shows "invar (ins_tree t ts)"
 using assms
-by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
-
-lemma invar_oheap_Cons[simp]:
-  "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"
-by (auto simp: invar_oheap_def)
-
-lemma invar_oheap_ins_tree:
-  assumes "invar_otree t"
-  assumes "invar_oheap ts"
-  shows "invar_oheap (ins_tree t ts)"
-using assms
-by (induction t ts rule: ins_tree.induct) (auto simp: invar_otree_link)
+by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric])
 
 lemma mset_heap_ins_tree[simp]:
   "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
@@ -174,7 +151,7 @@
 "insert x ts = ins_tree (Node 0 x []) ts"
 
 lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
-by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)
+by (auto intro!: invar_ins_tree simp: insert_def)
 
 lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
 by(auto simp: insert_def)
@@ -208,54 +185,79 @@
 by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
    (auto split: if_splits simp: ins_tree_rank_bound)
 
-lemma invar_bheap_merge:
-  assumes "invar_bheap ts\<^sub>1"
-  assumes "invar_bheap ts\<^sub>2"
-  shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
+lemma invar_merge[simp]:
+  assumes "invar ts\<^sub>1"
+  assumes "invar ts\<^sub>2"
+  shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
+using assms
+by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
+   (auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound)
+
+
+text \<open>Longer, more explicit proof of @{thm [source] invar_merge}, 
+      to illustrate the application of the @{thm [source] merge_rank_bound} lemma.\<close>
+lemma 
+  assumes "invar ts\<^sub>1"
+  assumes "invar ts\<^sub>2"
+  shows "invar (merge ts\<^sub>1 ts\<^sub>2)"
   using assms
 proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
   case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
-
-  from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"
+  \<comment> \<open>Invariants of the parts can be shown automatically\<close>
+  from "3.prems" have [simp]: 
+    "invar_tree t\<^sub>1" "invar_tree t\<^sub>2"
+    (*"invar (merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2)" 
+    "invar (merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2))"
+    "invar (merge ts\<^sub>1 ts\<^sub>2)"*)
     by auto
 
+  \<comment> \<open>These are the three cases of the @{const merge} function\<close>
   consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
          | (GT) "rank t\<^sub>1 > rank t\<^sub>2"
          | (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
     using antisym_conv3 by blast
   then show ?case proof cases
-    case LT
-    then show ?thesis using 3
-      by (force elim!: merge_rank_bound)
+    case LT 
+    \<comment> \<open>@{const merge} takes the first tree from the left heap\<close>
+    then have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)" by simp
+    also have "invar \<dots>" proof (simp, intro conjI)
+      \<comment> \<open>Invariant follows from induction hypothesis\<close>
+      show "invar (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2))"
+        using LT "3.IH" "3.prems" by simp
+
+      \<comment> \<open>It remains to show that \<open>t\<^sub>1\<close> has smallest rank.\<close>
+      show "\<forall>t'\<in>set (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)). rank t\<^sub>1 < rank t'"
+        \<comment> \<open>Which is done by auxiliary lemma @{thm [source] merge_rank_bound}\<close>
+        using LT "3.prems" by (force elim!: merge_rank_bound)
+    qed
+    finally show ?thesis .
   next
-    case GT
-    then show ?thesis using 3
-      by (force elim!: merge_rank_bound)
+    \<comment> \<open>@{const merge} takes the first tree from the right heap\<close>
+    case GT 
+    \<comment> \<open>The proof is anaologous to the \<open>LT\<close> case\<close>
+    then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound)
   next
     case [simp]: EQ
-
-    from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
-      by auto
+    \<comment> \<open>@{const merge} links both first trees, and inserts them into the merged remaining heaps\<close>
+    have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)" by simp
+    also have "invar \<dots>" proof (intro invar_ins_tree invar_link) 
+      \<comment> \<open>Invariant of merged remaining heaps follows by IH\<close>
+      show "invar (merge ts\<^sub>1 ts\<^sub>2)"
+        using EQ "3.prems" "3.IH" by auto
 
-    have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
-      using that
-      apply (rule merge_rank_bound)
-      using "3.prems" by auto
-    with EQ show ?thesis
-      by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link)
+      \<comment> \<open>For insertion, we have to show that the rank of the linked tree is \<open>\<le>\<close> the 
+          ranks in the merged remaining heaps\<close>
+      show "\<forall>t'\<in>set (merge ts\<^sub>1 ts\<^sub>2). rank (link t\<^sub>1 t\<^sub>2) \<le> rank t'"
+      proof -
+        \<comment> \<open>Which is, again, done with the help of @{thm [source] merge_rank_bound}\<close>
+        have "rank (link t\<^sub>1 t\<^sub>2) = Suc (rank t\<^sub>2)" by simp
+        thus ?thesis using "3.prems" by (auto simp: Suc_le_eq elim!: merge_rank_bound)
+      qed
+    qed simp_all
+    finally show ?thesis .
   qed
-qed simp_all
+qed auto
 
-lemma invar_oheap_merge:
-  assumes "invar_oheap ts\<^sub>1"
-  assumes "invar_oheap ts\<^sub>2"
-  shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
-using assms
-by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
-   (auto simp: invar_oheap_ins_tree invar_otree_link)
-
-lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
-by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
 
 lemma mset_heap_merge[simp]:
   "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
@@ -267,32 +269,25 @@
   "get_min [t] = root t"
 | "get_min (t#ts) = min (root t) (get_min ts)"
 
-lemma invar_otree_root_min:
-  assumes "invar_otree t"
+lemma invar_tree_root_min:
+  assumes "invar_tree t"
   assumes "x \<in># mset_tree t"
   shows "root t \<le> x"
-using assms
+using assms unfolding invar_tree_def
 by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
 
-lemma get_min_mset_aux:
-  assumes "ts\<noteq>[]"
-  assumes "invar_oheap ts"
-  assumes "x \<in># mset_heap ts"
-  shows "get_min ts \<le> x"
-  using assms
-apply (induction ts arbitrary: x rule: get_min.induct)
-apply (auto
-      simp: invar_otree_root_min min_def intro: order_trans;
-      meson linear order_trans invar_otree_root_min
-      )+
-done
-
 lemma get_min_mset:
   assumes "ts\<noteq>[]"
   assumes "invar ts"
   assumes "x \<in># mset_heap ts"
   shows "get_min ts \<le> x"
-using assms by (auto simp: invar_def get_min_mset_aux)
+  using assms
+apply (induction ts arbitrary: x rule: get_min.induct)
+apply (auto
+      simp: invar_tree_root_min min_def intro: order_trans;
+      meson linear order_trans invar_tree_root_min
+      )+
+done
 
 lemma get_min_member:
   "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
@@ -333,13 +328,13 @@
 using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
 by auto
 
-lemma invar_bheap_get_min_rest:
+lemma invar_get_min_rest:
   assumes "get_min_rest ts = (t',ts')"
   assumes "ts\<noteq>[]"
-  assumes "invar_bheap ts"
-  shows "invar_btree t'" and "invar_bheap ts'"
+  assumes "invar ts"
+  shows "invar_tree t'" and "invar ts'"
 proof -
-  have "invar_btree t' \<and> invar_bheap ts'"
+  have "invar_tree t' \<and> invar ts'"
     using assms
     proof (induction ts arbitrary: t' ts' rule: get_min.induct)
       case (2 t v va)
@@ -348,17 +343,9 @@
         apply (drule set_get_min_rest; fastforce)
         done
     qed auto
-  thus "invar_btree t'" and "invar_bheap ts'" by auto
+  thus "invar_tree t'" and "invar ts'" by auto
 qed
 
-lemma invar_oheap_get_min_rest:
-  assumes "get_min_rest ts = (t',ts')"
-  assumes "ts\<noteq>[]"
-  assumes "invar_oheap ts"
-  shows "invar_otree t'" and "invar_oheap ts'"
-using assms
-by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
-
 subsubsection \<open>\<open>del_min\<close>\<close>
 
 definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
@@ -370,12 +357,11 @@
   assumes "invar ts"
   shows "invar (del_min ts)"
 using assms
-unfolding invar_def del_min_def
+unfolding del_min_def
 by (auto
       split: prod.split tree.split
-      intro!: invar_bheap_merge invar_oheap_merge
-      dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
-      intro!: invar_oheap_children invar_bheap_children
+      intro!: invar_merge invar_children 
+      dest: invar_get_min_rest
     )
 
 lemma mset_heap_del_min:
@@ -412,7 +398,7 @@
 next
   case (5 q) thus ?case using get_min[of q] by auto
 next
-  case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
+  case 6 thus ?case by (auto simp add: invar_def)
 next
   case 7 thus ?case by simp
 next
@@ -453,15 +439,21 @@
     by (simp)
 qed
 
+lemma size_mset_tree:
+  assumes "invar_tree t"
+  shows "size (mset_tree t) = 2^rank t"
+using assms unfolding invar_tree_def
+by (simp add: size_mset_btree)
+
 text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
-lemma size_mset_bheap:
-  assumes "invar_bheap ts"
+lemma size_mset_heap:
+  assumes "invar ts"
   shows "2^length ts \<le> size (mset_heap ts) + 1"
 proof -
-  from \<open>invar_bheap ts\<close> have
+  from \<open>invar ts\<close> have
     ASC: "sorted_wrt (<) (map rank ts)" and
-    TINV: "\<forall>t\<in>set ts. invar_btree t"
-    unfolding invar_bheap_def by auto
+    TINV: "\<forall>t\<in>set ts. invar_tree t"
+    unfolding invar_def by auto
 
   have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
     by (simp add: sum_power2)
@@ -470,7 +462,7 @@
     using power_increasing[where a="2::nat"]
     by (auto simp: o_def)
   also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
-    by (auto cong: map_cong simp: size_mset_btree)
+    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 .
@@ -509,7 +501,7 @@
     unfolding T_insert_def by (rule T_ins_tree_simple_bound)
   also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
   proof -
-    from size_mset_bheap[of ts] assms
+    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
@@ -553,7 +545,7 @@
   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_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
+  assumes BINVARS: "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"
@@ -564,8 +556,8 @@
     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_bheap]
-  also note BINVARS(2)[THEN size_mset_bheap]
+  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>"
@@ -608,7 +600,7 @@
   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_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+    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
@@ -625,14 +617,14 @@
   by (induction ts rule: T_get_min_rest.induct) auto
 
 lemma T_get_min_rest_bound_aux:
-  assumes "invar_bheap ts"
+  assumes "invar ts"
   assumes "ts\<noteq>[]"
   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_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
+    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
@@ -659,12 +651,12 @@
 lemma T_rev_ts1_bound_aux:
   fixes ts
   defines "n \<equiv> size (mset_heap ts)"
-  assumes BINVAR: "invar_bheap (rev 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_bheap[OF BINVAR] by (auto simp: n_def)
+  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
@@ -676,15 +668,15 @@
 lemma T_del_min_bound_aux:
   fixes ts
   defines "n \<equiv> size (mset_heap ts)"
-  assumes BINVAR: "invar_bheap ts"
+  assumes BINVAR: "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_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
-  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
+  note BINVAR' = invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
+  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)"
   define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
@@ -706,7 +698,7 @@
   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_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
+    using T_merge_bound_aux[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