Theory Binomial_Heap

(* Author: Peter Lammich
           Tobias Nipkow (tuning)
*)

section ‹Binomial Priority Queue›

theory Binomial_Heap
imports
  "HOL-Library.Pattern_Aliases"
  Complex_Main
  Priority_Queue_Specs
  Time_Funs
begin

text ‹
  We formalize the presentation from Okasaki's book.
  We show the functional correctness and complexity of all operations.

  The presentation is engineered for simplicity, and most
  proofs are straightforward and automatic.
›

subsection ‹Binomial Tree and Forest Types›

datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")

type_synonym 'a forest = "'a tree list"

subsubsection ‹Multiset of elements›

fun mset_tree :: "'a::linorder tree ⇒ 'a multiset" where
  "mset_tree (Node _ a ts) = {#a#} + (∑t∈#mset ts. mset_tree t)"

definition mset_forest :: "'a::linorder forest ⇒ 'a multiset" where
  "mset_forest ts = (∑t∈#mset ts. mset_tree t)"

lemma mset_tree_simp_alt[simp]:
  "mset_tree (Node r a ts) = {#a#} + mset_forest ts"
  unfolding mset_forest_def by auto
declare mset_tree.simps[simp del]

lemma mset_tree_nonempty[simp]: "mset_tree t ≠ {#}"
by (cases t) auto

lemma mset_forest_Nil[simp]:
  "mset_forest [] = {#}"
by (auto simp: mset_forest_def)

lemma mset_forest_Cons[simp]: "mset_forest (t#ts) = mset_tree t + mset_forest ts"
by (auto simp: mset_forest_def)

lemma mset_forest_empty_iff[simp]: "mset_forest ts = {#} ⟷ ts=[]"
by (auto simp: mset_forest_def)

lemma root_in_mset[simp]: "root t ∈# mset_tree t"
by (cases t) auto

lemma mset_forest_rev_eq[simp]: "mset_forest (rev ts) = mset_forest ts"
by (auto simp: mset_forest_def)

subsubsection ‹Invariants›

text ‹Binomial tree›
fun btree :: "'a::linorder tree ⇒ bool" where
"btree (Node r x ts) ⟷
   (∀t∈set ts. btree t) ∧ map rank ts = rev [0..<r]"

text ‹Heap invariant›
fun heap :: "'a::linorder tree ⇒ bool" where
"heap (Node _ x ts) ⟷ (∀t∈set ts. heap t ∧ x ≤ root t)"

definition "bheap t ⟷ btree t ∧ heap t"

text ‹Binomial Forest invariant:›
definition "invar ts ⟷ (∀t∈set ts. bheap t) ∧ (sorted_wrt (<) (map rank ts))"

text ‹A binomial forest is often called a binomial heap, but this overloads the latter term.›

text ‹The children of a binomial heap node are a valid forest:›
lemma invar_children:
  "bheap (Node r v ts) ⟹ invar (rev ts)"
  by (auto simp: bheap_def invar_def rev_map[symmetric])


subsection ‹Operations and Their Functional Correctness›

subsubsection ‹‹link››

context
includes pattern_aliases
begin

