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