src/HOL/Data_Structures/Binomial_Heap.thy
author nipkow
Sat Apr 21 08:41:42 2018 +0200 (14 months ago)
changeset 68020 6aade817bee5
parent 67486 d617e84bb2b1
child 68021 b91a043c0dcb
permissions -rw-r--r--
del_min -> split_min
nipkow@66522
     1
(* Author: Peter Lammich
nipkow@66522
     2
           Tobias Nipkow (tuning)
nipkow@66522
     3
*)
nipkow@66434
     4
nipkow@66434
     5
section \<open>Binomial Heap\<close>
nipkow@66434
     6
nipkow@66434
     7
theory Binomial_Heap
nipkow@66434
     8
imports
nipkow@66491
     9
  Base_FDS
nipkow@66434
    10
  Complex_Main
nipkow@66434
    11
  Priority_Queue
nipkow@66434
    12
begin
nipkow@66434
    13
nipkow@66434
    14
text \<open>
nipkow@66434
    15
  We formalize the binomial heap presentation from Okasaki's book.
nipkow@66434
    16
  We show the functional correctness and complexity of all operations.
nipkow@66434
    17
lars@67486
    18
  The presentation is engineered for simplicity, and most
nipkow@66434
    19
  proofs are straightforward and automatic.
nipkow@66434
    20
\<close>
nipkow@66434
    21
nipkow@66434
    22
subsection \<open>Binomial Tree and Heap Datatype\<close>
nipkow@66434
    23
nipkow@66434
    24
datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list")
nipkow@66434
    25
nipkow@66434
    26
type_synonym 'a heap = "'a tree list"
nipkow@66434
    27
nipkow@66434
    28
subsubsection \<open>Multiset of elements\<close>
nipkow@66434
    29
nipkow@66434
    30
fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where
nipkow@66434
    31
  "mset_tree (Node _ a c) = {#a#} + (\<Sum>t\<in>#mset c. mset_tree t)"
lars@67486
    32
lars@67486
    33
definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where
nipkow@66434
    34
  "mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)"
lars@67486
    35
lars@67486
    36
lemma mset_tree_simp_alt[simp]:
nipkow@66434
    37
  "mset_tree (Node r a c) = {#a#} + mset_heap c"
nipkow@66434
    38
  unfolding mset_heap_def by auto
lars@67486
    39
declare mset_tree.simps[simp del]
lars@67486
    40
lars@67486
    41
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}"
nipkow@66522
    42
by (cases t) auto
lars@67486
    43
lars@67486
    44
lemma mset_heap_Nil[simp]:
nipkow@66434
    45
  "mset_heap [] = {#}"
nipkow@66522
    46
by (auto simp: mset_heap_def)
nipkow@66522
    47
nipkow@66434
    48
lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts"
nipkow@66522
    49
by (auto simp: mset_heap_def)
lars@67486
    50
nipkow@66434
    51
lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]"
nipkow@66522
    52
by (auto simp: mset_heap_def)
lars@67486
    53
nipkow@66522
    54
lemma root_in_mset[simp]: "root t \<in># mset_tree t"
lars@67486
    55
by (cases t) auto
lars@67486
    56
lars@67486
    57
lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts"
nipkow@66522
    58
by (auto simp: mset_heap_def)
lars@67486
    59
lars@67486
    60
subsubsection \<open>Invariants\<close>
lars@67486
    61
lars@67486
    62
text \<open>Binomial invariant\<close>
nipkow@66522
    63
fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" where
lars@67486
    64
"invar_btree (Node r x ts) \<longleftrightarrow>
nipkow@66522
    65
   (\<forall>t\<in>set ts. invar_btree t) \<and> map rank ts = rev [0..<r]"
nipkow@66434
    66
nipkow@66434
    67
definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where
nipkow@66522
    68
"invar_bheap ts
nipkow@67399
    69
  \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (<) (map rank ts))"
nipkow@66434
    70
nipkow@66434
    71
text \<open>Ordering (heap) invariant\<close>
nipkow@66522
    72
fun invar_otree :: "'a::linorder tree \<Rightarrow> bool" where
nipkow@66522
    73
"invar_otree (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t \<and> x \<le> root t)"
nipkow@66434
    74
nipkow@66522
    75
definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where
nipkow@66522
    76
"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)"
lars@67486
    77
nipkow@66434
    78
definition invar :: "'a::linorder heap \<Rightarrow> bool" where
nipkow@66522
    79
"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts"
lars@67486
    80
nipkow@66434
    81
text \<open>The children of a node are a valid heap\<close>
lars@67486
    82
lemma invar_oheap_children:
lars@67486
    83
  "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)"
nipkow@66522
    84
by (auto simp: invar_oheap_def)
nipkow@66434
    85
lars@67486
    86
lemma invar_bheap_children:
lars@67486
    87
  "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)"
nipkow@66522
    88
by (auto simp: invar_bheap_def rev_map[symmetric])
nipkow@66522
    89
nipkow@66522
    90
lars@67486
    91
subsection \<open>Operations and Their Functional Correctness\<close>
lars@67486
    92