fun link :: "('a::linorder) tree ⇒ 'a tree ⇒ 'a tree" where
  "link (Node r x⇩1 ts⇩1 =: t⇩1) (Node r' x⇩2 ts⇩2 =: t⇩2) =
    (if x⇩1≤x⇩2 then Node (r+1) x⇩1 (t⇩2#ts⇩1) else Node (r+1) x⇩2 (t⇩1#ts⇩2))"

end

lemma invar_link:
  assumes "bheap t⇩1"
  assumes "bheap t⇩2"
  assumes "rank t⇩1 = rank t⇩2"
  shows "bheap (link t⇩1 t⇩2)"
using assms unfolding bheap_def
by (cases "(t⇩1, t⇩2)" rule: link.cases) auto

lemma rank_link[simp]: "rank (link t⇩1 t⇩2) = rank t⇩1 + 1"
by (cases "(t⇩1, t⇩2)" rule: link.cases) simp

lemma mset_link[simp]: "mset_tree (link t⇩1 t⇩2) = mset_tree t⇩1 + mset_tree t⇩2"
by (cases "(t⇩1, t⇩2)" rule: link.cases) simp

subsubsection ‹‹ins_tree››

fun ins_tree :: "'a::linorder tree ⇒ 'a forest ⇒ 'a forest" where
  "ins_tree t [] = [t]"
| "ins_tree t⇩1 (t⇩2#ts) =
  (if rank t⇩1 < rank t⇩2 then t⇩1#t⇩2#ts else ins_tree (link t⇩1 t⇩2) ts)"

lemma bheap0[simp]: "bheap (Node 0 x [])"
unfolding bheap_def by auto

lemma invar_Cons[simp]:
  "invar (t#ts)
  ⟷ bheap t ∧ invar ts ∧ (∀t'∈set ts. rank t < rank t')"
by (auto simp: invar_def)

lemma invar_ins_tree:
  assumes "bheap t"
  assumes "invar ts"
  assumes "∀t'∈set ts. rank t ≤ rank t'"
  shows "invar (ins_tree t ts)"
using assms
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric])

lemma mset_forest_ins_tree[simp]:
  "mset_forest (ins_tree t ts) = mset_tree t + mset_forest ts"
by (induction t ts rule: ins_tree.induct) auto

lemma ins_tree_rank_bound:
  assumes "t' ∈ set (ins_tree t ts)"
  assumes "∀t'∈set ts. rank t⇩0 < rank t'"
  assumes "rank t⇩0 < rank t"
  shows "rank t⇩0 < rank t'"
using assms
by (induction t ts rule: ins_tree.induct) (auto split: if_splits)

subsubsection ‹‹insert››

hide_const (open) insert

definition insert :: "'a::linorder ⇒ 'a forest ⇒ 'a forest" where
"insert x ts = ins_tree (Node 0 x []) ts"

lemma invar_insert[simp]: "invar t ⟹ invar (insert x t)"
by (auto intro!: invar_ins_tree simp: insert_def)

lemma mset_forest_insert[simp]: "mset_forest (insert x t) = {#x#} + mset_forest t"
by(auto simp: insert_def)

subsubsection ‹‹merge››

context
includes pattern_aliases
begin

fun merge :: "'a::linorder forest ⇒ 'a forest ⇒ 'a forest" where
  "merge ts⇩1 [] = ts⇩1"
| "merge [] ts⇩2 = ts⇩2"
| "merge (t⇩1#ts⇩1 =: f⇩1) (t⇩2#ts⇩2 =: f⇩2) = (
    if rank t⇩1 < rank t⇩2 then t⇩1 # merge ts⇩1 f⇩2 else
    if rank t⇩2 < rank t⇩1 then t⇩2 # merge f⇩1 ts⇩2
    else ins_tree (link t⇩1 t⇩2) (merge ts⇩1 ts⇩2)
  )"

end

lemma merge_simp2[simp]: "merge [] ts⇩2 = ts⇩2"
by (cases ts⇩2) auto

lemma merge_rank_bound:
  assumes "t' ∈ set (merge ts⇩1 ts⇩2)"
  assumes "∀t⇩1⇩2∈set ts⇩1 ∪ set ts⇩2. rank t < rank t⇩1⇩2"
  shows "rank t < rank t'"
