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`