nipkow@66522
    93
subsubsection \<open>\<open>link\<close>\<close>
nipkow@66522
    94
nipkow@66548
    95
context
nipkow@66548
    96
includes pattern_aliases
nipkow@66548
    97
begin
nipkow@66548
    98
nipkow@66548
    99
fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where
lars@67486
   100
  "link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) =
nipkow@66549
   101
    (if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#ts\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#ts\<^sub>2))"
nipkow@66548
   102
nipkow@66548
   103
end
nipkow@66491
   104
nipkow@66522
   105
lemma invar_btree_link:
nipkow@66434
   106
  assumes "invar_btree t\<^sub>1"
nipkow@66434
   107
  assumes "invar_btree t\<^sub>2"
lars@67486
   108
  assumes "rank t\<^sub>1 = rank t\<^sub>2"
lars@67486
   109
  shows "invar_btree (link t\<^sub>1 t\<^sub>2)"
lars@67486
   110
using assms
nipkow@66548
   111
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
nipkow@66522
   112
lars@67486
   113
lemma invar_link_otree:
nipkow@66522
   114
  assumes "invar_otree t\<^sub>1"
nipkow@66522
   115
  assumes "invar_otree t\<^sub>2"
lars@67486
   116
  shows "invar_otree (link t\<^sub>1 t\<^sub>2)"
lars@67486
   117
using assms
nipkow@66548
   118
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto
nipkow@66522
   119
nipkow@66522
   120
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1"
nipkow@66548
   121
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
lars@67486
   122
nipkow@66522
   123
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2"
nipkow@66548
   124
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp
lars@67486
   125
nipkow@66522
   126
subsubsection \<open>\<open>ins_tree\<close>\<close>
nipkow@66522
   127
nipkow@66434
   128
fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow@66434
   129
  "ins_tree t [] = [t]"
nipkow@66522
   130
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) =
lars@67486
   131
  (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)"
lars@67486
   132
lars@67486
   133
lemma invar_bheap_Cons[simp]:
lars@67486
   134
  "invar_bheap (t#ts)
nipkow@66434
   135
  \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')"
nipkow@66522
   136
by (auto simp: sorted_wrt_Cons invar_bheap_def)
lars@67486
   137
nipkow@66522
   138
lemma invar_btree_ins_tree:
lars@67486
   139
  assumes "invar_btree t"
nipkow@66434
   140
  assumes "invar_bheap ts"
lars@67486
   141
  assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'"
lars@67486
   142
  shows "invar_bheap (ins_tree t ts)"
nipkow@66522
   143
using assms
nipkow@66522
   144
by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric])
lars@67486
   145
lars@67486
   146
lemma invar_oheap_Cons[simp]:
lars@67486
   147
  "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts"
nipkow@66522
   148
by (auto simp: invar_oheap_def)
nipkow@66522
   149
nipkow@66522
   150
lemma invar_oheap_ins_tree:
lars@67486
   151
  assumes "invar_otree t"
nipkow@66522
   152
  assumes "invar_oheap ts"
lars@67486
   153
  shows "invar_oheap (ins_tree t ts)"
lars@67486
   154
using assms
nipkow@66522
   155
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree)
lars@67486
   156
lars@67486
   157
lemma mset_heap_ins_tree[simp]:
lars@67486
   158
  "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts"
lars@67486
   159
by (induction t ts rule: ins_tree.induct) auto
nipkow@66434
   160
nipkow@66434
   161
lemma ins_tree_rank_bound:
lars@67486
   162
  assumes "t' \<in> set (ins_tree t ts)"
nipkow@66434
   163
  assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'"
lars@67486
   164
  assumes "rank t\<^sub>0 < rank t"
nipkow@66434
   165
  shows "rank t\<^sub>0 < rank t'"
lars@67486
   166
using assms
nipkow@66522
   167
by (induction t ts rule: ins_tree.induct) (auto split: if_splits)
nipkow@66522
   168
nipkow@66522
   169
subsubsection \<open>\<open>insert\<close>\<close>
nipkow@66522
   170
nipkow@66522
   171
hide_const (open) insert
nipkow@66522
   172
nipkow@66522
   173
definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow@66522
   174
"insert x ts = ins_tree (Node 0 x []) ts"
lars@67486
   175
nipkow@66522
   176
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)"
lars@67486
   177
by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def)
lars@67486
   178
nipkow@66522
   179
lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t"
nipkow@66522
   180
by(auto simp: insert_def)
nipkow@66522
   181
nipkow@66522
   182
subsubsection \<open>\<open>merge\<close>\<close>
nipkow@66491
   183
nipkow@66434
   184
fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where
nipkow@66434
   185
  "merge ts\<^sub>1 [] = ts\<^sub>1"
lars@67486
   186
| "merge [] ts\<^sub>2 = ts\<^sub>2"
nipkow@66434
   187
| "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = (
nipkow@66491
   188
    if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) else
nipkow@66491
   189
    if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
nipkow@66434
   190
    else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)
nipkow@66491
   191
  )"
nipkow@66491
   192
