94 |
92 |
95 definition link :: "'a::linorder tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
93 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> |
94 "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) |
95 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 )" |
96 )" |
99 |
97 |
100 lemma link_invar_btree: |
98 lemma link_invar_btree: |
101 assumes "invar_btree t\<^sub>1" |
99 assumes "invar_btree t\<^sub>1" |
102 assumes "invar_btree t\<^sub>2" |
100 assumes "invar_btree t\<^sub>2" |
103 assumes "rank t\<^sub>1 = rank t\<^sub>2" |
101 assumes "rank t\<^sub>1 = rank t\<^sub>2" |
104 shows "invar_btree (link t\<^sub>1 t\<^sub>2)" |
102 shows "invar_btree (link t\<^sub>1 t\<^sub>2)" |
105 using assms |
103 using assms |
106 unfolding link_def |
104 unfolding link_def |
107 by (force split: tree.split ) |
105 by (force split: tree.split) |
108 |
106 |
109 lemma link_otree_invar: |
107 lemma link_otree_invar: |
110 assumes "otree_invar t\<^sub>1" |
108 assumes "otree_invar t\<^sub>1" |
111 assumes "otree_invar t\<^sub>2" |
109 assumes "otree_invar t\<^sub>2" |
112 shows "otree_invar (link t\<^sub>1 t\<^sub>2)" |
110 shows "otree_invar (link t\<^sub>1 t\<^sub>2)" |
177 unfolding ins_def invar_def |
175 unfolding ins_def invar_def |
178 by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar) |
176 by (auto intro!: ins_tree_invar_btree simp: ins_tree_otree_invar) |
179 |
177 |
180 lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t" |
178 lemma ins_mset[simp]: "mset_heap (ins x t) = {#x#} + mset_heap t" |
181 unfolding ins_def |
179 unfolding ins_def |
182 by auto |
180 by auto |
183 |
181 |
184 fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
182 fun merge :: "'a::linorder heap \<Rightarrow> 'a heap \<Rightarrow> 'a heap" where |
185 "merge ts\<^sub>1 [] = ts\<^sub>1" |
183 "merge ts\<^sub>1 [] = ts\<^sub>1" |
186 | "merge [] ts\<^sub>2 = ts\<^sub>2" |
184 | "merge [] ts\<^sub>2 = ts\<^sub>2" |
187 | "merge (t\<^sub>1#ts\<^sub>1) (t\<^sub>2#ts\<^sub>2) = ( |
185 | "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) |
186 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 else if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2#merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2 |
187 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) |
188 else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) |
191 )" |
189 )" |
192 |
190 |
193 lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto |
191 lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" by (cases ts\<^sub>2) auto |
194 |
192 |
195 lemma merge_rank_bound: |
193 lemma merge_rank_bound: |
196 assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" |
194 assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" |
197 assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'" |
195 assumes "\<forall>t'\<in>set ts\<^sub>1. rank t < rank t'" |
279 assumes "x \<in># mset_heap ts" |
277 assumes "x \<in># mset_heap ts" |
280 shows "find_min ts \<le> x" |
278 shows "find_min ts \<le> x" |
281 using assms |
279 using assms |
282 apply (induction ts arbitrary: x rule: find_min.induct) |
280 apply (induction ts arbitrary: x rule: find_min.induct) |
283 apply (auto |
281 apply (auto |
284 simp: Let_def otree_invar_root_min intro: order_trans; |
282 simp: otree_invar_root_min intro: order_trans; |
285 meson linear order_trans otree_invar_root_min |
283 meson linear order_trans otree_invar_root_min |
286 )+ |
284 )+ |
287 done |
285 done |
288 |
286 |
289 lemma find_min_mset: |
287 lemma find_min_mset: |
298 lemma find_min_member: |
296 lemma find_min_member: |
299 assumes "ts\<noteq>[]" |
297 assumes "ts\<noteq>[]" |
300 shows "find_min ts \<in># mset_heap ts" |
298 shows "find_min ts \<in># mset_heap ts" |
301 using assms |
299 using assms |
302 apply (induction ts rule: find_min.induct) |
300 apply (induction ts rule: find_min.induct) |
303 apply (auto simp: Let_def) |
301 apply (auto) |
304 done |
302 done |
305 |
303 |
306 lemma find_min: |
304 lemma find_min: |
307 assumes "mset_heap ts \<noteq> {#}" |
305 assumes "mset_heap ts \<noteq> {#}" |
308 assumes "invar ts" |
306 assumes "invar ts" |
321 assumes "ts\<noteq>[]" |
319 assumes "ts\<noteq>[]" |
322 assumes "get_min ts = (t',ts')" |
320 assumes "get_min ts = (t',ts')" |
323 shows "root t' = find_min ts" |
321 shows "root t' = find_min ts" |
324 using assms |
322 using assms |
325 apply (induction ts arbitrary: t' ts' rule: find_min.induct) |
323 apply (induction ts arbitrary: t' ts' rule: find_min.induct) |
326 apply (auto simp: Let_def split: prod.splits) |
324 apply (auto split: prod.splits) |
327 done |
325 done |
328 |
326 |
329 lemma get_min_mset: |
327 lemma get_min_mset: |
330 assumes "get_min ts = (t',ts')" |
328 assumes "get_min ts = (t',ts')" |
331 assumes "ts\<noteq>[]" |
329 assumes "ts\<noteq>[]" |
332 shows "mset ts = {#t'#} + mset ts'" |
330 shows "mset ts = {#t'#} + mset ts'" |