using assms
by (induction ts⇩1 ts⇩2 arbitrary: t' rule: merge.induct)
   (auto split: if_splits simp: ins_tree_rank_bound)

lemma invar_merge[simp]:
  assumes "invar ts⇩1"
  assumes "invar ts⇩2"
  shows "invar (merge ts⇩1 ts⇩2)"
using assms
by (induction ts⇩1 ts⇩2 rule: merge.induct)
   (auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound)


text ‹Longer, more explicit proof of @{thm [source] invar_merge}, 
      to illustrate the application of the @{thm [source] merge_rank_bound} lemma.›
lemma 
  assumes "invar ts⇩1"
  assumes "invar ts⇩2"
  shows "invar (merge ts⇩1 ts⇩2)"
  using assms
proof (induction ts⇩1 ts⇩2 rule: merge.induct)
  case (3 t⇩1 ts⇩1 t⇩2 ts⇩2)
  ― ‹Invariants of the parts can be shown automatically›
  from "3.prems" have [simp]: 
    "bheap t⇩1" "bheap t⇩2"
    (*"invar (merge (t⇩1#ts⇩1) ts⇩2)" 
    "invar (merge ts⇩1 (t⇩2#ts⇩2))"
    "invar (merge ts⇩1 ts⇩2)"*)
    by auto

  ― ‹These are the three cases of the @{const merge} function›
  consider (LT) "rank t⇩1 < rank t⇩2"
         | (GT) "rank t⇩1 > rank t⇩2"
         | (EQ) "rank t⇩1 = rank t⇩2"
    using antisym_conv3 by blast
  then show ?case proof cases
    case LT 
    ― ‹@{const merge} takes the first tree from the left heap›
    then have "merge (t⇩1 # ts⇩1) (t⇩2 # ts⇩2) = t⇩1 # merge ts⇩1 (t⇩2 # ts⇩2)" by simp
    also have "invar …" proof (simp, intro conjI)
      ― ‹Invariant follows from induction hypothesis›
      show "invar (merge ts⇩1 (t⇩2 # ts⇩2))"
        using LT "3.IH" "3.prems" by simp

      ― ‹It remains to show that ‹t⇩1› has smallest rank.›
      show "∀t'∈set (merge ts⇩1 (t⇩2 # ts⇩2)). rank t⇩1 < rank t'"
        ― ‹Which is done by auxiliary lemma @{thm [source] merge_rank_bound}›
        using LT "3.prems" by (force elim!: merge_rank_bound)
    qed
    finally show ?thesis .
  next
    ― ‹@{const merge} takes the first tree from the right heap›
    case GT 
    ― ‹The proof is anaologous to the ‹LT› case›
    then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound)
  next
    case [simp]: EQ
    ― ‹@{const merge} links both first forest, and inserts them into the merged remaining heaps›
    have "merge (t⇩1 # ts⇩1) (t⇩2 # ts⇩2) = ins_tree (link t⇩1 t⇩2) (merge ts⇩1 ts⇩2)" by simp
    also have "invar …" proof (intro invar_ins_tree invar_link) 
      ― ‹Invariant of merged remaining heaps follows by IH›
      show "invar (merge ts⇩1 ts⇩2)"
        using EQ "3.prems" "3.IH" by auto

      ― ‹For insertion, we have to show that the rank of the linked tree is ‹≤› the 
          ranks in the merged remaining heaps›
      show "∀t'∈set (merge ts⇩1 ts⇩2). rank (link t⇩1 t⇩2) ≤ rank t'"
      proof -
        ― ‹Which is, again, done with the help of @{thm [source] merge_rank_bound}›
        have "rank (link t⇩1 t⇩2) = Suc (rank t⇩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 auto


lemma mset_forest_merge[simp]:
  "mset_forest (merge ts⇩1 ts⇩2) = mset_forest ts⇩1 + mset_forest ts⇩2"
by (induction ts⇩1 ts⇩2 rule: merge.induct) auto

subsubsection ‹‹get_min››

fun get_min :: "'a::linorder forest ⇒ 'a" where
  "get_min [t] = root t"
| "get_min (t#ts) = min (root t) (get_min ts)"

lemma bheap_root_min:
  assumes "bheap t"
  assumes "x ∈# mset_tree t"
  shows "root t ≤ x"
using assms unfolding bheap_def
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_forest_def)

lemma get_min_mset:
  assumes "ts≠[]"
  assumes "invar ts"
  assumes "x ∈# mset_forest ts"
  shows "get_min ts ≤ x"
  using assms
apply (induction ts arbitrary: x rule: get_min.induct)
apply (auto
      simp: bheap_root_min min_def intro: order_trans;
      meson linear order_trans bheap_root_min
      )+
done

lemma get_min_member:
  "ts≠[] ⟹ get_min ts ∈# mset_forest ts"
by (induction ts rule: get_min.induct) (auto simp: min_def)

lemma get_min:
  assumes "mset_forest ts ≠ {#}"
  assumes "invar ts"
  shows "get_min ts = Min_mset (mset_forest ts)"
using assms get_min_member get_min_mset
by (auto simp: eq_Min_iff)

subsubsection ‹‹get_min_rest››

fun get_min_rest :: "'a::linorder forest ⇒ 'a tree × 'a forest" where
  "get_min_rest [t] = (t,[])"