nipkow@66522
   193
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2"
nipkow@66522
   194
by (cases ts\<^sub>2) auto
lars@67486
   195
nipkow@66434
   196
lemma merge_rank_bound:
nipkow@66434
   197
  assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)"
nipkow@66434
   198
  assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'"
nipkow@66434
   199
  assumes "\<forall>t'\<in>set ts\<^sub>2. rank t < rank t'"
nipkow@66434
   200
  shows "rank t < rank t'"
nipkow@66522
   201
using assms
nipkow@66522
   202
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct)
nipkow@66522
   203
   (auto split: if_splits simp: ins_tree_rank_bound)
nipkow@66522
   204
nipkow@66522
   205
lemma invar_bheap_merge:
nipkow@66434
   206
  assumes "invar_bheap ts\<^sub>1"
nipkow@66434
   207
  assumes "invar_bheap ts\<^sub>2"
lars@67486
   208
  shows "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
nipkow@66434
   209
  using assms
nipkow@66434
   210
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
nipkow@66434
   211
  case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2)
lars@67486
   212
lars@67486
   213
  from "3.prems" have [simp]: "invar_btree t\<^sub>1" "invar_btree t\<^sub>2"
nipkow@66434
   214
    by auto
lars@67486
   215
lars@67486
   216
  consider (LT) "rank t\<^sub>1 < rank t\<^sub>2"
lars@67486
   217
         | (GT) "rank t\<^sub>1 > rank t\<^sub>2"
nipkow@66434
   218
         | (EQ) "rank t\<^sub>1 = rank t\<^sub>2"
nipkow@66434
   219
    using antisym_conv3 by blast
nipkow@66434
   220
  then show ?case proof cases
nipkow@66434
   221
    case LT
nipkow@66434
   222
    then show ?thesis using 3
nipkow@66434
   223
      by (force elim!: merge_rank_bound)
nipkow@66434
   224
  next
nipkow@66434
   225
    case GT
nipkow@66434
   226
    then show ?thesis using 3
nipkow@66434
   227
      by (force elim!: merge_rank_bound)
nipkow@66434
   228
  next
nipkow@66434
   229
    case [simp]: EQ
nipkow@66434
   230
nipkow@66434
   231
    from "3.IH"(3) "3.prems" have [simp]: "invar_bheap (merge ts\<^sub>1 ts\<^sub>2)"
nipkow@66434
   232
      by auto
lars@67486
   233
nipkow@66434
   234
    have "rank t\<^sub>2 < rank t'" if "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" for t'
nipkow@66434
   235
      using that
nipkow@66434
   236
      apply (rule merge_rank_bound)
nipkow@66434
   237
      using "3.prems" by auto
nipkow@66434
   238
    with EQ show ?thesis
nipkow@66522
   239
      by (auto simp: Suc_le_eq invar_btree_ins_tree invar_btree_link)
nipkow@66434
   240
  qed
nipkow@66434
   241
qed simp_all
lars@67486
   242
nipkow@66522
   243
lemma invar_oheap_merge:
nipkow@66522
   244
  assumes "invar_oheap ts\<^sub>1"
nipkow@66522
   245
  assumes "invar_oheap ts\<^sub>2"
lars@67486
   246
  shows "invar_oheap (merge ts\<^sub>1 ts\<^sub>2)"
nipkow@66522
   247
using assms
nipkow@66522
   248
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct)
lars@67486
   249
   (auto simp: invar_oheap_ins_tree invar_link_otree)
lars@67486
   250
nipkow@66522
   251
lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)"
nipkow@66522
   252
by (auto simp: invar_def invar_bheap_merge invar_oheap_merge)
lars@67486
   253
lars@67486
   254
lemma mset_heap_merge[simp]:
nipkow@66434
   255
  "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2"
lars@67486
   256
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto
lars@67486
   257
nipkow@66522
   258
subsubsection \<open>\<open>get_min\<close>\<close>
nipkow@66434
   259
nipkow@66522
   260
fun get_min :: "'a::linorder heap \<Rightarrow> 'a" where
nipkow@66522
   261
  "get_min [t] = root t"
nipkow@66546
   262
| "get_min (t#ts) = min (root t) (get_min ts)"
lars@67486
   263
nipkow@66522
   264
lemma invar_otree_root_min:
nipkow@66522
   265
  assumes "invar_otree t"
lars@67486
   266
  assumes "x \<in># mset_tree t"
lars@67486
   267
  shows "root t \<le> x"
nipkow@66522
   268
using assms
nipkow@66522
   269
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def)
lars@67486
   270
lars@67486
   271
lemma get_min_mset_aux:
lars@67486
   272
  assumes "ts\<noteq>[]"
nipkow@66522
   273
  assumes "invar_oheap ts"
lars@67486
   274
  assumes "x \<in># mset_heap ts"
nipkow@66522
   275
  shows "get_min ts \<le> x"
lars@67486
   276
  using assms
lars@67486
   277
apply (induction ts arbitrary: x rule: get_min.induct)
lars@67486
   278
