|
1 (* Author: Peter Lammich *) |
|
2 |
|
3 section \<open>Binomial Heap\<close> |
|
4 |
|
5 theory Binomial_Heap |
|
6 imports |
|
7 Complex_Main |
|
8 Priority_Queue |
|
9 begin |
|
10 |
|
11 lemma sum_power2: "(\<Sum>i\<in>{0..<k}. (2::nat)^i) = 2^k-1" |
|
12 by (induction k) auto |
|
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 unfolding mset_heap_def |
|
47 by auto |
|
48 |
|
49 lemma mset_heap_Cons[simp]: "mset_heap (t#ts) = mset_tree t + mset_heap ts" |
|
50 unfolding mset_heap_def by auto |
|
51 |
|
52 lemma mset_heap_empty_iff[simp]: "mset_heap ts = {#} \<longleftrightarrow> ts=[]" |
|
53 unfolding mset_heap_def by auto |
|
54 |
|
55 lemma root_in_mset[simp]: "root t \<in># mset_tree t" by (cases t) auto |
|
56 |
|
57 lemma mset_heap_rev_eq[simp]: "mset_heap (rev ts) = mset_heap ts" |
|
58 unfolding mset_heap_def by auto |
|
59 |
|
60 subsubsection \<open>Invariants\<close> |
|
61 |
|
62 text \<open>Binomial invariant\<close> |
|
63 fun invar_btree :: "'a::linorder tree \<Rightarrow> bool" |
|
64 where |
|
65 "invar_btree (Node r x ts) \<longleftrightarrow> |
|
66 (\<forall>t\<in>set ts. invar_btree t) |
|
67 \<and> (map rank ts = rev [0..<r])" |
|
68 |
|
69 definition invar_bheap :: "'a::linorder heap \<Rightarrow> bool" where |
|
70 "invar_bheap ts |
|
71 \<longleftrightarrow> (\<forall>t\<in>set ts. invar_btree t) \<and> (sorted_wrt (op <) (map rank ts))" |
|
72 |
|
73 text \<open>Ordering (heap) invariant\<close> |
|
74 fun otree_invar :: "'a::linorder tree \<Rightarrow> bool" |
|
75 where |
|
76 "otree_invar (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t \<and> x \<le> root t)" |
|
77 |
|
78 definition oheap_invar :: "'a::linorder heap \<Rightarrow> bool" where |
|
79 "oheap_invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. otree_invar t)" |
|
80 |
|
81 definition invar :: "'a::linorder heap \<Rightarrow> bool" where |
|
82 "invar ts \<longleftrightarrow> invar_bheap ts \<and> oheap_invar ts" |
|
83 |
|
84 text \<open>The children of a node are a valid heap\<close> |
|
85 lemma children_oheap_invar: |
|
86 "otree_invar (Node r v ts) \<Longrightarrow> oheap_invar (rev ts)" |
|
87 by (auto simp: oheap_invar_def) |
|
88 |
|
89 lemma children_invar_bheap: |
|
90 "invar_btree (Node r v ts) \<Longrightarrow> invar_bheap (rev ts)" |
|
91 by (auto simp: invar_bheap_def rev_map[symmetric]) |
|
92 |
|
93 subsection \<open>Operations\<close> |
|
94 |
|
95 definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
96 "link t\<^sub>1 t\<^sub>2 = (case (t\<^sub>1,t\<^sub>2) of (Node r x\<^sub>1 c\<^sub>1, Node _ x\<^sub>2 c\<^sub>2) \<Rightarrow> |
|
97 if x\<^sub>1\<le>x\<^sub>2 then Node (r+1) x\<^sub>1 (t\<^sub>2#c\<^sub>1) else Node (r+1) x\<^sub>2 (t\<^sub>1#c\<^sub>2) |
|
98 )" |
|
99 |
|
100 lemma link_invar_btree: |
|
101 assumes "invar_btree t\<^sub>1" |
|
102 assumes "invar_btree t\<^sub>2" |
|
103 assumes "rank t\<^sub>1 = rank t\<^sub>2" |
|
104 shows "invar_btree (link t\<^sub>1 t\<^sub>2)" |
|
105 using assms |
|
106 unfolding link_def |
|
107 by (force split: tree.split ) |
|
108 |
|
109 lemma link_otree_invar: |
|
110 assumes "otree_invar t\<^sub>1" |
|
111 assumes "otree_invar t\<^sub>2" |
|
112 shows "otree_invar (link t\<^sub>1 t\<^sub>2)" |
|
113 using assms |
|
114 unfolding link_def |
|
115 by (auto split: tree.split) |
|
116 |
|
117 lemma link_rank[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" |
|
118 unfolding link_def |
|
119 by (auto split: tree.split) |
|
120 |
|
121 lemma link_mset[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" |
|
122 unfolding link_def |
|
123 by (auto split: tree.split) |
|
124 |
|
125 fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
|
126 "ins_tree t [] = [t]" |
|
127 | "ins_tree t\<^sub>1 (t\<^sub>2#ts) = ( |
|
128 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 |
|
129 )" |
|
130 |
|
131 lemma invar_bheap_Cons[simp]: |
|
132 "invar_bheap (t#ts) |
|
133 \<longleftrightarrow> invar_btree t \<and> invar_bheap ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" |
|
134 unfolding invar_bheap_def |
|
135 by (auto simp: sorted_wrt_Cons) |
|
136 |
|
137 lemma ins_tree_invar_btree: |
|
138 assumes "invar_btree t" |
|
139 assumes "invar_bheap ts" |
|
140 assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'" |
|
141 shows "invar_bheap (ins_tree t ts)" |
|
142 using assms |
|
143 apply (induction t ts rule: ins_tree.induct) |
|
144 apply (auto simp: link_invar_btree less_eq_Suc_le[symmetric]) |
|
145 done |
|
146 |
|
147 lemma oheap_invar_Cons[simp]: |
|
148 "oheap_invar (t#ts) \<longleftrightarrow> otree_invar t \<and> oheap_invar ts" |
|
149 unfolding oheap_invar_def by auto |
|
150 |
|
151 lemma ins_tree_otree_invar: |
|
152 assumes "otree_invar t" |
|
153 assumes "oheap_invar ts" |
|
154 shows "oheap_invar (ins_tree t ts)" |
|
155 using assms |
|
156 apply (induction t ts rule: ins_tree.induct) |
|
157 apply (auto simp: link_otree_invar) |
|
158 done |
|
159 |
|
160 lemma ins_tree_mset[simp]: |
|
161 "mset_heap (ins_tree t ts) = mset_tree t + mset_heap ts" |
|
162 by (induction t ts rule: ins_tree.induct) auto |
|
163 |
|
164 lemma ins_tree_rank_bound: |
|
165 assumes "t' \<in> set (ins_tree t ts)" |
|
166 assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'" |
|
167 assumes "rank t\<^sub>0 < rank t" |
|
168 shows "rank t\<^sub>0 < rank t'" |
|
169 using assms |
|
170 by (induction t ts rule: ins_tree.induct) (auto split: if_splits) |
|
171 |
|
172 |
|
173 definition ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
|
174 "ins x ts = ins_tree (Node 0 x []) ts" |
|
175 |
|
176 lemma ins_invar[simp]: "invar t \<Longrightarrow> invar (ins x t)" |
|
177 unfolding ins_def invar_def |
|
178 by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar) |
|
179 |
|
180 lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t" |
|
181 unfolding ins_def |
|
182 by auto |
|
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) |
|
189 else 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" by (cases ts\<^sub>2) auto |
|
194 |
|
195 lemma merge_rank_bound: |
|
196 assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" |
|
197 assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'" |
|
198 assumes "\<forall>t'\<in>set ts\<^sub>2. rank t < rank t'" |
|
199 shows "rank t < rank t'" |
|
200 using assms |
|
201 apply (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct) |
|
202 apply (auto split: if_splits simp: ins_tree_rank_bound) |
|
203 done |
|
204 |
|
205 lemma merge_invar_bheap: |
|
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 ins_tree_invar_btree link_invar_btree) |
|
240 qed |
|
241 qed simp_all |
|
242 |
|
243 lemma merge_oheap_invar: |
|
244 assumes "oheap_invar ts\<^sub>1" |
|
245 assumes "oheap_invar ts\<^sub>2" |
|
246 shows "oheap_invar (merge ts\<^sub>1 ts\<^sub>2)" |
|
247 using assms |
|
248 apply (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) |
|
249 apply (auto simp: ins_tree_otree_invar link_otree_invar) |
|
250 done |
|
251 |
|
252 lemma merge_invar[simp]: "\<lbrakk> invar ts\<^sub>1; invar ts\<^sub>2 \<rbrakk> \<Longrightarrow> invar (merge ts\<^sub>1 ts\<^sub>2)" |
|
253 unfolding invar_def by (auto simp: merge_invar_bheap merge_oheap_invar) |
|
254 |
|
255 lemma merge_mset[simp]: |
|
256 "mset_heap (merge ts\<^sub>1 ts\<^sub>2) = mset_heap ts\<^sub>1 + mset_heap ts\<^sub>2" |
|
257 by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto |
|
258 |
|
259 |
|
260 fun find_min :: "'a::linorder heap \<Rightarrow> 'a" where |
|
261 "find_min [t] = root t" |
|
262 | "find_min (t#ts) = (let x=root t; |
|
263 y=find_min ts |
|
264 in if x\<le>y then x else y)" |
|
265 |
|
266 lemma otree_invar_root_min: |
|
267 assumes "otree_invar t" |
|
268 assumes "x \<in># mset_tree t" |
|
269 shows "root t \<le> x" |
|
270 using assms |
|
271 apply (induction t arbitrary: x rule: mset_tree.induct) |
|
272 apply (force simp: mset_heap_def) |
|
273 done |
|
274 |
|
275 |
|
276 lemma find_min_mset_aux: |
|
277 assumes "ts\<noteq>[]" |
|
278 assumes "oheap_invar ts" |
|
279 assumes "x \<in># mset_heap ts" |
|
280 shows "find_min ts \<le> x" |
|
281 using assms |
|
282 apply (induction ts arbitrary: x rule: find_min.induct) |
|
283 apply (auto |
|
284 simp: Let_def otree_invar_root_min intro: order_trans; |
|
285 meson linear order_trans otree_invar_root_min |
|
286 )+ |
|
287 done |
|
288 |
|
289 lemma find_min_mset: |
|
290 assumes "ts\<noteq>[]" |
|
291 assumes "invar ts" |
|
292 assumes "x \<in># mset_heap ts" |
|
293 shows "find_min ts \<le> x" |
|
294 using assms unfolding invar_def |
|
295 by (auto simp: find_min_mset_aux) |
|
296 |
|
297 |
|
298 lemma find_min_member: |
|
299 assumes "ts\<noteq>[]" |
|
300 shows "find_min ts \<in># mset_heap ts" |
|
301 using assms |
|
302 apply (induction ts rule: find_min.induct) |
|
303 apply (auto simp: Let_def) |
|
304 done |
|
305 |
|
306 lemma find_min: |
|
307 assumes "mset_heap ts \<noteq> {#}" |
|
308 assumes "invar ts" |
|
309 shows "find_min ts = Min_mset (mset_heap ts)" |
|
310 using assms find_min_member find_min_mset |
|
311 by (auto simp: eq_Min_iff) |
|
312 |
|
313 |
|
314 fun get_min :: "'a::linorder heap \<Rightarrow> 'a tree \<times> 'a heap" where |
|
315 "get_min [t] = (t,[])" |
|
316 | "get_min (t#ts) = (let (t',ts') = get_min ts |
|
317 in if root t \<le> root t' then (t,ts) else (t',t#ts'))" |
|
318 |
|
319 |
|
320 lemma get_min_find_min_same_root: |
|
321 assumes "ts\<noteq>[]" |
|
322 assumes "get_min ts = (t',ts')" |
|
323 shows "root t' = find_min ts" |
|
324 using assms |
|
325 apply (induction ts arbitrary: t' ts' rule: find_min.induct) |
|
326 apply (auto simp: Let_def split: prod.splits) |
|
327 done |
|
328 |
|
329 lemma get_min_mset: |
|
330 assumes "get_min ts = (t',ts')" |
|
331 assumes "ts\<noteq>[]" |
|
332 shows "mset ts = {#t'#} + mset ts'" |
|
333 using assms |
|
334 apply (induction ts arbitrary: t' ts' rule: find_min.induct) |
|
335 apply (auto split: prod.splits if_splits) |
|
336 done |
|
337 |
|
338 lemma get_min_set: |
|
339 assumes "get_min ts = (t', ts')" |
|
340 assumes "ts\<noteq>[]" |
|
341 shows "set ts = insert t' (set ts')" |
|
342 using get_min_mset[OF assms, THEN arg_cong[where f=set_mset]] |
|
343 by auto |
|
344 |
|
345 |
|
346 lemma get_min_invar_bheap: |
|
347 assumes "get_min ts = (t',ts')" |
|
348 assumes "ts\<noteq>[]" |
|
349 assumes "invar_bheap ts" |
|
350 shows "invar_btree t'" and "invar_bheap ts'" |
|
351 proof - |
|
352 have "invar_btree t' \<and> invar_bheap ts'" |
|
353 using assms |
|
354 proof (induction ts arbitrary: t' ts' rule: find_min.induct) |
|
355 case (2 t v va) |
|
356 then show ?case |
|
357 apply (clarsimp split: prod.splits if_splits) |
|
358 apply (drule get_min_set; fastforce) |
|
359 done |
|
360 qed auto |
|
361 thus "invar_btree t'" and "invar_bheap ts'" by auto |
|
362 qed |
|
363 |
|
364 lemma get_min_oheap_invar: |
|
365 assumes "get_min ts = (t',ts')" |
|
366 assumes "ts\<noteq>[]" |
|
367 assumes "oheap_invar ts" |
|
368 shows "otree_invar t'" and "oheap_invar ts'" |
|
369 using assms |
|
370 apply (induction ts arbitrary: t' ts' rule: find_min.induct) |
|
371 apply (auto split: prod.splits if_splits) |
|
372 done |
|
373 |
|
374 definition del_min :: "'a::linorder heap \<Rightarrow> 'a::linorder heap" where |
|
375 "del_min ts = (case get_min ts of |
|
376 (Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)" |
|
377 |
|
378 lemma del_min_invar[simp]: |
|
379 assumes "ts \<noteq> []" |
|
380 assumes "invar ts" |
|
381 shows "invar (del_min ts)" |
|
382 using assms |
|
383 unfolding invar_def del_min_def |
|
384 by (auto |
|
385 split: prod.split tree.split |
|
386 intro!: merge_invar_bheap merge_oheap_invar |
|
387 dest: get_min_invar_bheap get_min_oheap_invar |
|
388 intro!: children_oheap_invar children_invar_bheap |
|
389 ) |
|
390 |
|
391 lemma del_min_mset: |
|
392 assumes "ts \<noteq> []" |
|
393 shows "mset_heap ts = mset_heap (del_min ts) + {# find_min ts #}" |
|
394 using assms |
|
395 unfolding del_min_def |
|
396 apply (clarsimp split: tree.split prod.split) |
|
397 apply (frule (1) get_min_find_min_same_root) |
|
398 apply (frule (1) get_min_mset) |
|
399 apply (auto simp: mset_heap_def) |
|
400 done |
|
401 |
|
402 subsection \<open>Complexity\<close> |
|
403 |
|
404 text \<open>The size of a binomial tree is determined by its rank\<close> |
|
405 lemma size_btree: |
|
406 assumes "invar_btree t" |
|
407 shows "size (mset_tree t) = 2^rank t" |
|
408 using assms |
|
409 proof (induction t) |
|
410 case (Node r v ts) |
|
411 hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t |
|
412 using that by auto |
|
413 |
|
414 from Node have COMPL: "map rank ts = rev [0..<r]" by auto |
|
415 |
|
416 have "size (mset_heap ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))" |
|
417 by (induction ts) auto |
|
418 also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH |
|
419 by (auto cong: sum_list_cong) |
|
420 also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" |
|
421 by (induction ts) auto |
|
422 also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" |
|
423 unfolding COMPL |
|
424 by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat) |
|
425 also have "\<dots> = 2^r - 1" |
|
426 by (induction r) auto |
|
427 finally show ?case |
|
428 by (simp) |
|
429 qed |
|
430 |
|
431 text \<open>The length of a binomial heap is bounded by the number of its elements\<close> |
|
432 lemma size_bheap: |
|
433 assumes "invar_bheap ts" |
|
434 shows "2^length ts \<le> size (mset_heap ts) + 1" |
|
435 proof - |
|
436 from \<open>invar_bheap ts\<close> have |
|
437 ASC: "sorted_wrt (op <) (map rank ts)" and |
|
438 TINV: "\<forall>t\<in>set ts. invar_btree t" |
|
439 unfolding invar_bheap_def by auto |
|
440 |
|
441 have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" |
|
442 by (simp add: sum_power2) |
|
443 also have "\<dots> \<le> (\<Sum>t\<leftarrow>ts. 2^rank t) + 1" |
|
444 using sorted_wrt_less_sum_mono_lowerbound[OF _ ASC, of "op ^ (2::nat)"] |
|
445 using power_increasing[where a="2::nat"] |
|
446 by (auto simp: o_def) |
|
447 also have "\<dots> = (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV |
|
448 by (auto cong: sum_list_cong simp: size_btree) |
|
449 also have "\<dots> = size (mset_heap ts) + 1" |
|
450 unfolding mset_heap_def by (induction ts) auto |
|
451 finally show ?thesis . |
|
452 qed |
|
453 |
|
454 subsubsection \<open>Timing Functions\<close> |
|
455 text \<open> |
|
456 We define timing functions for each operation, and provide |
|
457 estimations of their complexity. |
|
458 \<close> |
|
459 definition t_link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> nat" where |
|
460 [simp]: "t_link _ _ = 1" |
|
461 |
|
462 fun t_ins_tree :: "'a::linorder tree \<Rightarrow> 'a heap \<Rightarrow> nat" where |
|
463 "t_ins_tree t [] = 1" |
|
464 | "t_ins_tree t\<^sub>1 (t\<^sub>2#rest) = ( |
|
465 (if rank t\<^sub>1 < rank t\<^sub>2 then 1 |
|
466 else t_link t\<^sub>1 t\<^sub>2 + t_ins_tree (link t\<^sub>1 t\<^sub>2) rest) |
|
467 )" |
|
468 |
|
469 |
|
470 definition t_ins :: "'a::linorder \<Rightarrow> 'a heap \<Rightarrow> nat" where |
|
471 "t_ins x ts = t_ins_tree (Node 0 x []) ts" |
|
472 |
|
473 lemma t_ins_tree_simple_bound: "t_ins_tree t ts \<le> length ts + 1" for t |
|
474 by (induction t ts rule: t_ins_tree.induct) auto |
|
475 |
|
476 lemma t_ins_bound: |
|
477 assumes "invar ts" |
|
478 shows "t_ins x ts \<le> log 2 (size (mset_heap ts) + 1) + 1" |
|
479 proof - |
|
480 |
|
481 have 1: "t_ins x ts \<le> length ts + 1" |
|
482 unfolding t_ins_def by (rule t_ins_tree_simple_bound) |
|
483 also have "\<dots> \<le> log 2 (2 * (size (mset_heap ts) + 1))" |
|
484 proof - |
|
485 from size_bheap[of ts] assms |
|
486 have "2 ^ length ts \<le> size (mset_heap ts) + 1" |
|
487 unfolding invar_def by auto |
|
488 hence "2 ^ (length ts + 1) \<le> 2 * (size (mset_heap ts) + 1)" by auto |
|
489 thus ?thesis using le_log2_of_power by blast |
|
490 qed |
|
491 finally show ?thesis |
|
492 by (simp only: log_mult of_nat_mult) auto |
|
493 qed |
|
494 |
|
495 fun t_merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> nat" where |
|
496 "t_merge ts\<^sub>1 [] = 1" |
|
497 | "t_merge [] ts\<^sub>2 = 1" |
|
498 | "t_merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = 1 + ( |
|
499 if rank t\<^sub>1 < rank t\<^sub>2 then t_merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2) |
|
500 else if rank t\<^sub>2 < rank t\<^sub>1 then t_merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2 |
|
501 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 |
|
502 )" |
|
503 |
|
504 text \<open>A crucial idea is to estimate the time in correlation with the |
|
505 result length, as each carry reduces the length of the result.\<close> |
|
506 lemma l_ins_tree_estimate: |
|
507 "t_ins_tree t ts + length (ins_tree t ts) = 2 + length ts" |
|
508 by (induction t ts rule: ins_tree.induct) auto |
|
509 |
|
510 lemma l_merge_estimate: |
|
511 "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" |
|
512 apply (induction ts\<^sub>1 ts\<^sub>2 rule: t_merge.induct) |
|
513 apply (auto simp: l_ins_tree_estimate algebra_simps) |
|
514 done |
|
515 |
|
516 text \<open>Finally, we get the desired logarithmic bound\<close> |
|
517 lemma t_merge_bound_aux: |
|
518 fixes ts\<^sub>1 ts\<^sub>2 |
|
519 defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)" |
|
520 defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)" |
|
521 assumes BINVARS: "invar_bheap ts\<^sub>1" "invar_bheap ts\<^sub>2" |
|
522 shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2" |
|
523 proof - |
|
524 define n where "n = n\<^sub>1 + n\<^sub>2" |
|
525 |
|
526 from l_merge_estimate[of ts\<^sub>1 ts\<^sub>2] |
|
527 have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" by auto |
|
528 hence "(2::nat)^t_merge ts\<^sub>1 ts\<^sub>2 \<le> 2^(2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1)" |
|
529 by (rule power_increasing) auto |
|
530 also have "\<dots> = 2*(2^length ts\<^sub>1)\<^sup>2*(2^length ts\<^sub>2)\<^sup>2" |
|
531 by (auto simp: algebra_simps power_add power_mult) |
|
532 also note BINVARS(1)[THEN size_bheap] |
|
533 also note BINVARS(2)[THEN size_bheap] |
|
534 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" |
|
535 by (auto simp: power2_nat_le_eq_le n\<^sub>1_def n\<^sub>2_def) |
|
536 from le_log2_of_power[OF this] have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 \<dots>" |
|
537 by simp |
|
538 also have "\<dots> = log 2 2 + 2*log 2 (n\<^sub>1 + 1) + 2*log 2 (n\<^sub>2 + 1)" |
|
539 by (simp add: log_mult log_nat_power) |
|
540 also have "n\<^sub>2 \<le> n" by (auto simp: n_def) |
|
541 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)" |
|
542 by auto |
|
543 also have "n\<^sub>1 \<le> n" by (auto simp: n_def) |
|
544 finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> log 2 2 + 4*log 2 (n + 1)" |
|
545 by auto |
|
546 also have "log 2 2 \<le> 2" by auto |
|
547 finally have "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n + 1) + 2" by auto |
|
548 thus ?thesis unfolding n_def by (auto simp: algebra_simps) |
|
549 qed |
|
550 |
|
551 lemma t_merge_bound: |
|
552 fixes ts\<^sub>1 ts\<^sub>2 |
|
553 defines "n\<^sub>1 \<equiv> size (mset_heap ts\<^sub>1)" |
|
554 defines "n\<^sub>2 \<equiv> size (mset_heap ts\<^sub>2)" |
|
555 assumes "invar ts\<^sub>1" "invar ts\<^sub>2" |
|
556 shows "t_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 2" |
|
557 using assms t_merge_bound_aux unfolding invar_def by blast |
|
558 |
|
559 |
|
560 fun t_find_min :: "'a::linorder heap \<Rightarrow> nat" where |
|
561 "t_find_min [t] = 1" |
|
562 | "t_find_min (t#ts) = 1 + t_find_min ts" |
|
563 |
|
564 lemma t_find_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_find_min ts = length ts" |
|
565 by (induction ts rule: t_find_min.induct) auto |
|
566 |
|
567 lemma t_find_min_bound: |
|
568 assumes "invar ts" |
|
569 assumes "ts\<noteq>[]" |
|
570 shows "t_find_min ts \<le> log 2 (size (mset_heap ts) + 1)" |
|
571 proof - |
|
572 have 1: "t_find_min ts = length ts" using assms t_find_min_estimate by auto |
|
573 also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)" |
|
574 proof - |
|
575 from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1" |
|
576 unfolding invar_def by auto |
|
577 thus ?thesis using le_log2_of_power by blast |
|
578 qed |
|
579 finally show ?thesis by auto |
|
580 qed |
|
581 |
|
582 fun t_get_min :: "'a::linorder heap \<Rightarrow> nat" where |
|
583 "t_get_min [t] = 1" |
|
584 | "t_get_min (t#ts) = 1 + t_get_min ts" |
|
585 |
|
586 lemma t_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> t_get_min ts = length ts" |
|
587 by (induction ts rule: t_get_min.induct) auto |
|
588 |
|
589 lemma t_get_min_bound_aux: |
|
590 assumes "invar_bheap ts" |
|
591 assumes "ts\<noteq>[]" |
|
592 shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)" |
|
593 proof - |
|
594 have 1: "t_get_min ts = length ts" using assms t_get_min_estimate by auto |
|
595 also have "\<dots> \<le> log 2 (size (mset_heap ts) + 1)" |
|
596 proof - |
|
597 from size_bheap[of ts] assms have "2 ^ length ts \<le> size (mset_heap ts) + 1" |
|
598 by auto |
|
599 thus ?thesis using le_log2_of_power by blast |
|
600 qed |
|
601 finally show ?thesis by auto |
|
602 qed |
|
603 |
|
604 lemma t_get_min_bound: |
|
605 assumes "invar ts" |
|
606 assumes "ts\<noteq>[]" |
|
607 shows "t_get_min ts \<le> log 2 (size (mset_heap ts) + 1)" |
|
608 using assms t_get_min_bound_aux unfolding invar_def by blast |
|
609 |
|
610 thm fold_simps -- \<open>Theorems used by code generator\<close> |
|
611 fun t_fold :: "('a \<Rightarrow> 'b \<Rightarrow> nat) \<Rightarrow> ('a \<Rightarrow> 'b \<Rightarrow> 'b) \<Rightarrow> 'a list \<Rightarrow> 'b \<Rightarrow> nat" |
|
612 where |
|
613 "t_fold t_f f [] s = 1" |
|
614 | "t_fold t_f f (x # xs) s = t_f x s + t_fold t_f f xs (f x s)" |
|
615 |
|
616 text \<open>Estimation for constant function is enough for our purpose\<close> |
|
617 lemma t_fold_const_bound: |
|
618 shows "t_fold (\<lambda>_ _. K) f l s = K*length l + 1" |
|
619 by (induction l arbitrary: s) auto |
|
620 |
|
621 lemma t_fold_bounded_bound: |
|
622 assumes "\<forall>x s. x\<in>set l \<longrightarrow> t_f x s \<le> K" |
|
623 shows "t_fold t_f f l s \<le> K*length l + 1" |
|
624 using assms |
|
625 apply (induction l arbitrary: s) |
|
626 apply (simp; fail) |
|
627 using add_mono |
|
628 by (fastforce simp: algebra_simps) |
|
629 |
|
630 thm rev_conv_fold -- \<open>Theorem used by code generator\<close> |
|
631 definition "t_rev xs = t_fold (\<lambda>_ _. 1) op # xs []" |
|
632 lemma t_rev_bound: "t_rev xs = length xs + 1" |
|
633 unfolding t_rev_def t_fold_const_bound by auto |
|
634 |
|
635 definition t_del_min :: "'a::linorder heap \<Rightarrow> nat" |
|
636 where |
|
637 "t_del_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) |
|
638 \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2 |
|
639 )" |
|
640 |
|
641 lemma t_rev_ts1_bound_aux: |
|
642 fixes ts |
|
643 defines "n \<equiv> size (mset_heap ts)" |
|
644 assumes BINVAR: "invar_bheap (rev ts)" |
|
645 shows "t_rev ts \<le> 1 + log 2 (n+1)" |
|
646 proof - |
|
647 have "t_rev ts = length ts + 1" |
|
648 by (auto simp: t_rev_bound) |
|
649 hence "2^t_rev ts = 2*2^length ts" by auto |
|
650 also have "\<dots> \<le> 2*n+2" using size_bheap[OF BINVAR] by (auto simp: n_def) |
|
651 finally have "2 ^ t_rev ts \<le> 2 * n + 2" . |
|
652 from le_log2_of_power[OF this] have "t_rev ts \<le> log 2 (2 * (n + 1))" |
|
653 by auto |
|
654 also have "\<dots> = 1 + log 2 (n+1)" |
|
655 by (simp only: of_nat_mult log_mult) auto |
|
656 finally show ?thesis by (auto simp: algebra_simps) |
|
657 qed |
|
658 |
|
659 |
|
660 lemma t_del_min_bound_aux: |
|
661 fixes ts |
|
662 defines "n \<equiv> size (mset_heap ts)" |
|
663 assumes BINVAR: "invar_bheap ts" |
|
664 assumes "ts\<noteq>[]" |
|
665 shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3" |
|
666 proof - |
|
667 obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)" |
|
668 by (metis surj_pair tree.exhaust_sel) |
|
669 |
|
670 note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR] |
|
671 hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap) |
|
672 |
|
673 define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)" |
|
674 define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)" |
|
675 |
|
676 have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)" |
|
677 proof - |
|
678 note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def] |
|
679 also have "n\<^sub>1 \<le> n" |
|
680 unfolding n\<^sub>1_def n_def |
|
681 using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>] |
|
682 by (auto simp: mset_heap_def) |
|
683 finally show ?thesis by (auto simp: algebra_simps) |
|
684 qed |
|
685 |
|
686 have "t_del_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" |
|
687 unfolding t_del_min_def by (simp add: GM) |
|
688 also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" |
|
689 using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def) |
|
690 also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1" |
|
691 using t_rev_ts1_bound by auto |
|
692 also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3" |
|
693 using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>] |
|
694 by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps) |
|
695 also have "n\<^sub>1 + n\<^sub>2 \<le> n" |
|
696 unfolding n\<^sub>1_def n\<^sub>2_def n_def |
|
697 using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>] |
|
698 by (auto simp: mset_heap_def) |
|
699 finally have "t_del_min ts \<le> 6 * log 2 (n+1) + 3" |
|
700 by auto |
|
701 thus ?thesis by (simp add: algebra_simps) |
|
702 qed |
|
703 |
|
704 lemma t_del_min_bound: |
|
705 fixes ts |
|
706 defines "n \<equiv> size (mset_heap ts)" |
|
707 assumes "invar ts" |
|
708 assumes "ts\<noteq>[]" |
|
709 shows "t_del_min ts \<le> 6 * log 2 (n+1) + 3" |
|
710 using assms t_del_min_bound_aux unfolding invar_def by blast |
|
711 |
|
712 subsection \<open>Instantiating the Priority Queue Locale\<close> |
|
713 |
|
714 interpretation binheap: |
|
715 Priority_Queue "[]" "op = []" ins find_min del_min invar mset_heap |
|
716 proof (unfold_locales, goal_cases) |
|
717 case 1 |
|
718 then show ?case by simp |
|
719 next |
|
720 case (2 q) |
|
721 then show ?case by auto |
|
722 next |
|
723 case (3 q x) |
|
724 then show ?case by auto |
|
725 next |
|
726 case (4 q) |
|
727 then show ?case using del_min_mset[of q] find_min[OF _ \<open>invar q\<close>] |
|
728 by (auto simp: union_single_eq_diff) |
|
729 next |
|
730 case (5 q) |
|
731 then show ?case using find_min[of q] by auto |
|
732 next |
|
733 case 6 |
|
734 then show ?case by (auto simp add: invar_def invar_bheap_def oheap_invar_def) |
|
735 next |
|
736 case (7 q x) |
|
737 then show ?case by simp |
|
738 next |
|
739 case (8 q) |
|
740 then show ?case by simp |
|
741 qed |
|
742 |
|
743 |
|
744 (* Exercise? *) |
|
745 subsection \<open>Combined Find and Delete Operation\<close> |
|
746 |
|
747 text \<open>We define an operation that returns the minimum element and |
|
748 a heap with this element removed. \<close> |
|
749 definition pop_min :: "'a::linorder heap \<Rightarrow> 'a \<times> 'a::linorder heap" |
|
750 where |
|
751 "pop_min ts = (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) |
|
752 \<Rightarrow> (x,merge (rev ts\<^sub>1) ts\<^sub>2) |
|
753 )" |
|
754 |
|
755 lemma pop_min_refine: |
|
756 assumes "ts \<noteq> []" |
|
757 shows "pop_min ts = (find_min ts, del_min ts)" |
|
758 unfolding pop_min_def del_min_def |
|
759 by (auto |
|
760 split: prod.split tree.split |
|
761 dest: get_min_find_min_same_root[OF assms]) |
|
762 |
|
763 lemma pop_min_invar: |
|
764 assumes "ts \<noteq> []" |
|
765 assumes "invar ts" |
|
766 assumes "pop_min ts = (x,ts')" |
|
767 shows "invar ts'" |
|
768 using del_min_invar[of ts] pop_min_refine[of ts] assms by simp |
|
769 |
|
770 lemma pop_min_mset: |
|
771 assumes "ts \<noteq> []" |
|
772 assumes "invar ts" |
|
773 assumes "pop_min ts = (x,ts')" |
|
774 shows "mset_heap ts = add_mset x (mset_heap ts')" |
|
775 using del_min_mset[of ts] pop_min_refine[of ts] assms by simp |
|
776 |
|
777 lemma pop_min_min: |
|
778 assumes "ts \<noteq> []" |
|
779 assumes "invar ts" |
|
780 assumes "pop_min ts = (x,ts')" |
|
781 shows "\<forall>y\<in>#mset_heap ts'. x\<le>y" |
|
782 using pop_min_refine[of ts] del_min_mset[of ts] find_min_mset[of ts] assms |
|
783 by (auto simp del: binheap.mset_simps) |
|
784 |
|
785 |
|
786 definition t_pop_min :: "'a::linorder heap \<Rightarrow> nat" |
|
787 where |
|
788 "t_pop_min ts = t_get_min ts + (case get_min ts of (Node _ x ts\<^sub>1, ts\<^sub>2) |
|
789 \<Rightarrow> t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2 |
|
790 )" |
|
791 |
|
792 lemma t_pop_min_bound_aux: |
|
793 fixes ts |
|
794 defines "n \<equiv> size (mset_heap ts)" |
|
795 assumes BINVAR: "invar_bheap ts" |
|
796 assumes "ts\<noteq>[]" |
|
797 shows "t_pop_min ts \<le> 6 * log 2 (n+1) + 3" |
|
798 proof - |
|
799 obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min ts = (Node r x ts\<^sub>1, ts\<^sub>2)" |
|
800 by (metis surj_pair tree.exhaust_sel) |
|
801 |
|
802 note BINVAR' = get_min_invar_bheap[OF GM \<open>ts\<noteq>[]\<close> BINVAR] |
|
803 hence BINVAR1: "invar_bheap (rev ts\<^sub>1)" by (blast intro: children_invar_bheap) |
|
804 |
|
805 define n\<^sub>1 where "n\<^sub>1 = size (mset_heap ts\<^sub>1)" |
|
806 define n\<^sub>2 where "n\<^sub>2 = size (mset_heap ts\<^sub>2)" |
|
807 |
|
808 have t_rev_ts1_bound: "t_rev ts\<^sub>1 \<le> 1 + log 2 (n+1)" |
|
809 proof - |
|
810 note t_rev_ts1_bound_aux[OF BINVAR1, simplified, folded n\<^sub>1_def] |
|
811 also have "n\<^sub>1 \<le> n" |
|
812 unfolding n\<^sub>1_def n_def |
|
813 using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>] |
|
814 by (auto simp: mset_heap_def) |
|
815 finally show ?thesis by (auto simp: algebra_simps) |
|
816 qed |
|
817 |
|
818 have "t_pop_min ts = t_get_min ts + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" |
|
819 unfolding t_pop_min_def by (simp add: GM) |
|
820 also have "\<dots> \<le> log 2 (n+1) + t_rev ts\<^sub>1 + t_merge (rev ts\<^sub>1) ts\<^sub>2" |
|
821 using t_get_min_bound_aux[OF assms(2-)] by (auto simp: n_def) |
|
822 also have "\<dots> \<le> 2*log 2 (n+1) + t_merge (rev ts\<^sub>1) ts\<^sub>2 + 1" |
|
823 using t_rev_ts1_bound by auto |
|
824 also have "\<dots> \<le> 2*log 2 (n+1) + 4 * log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 3" |
|
825 using t_merge_bound_aux[OF \<open>invar_bheap (rev ts\<^sub>1)\<close> \<open>invar_bheap ts\<^sub>2\<close>] |
|
826 by (auto simp: n\<^sub>1_def n\<^sub>2_def algebra_simps) |
|
827 also have "n\<^sub>1 + n\<^sub>2 \<le> n" |
|
828 unfolding n\<^sub>1_def n\<^sub>2_def n_def |
|
829 using get_min_mset[OF GM \<open>ts\<noteq>[]\<close>] |
|
830 by (auto simp: mset_heap_def) |
|
831 finally have "t_pop_min ts \<le> 6 * log 2 (n+1) + 3" |
|
832 by auto |
|
833 thus ?thesis by (simp add: algebra_simps) |
|
834 qed |
|
835 |
|
836 end |