1(* Author: Peter Lammich 2 Tobias Nipkow (tuning) 3*) 4 5section \<open>Binomial Heap\<close> 6 7theory Binomial_Heap 8imports 9 Base_FDS 10 Complex_Main 11 Priority_Queue_Specs 12begin 13 14text \<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 22subsection \<open>Binomial Tree and Heap Datatype\<close> 23 24datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list") 25 26type_synonym 'a heap = "'a tree list" 27 28subsubsection \<open>Multiset of elements\<close> 29 30fun 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 33definition mset_heap :: "'a::linorder heap \<Rightarrow> 'a multiset" where 34 "mset_heap c = (\<Sum>t\<in>#mset c. mset_tree t)" 35 36lemma mset_tree_simp_alt[simp]: 37 "mset_tree (Node r a c) = {#a#} + mset_heap c" 38 unfolding mset_heap_def by auto 39declare mset_tree.simps[simp del] 40 41lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}" 42by (cases t) auto 43 44lemma mset_heap_Nil[simp]: 45 "mset_heap [] = {#}" 46by (auto simp: mset_heap_def) 47 48lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts" 49by (auto simp: mset_heap_def) 50 51lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]" 52by (auto simp: mset_heap_def) 53 54lemma root_in_mset[simp]: "root t \<in># mset_tree t" 55by (cases t) auto 56 57lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts" 58by (auto simp: mset_heap_def) 59 60subsubsection \<open>Invariants\<close> 61 62text \<open>Binomial invariant\<close> 63fun 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 67definition 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 71text \<open>Ordering (heap) invariant\<close> 72fun 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 75definition invar_oheap :: "'a::linorder heap \<Rightarrow> bool" where 76"invar_oheap ts \<longleftrightarrow> (\<forall>t\<in>set ts. invar_otree t)" 77 78definition invar :: "'a::linorder heap \<Rightarrow> bool" where 79"invar ts \<longleftrightarrow> invar_bheap ts \<and> invar_oheap ts" 80 81text \<open>The children of a node are a valid heap\<close> 82lemma invar_oheap_children: 83 "invar_otree (Node r v ts) \<Longrightarrow> invar_oheap (rev ts)" 84by (auto simp: invar_oheap_def) 85 86lemma invar_bheap_children: 87 "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)" 88by (auto simp: invar_bheap_def rev_map[symmetric]) 89 90 91subsection \<open>Operations and Their Functional Correctness\<close> 92 93subsubsection \<open>\<open>link\<close>\<close> 94 95context 96includes pattern_aliases 97begin 98 99fun 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 103end 104 105lemma 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)" 110using assms 111by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 112 113lemma 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)" 117using assms 118by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto 119 120lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" 121by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 122 123lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" 124by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp 125 126subsubsection \<open>\<open>ins_tree\<close>\<close> 127 128fun 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 133lemma 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')" 136by (auto simp: invar_bheap_def) 137 138lemma 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)" 143using assms 144by (induction t ts rule: ins_tree.induct) (auto simp: invar_btree_link less_eq_Suc_le[symmetric]) 145 146lemma invar_oheap_Cons[simp]: 147 "invar_oheap (t#ts) \<longleftrightarrow> invar_otree t \<and> invar_oheap ts" 148by (auto simp: invar_oheap_def) 149 150lemma invar_oheap_ins_tree: 151 assumes "invar_otree t" 152 assumes "invar_oheap ts" 153 shows "invar_oheap (ins_tree t ts)" 154using assms 155by (induction t ts rule: ins_tree.induct) (auto simp: invar_link_otree) 156 157lemma mset_heap_ins_tree[simp]: 158 "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" 159by (induction t ts rule: ins_tree.induct) auto 160 161lemma 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'" 166using assms 167by (induction t ts rule: ins_tree.induct) (auto split: if_splits) 168 169subsubsection \<open>\<open>insert\<close>\<close> 170 171hide_const (open) insert 172 173definition insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where 174"insert x ts = ins_tree (Node 0 x []) ts" 175 176lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)" 177by (auto intro!: invar_btree_ins_tree simp: invar_oheap_ins_tree insert_def invar_def) 178 179lemma mset_heap_insert[simp]: "mset_heap (insert x t) = {#x#} + mset_heap t" 180by(auto simp: insert_def) 181 182subsubsection \<open>\<open>merge\<close>\<close> 183 184fun 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 193lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" 194by (cases ts\<^sub>2) auto 195 196lemma 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'" 201using assms 202by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct) 203 (auto split: if_splits simp: ins_tree_rank_bound) 204 205lemma 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 210proof (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 241qed simp_all 242 243lemma 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)" 247using assms 248by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) 249 (auto simp: invar_oheap_ins_tree invar_link_otree) 250 251lemma invar_merge[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)" 252by (auto simp: invar_def invar_bheap_merge invar_oheap_merge) 253 254lemma mset_heap_merge[simp]: 255 "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2" 256by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto 257 258subsubsection \<open>\<open>get_min\<close>\<close> 259 260fun 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 264lemma invar_otree_root_min: 265 assumes "invar_otree t" 266 assumes "x \<in># mset_tree t" 267 shows "root t \<le> x" 268using assms 269by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_heap_def) 270 271lemma 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 277apply (induction ts arbitrary: x rule: get_min.induct) 278apply (auto 279 simp: invar_otree_root_min min_def intro: order_trans; 280 meson linear order_trans invar_otree_root_min 281 )+ 282done 283 284lemma 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" 289using assms by (auto simp: invar_def get_min_mset_aux) 290 291lemma get_min_member: 292 "ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_heap ts" 293by (induction ts rule: get_min.induct) (auto simp: min_def) 294 295lemma get_min: 296 assumes "mset_heap ts \<noteq> {#}" 297 assumes "invar ts" 298 shows "get_min ts = Min_mset (mset_heap ts)" 299using assms get_min_member get_min_mset 300by (auto simp: eq_Min_iff) 301 302subsubsection \<open>\<open>get_min_rest\<close>\<close> 303 304fun 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 309lemma 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" 313using assms 314by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits) 315 316lemma mset_get_min_rest: 317 assumes "get_min_rest ts = (t',ts')" 318 assumes "ts\<noteq>[]" 319 shows "mset ts = {#t'#} + mset ts'" 320using assms 321by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) 322 323lemma 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')" 327using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]] 328by auto 329 330lemma 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'" 335proof - 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 346qed 347 348lemma 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'" 353using assms 354by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) 355 356subsubsection \<open>\<open>del_min\<close>\<close> 357 358definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where 359"del_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 362lemma invar_del_min[simp]: 363 assumes "ts \<noteq> []" 364 assumes "invar ts" 365 shows "invar (del_min ts)" 366using assms 367unfolding invar_def del_min_def 368by (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 375lemma mset_heap_del_min: 376 assumes "ts \<noteq> []" 377 shows "mset_heap ts = mset_heap (del_min ts) + {# get_min ts #}" 378using assms 379unfolding del_min_def 380apply (clarsimp split: tree.split prod.split) 381apply (frule (1) get_min_rest_get_min_same_root) 382apply (frule (1) mset_get_min_rest) 383apply (auto simp: mset_heap_def) 384done 385 386 387subsubsection \<open>Instantiating the Priority Queue Locale\<close> 388 389text \<open>Last step of functional correctness proof: combine all the above lemmas 390to show that binomial heaps satisfy the specification of priority queues with merge.\<close> 391 392interpretation binheap: Priority_Queue_Merge 393 where empty = "[]" and is_empty = "(=) []" and insert = insert 394 and get_min = get_min and del_min = del_min and merge = merge 395 and invar = invar and mset = mset_heap 396proof (unfold_locales, goal_cases) 397 case 1 thus ?case by simp 398next 399 case 2 thus ?case by auto 400next 401 case 3 thus ?case by auto 402next 403 case (4 q) 404 thus ?case using mset_heap_del_min[of q] get_min[OF _ \<open>invar q\<close>] 405 by (auto simp: union_single_eq_diff) 406next 407 case (5 q) thus ?case using get_min[of q] by auto 408next 409 case 6 thus ?case by (auto simp add: invar_def invar_bheap_def invar_oheap_def) 410next 411 case 7 thus ?case by simp 412next 413 case 8 thus ?case by simp 414next 415 case 9 thus ?case by simp 416next 417 case 10 thus ?case by simp 418qed 419 420 421subsection \<open>Complexity\<close> 422 423text \<open>The size of a binomial tree is determined by its rank\<close> 424lemma size_mset_btree: 425 assumes "invar_btree t" 426 shows "size (mset_tree t) = 2^rank t" 427 using assms 428proof (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) 448qed 449 450text \<open>The length of a binomial heap is bounded by the number of its elements\<close> 451lemma size_mset_bheap: 452 assumes "invar_bheap ts" 453 shows "2^length ts \<le> size (mset_heap ts) + 1" 454proof - 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 . 471qed 472 473subsubsection \<open>Timing Functions\<close> 474 475text \<open> 476 We define timing functions for each operation, and provide 477 estimations of their complexity. 478\<close> 479definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where 480[simp]: "t_link _ _ = 1" 481 482fun 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 489definition t_insert :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where 490"t_insert x ts = t_ins_tree (Node 0 x []) ts" 491 492lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" 493by (induction t ts rule: t_ins_tree.induct) auto 494 495subsubsection \<open>\<open>t_insert\<close>\<close> 496 497lemma t_insert_bound: 498 assumes "invar ts" 499 shows "t_insert x ts \<le> log 2 (size (mset_heap ts) + 1) + 1" 500proof - 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 514qed 515 516subsubsection \<open>\<open>t_merge\<close>\<close> 517 518fun 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 527text \<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 530lemma t_ins_tree_length: 531 "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts" 532by (induction t ts rule: ins_tree.induct) auto 533 534lemma 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" 536by (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct) 537 (auto simp: t_ins_tree_length algebra_simps) 538 539text \<open>Finally, we get the desired logarithmic bound\<close> 540lemma 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" 546proof - 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) 572qed 573 574lemma 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" 580using assms t_merge_bound_aux unfolding invar_def by blast 581 582subsubsection \<open>\<open>t_get_min\<close>\<close> 583 584fun 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 588lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts" 589by (induction ts rule: t_get_min.induct) auto 590 591lemma 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)" 595proof - 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 604qed 605 606subsubsection \<open>\<open>t_del_min\<close>\<close> 607 608fun 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 612lemma 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 615lemma 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)" 619proof - 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 628qed 629 630lemma 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)" 634using assms t_get_min_rest_bound_aux unfolding invar_def by blast 635 636text\<open>Note that although the definition of function @{const rev} has quadratic complexity, 637it can and is implemented (via suitable code lemmas) as a linear time function. 638Thus the following definition is justified:\<close> 639 640definition "t_rev xs = length xs + 1" 641 642definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" where 643 "t_del_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 647lemma 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)" 652proof - 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) 662qed 663 664lemma t_del_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_del_min ts \<le> 6 * log 2 (n+1) + 3" 670proof - 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_del_min ts = t_get_min_rest ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" 691 unfolding t_del_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_del_min ts \<le> 6 * log 2 (n+1) + 3" 704 by auto 705 thus ?thesis by (simp add: algebra_simps) 706qed 707 708lemma t_del_min_bound: 709 fixes ts 710 defines "n \<equiv> size (mset_heap ts)" 711 assumes "invar ts" 712 assumes "ts\<noteq>[]" 713 shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3" 714using assms t_del_min_bound_aux unfolding invar_def by blast 715 716end