apply (auto
nipkow@66546
   279
      simp: invar_otree_root_min min_def intro: order_trans;
nipkow@66522
   280
      meson linear order_trans invar_otree_root_min
nipkow@66434
   281
      )+
lars@67486
   282
done
nipkow@66434
   283
lars@67486
   284
lemma get_min_mset:
lars@67486
   285
  assumes "ts\<noteq>[]"
nipkow@66434
   286
  assumes "invar ts"
lars@67486
   287
  assumes "x \<in># mset_heap ts"
nipkow@66522
   288
  shows "get_min ts \<le> x"
nipkow@66522
   289
using assms by (auto simp: invar_def get_min_mset_aux)
nipkow@66434
   290
lars@67486
   291
lemma get_min_member:
lars@67486
   292
  "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts"
nipkow@66546
   293
by (induction ts rule: get_min.induct) (auto simp: min_def)
nipkow@66522
   294
lars@67486
   295
lemma get_min:
nipkow@66434
   296
  assumes "mset_heap ts \<noteq> {#}"
nipkow@66434
   297
  assumes "invar ts"
nipkow@66522
   298
  shows "get_min ts = Min_mset (mset_heap ts)"
lars@67486
   299
using assms get_min_member get_min_mset
nipkow@66522
   300
by (auto simp: eq_Min_iff)
lars@67486
   301
nipkow@66522
   302
subsubsection \<open>\<open>get_min_rest\<close>\<close>
nipkow@66434
   303
nipkow@66522
   304
fun get_min_rest :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where
nipkow@66522
   305
  "get_min_rest [t] = (t,[])"
nipkow@66522
   306
| "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts
nipkow@66434
   307
                     in if root t \<le> root t' then (t,ts) else (t',t#ts'))"
nipkow@66434
   308
lars@67486
   309
lemma get_min_rest_get_min_same_root:
nipkow@66434
   310
  assumes "ts\<noteq>[]"
lars@67486
   311
  assumes "get_min_rest ts = (t',ts')"
lars@67486
   312
  shows "root t' = get_min ts"
lars@67486
   313
using assms
nipkow@66546
   314
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits)
nipkow@66522
   315
lars@67486
   316
lemma mset_get_min_rest:
lars@67486
   317
  assumes "get_min_rest ts = (t',ts')"
nipkow@66434
   318
  assumes "ts\<noteq>[]"
lars@67486
   319
  shows "mset ts = {#t'#} + mset ts'"
lars@67486
   320
using assms
nipkow@66522
   321
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
lars@67486
   322
nipkow@66522
   323
lemma set_get_min_rest:
lars@67486
   324
  assumes "get_min_rest ts = (t', ts')"
nipkow@66434
   325
  assumes "ts\<noteq>[]"
nipkow@66522
   326
  shows "set ts = Set.insert t' (set ts')"
nipkow@66522
   327
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]]
lars@67486
   328
by auto
nipkow@66434
   329
lars@67486
   330
lemma invar_bheap_get_min_rest:
lars@67486
   331
  assumes "get_min_rest ts = (t',ts')"
nipkow@66434
   332
  assumes "ts\<noteq>[]"
lars@67486
   333
  assumes "invar_bheap ts"
nipkow@66434
   334
  shows "invar_btree t'" and "invar_bheap ts'"
nipkow@66434
   335
proof -
nipkow@66434
   336
  have "invar_btree t' \<and> invar_bheap ts'"
lars@67486
   337
    using assms
nipkow@66522
   338
    proof (induction ts arbitrary: t' ts' rule: get_min.induct)
nipkow@66434
   339
      case (2 t v va)
nipkow@66434
   340
      then show ?case
nipkow@66434
   341
        apply (clarsimp split: prod.splits if_splits)
nipkow@66522
   342
        apply (drule set_get_min_rest; fastforce)
lars@67486
   343
        done
nipkow@66434
   344
    qed auto
nipkow@66434
   345
  thus "invar_btree t'" and "invar_bheap ts'" by auto
nipkow@66434
   346
qed
nipkow@66522
   347
lars@67486
   348
lemma invar_oheap_get_min_rest:
lars@67486
   349
  assumes "get_min_rest ts = (t',ts')"
nipkow@66434
   350
  assumes "ts\<noteq>[]"
lars@67486
   351
  assumes "invar_oheap ts"
nipkow@66522
   352
  shows "invar_otree t'" and "invar_oheap ts'"
lars@67486
   353
using assms
nipkow@66522
   354
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits)
nipkow@66522
   355
nipkow@68020
   356
subsubsection \<open>\<open>split_min\<close>\<close>
nipkow@66522
   357
nipkow@68020
   358
definition split_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where
nipkow@68020
   359
"split_min ts = (case get_min_rest ts of
nipkow@66434
   360
   (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)"
lars@67486
   361
nipkow@68020
   362
lemma invar_split_min[simp]:
nipkow@66434
   363
  assumes "ts \<noteq> []"
nipkow@66434
   364
  assumes "invar ts"
nipkow@68020
   365
  shows "invar (split_min ts)"
lars@67486
   366
using assms
nipkow@68020
   367
