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 \Binomial Heap\ 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 \ 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 \ nipkow@66434 21 nipkow@66434 22 subsection \Binomial Tree and Heap Datatype\ 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 \Multiset of elements\ nipkow@66434 29 nipkow@66434 30 fun mset_tree :: "'a::linorder tree \ 'a multiset" where nipkow@66434 31 "mset_tree (Node _ a c) = {#a#} + (\t\#mset c. mset_tree t)" lars@67486 32 lars@67486 33 definition mset_heap :: "'a::linorder heap \ 'a multiset" where nipkow@66434 34 "mset_heap c = (\t\#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 \ {#}" 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 = {#} \ ts=[]" nipkow@66522 52 by (auto simp: mset_heap_def) lars@67486 53 nipkow@66522 54 lemma root_in_mset[simp]: "root t \# 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 \Invariants\ lars@67486 61 lars@67486 62 text \Binomial invariant\ nipkow@66522 63 fun invar_btree :: "'a::linorder tree \ bool" where lars@67486 64 "invar_btree (Node r x ts) \ nipkow@66522 65 (\t\set ts. invar_btree t) \ map rank ts = rev [0.. bool" where nipkow@66522 68 "invar_bheap ts nipkow@67399 69 \ (\t\set ts. invar_btree t) \ (sorted_wrt (<) (map rank ts))" nipkow@66434 70 nipkow@66434 71 text \Ordering (heap) invariant\ nipkow@66522 72 fun invar_otree :: "'a::linorder tree \ bool" where nipkow@66522 73 "invar_otree (Node _ x ts) \ (\t\set ts. invar_otree t \ x \ root t)" nipkow@66434 74 nipkow@66522 75 definition invar_oheap :: "'a::linorder heap \ bool" where nipkow@66522 76 "invar_oheap ts \ (\t\set ts. invar_otree t)" lars@67486 77 nipkow@66434 78 definition invar :: "'a::linorder heap \ bool" where nipkow@66522 79 "invar ts \ invar_bheap ts \ invar_oheap ts" lars@67486 80 nipkow@66434 81 text \The children of a node are a valid heap\ lars@67486 82 lemma invar_oheap_children: lars@67486 83 "invar_otree (Node r v ts) \ 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) \ 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 \Operations and Their Functional Correctness\ lars@67486 92 nipkow@66522 93 subsubsection \\link\\ 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 \ 'a tree \ '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\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 \\ins_tree\\ nipkow@66522 127 nipkow@66434 128 fun ins_tree :: "'a::linorder tree \ 'a heap \ '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 \ invar_btree t \ invar_bheap ts \ (\t'\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 "\t'\set ts. rank t \ 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) \ invar_otree t \ 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' \ set (ins_tree t ts)" nipkow@66434 163 assumes "\t'\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 \\insert\\ nipkow@66522 170 nipkow@66522 171 hide_const (open) insert nipkow@66522 172 nipkow@66522 173 definition insert :: "'a::linorder \ 'a heap \ '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 \ 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 \\merge\\ nipkow@66491 183 nipkow@66434 184 fun merge :: "'a::linorder heap \ 'a heap \ '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' \ set (merge ts\<^sub>1 ts\<^sub>2)" nipkow@66434 198 assumes "\t'\set ts\<^sub>1. rank t < rank t'" nipkow@66434 199 assumes "\t'\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' \ 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]: "\ invar ts\<^sub>1; invar ts\<^sub>2 \ \ 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 \\get_min\\ nipkow@66434 259 nipkow@66522 260 fun get_min :: "'a::linorder heap \ '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 \# mset_tree t" lars@67486 267 shows "root t \ 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\[]" nipkow@66522 273 assumes "invar_oheap ts" lars@67486 274 assumes "x \# mset_heap ts" nipkow@66522 275 shows "get_min ts \ 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\[]" nipkow@66434 286 assumes "invar ts" lars@67486 287 assumes "x \# mset_heap ts" nipkow@66522 288 shows "get_min ts \ 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\[] \ get_min ts \# 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 \ {#}" 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 \\get_min_rest\\ nipkow@66434 303 nipkow@66522 304 fun get_min_rest :: "'a::linorder heap \ 'a tree \ '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 \ 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\[]" 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\[]" 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\[]" 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\[]" 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' \ 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\[]" 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 \\split_min\\ nipkow@66522 357 nipkow@68020 358 definition split_min :: "'a::linorder heap \ '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) \ merge (rev ts\<^sub>1) ts\<^sub>2)" lars@67486 361 nipkow@68020 362 lemma invar_split_min[simp]: nipkow@66434 363 assumes "ts \ []" 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 \ []" 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 \Instantiating the Priority Queue Locale\ nipkow@66522 388 nipkow@66565 389 text \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.\ 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 _ \invar q\] 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 \Complexity\ lars@67486 422 lars@67486 423 text \The size of a binomial tree is determined by its rank\ 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 \ 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..t\ts. size (mset_tree t))" nipkow@66434 436 by (induction ts) auto nipkow@66434 437 also have "\ = (\t\ts. 2^rank t)" using IH lars@67486 438 by (auto cong: map_cong) lars@67486 439 also have "\ = (\r\map rank ts. 2^r)" nipkow@66434 440 by (induction ts) auto lars@67486 441 also have "\ = (\i\{0.. = 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 \The length of a binomial heap is bounded by the number of its elements\ lars@67486 451 lemma size_mset_bheap: nipkow@66434 452 assumes "invar_bheap ts" nipkow@66434 453 shows "2^length ts \ size (mset_heap ts) + 1" nipkow@66434 454 proof - lars@67486 455 from \invar_bheap ts\ have nipkow@67399 456 ASC: "sorted_wrt (<) (map rank ts)" and nipkow@66434 457 TINV: "\t\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 = (\i\{0.. \ (\t\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 "\ = (\t\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 "\ = 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 \Timing Functions\ nipkow@66522 474 nipkow@66434 475 text \ nipkow@66434 476 We define timing functions for each operation, and provide nipkow@66434 477 estimations of their complexity. nipkow@66434 478 \ nipkow@66434 479 definition t_link :: "'a::linorder tree \ 'a tree \ nat" where lars@67486 480 [simp]: "t_link _ _ = 1" nipkow@66434 481 nipkow@66434 482 fun t_ins_tree :: "'a::linorder tree \ 'a heap \ 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 \ 'a heap \ 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 \ length ts + 1" nipkow@66522 493 by (induction t ts rule: t_ins_tree.induct) auto nipkow@66522 494 nipkow@66522 495 subsubsection \\t_insert\\ nipkow@66522 496 lars@67486 497 lemma t_insert_bound: nipkow@66434 498 assumes "invar ts" nipkow@66522 499 shows "t_insert x ts \ log 2 (size (mset_heap ts) + 1) + 1" nipkow@66434 500 proof - nipkow@66434 501 lars@67486 502 have 1: "t_insert x ts \ length ts + 1" nipkow@66522 503 unfolding t_insert_def by (rule t_ins_tree_simple_bound) lars@67486 504 also have "\ \ 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 \ size (mset_heap ts) + 1" nipkow@66434 508 unfolding invar_def by auto nipkow@66434 509 hence "2 ^ (length ts + 1) \ 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 \\t_merge\\ nipkow@66522 517 nipkow@66434 518 fun t_merge :: "'a::linorder heap \ 'a heap \ 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 \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.\ 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 \ 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 \Finally, we get the desired logarithmic bound\ 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 \ size (mset_heap ts\<^sub>1)" nipkow@66434 543 defines "n\<^sub>2 \ 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 \ 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 \ 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 \ 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)" nipkow@66434 552 by (rule power_increasing) auto lars@67486 553 also have "\ = 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 \ 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 \ log 2 \" nipkow@66434 560 by simp nipkow@66434 561 also have "\ = 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 \ n" by (auto simp: n_def) lars@67486 564 finally have "t_merge ts\<^sub>1 ts\<^sub>2 \ 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 \ n" by (auto simp: n_def) nipkow@66434 567 finally have "t_merge ts\<^sub>1 ts\<^sub>2 \ log 2 2 + 4*log 2 (n + 1)" nipkow@66434 568 by auto nipkow@66434 569 also have "log 2 2 \ 2" by auto nipkow@66434 570 finally have "t_merge ts\<^sub>1 ts\<^sub>2 \ 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 \ size (mset_heap ts\<^sub>1)" nipkow@66434 577 defines "n\<^sub>2 \ 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 \ 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 \\t_get_min\\ nipkow@66522 583 nipkow@66434 584 fun t_get_min :: "'a::linorder heap \ 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\[] \ 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\[]" nipkow@66434 594 shows "t_get_min ts \ 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 "\ \ 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 \ 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 \\t_split_min\\ nipkow@66522 607 nipkow@66522 608 fun t_get_min_rest :: "'a::linorder heap \ 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\[] \ 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\[]" nipkow@66522 618 shows "t_get_min_rest ts \ 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 "\ \ 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 \ 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\[]" nipkow@66522 633 shows "t_get_min_rest ts \ 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\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:\ 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 \ 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 \ 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 \ size (mset_heap ts)" nipkow@66434 650 assumes BINVAR: "invar_bheap (rev ts)" nipkow@66434 651 shows "t_rev ts \ 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 "\ \ 2*n+2" using size_mset_bheap[OF BINVAR] by (auto simp: n_def) nipkow@66434 656 finally have "2 ^ t_rev ts \ 2 * n + 2" . nipkow@66434 657 from le_log2_of_power[OF this] have "t_rev ts \ log 2 (2 * (n + 1))" nipkow@66434 658 by auto nipkow@66434 659 also have "\ = 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 \ size (mset_heap ts)" nipkow@66434 667 assumes BINVAR: "invar_bheap ts" nipkow@66434 668 assumes "ts\[]" nipkow@68020 669 shows "t_split_min ts \ 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 \ts\[]\ 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 \ 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 \ n" nipkow@66434 684 unfolding n\<^sub>1_def n_def nipkow@66522 685 using mset_get_min_rest[OF GM \ts\[]\] 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 "\ \ 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 "\ \ 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 "\ \ 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 \invar_bheap (rev ts\<^sub>1)\ \invar_bheap ts\<^sub>2\] 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 \ 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 \ts\[]\] nipkow@66434 702 by (auto simp: mset_heap_def) nipkow@68020 703 finally have "t_split_min ts \ 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 \ size (mset_heap ts)" nipkow@66434 711 assumes "invar ts" nipkow@66434 712 assumes "ts\[]" nipkow@68020 713 shows "t_split_min ts \ 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