| "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts
                     in if root t ≤ root t' then (t,ts) else (t',t#ts'))"

lemma get_min_rest_get_min_same_root:
  assumes "ts≠[]"
  assumes "get_min_rest ts = (t',ts')"
  shows "root t' = get_min ts"
using assms
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)

lemma mset_get_min_rest:
  assumes "get_min_rest ts = (t',ts')"
  assumes "ts≠[]"
  shows "mset ts = {#t'#} + mset ts'"
using assms
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)

lemma set_get_min_rest:
  assumes "get_min_rest ts = (t', ts')"
  assumes "ts≠[]"
  shows "set ts = Set.insert t' (set ts')"
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
by auto

lemma invar_get_min_rest:
  assumes "get_min_rest ts = (t',ts')"
  assumes "ts≠[]"
  assumes "invar ts"
  shows "bheap t'" and "invar ts'"
proof -
  have "bheap t' ∧ invar ts'"
    using assms
    proof (induction ts arbitrary: t' ts' rule: get_min.induct)
      case (2 t v va)
      then show ?case
        apply (clarsimp split: prod.splits if_splits)
        apply (drule set_get_min_rest; fastforce)
        done
    qed auto
  thus "bheap t'" and "invar ts'" by auto
qed

subsubsection ‹‹del_min››

definition del_min :: "'a::linorder forest ⇒ 'a::linorder forest" where
"del_min ts = (case get_min_rest ts of
   (Node r x ts⇩1, ts⇩2) ⇒ merge (itrev ts⇩1 []) ts⇩2)"

lemma invar_del_min[simp]:
  assumes "ts ≠ []"
  assumes "invar ts"
  shows "invar (del_min ts)"
using assms
unfolding del_min_def itrev_Nil
by (auto
      split: prod.split tree.split
      intro!: invar_merge invar_children 
      dest: invar_get_min_rest
    )

lemma mset_forest_del_min:
  assumes "ts ≠ []"
  shows "mset_forest ts = mset_forest (del_min ts) + {# get_min ts #}"
using assms
unfolding del_min_def itrev_Nil
apply (clarsimp split: tree.split prod.split)
apply (frule (1) get_min_rest_get_min_same_root)
apply (frule (1) mset_get_min_rest)
apply (auto simp: mset_forest_def)
done


subsubsection ‹Instantiating the Priority Queue Locale›

text ‹Last step of functional correctness proof: combine all the above lemmas
to show that binomial heaps satisfy the specification of priority queues with merge.›

interpretation bheaps: Priority_Queue_Merge
  where empty = "[]" and is_empty = "(=) []" and insert = insert
  and get_min = get_min and del_min = del_min and merge = merge
  and invar = invar and mset = mset_forest
proof (unfold_locales, goal_cases)
  case 1 thus ?case by simp
next
  case 2 thus ?case by auto
next
  case 3 thus ?case by auto
next
  case (4 q)
  thus ?case using mset_forest_del_min[of q] get_min[OF _ ‹invar q›]
    by (auto simp: union_single_eq_diff)
next
  case (5 q) thus ?case using get_min[of q] by auto
next
  case 6 thus ?case by (auto simp add: invar_def)
next
  case 7 thus ?case by simp
next
  case 8 thus ?case by simp
next
  case 9 thus ?case by simp
next
  case 10 thus ?case by simp
qed


subsection ‹Complexity›

text ‹The size of a binomial tree is determined by its rank›
lemma size_mset_btree:
  assumes "btree t"
  shows "size (mset_tree t) = 2^rank t"
  using assms
proof (induction t)
  case (Node r v ts)
  hence IH: "size (mset_tree t) = 2^rank t" if "t ∈ set ts" for t
    using that by auto

  from Node have COMPL: "map rank ts = rev [0..<r]" by auto

  have "size (mset_forest ts) = (∑t←ts. size (mset_tree t))"
    by (induction ts) auto
  also have "… = (∑t←ts. 2^rank t)" using IH
    by (auto cong: map_cong)
  also have "… = (∑r←map rank ts. 2^r)"
    by (induction ts) auto
  also have "… = (∑i∈{0..<r}. 2^i)"
    unfolding COMPL
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
  also have "… = 2^r - 1"
    by (induction r) auto
  finally show ?case
    by (simp)