unfolding invar_def split_min_def
lars@67486
   368
by (auto
lars@67486
   369
      split: prod.split tree.split
nipkow@66522
   370
      intro!: invar_bheap_merge invar_oheap_merge
nipkow@66522
   371
      dest: invar_bheap_get_min_rest invar_oheap_get_min_rest
nipkow@66522
   372
      intro!: invar_oheap_children invar_bheap_children
nipkow@66522
   373
    )
lars@67486
   374
nipkow@68020
   375
lemma mset_heap_split_min:
nipkow@66434
   376
  assumes "ts \<noteq> []"
nipkow@68020
   377
  shows "mset_heap ts = mset_heap (split_min ts) + {# get_min ts #}"
nipkow@66522
   378
using assms
nipkow@68020
   379
unfolding split_min_def
nipkow@66522
   380
apply (clarsimp split: tree.split prod.split)
lars@67486
   381
apply (frule (1) get_min_rest_get_min_same_root)
lars@67486
   382
apply (frule (1) mset_get_min_rest)
nipkow@66522
   383
apply (auto simp: mset_heap_def)
lars@67486
   384
done
nipkow@66522
   385
nipkow@66522
   386
nipkow@66522
   387
subsubsection \<open>Instantiating the Priority Queue Locale\<close>
nipkow@66522
   388
nipkow@66565
   389
text \<open>Last step of functional correctness proof: combine all the above lemmas
nipkow@66565
   390
to show that binomial heaps satisfy the specification of priority queues with merge.\<close>
nipkow@66565
   391
nipkow@66565
   392
interpretation binheap: Priority_Queue_Merge
nipkow@67399
   393
  where empty = "[]" and is_empty = "(=) []" and insert = insert
nipkow@68020
   394
  and get_min = get_min and split_min = split_min and merge = merge
nipkow@66522
   395
  and invar = invar and mset = mset_heap
nipkow@66522
   396
proof (unfold_locales, goal_cases)
nipkow@66565
   397
  case 1 thus ?case by simp
nipkow@66522
   398
next
nipkow@66565
   399
  case 2 thus ?case by auto
nipkow@66522
   400
next
nipkow@66565
   401
  case 3 thus ?case by auto
nipkow@66522
   402
next
nipkow@66522
   403
  case (4 q)
nipkow@68020
   404
  thus ?case using mset_heap_split_min[of q] get_min[OF _ \<open>invar q\<close>]
nipkow@66522
   405
    by (auto simp: union_single_eq_diff)
nipkow@66522
   406
next
nipkow@66565
   407
  case (5 q) thus ?case using get_min[of q] by auto
lars@67486
   408
next
nipkow@66565
   409
  case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def)
nipkow@66565
   410
next
nipkow@66565
   411
  case 7 thus ?case by simp
nipkow@66522
   412
next
nipkow@66565
   413
  case 8 thus ?case by simp
nipkow@66522
   414
next
nipkow@66565
   415
  case 9 thus ?case by simp
nipkow@66565
   416
next
nipkow@66565
   417
  case 10 thus ?case by simp
nipkow@66522
   418
qed
nipkow@66522
   419
nipkow@66434
   420
nipkow@66434
   421
subsection \<open>Complexity\<close>
lars@67486
   422
lars@67486
   423
text \<open>The size of a binomial tree is determined by its rank\<close>
nipkow@66522
   424
lemma size_mset_btree:
nipkow@66434
   425
  assumes "invar_btree t"
lars@67486
   426
  shows "size (mset_tree t) = 2^rank t"
nipkow@66434
   427
  using assms
nipkow@66434
   428
proof (induction t)
nipkow@66434
   429
  case (Node r v ts)
nipkow@66434
   430
  hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t
nipkow@66434
   431
    using that by auto
lars@67486
   432
nipkow@66434
   433
  from Node have COMPL: "map rank ts = rev [0..<r]" by auto
lars@67486
   434
nipkow@66434
   435
  have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))"
nipkow@66434
   436
    by (induction ts) auto
nipkow@66434
   437
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH
lars@67486
   438
    by (auto cong: map_cong)
lars@67486
   439
  also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)"
nipkow@66434
   440
    by (induction ts) auto
lars@67486
   441
  also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)"
lars@67486
   442
    unfolding COMPL
nipkow@66434
   443
    by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat)
lars@67486
   444
  also have "\<dots> = 2^r - 1"
nipkow@66434
   445
    by (induction r) auto
lars@67486
   446
  finally show ?case
nipkow@66434
   447
    by (simp)
nipkow@66434
   448
qed
lars@67486
   449
lars@67486
   450
text \<open>The length of a binomial heap is bounded by the number of its elements\<close>
lars@67486
   451
lemma size_mset_bheap:
nipkow@66434
   452
  assumes "invar_bheap ts"
nipkow@66434
   453
  shows "2^length ts \<le> size (mset_heap ts) + 1"
nipkow@66434
   454
proof -
lars@67486
   455
  from \<open>invar_bheap ts\<close> have
nipkow@67399
   456
    ASC: "sorted_wrt (<) (map rank ts)" and