qed

lemma size_mset_tree:
  assumes "bheap t"
  shows "size (mset_tree t) = 2^rank t"
using assms unfolding bheap_def
by (simp add: size_mset_btree)

text ‹The length of a binomial heap is bounded by the number of its elements›
lemma size_mset_forest:
  assumes "invar ts"
  shows "length ts ≤ log 2 (size (mset_forest ts) + 1)"
proof -
  from ‹invar ts› have
    ASC: "sorted_wrt (<) (map rank ts)" and
    TINV: "∀t∈set ts. bheap t"
    unfolding invar_def by auto

  have "(2::nat)^length ts = (∑i∈{0..<length ts}. 2^i) + 1"
    by (simp add: sum_power2)
  also have "… = (∑i←[0..<length ts]. 2^i) + 1" (is "_ = ?S + 1")
    by (simp add: interv_sum_list_conv_sum_set_nat)
  also have "?S ≤ (∑t←ts. 2^rank t)" (is "_ ≤ ?T")
    using sorted_wrt_less_idx[OF ASC] by(simp add: sum_list_mono2)
  also have "?T + 1 ≤ (∑t←ts. size (mset_tree t)) + 1" using TINV
    by (auto cong: map_cong simp: size_mset_tree)
  also have "… = size (mset_forest ts) + 1"
    unfolding mset_forest_def by (induction ts) auto
  finally have "2^length ts ≤ size (mset_forest ts) + 1" by simp
  then show ?thesis using le_log2_of_power by blast
qed

subsubsection ‹Timing Functions›

time_fun link

lemma T_link[simp]: "T_link t⇩1 t⇩2 = 0"
by(cases t⇩1; cases t⇩2, auto)

time_fun rank

lemma T_rank[simp]: "T_rank t = 0"
by(cases t, auto)

time_fun ins_tree

time_fun insert

lemma T_ins_tree_simple_bound: "T_ins_tree t ts ≤ length ts + 1"
by (induction t ts rule: T_ins_tree.induct) auto

subsubsection ‹‹T_insert››

lemma T_insert_bound:
  assumes "invar ts"
  shows "T_insert x ts ≤ log 2 (size (mset_forest ts) + 1) + 1"
proof -
  have "real (T_insert x ts) ≤ real (length ts) + 1"
    unfolding T_insert.simps using T_ins_tree_simple_bound
    by (metis of_nat_1 of_nat_add of_nat_mono) 
  also note size_mset_forest[OF ‹invar ts›]
  finally show ?thesis by simp
qed

subsubsection ‹‹T_merge››

time_fun merge

(* Warning: ‹T_merge.induct› is less convenient than the equivalent ‹merge.induct›,
apparently because of the ‹let› clauses introduced by pattern_aliases; should be investigated.
*)

text ‹A crucial idea is to estimate the time in correlation with the
  result length, as each carry reduces the length of the result.›

lemma T_ins_tree_length:
  "T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
by (induction t ts rule: ins_tree.induct) auto

lemma T_merge_length:
  "T_merge ts⇩1 ts⇩2 + length (merge ts⇩1 ts⇩2) ≤ 2 * (length ts⇩1 + length ts⇩2) + 1"
by (induction ts⇩1 ts⇩2 rule: merge.induct)
   (auto simp: T_ins_tree_length algebra_simps)

text ‹Finally, we get the desired logarithmic bound›
lemma T_merge_bound:
  fixes ts⇩1 ts⇩2
  defines "n⇩1 ≡ size (mset_forest ts⇩1)"
  defines "n⇩2 ≡ size (mset_forest ts⇩2)"
  assumes "invar ts⇩1" "invar ts⇩2"
  shows "T_merge ts⇩1 ts⇩2 ≤ 4*log 2 (n⇩1 + n⇩2 + 1) + 1"