nipkow@66434
   457
    TINV: "\<forall>t\<in>set ts. invar_btree t"
nipkow@66434
   458
    unfolding invar_bheap_def by auto
lars@67486
   459
lars@67486
   460
  have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1"
nipkow@66434
   461
    by (simp add: sum_power2)
nipkow@66434
   462
  also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1"
nipkow@67399
   463
    using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "(^) (2::nat)"]
lars@67486
   464
    using power_increasing[where a="2::nat"]
nipkow@66434
   465
    by (auto simp: o_def)
lars@67486
   466
  also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV
lars@67486
   467
    by (auto cong: map_cong simp: size_mset_btree)
nipkow@66434
   468
  also have "\<dots> = size (mset_heap ts) + 1"
nipkow@66434
   469
    unfolding mset_heap_def by (induction ts) auto
nipkow@66434
   470
  finally show ?thesis .
lars@67486
   471
qed
lars@67486
   472
nipkow@66522
   473
subsubsection \<open>Timing Functions\<close>
nipkow@66522
   474
nipkow@66434
   475
text \<open>
nipkow@66434
   476
  We define timing functions for each operation, and provide
nipkow@66434
   477
  estimations of their complexity.
nipkow@66434
   478
\<close>
nipkow@66434
   479
definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where
lars@67486
   480
[simp]: "t_link _ _ = 1"
nipkow@66434
   481
nipkow@66434
   482
fun t_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where
nipkow@66434
   483
  "t_ins_tree t [] = 1"
nipkow@66522
   484
| "t_ins_tree t\<^sub>1 (t\<^sub>2 # rest) = (
lars@67486
   485
    (if rank t\<^sub>1 < rank t\<^sub>2 then 1
nipkow@66434
   486
     else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest)
lars@67486
   487
  )"
nipkow@66522
   488
nipkow@66522
   489
definition t_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where
nipkow@66522
   490
"t_insert x ts = t_ins_tree (Node 0 x []) ts"
nipkow@66434
   491
nipkow@66522
   492
lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1"
nipkow@66522
   493
by (induction t ts rule: t_ins_tree.induct) auto
nipkow@66522
   494
nipkow@66522
   495
subsubsection \<open>\<open>t_insert\<close>\<close>
nipkow@66522
   496
lars@67486
   497
lemma t_insert_bound:
nipkow@66434
   498
  assumes "invar ts"
nipkow@66522
   499
  shows "t_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1"
nipkow@66434
   500
proof -
nipkow@66434
   501
lars@67486
   502
  have 1: "t_insert x ts \<le> length ts + 1"
nipkow@66522
   503
    unfolding t_insert_def by (rule t_ins_tree_simple_bound)
lars@67486
   504
  also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))"
nipkow@66434
   505
  proof -
lars@67486
   506
    from size_mset_bheap[of ts] assms
nipkow@66434
   507
    have "2 ^ length ts \<le> size (mset_heap ts) + 1"
nipkow@66434
   508
      unfolding invar_def by auto
nipkow@66434
   509
    hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto
nipkow@66434
   510
    thus ?thesis using le_log2_of_power by blast
nipkow@66434
   511
  qed
lars@67486
   512
  finally show ?thesis
nipkow@66434
   513
    by (simp only: log_mult of_nat_mult) auto
lars@67486
   514
qed
nipkow@66522
   515
nipkow@66522
   516
subsubsection \<open>\<open>t_merge\<close>\<close>
nipkow@66522
   517
nipkow@66434
   518
fun t_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where
nipkow@66434
   519
  "t_merge ts\<^sub>1 [] = 1"
lars@67486
   520
| "t_merge [] ts\<^sub>2 = 1"
nipkow@66434
   521
| "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + (
nipkow@66434
   522
    if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2)
nipkow@66434
   523
    else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2
nipkow@66434
   524
    else t_ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2
lars@67486
   525
  )"
lars@67486
   526
lars@67486
   527
text \<open>A crucial idea is to estimate the time in correlation with the
lars@67486
   528
  result length, as each carry reduces the length of the result.\<close>
nipkow@66522
   529
nipkow@66522
   530
lemma t_ins_tree_length:
nipkow@66434
   531
  "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts"
nipkow@66434
   532
by (induction t ts rule: ins_tree.induct) auto
nipkow@66434
   533
lars@67486
   534
lemma t_merge_length:
nipkow@66434
   535
  "length (merge ts\<^sub>1 ts\<^sub>2) + t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1"
lars@67486
   536
by (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct)
nipkow@66522
   537
   (auto simp: t_ins_tree_length algebra_simps)
nipkow@66522
   538
nipkow@66434
   539
text \<open>Finally, we get the desired logarithmic bound\<close>
nipkow@66434
   540
lemma t_merge_bound_aux:
nipkow@66434
   541
  fixes ts\<^sub>1 ts\<^sub>2
lars@67486
   542
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
nipkow@66434
   543
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
nipkow@66434
   544
  assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2"
nipkow@66434
   545
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
nipkow@66434
   546
proof -
lars@67486
   547
  define n where "n = n\<^sub>1 + n\<^sub>2"