proof -
  note n_defs = assms(1,2)

  have "T_merge ts⇩1 ts⇩2 ≤ 2 * real (length ts⇩1) + 2 * real (length ts⇩2) + 1"
    using T_merge_length[of ts⇩1 ts⇩2] by simp
  also note size_mset_forest[OF ‹invar ts⇩1›]
  also note size_mset_forest[OF ‹invar ts⇩2›]
  finally have "T_merge ts⇩1 ts⇩2 ≤ 2 * log 2 (n⇩1 + 1) + 2 * log 2 (n⇩2 + 1) + 1"
    unfolding n_defs by (simp add: algebra_simps)
  also have "log 2 (n⇩1 + 1) ≤ log 2 (n⇩1 + n⇩2 + 1)" 
    unfolding n_defs by (simp add: algebra_simps)
  also have "log 2 (n⇩2 + 1) ≤ log 2 (n⇩1 + n⇩2 + 1)" 
    unfolding n_defs by (simp add: algebra_simps)
  finally show ?thesis by (simp add: algebra_simps)
qed

subsubsection ‹‹T_get_min››

time_fun root

lemma T_root[simp]: "T_root t = 0"
by(cases t)(simp_all)

time_fun min

time_fun get_min

lemma T_get_min_estimate: "ts≠[] ⟹ T_get_min ts = length ts"
by (induction ts rule: T_get_min.induct) auto

lemma T_get_min_bound:
  assumes "invar ts"
  assumes "ts≠[]"
  shows "T_get_min ts ≤ log 2 (size (mset_forest ts) + 1)"
proof -
  have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto
  also note size_mset_forest[OF ‹invar ts›]
  finally show ?thesis .
qed

subsubsection ‹‹T_del_min››

time_fun get_min_rest

lemma T_get_min_rest_estimate: "ts≠[] ⟹ T_get_min_rest ts = length ts"
  by (induction ts rule: T_get_min_rest.induct) auto

lemma T_get_min_rest_bound:
  assumes "invar ts"
  assumes "ts≠[]"
  shows "T_get_min_rest ts ≤ log 2 (size (mset_forest ts) + 1)"
proof -
  have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto
  also note size_mset_forest[OF ‹invar ts›]
  finally show ?thesis .
qed

time_fun del_min

lemma T_del_min_bound:
  fixes ts
  defines "n ≡ size (mset_forest ts)"
  assumes "invar ts" and "ts≠[]"
  shows "T_del_min ts ≤ 6 * log 2 (n+1) + 2"
proof -
  obtain r x ts⇩1 ts⇩2 where GM: "get_min_rest ts = (Node r x ts⇩1, ts⇩2)"
    by (metis surj_pair tree.exhaust_sel)

  have I1: "invar (rev ts⇩1)" and I2: "invar ts⇩2"
    using invar_get_min_rest[OF GM ‹ts≠[]› ‹invar ts›] invar_children
    by auto

  define n⇩1 where "n⇩1 = size (mset_forest ts⇩1)"
  define n⇩2 where "n⇩2 = size (mset_forest ts⇩2)"

  have "n⇩1 ≤ n" "n⇩1 + n⇩2 ≤ n" unfolding n_def n⇩1_def n⇩2_def
    using mset_get_min_rest[OF GM ‹ts≠[]›]
    by (auto simp: mset_forest_def)

  have "T_del_min ts = real (T_get_min_rest ts) + real (T_itrev ts⇩1 []) + real (T_merge (rev ts⇩1) ts⇩2)"
    unfolding T_del_min.simps GM T_itrev itrev_Nil
    by simp
  also have "T_get_min_rest ts ≤ log 2 (n+1)" 
    using T_get_min_rest_bound[OF ‹invar ts› ‹ts≠[]›] unfolding n_def by simp
  also have "T_itrev ts⇩1 [] ≤ 1 + log 2 (n⇩1 + 1)"
    unfolding T_itrev n⇩1_def using size_mset_forest[OF I1] by simp
  also have "T_merge (rev ts⇩1) ts⇩2 ≤ 4*log 2 (n⇩1 + n⇩2 + 1) + 1"
    unfolding n⇩1_def n⇩2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps)
  finally have "T_del_min ts ≤ log 2 (n+1) + log 2 (n⇩1 + 1) + 4*log 2 (real (n⇩1 + n⇩2) + 1) + 2"
    by (simp add: algebra_simps)
  also note ‹n⇩1 + n⇩2 ≤ n›
  also note ‹n⇩1 ≤ n›
  finally show ?thesis by (simp add: algebra_simps)
qed

end