lars@67486
   548
lars@67486
   549
  from t_merge_length[of ts\<^sub>1 ts\<^sub>2]
nipkow@66434
   550
  have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto
lars@67486
   551
  hence "(2::nat)^t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)"
nipkow@66434
   552
    by (rule power_increasing) auto
lars@67486
   553
  also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2"
nipkow@66434
   554
    by (auto simp: algebra_simps power_add power_mult)
nipkow@66547
   555
  also note BINVARS(1)[THEN size_mset_bheap]
nipkow@66547
   556
  also note BINVARS(2)[THEN size_mset_bheap]
lars@67486
   557
  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"
nipkow@66434
   558
    by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def)
lars@67486
   559
  from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>"
nipkow@66434
   560
    by simp
nipkow@66434
   561
  also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)"
nipkow@66434
   562
    by (simp add: log_mult log_nat_power)
nipkow@66434
   563
  also have "n\<^sub>2 \<le> n" by (auto simp: n_def)
lars@67486
   564
  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)"
nipkow@66434
   565
    by auto
nipkow@66434
   566
  also have "n\<^sub>1 \<le> n" by (auto simp: n_def)
nipkow@66434
   567
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)"
nipkow@66434
   568
    by auto
nipkow@66434
   569
  also have "log 2 2 \<le> 2" by auto
nipkow@66434
   570
  finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto
nipkow@66434
   571
  thus ?thesis unfolding n_def by (auto simp: algebra_simps)
lars@67486
   572
qed
lars@67486
   573
nipkow@66434
   574
lemma t_merge_bound:
nipkow@66434
   575
  fixes ts\<^sub>1 ts\<^sub>2
lars@67486
   576
  defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)"
nipkow@66434
   577
  defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)"
nipkow@66434
   578
  assumes "invar ts\<^sub>1" "invar ts\<^sub>2"
nipkow@66434
   579
  shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2"
lars@67486
   580
using assms t_merge_bound_aux unfolding invar_def by blast
nipkow@66434
   581
nipkow@66522
   582
subsubsection \<open>\<open>t_get_min\<close>\<close>
nipkow@66522
   583
nipkow@66434
   584
fun t_get_min :: "'a::linorder heap \<Rightarrow> nat" where
nipkow@66434
   585
  "t_get_min [t] = 1"
nipkow@66434
   586
| "t_get_min (t#ts) = 1 + t_get_min ts"
nipkow@66434
   587
lars@67486
   588
lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts"
nipkow@66522
   589
by (induction ts rule: t_get_min.induct) auto
lars@67486
   590
lars@67486
   591
lemma t_get_min_bound:
nipkow@66522
   592
  assumes "invar ts"
nipkow@66434
   593
  assumes "ts\<noteq>[]"
nipkow@66434
   594
  shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)"
nipkow@66434
   595
proof -
nipkow@66434
   596
  have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto
nipkow@66434
   597
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
nipkow@66434
   598
  proof -
nipkow@66547
   599
    from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
nipkow@66522
   600
      unfolding invar_def by auto
nipkow@66522
   601
    thus ?thesis using le_log2_of_power by blast
nipkow@66522
   602
  qed
lars@67486
   603
  finally show ?thesis by auto
lars@67486
   604
qed
nipkow@66522
   605
nipkow@68020
   606
subsubsection \<open>\<open>t_split_min\<close>\<close>
nipkow@66522
   607
nipkow@66522
   608
fun t_get_min_rest :: "'a::linorder heap \<Rightarrow> nat" where
nipkow@66522
   609
  "t_get_min_rest [t] = 1"
nipkow@66522
   610
| "t_get_min_rest (t#ts) = 1 + t_get_min_rest ts"
nipkow@66522
   611
lars@67486
   612
lemma t_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min_rest ts = length ts"
nipkow@66522
   613
  by (induction ts rule: t_get_min_rest.induct) auto
lars@67486
   614
lars@67486
   615
lemma t_get_min_rest_bound_aux:
nipkow@66522
   616
  assumes "invar_bheap ts"
nipkow@66522
   617
  assumes "ts\<noteq>[]"
nipkow@66522
   618
  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
nipkow@66522
   619
proof -
nipkow@66522
   620
  have 1: "t_get_min_rest ts = length ts" using assms t_get_min_rest_estimate by auto
nipkow@66522
   621
  also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)"
nipkow@66522
   622
  proof -
nipkow@66547
   623
    from size_mset_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1"
nipkow@66434
   624
      by auto
nipkow@66434
   625
    thus ?thesis using le_log2_of_power by blast
nipkow@66434
   626
  qed
lars@67486
   627
  finally show ?thesis by auto
lars@67486
   628
qed
nipkow@66434
   629
lars@67486
   630
lemma t_get_min_rest_bound:
nipkow@66434
   631
  assumes "invar ts"
nipkow@66434
   632
  assumes "ts\<noteq>[]"
nipkow@66522
   633
  shows "t_get_min_rest ts \<le> log 2 (size (mset_heap ts) + 1)"
lars@67486
   634
using assms t_get_min_rest_bound_aux unfolding invar_def by blast
nipkow@66434
   635
nipkow@66522
   636
text\<open>Note that although the definition of function @{const rev} has quadratic complexity,
nipkow@66522
   637
it can and is implemented (via suitable code lemmas) as a linear time function.
nipkow@66522
   638
Thus the following definition is justified:\<close>
nipkow@66522
   639
nipkow@66522
   640
definition "t_rev xs = length xs + 1"
nipkow@66522
   641
nipkow@68020
   642
definition t_split_min :: "'a::linorder heap \<Rightarrow> nat" where
nipkow@68020
   643
  "t_split_min ts = t_get_min_rest ts + (case get_min_rest ts of (Node _ x ts\<^sub>1, ts\<^sub>2)
nipkow@66434
   644
                    \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2
nipkow@66434
   645
  )"
lars@67486
   646
lars@67486
   647
lemma t_rev_ts1_bound_aux:
nipkow@66434
   648
  fixes ts
nipkow@66434
   649
  defines "n \<equiv> size (mset_heap ts)"
nipkow@66434
   650
  assumes BINVAR: "invar_bheap (rev ts)"
nipkow@66434
   651
  shows "t_rev ts \<le> 1 + log 2 (n+1)"
nipkow@66434
   652
proof -
nipkow@66522
   653
  have "t_rev ts = length ts + 1" by (auto simp: t_rev_def)
nipkow@66434
   654
  hence "2^t_rev ts = 2*2^length ts" by auto
nipkow@66547
   655
  also have "\<dots> \<le> 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def)
nipkow@66434
   656
  finally have "2 ^ t_rev ts \<le> 2 * n + 2" .
nipkow@66434
   657
  from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))"
nipkow@66434
   658
    by auto
nipkow@66434
   659
  also have "\<dots> = 1 + log 2 (n+1)"
lars@67486
   660
    by (simp only: of_nat_mult log_mult) auto
nipkow@66434
   661
  finally show ?thesis by (auto simp: algebra_simps)
lars@67486
   662
qed
nipkow@66522
   663
nipkow@68020
   664
lemma t_split_min_bound_aux:
nipkow@66434
   665
  fixes ts
nipkow@66434
   666
  defines "n \<equiv> size (mset_heap ts)"
nipkow@66434
   667
  assumes BINVAR: "invar_bheap ts"
nipkow@66434
   668
  assumes "ts\<noteq>[]"
nipkow@68020
   669
  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
nipkow@66434
   670
proof -
nipkow@66522
   671
  obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)"
nipkow@66434
   672
    by (metis surj_pair tree.exhaust_sel)
nipkow@66434
   673
nipkow@66522
   674
  note BINVAR' = invar_bheap_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> BINVAR]
nipkow@66522
   675
  hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: invar_bheap_children)
nipkow@66434
   676
nipkow@66434
   677
  define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)"
nipkow@66434
   678
  define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)"
lars@67486
   679
nipkow@66434
   680
  have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)"
nipkow@66434
   681
  proof -
nipkow@66434
   682
    note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def]
lars@67486
   683
    also have "n\<^sub>1 \<le> n"
nipkow@66434
   684
      unfolding n\<^sub>1_def n_def
nipkow@66522
   685
      using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
nipkow@66434
   686
      by (auto simp: mset_heap_def)
nipkow@66434
   687
    finally show ?thesis by (auto simp: algebra_simps)
lars@67486
   688
  qed
lars@67486
   689
nipkow@68020
   690
  have "t_split_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
nipkow@68020
   691
    unfolding t_split_min_def by (simp add: GM)
nipkow@66434
   692
  also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2"
nipkow@66522
   693
    using t_get_min_rest_bound_aux[OF assms(2-)] by (auto simp: n_def)
nipkow@66434
   694
  also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1"
nipkow@66434
   695
    using t_rev_ts1_bound by auto
nipkow@66434
   696
  also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3"
nipkow@66434
   697
    using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>]
nipkow@66434
   698
    by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps)
nipkow@66434
   699
  also have "n\<^sub>1 + n\<^sub>2 \<le> n"
nipkow@66434
   700
    unfolding n\<^sub>1_def n\<^sub>2_def n_def
nipkow@66522
   701
    using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>]
nipkow@66434
   702
    by (auto simp: mset_heap_def)
nipkow@68020
   703
  finally have "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
nipkow@66434
   704
    by auto
nipkow@66434
   705
  thus ?thesis by (simp add: algebra_simps)
lars@67486
   706
qed
lars@67486
   707
nipkow@68020
   708
lemma t_split_min_bound:
nipkow@66434
   709
  fixes ts
nipkow@66434
   710
  defines "n \<equiv> size (mset_heap ts)"
nipkow@66434
   711
  assumes "invar ts"
nipkow@66434
   712
  assumes "ts\<noteq>[]"
nipkow@68020
   713
  shows "t_split_min ts \<le> 6 * log 2 (n+1) + 3"
nipkow@68020
   714
using assms t_split_min_bound_aux unfolding invar_def by blast
nipkow@66434
   715
lars@67486
   716
end