author | nipkow |
Mon, 19 Feb 2024 08:23:23 +0100 | |
changeset 79666 | 65223730d7e1 |
parent 79138 | e6ae63d1b480 |
child 79969 | 4aeb25ba90f3 |
permissions | -rw-r--r-- |
66522 | 1 |
(* Author: Peter Lammich |
2 |
Tobias Nipkow (tuning) |
|
3 |
*) |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
4 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
5 |
section \<open>Binomial Heap\<close> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
6 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
7 |
theory Binomial_Heap |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
8 |
imports |
70450 | 9 |
"HOL-Library.Pattern_Aliases" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
10 |
Complex_Main |
72812 | 11 |
Priority_Queue_Specs |
79666 | 12 |
Define_Time_Function |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
13 |
begin |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
14 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
15 |
text \<open> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
16 |
We formalize the binomial heap presentation from Okasaki's book. |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
17 |
We show the functional correctness and complexity of all operations. |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
18 |
|
67486 | 19 |
The presentation is engineered for simplicity, and most |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
20 |
proofs are straightforward and automatic. |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
21 |
\<close> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
22 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
23 |
subsection \<open>Binomial Tree and Heap Datatype\<close> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
24 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
25 |
datatype 'a tree = Node (rank: nat) (root: 'a) (children: "'a tree list") |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
26 |
|
75667 | 27 |
type_synonym 'a trees = "'a tree list" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
28 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
29 |
subsubsection \<open>Multiset of elements\<close> |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
30 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
31 |
fun mset_tree :: "'a::linorder tree \<Rightarrow> 'a multiset" where |
70607 | 32 |
"mset_tree (Node _ a ts) = {#a#} + (\<Sum>t\<in>#mset ts. mset_tree t)" |
67486 | 33 |
|
75667 | 34 |
definition mset_trees :: "'a::linorder trees \<Rightarrow> 'a multiset" where |
35 |
"mset_trees ts = (\<Sum>t\<in>#mset ts. mset_tree t)" |
|
67486 | 36 |
|
37 |
lemma mset_tree_simp_alt[simp]: |
|
75667 | 38 |
"mset_tree (Node r a ts) = {#a#} + mset_trees ts" |
39 |
unfolding mset_trees_def by auto |
|
67486 | 40 |
declare mset_tree.simps[simp del] |
41 |
||
42 |
lemma mset_tree_nonempty[simp]: "mset_tree t \<noteq> {#}" |
|
66522 | 43 |
by (cases t) auto |
67486 | 44 |
|
75667 | 45 |
lemma mset_trees_Nil[simp]: |
46 |
"mset_trees [] = {#}" |
|
47 |
by (auto simp: mset_trees_def) |
|
66522 | 48 |
|
75667 | 49 |
lemma mset_trees_Cons[simp]: "mset_trees (t#ts) = mset_tree t + mset_trees ts" |
50 |
by (auto simp: mset_trees_def) |
|
67486 | 51 |
|
75667 | 52 |
lemma mset_trees_empty_iff[simp]: "mset_trees ts = {#} \<longleftrightarrow> ts=[]" |
53 |
by (auto simp: mset_trees_def) |
|
67486 | 54 |
|
66522 | 55 |
lemma root_in_mset[simp]: "root t \<in># mset_tree t" |
67486 | 56 |
by (cases t) auto |
57 |
||
75667 | 58 |
lemma mset_trees_rev_eq[simp]: "mset_trees (rev ts) = mset_trees ts" |
59 |
by (auto simp: mset_trees_def) |
|
67486 | 60 |
|
61 |
subsubsection \<open>Invariants\<close> |
|
62 |
||
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
63 |
text \<open>Binomial tree\<close> |
75667 | 64 |
fun btree :: "'a::linorder tree \<Rightarrow> bool" where |
65 |
"btree (Node r x ts) \<longleftrightarrow> |
|
66 |
(\<forall>t\<in>set ts. btree t) \<and> map rank ts = rev [0..<r]" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
67 |
|
75667 | 68 |
text \<open>Heap invariant\<close> |
69 |
fun heap :: "'a::linorder tree \<Rightarrow> bool" where |
|
70 |
"heap (Node _ x ts) \<longleftrightarrow> (\<forall>t\<in>set ts. heap t \<and> x \<le> root t)" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
71 |
|
75667 | 72 |
definition "bheap t \<longleftrightarrow> btree t \<and> heap t" |
67486 | 73 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
74 |
text \<open>Binomial Heap invariant\<close> |
75667 | 75 |
definition "invar ts \<longleftrightarrow> (\<forall>t\<in>set ts. bheap t) \<and> (sorted_wrt (<) (map rank ts))" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
76 |
|
67486 | 77 |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
78 |
text \<open>The children of a node are a valid heap\<close> |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
79 |
lemma invar_children: |
75667 | 80 |
"bheap (Node r v ts) \<Longrightarrow> invar (rev ts)" |
81 |
by (auto simp: bheap_def invar_def rev_map[symmetric]) |
|
66522 | 82 |
|
83 |
||
67486 | 84 |
subsection \<open>Operations and Their Functional Correctness\<close> |
85 |
||
66522 | 86 |
subsubsection \<open>\<open>link\<close>\<close> |
87 |
||
66548 | 88 |
context |
89 |
includes pattern_aliases |
|
90 |
begin |
|
91 |
||
92 |
fun link :: "('a::linorder) tree \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
67486 | 93 |
"link (Node r x\<^sub>1 ts\<^sub>1 =: t\<^sub>1) (Node r' x\<^sub>2 ts\<^sub>2 =: t\<^sub>2) = |
66549 | 94 |
(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))" |
66548 | 95 |
|
96 |
end |
|
66491 | 97 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
98 |
lemma invar_link: |
75667 | 99 |
assumes "bheap t\<^sub>1" |
100 |
assumes "bheap t\<^sub>2" |
|
67486 | 101 |
assumes "rank t\<^sub>1 = rank t\<^sub>2" |
75667 | 102 |
shows "bheap (link t\<^sub>1 t\<^sub>2)" |
103 |
using assms unfolding bheap_def |
|
66548 | 104 |
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) auto |
66522 | 105 |
|
106 |
lemma rank_link[simp]: "rank (link t\<^sub>1 t\<^sub>2) = rank t\<^sub>1 + 1" |
|
66548 | 107 |
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp |
67486 | 108 |
|
66522 | 109 |
lemma mset_link[simp]: "mset_tree (link t\<^sub>1 t\<^sub>2) = mset_tree t\<^sub>1 + mset_tree t\<^sub>2" |
66548 | 110 |
by (cases "(t\<^sub>1, t\<^sub>2)" rule: link.cases) simp |
67486 | 111 |
|
66522 | 112 |
subsubsection \<open>\<open>ins_tree\<close>\<close> |
113 |
||
75667 | 114 |
fun ins_tree :: "'a::linorder tree \<Rightarrow> 'a trees \<Rightarrow> 'a trees" where |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
115 |
"ins_tree t [] = [t]" |
66522 | 116 |
| "ins_tree t\<^sub>1 (t\<^sub>2#ts) = |
67486 | 117 |
(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)" |
118 |
||
75667 | 119 |
lemma bheap0[simp]: "bheap (Node 0 x [])" |
120 |
unfolding bheap_def by auto |
|
67486 | 121 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
122 |
lemma invar_Cons[simp]: |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
123 |
"invar (t#ts) |
75667 | 124 |
\<longleftrightarrow> bheap t \<and> invar ts \<and> (\<forall>t'\<in>set ts. rank t < rank t')" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
125 |
by (auto simp: invar_def) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
126 |
|
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
127 |
lemma invar_ins_tree: |
75667 | 128 |
assumes "bheap t" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
129 |
assumes "invar ts" |
67486 | 130 |
assumes "\<forall>t'\<in>set ts. rank t \<le> rank t'" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
131 |
shows "invar (ins_tree t ts)" |
66522 | 132 |
using assms |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
133 |
by (induction t ts rule: ins_tree.induct) (auto simp: invar_link less_eq_Suc_le[symmetric]) |
67486 | 134 |
|
75667 | 135 |
lemma mset_trees_ins_tree[simp]: |
136 |
"mset_trees (ins_tree t ts) = mset_tree t + mset_trees ts" |
|
67486 | 137 |
by (induction t ts rule: ins_tree.induct) auto |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
138 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
139 |
lemma ins_tree_rank_bound: |
67486 | 140 |
assumes "t' \<in> set (ins_tree t ts)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
141 |
assumes "\<forall>t'\<in>set ts. rank t\<^sub>0 < rank t'" |
67486 | 142 |
assumes "rank t\<^sub>0 < rank t" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
143 |
shows "rank t\<^sub>0 < rank t'" |
67486 | 144 |
using assms |
66522 | 145 |
by (induction t ts rule: ins_tree.induct) (auto split: if_splits) |
146 |
||
147 |
subsubsection \<open>\<open>insert\<close>\<close> |
|
148 |
||
149 |
hide_const (open) insert |
|
150 |
||
75667 | 151 |
definition insert :: "'a::linorder \<Rightarrow> 'a trees \<Rightarrow> 'a trees" where |
66522 | 152 |
"insert x ts = ins_tree (Node 0 x []) ts" |
67486 | 153 |
|
66522 | 154 |
lemma invar_insert[simp]: "invar t \<Longrightarrow> invar (insert x t)" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
155 |
by (auto intro!: invar_ins_tree simp: insert_def) |
67486 | 156 |
|
75667 | 157 |
lemma mset_trees_insert[simp]: "mset_trees (insert x t) = {#x#} + mset_trees t" |
66522 | 158 |
by(auto simp: insert_def) |
159 |
||
160 |
subsubsection \<open>\<open>merge\<close>\<close> |
|
66491 | 161 |
|
70607 | 162 |
context |
163 |
includes pattern_aliases |
|
164 |
begin |
|
165 |
||
75667 | 166 |
fun merge :: "'a::linorder trees \<Rightarrow> 'a trees \<Rightarrow> 'a trees" where |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
167 |
"merge ts\<^sub>1 [] = ts\<^sub>1" |
67486 | 168 |
| "merge [] ts\<^sub>2 = ts\<^sub>2" |
70607 | 169 |
| "merge (t\<^sub>1#ts\<^sub>1 =: h\<^sub>1) (t\<^sub>2#ts\<^sub>2 =: h\<^sub>2) = ( |
170 |
if rank t\<^sub>1 < rank t\<^sub>2 then t\<^sub>1 # merge ts\<^sub>1 h\<^sub>2 else |
|
171 |
if rank t\<^sub>2 < rank t\<^sub>1 then t\<^sub>2 # merge h\<^sub>1 ts\<^sub>2 |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
172 |
else ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2) |
66491 | 173 |
)" |
174 |
||
70607 | 175 |
end |
176 |
||
66522 | 177 |
lemma merge_simp2[simp]: "merge [] ts\<^sub>2 = ts\<^sub>2" |
178 |
by (cases ts\<^sub>2) auto |
|
67486 | 179 |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
180 |
lemma merge_rank_bound: |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
181 |
assumes "t' \<in> set (merge ts\<^sub>1 ts\<^sub>2)" |
70607 | 182 |
assumes "\<forall>t\<^sub>1\<in>set ts\<^sub>1. rank t < rank t\<^sub>1" |
183 |
assumes "\<forall>t\<^sub>2\<in>set ts\<^sub>2. rank t < rank t\<^sub>2" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
184 |
shows "rank t < rank t'" |
66522 | 185 |
using assms |
186 |
by (induction ts\<^sub>1 ts\<^sub>2 arbitrary: t' rule: merge.induct) |
|
187 |
(auto split: if_splits simp: ins_tree_rank_bound) |
|
188 |
||
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
189 |
lemma invar_merge[simp]: |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
190 |
assumes "invar ts\<^sub>1" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
191 |
assumes "invar ts\<^sub>2" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
192 |
shows "invar (merge ts\<^sub>1 ts\<^sub>2)" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
193 |
using assms |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
194 |
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
195 |
(auto 0 3 simp: Suc_le_eq intro!: invar_ins_tree invar_link elim!: merge_rank_bound) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
196 |
|
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
197 |
|
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
198 |
text \<open>Longer, more explicit proof of @{thm [source] invar_merge}, |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
199 |
to illustrate the application of the @{thm [source] merge_rank_bound} lemma.\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
200 |
lemma |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
201 |
assumes "invar ts\<^sub>1" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
202 |
assumes "invar ts\<^sub>2" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
203 |
shows "invar (merge ts\<^sub>1 ts\<^sub>2)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
204 |
using assms |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
205 |
proof (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
206 |
case (3 t\<^sub>1 ts\<^sub>1 t\<^sub>2 ts\<^sub>2) |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
207 |
\<comment> \<open>Invariants of the parts can be shown automatically\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
208 |
from "3.prems" have [simp]: |
75667 | 209 |
"bheap t\<^sub>1" "bheap t\<^sub>2" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
210 |
(*"invar (merge (t\<^sub>1#ts\<^sub>1) ts\<^sub>2)" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
211 |
"invar (merge ts\<^sub>1 (t\<^sub>2#ts\<^sub>2))" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
212 |
"invar (merge ts\<^sub>1 ts\<^sub>2)"*) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
213 |
by auto |
67486 | 214 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
215 |
\<comment> \<open>These are the three cases of the @{const merge} function\<close> |
67486 | 216 |
consider (LT) "rank t\<^sub>1 < rank t\<^sub>2" |
217 |
| (GT) "rank t\<^sub>1 > rank t\<^sub>2" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
218 |
| (EQ) "rank t\<^sub>1 = rank t\<^sub>2" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
219 |
using antisym_conv3 by blast |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
220 |
then show ?case proof cases |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
221 |
case LT |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
222 |
\<comment> \<open>@{const merge} takes the first tree from the left heap\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
223 |
then have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = t\<^sub>1 # merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)" by simp |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
224 |
also have "invar \<dots>" proof (simp, intro conjI) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
225 |
\<comment> \<open>Invariant follows from induction hypothesis\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
226 |
show "invar (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2))" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
227 |
using LT "3.IH" "3.prems" by simp |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
228 |
|
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
229 |
\<comment> \<open>It remains to show that \<open>t\<^sub>1\<close> has smallest rank.\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
230 |
show "\<forall>t'\<in>set (merge ts\<^sub>1 (t\<^sub>2 # ts\<^sub>2)). rank t\<^sub>1 < rank t'" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
231 |
\<comment> \<open>Which is done by auxiliary lemma @{thm [source] merge_rank_bound}\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
232 |
using LT "3.prems" by (force elim!: merge_rank_bound) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
233 |
qed |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
234 |
finally show ?thesis . |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
235 |
next |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
236 |
\<comment> \<open>@{const merge} takes the first tree from the right heap\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
237 |
case GT |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
238 |
\<comment> \<open>The proof is anaologous to the \<open>LT\<close> case\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
239 |
then show ?thesis using "3.prems" "3.IH" by (force elim!: merge_rank_bound) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
240 |
next |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
241 |
case [simp]: EQ |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
242 |
\<comment> \<open>@{const merge} links both first trees, and inserts them into the merged remaining heaps\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
243 |
have "merge (t\<^sub>1 # ts\<^sub>1) (t\<^sub>2 # ts\<^sub>2) = ins_tree (link t\<^sub>1 t\<^sub>2) (merge ts\<^sub>1 ts\<^sub>2)" by simp |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
244 |
also have "invar \<dots>" proof (intro invar_ins_tree invar_link) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
245 |
\<comment> \<open>Invariant of merged remaining heaps follows by IH\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
246 |
show "invar (merge ts\<^sub>1 ts\<^sub>2)" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
247 |
using EQ "3.prems" "3.IH" by auto |
67486 | 248 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
249 |
\<comment> \<open>For insertion, we have to show that the rank of the linked tree is \<open>\<le>\<close> the |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
250 |
ranks in the merged remaining heaps\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
251 |
show "\<forall>t'\<in>set (merge ts\<^sub>1 ts\<^sub>2). rank (link t\<^sub>1 t\<^sub>2) \<le> rank t'" |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
252 |
proof - |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
253 |
\<comment> \<open>Which is, again, done with the help of @{thm [source] merge_rank_bound}\<close> |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
254 |
have "rank (link t\<^sub>1 t\<^sub>2) = Suc (rank t\<^sub>2)" by simp |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
255 |
thus ?thesis using "3.prems" by (auto simp: Suc_le_eq elim!: merge_rank_bound) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
256 |
qed |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
257 |
qed simp_all |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
258 |
finally show ?thesis . |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
259 |
qed |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
260 |
qed auto |
67486 | 261 |
|
262 |
||
75667 | 263 |
lemma mset_trees_merge[simp]: |
264 |
"mset_trees (merge ts\<^sub>1 ts\<^sub>2) = mset_trees ts\<^sub>1 + mset_trees ts\<^sub>2" |
|
67486 | 265 |
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) auto |
266 |
||
66522 | 267 |
subsubsection \<open>\<open>get_min\<close>\<close> |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
268 |
|
75667 | 269 |
fun get_min :: "'a::linorder trees \<Rightarrow> 'a" where |
66522 | 270 |
"get_min [t] = root t" |
66546 | 271 |
| "get_min (t#ts) = min (root t) (get_min ts)" |
67486 | 272 |
|
75667 | 273 |
lemma bheap_root_min: |
274 |
assumes "bheap t" |
|
67486 | 275 |
assumes "x \<in># mset_tree t" |
276 |
shows "root t \<le> x" |
|
75667 | 277 |
using assms unfolding bheap_def |
278 |
by (induction t arbitrary: x rule: mset_tree.induct) (fastforce simp: mset_trees_def) |
|
67486 | 279 |
|
280 |
lemma get_min_mset: |
|
281 |
assumes "ts\<noteq>[]" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
282 |
assumes "invar ts" |
75667 | 283 |
assumes "x \<in># mset_trees ts" |
66522 | 284 |
shows "get_min ts \<le> x" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
285 |
using assms |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
286 |
apply (induction ts arbitrary: x rule: get_min.induct) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
287 |
apply (auto |
75667 | 288 |
simp: bheap_root_min min_def intro: order_trans; |
289 |
meson linear order_trans bheap_root_min |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
290 |
)+ |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
291 |
done |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
292 |
|
67486 | 293 |
lemma get_min_member: |
75667 | 294 |
"ts\<noteq>[] \<Longrightarrow> get_min ts \<in># mset_trees ts" |
66546 | 295 |
by (induction ts rule: get_min.induct) (auto simp: min_def) |
66522 | 296 |
|
67486 | 297 |
lemma get_min: |
75667 | 298 |
assumes "mset_trees ts \<noteq> {#}" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
299 |
assumes "invar ts" |
75667 | 300 |
shows "get_min ts = Min_mset (mset_trees ts)" |
67486 | 301 |
using assms get_min_member get_min_mset |
66522 | 302 |
by (auto simp: eq_Min_iff) |
67486 | 303 |
|
66522 | 304 |
subsubsection \<open>\<open>get_min_rest\<close>\<close> |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
305 |
|
75667 | 306 |
fun get_min_rest :: "'a::linorder trees \<Rightarrow> 'a tree \<times> 'a trees" where |
66522 | 307 |
"get_min_rest [t] = (t,[])" |
308 |
| "get_min_rest (t#ts) = (let (t',ts') = get_min_rest ts |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
309 |
in if root t \<le> root t' then (t,ts) else (t',t#ts'))" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
310 |
|
67486 | 311 |
lemma get_min_rest_get_min_same_root: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
312 |
assumes "ts\<noteq>[]" |
67486 | 313 |
assumes "get_min_rest ts = (t',ts')" |
314 |
shows "root t' = get_min ts" |
|
315 |
using assms |
|
66546 | 316 |
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto simp: min_def split: prod.splits) |
66522 | 317 |
|
67486 | 318 |
lemma mset_get_min_rest: |
319 |
assumes "get_min_rest ts = (t',ts')" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
320 |
assumes "ts\<noteq>[]" |
67486 | 321 |
shows "mset ts = {#t'#} + mset ts'" |
322 |
using assms |
|
66522 | 323 |
by (induction ts arbitrary: t' ts' rule: get_min.induct) (auto split: prod.splits if_splits) |
67486 | 324 |
|
72551 | 325 |
lemma set_get_min_rest: |
67486 | 326 |
assumes "get_min_rest ts = (t', ts')" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
327 |
assumes "ts\<noteq>[]" |
66522 | 328 |
shows "set ts = Set.insert t' (set ts')" |
329 |
using mset_get_min_rest[OF assms, THEN arg_cong[where f=set_mset]] |
|
67486 | 330 |
by auto |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
331 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
332 |
lemma invar_get_min_rest: |
67486 | 333 |
assumes "get_min_rest ts = (t',ts')" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
334 |
assumes "ts\<noteq>[]" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
335 |
assumes "invar ts" |
75667 | 336 |
shows "bheap t'" and "invar ts'" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
337 |
proof - |
75667 | 338 |
have "bheap t' \<and> invar ts'" |
67486 | 339 |
using assms |
66522 | 340 |
proof (induction ts arbitrary: t' ts' rule: get_min.induct) |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
341 |
case (2 t v va) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
342 |
then show ?case |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
343 |
apply (clarsimp split: prod.splits if_splits) |
72551 | 344 |
apply (drule set_get_min_rest; fastforce) |
67486 | 345 |
done |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
346 |
qed auto |
75667 | 347 |
thus "bheap t'" and "invar ts'" by auto |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
348 |
qed |
66522 | 349 |
|
68021 | 350 |
subsubsection \<open>\<open>del_min\<close>\<close> |
66522 | 351 |
|
75667 | 352 |
definition del_min :: "'a::linorder trees \<Rightarrow> 'a::linorder trees" where |
68021 | 353 |
"del_min ts = (case get_min_rest ts of |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
354 |
(Node r x ts\<^sub>1, ts\<^sub>2) \<Rightarrow> merge (rev ts\<^sub>1) ts\<^sub>2)" |
67486 | 355 |
|
68021 | 356 |
lemma invar_del_min[simp]: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
357 |
assumes "ts \<noteq> []" |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
358 |
assumes "invar ts" |
68021 | 359 |
shows "invar (del_min ts)" |
67486 | 360 |
using assms |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
361 |
unfolding del_min_def |
67486 | 362 |
by (auto |
363 |
split: prod.split tree.split |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
364 |
intro!: invar_merge invar_children |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
365 |
dest: invar_get_min_rest |
66522 | 366 |
) |
67486 | 367 |
|
75667 | 368 |
lemma mset_trees_del_min: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
369 |
assumes "ts \<noteq> []" |
75667 | 370 |
shows "mset_trees ts = mset_trees (del_min ts) + {# get_min ts #}" |
66522 | 371 |
using assms |
68021 | 372 |
unfolding del_min_def |
66522 | 373 |
apply (clarsimp split: tree.split prod.split) |
67486 | 374 |
apply (frule (1) get_min_rest_get_min_same_root) |
375 |
apply (frule (1) mset_get_min_rest) |
|
75667 | 376 |
apply (auto simp: mset_trees_def) |
67486 | 377 |
done |
66522 | 378 |
|
379 |
||
380 |
subsubsection \<open>Instantiating the Priority Queue Locale\<close> |
|
381 |
||
66565 | 382 |
text \<open>Last step of functional correctness proof: combine all the above lemmas |
383 |
to show that binomial heaps satisfy the specification of priority queues with merge.\<close> |
|
384 |
||
75667 | 385 |
interpretation bheaps: Priority_Queue_Merge |
67399 | 386 |
where empty = "[]" and is_empty = "(=) []" and insert = insert |
68021 | 387 |
and get_min = get_min and del_min = del_min and merge = merge |
75667 | 388 |
and invar = invar and mset = mset_trees |
66522 | 389 |
proof (unfold_locales, goal_cases) |
66565 | 390 |
case 1 thus ?case by simp |
66522 | 391 |
next |
66565 | 392 |
case 2 thus ?case by auto |
66522 | 393 |
next |
66565 | 394 |
case 3 thus ?case by auto |
66522 | 395 |
next |
396 |
case (4 q) |
|
75667 | 397 |
thus ?case using mset_trees_del_min[of q] get_min[OF _ \<open>invar q\<close>] |
66522 | 398 |
by (auto simp: union_single_eq_diff) |
399 |
next |
|
66565 | 400 |
case (5 q) thus ?case using get_min[of q] by auto |
67486 | 401 |
next |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
402 |
case 6 thus ?case by (auto simp add: invar_def) |
66565 | 403 |
next |
404 |
case 7 thus ?case by simp |
|
66522 | 405 |
next |
66565 | 406 |
case 8 thus ?case by simp |
66522 | 407 |
next |
66565 | 408 |
case 9 thus ?case by simp |
409 |
next |
|
410 |
case 10 thus ?case by simp |
|
66522 | 411 |
qed |
412 |
||
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
413 |
|
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
414 |
subsection \<open>Complexity\<close> |
67486 | 415 |
|
416 |
text \<open>The size of a binomial tree is determined by its rank\<close> |
|
66522 | 417 |
lemma size_mset_btree: |
75667 | 418 |
assumes "btree t" |
67486 | 419 |
shows "size (mset_tree t) = 2^rank t" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
420 |
using assms |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
421 |
proof (induction t) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
422 |
case (Node r v ts) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
423 |
hence IH: "size (mset_tree t) = 2^rank t" if "t \<in> set ts" for t |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
424 |
using that by auto |
67486 | 425 |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
426 |
from Node have COMPL: "map rank ts = rev [0..<r]" by auto |
67486 | 427 |
|
75667 | 428 |
have "size (mset_trees ts) = (\<Sum>t\<leftarrow>ts. size (mset_tree t))" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
429 |
by (induction ts) auto |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
430 |
also have "\<dots> = (\<Sum>t\<leftarrow>ts. 2^rank t)" using IH |
67486 | 431 |
by (auto cong: map_cong) |
432 |
also have "\<dots> = (\<Sum>r\<leftarrow>map rank ts. 2^r)" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
433 |
by (induction ts) auto |
67486 | 434 |
also have "\<dots> = (\<Sum>i\<in>{0..<r}. 2^i)" |
435 |
unfolding COMPL |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
436 |
by (auto simp: rev_map[symmetric] interv_sum_list_conv_sum_set_nat) |
67486 | 437 |
also have "\<dots> = 2^r - 1" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
438 |
by (induction r) auto |
67486 | 439 |
finally show ?case |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
440 |
by (simp) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
441 |
qed |
67486 | 442 |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
443 |
lemma size_mset_tree: |
75667 | 444 |
assumes "bheap t" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
445 |
shows "size (mset_tree t) = 2^rank t" |
75667 | 446 |
using assms unfolding bheap_def |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
447 |
by (simp add: size_mset_btree) |
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
448 |
|
67486 | 449 |
text \<open>The length of a binomial heap is bounded by the number of its elements\<close> |
75667 | 450 |
lemma size_mset_trees: |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
451 |
assumes "invar ts" |
75667 | 452 |
shows "length ts \<le> log 2 (size (mset_trees ts) + 1)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
453 |
proof - |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
454 |
from \<open>invar ts\<close> have |
67399 | 455 |
ASC: "sorted_wrt (<) (map rank ts)" and |
75667 | 456 |
TINV: "\<forall>t\<in>set ts. bheap t" |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
457 |
unfolding invar_def by auto |
67486 | 458 |
|
459 |
have "(2::nat)^length ts = (\<Sum>i\<in>{0..<length ts}. 2^i) + 1" |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
460 |
by (simp add: sum_power2) |
75693 | 461 |
also have "\<dots> = (\<Sum>i\<leftarrow>[0..<length ts]. 2^i) + 1" (is "_ = ?S + 1") |
462 |
by (simp add: interv_sum_list_conv_sum_set_nat) |
|
463 |
also have "?S \<le> (\<Sum>t\<leftarrow>ts. 2^rank t)" (is "_ \<le> ?T") |
|
464 |
using sorted_wrt_less_idx[OF ASC] by(simp add: sum_list_mono2) |
|
465 |
also have "?T + 1 \<le> (\<Sum>t\<leftarrow>ts. size (mset_tree t)) + 1" using TINV |
|
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
466 |
by (auto cong: map_cong simp: size_mset_tree) |
75667 | 467 |
also have "\<dots> = size (mset_trees ts) + 1" |
468 |
unfolding mset_trees_def by (induction ts) auto |
|
75693 | 469 |
finally have "2^length ts \<le> size (mset_trees ts) + 1" by simp |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
470 |
then show ?thesis using le_log2_of_power by blast |
67486 | 471 |
qed |
472 |
||
66522 | 473 |
subsubsection \<open>Timing Functions\<close> |
474 |
||
79666 | 475 |
define_time_fun link |
476 |
||
477 |
lemma T_link[simp]: "T_link t\<^sub>1 t\<^sub>2 = 0" |
|
478 |
by(cases t\<^sub>1; cases t\<^sub>2, auto) |
|
479 |
||
480 |
define_time_fun rank |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
481 |
|
79666 | 482 |
lemma T_rank[simp]: "T_rank t = 0" |
483 |
by(cases t, auto) |
|
66522 | 484 |
|
79666 | 485 |
define_time_fun ins_tree |
486 |
||
487 |
define_time_fun insert |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
488 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
489 |
lemma T_ins_tree_simple_bound: "T_ins_tree t ts \<le> length ts + 1" |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
490 |
by (induction t ts rule: T_ins_tree.induct) auto |
66522 | 491 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
492 |
subsubsection \<open>\<open>T_insert\<close>\<close> |
66522 | 493 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
494 |
lemma T_insert_bound: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
495 |
assumes "invar ts" |
79138 | 496 |
shows "T_insert x ts \<le> log 2 (size (mset_trees ts) + 1) + 1" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
497 |
proof - |
79138 | 498 |
have "real (T_insert x ts) \<le> real (length ts) + 1" |
79666 | 499 |
unfolding T_insert.simps using T_ins_tree_simple_bound |
79138 | 500 |
by (metis of_nat_1 of_nat_add of_nat_mono) |
75667 | 501 |
also note size_mset_trees[OF \<open>invar ts\<close>] |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
502 |
finally show ?thesis by simp |
67486 | 503 |
qed |
66522 | 504 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
505 |
subsubsection \<open>\<open>T_merge\<close>\<close> |
66522 | 506 |
|
79666 | 507 |
define_time_fun merge |
70607 | 508 |
|
79666 | 509 |
(* Warning: \<open>T_merge.induct\<close> is less convenient than the equivalent \<open>merge.induct\<close>, |
510 |
apparently because of the \<open>let\<close> clauses introduced by pattern_aliases; should be investigated. |
|
511 |
*) |
|
70607 | 512 |
|
67486 | 513 |
text \<open>A crucial idea is to estimate the time in correlation with the |
514 |
result length, as each carry reduces the length of the result.\<close> |
|
66522 | 515 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
516 |
lemma T_ins_tree_length: |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
517 |
"T_ins_tree t ts + length (ins_tree t ts) = 2 + length ts" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
518 |
by (induction t ts rule: ins_tree.induct) auto |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
519 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
520 |
lemma T_merge_length: |
75667 | 521 |
"T_merge ts\<^sub>1 ts\<^sub>2 + length (merge ts\<^sub>1 ts\<^sub>2) \<le> 2 * (length ts\<^sub>1 + length ts\<^sub>2) + 1" |
79666 | 522 |
by (induction ts\<^sub>1 ts\<^sub>2 rule: merge.induct) |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
523 |
(auto simp: T_ins_tree_length algebra_simps) |
66522 | 524 |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
525 |
text \<open>Finally, we get the desired logarithmic bound\<close> |
72910 | 526 |
lemma T_merge_bound: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
527 |
fixes ts\<^sub>1 ts\<^sub>2 |
75667 | 528 |
defines "n\<^sub>1 \<equiv> size (mset_trees ts\<^sub>1)" |
529 |
defines "n\<^sub>2 \<equiv> size (mset_trees ts\<^sub>2)" |
|
72910 | 530 |
assumes "invar ts\<^sub>1" "invar ts\<^sub>2" |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
531 |
shows "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
532 |
proof - |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
533 |
note n_defs = assms(1,2) |
72910 | 534 |
|
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
535 |
have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * real (length ts\<^sub>1) + 2 * real (length ts\<^sub>2) + 1" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
536 |
using T_merge_length[of ts\<^sub>1 ts\<^sub>2] by simp |
75667 | 537 |
also note size_mset_trees[OF \<open>invar ts\<^sub>1\<close>] |
538 |
also note size_mset_trees[OF \<open>invar ts\<^sub>2\<close>] |
|
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
539 |
finally have "T_merge ts\<^sub>1 ts\<^sub>2 \<le> 2 * log 2 (n\<^sub>1 + 1) + 2 * log 2 (n\<^sub>2 + 1) + 1" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
540 |
unfolding n_defs by (simp add: algebra_simps) |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
541 |
also have "log 2 (n\<^sub>1 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
542 |
unfolding n_defs by (simp add: algebra_simps) |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
543 |
also have "log 2 (n\<^sub>2 + 1) \<le> log 2 (n\<^sub>1 + n\<^sub>2 + 1)" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
544 |
unfolding n_defs by (simp add: algebra_simps) |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
545 |
finally show ?thesis by (simp add: algebra_simps) |
67486 | 546 |
qed |
547 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
548 |
subsubsection \<open>\<open>T_get_min\<close>\<close> |
66522 | 549 |
|
79666 | 550 |
define_time_fun root |
551 |
||
552 |
lemma T_root[simp]: "T_root t = 0" |
|
553 |
by(cases t)(simp_all) |
|
554 |
||
555 |
define_time_fun min |
|
556 |
||
557 |
define_time_fun get_min |
|
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
558 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
559 |
lemma T_get_min_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min ts = length ts" |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
560 |
by (induction ts rule: T_get_min.induct) auto |
67486 | 561 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
562 |
lemma T_get_min_bound: |
66522 | 563 |
assumes "invar ts" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
564 |
assumes "ts\<noteq>[]" |
75667 | 565 |
shows "T_get_min ts \<le> log 2 (size (mset_trees ts) + 1)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
566 |
proof - |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
567 |
have 1: "T_get_min ts = length ts" using assms T_get_min_estimate by auto |
75667 | 568 |
also note size_mset_trees[OF \<open>invar ts\<close>] |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
569 |
finally show ?thesis . |
67486 | 570 |
qed |
66522 | 571 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
572 |
subsubsection \<open>\<open>T_del_min\<close>\<close> |
66522 | 573 |
|
79666 | 574 |
define_time_fun get_min_rest |
575 |
(*fun T_get_min_rest :: "'a::linorder trees \<Rightarrow> nat" where |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
576 |
"T_get_min_rest [t] = 1" |
79666 | 577 |
| "T_get_min_rest (t#ts) = 1 + T_get_min_rest ts"*) |
66522 | 578 |
|
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
579 |
lemma T_get_min_rest_estimate: "ts\<noteq>[] \<Longrightarrow> T_get_min_rest ts = length ts" |
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
580 |
by (induction ts rule: T_get_min_rest.induct) auto |
67486 | 581 |
|
72910 | 582 |
lemma T_get_min_rest_bound: |
72808
ba65dc3e35af
summarized structural and ordering invariant for trees
Peter Lammich
parents:
72714
diff
changeset
|
583 |
assumes "invar ts" |
66522 | 584 |
assumes "ts\<noteq>[]" |
75667 | 585 |
shows "T_get_min_rest ts \<le> log 2 (size (mset_trees ts) + 1)" |
66522 | 586 |
proof - |
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
587 |
have 1: "T_get_min_rest ts = length ts" using assms T_get_min_rest_estimate by auto |
75667 | 588 |
also note size_mset_trees[OF \<open>invar ts\<close>] |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
589 |
finally show ?thesis . |
67486 | 590 |
qed |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
591 |
|
69597 | 592 |
text\<open>Note that although the definition of function \<^const>\<open>rev\<close> has quadratic complexity, |
66522 | 593 |
it can and is implemented (via suitable code lemmas) as a linear time function. |
594 |
Thus the following definition is justified:\<close> |
|
595 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
596 |
definition "T_rev xs = length xs + 1" |
66522 | 597 |
|
79666 | 598 |
define_time_fun del_min |
67486 | 599 |
|
72910 | 600 |
lemma T_del_min_bound: |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
601 |
fixes ts |
75667 | 602 |
defines "n \<equiv> size (mset_trees ts)" |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
603 |
assumes "invar ts" and "ts\<noteq>[]" |
79138 | 604 |
shows "T_del_min ts \<le> 6 * log 2 (n+1) + 2" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
605 |
proof - |
66522 | 606 |
obtain r x ts\<^sub>1 ts\<^sub>2 where GM: "get_min_rest ts = (Node r x ts\<^sub>1, ts\<^sub>2)" |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
607 |
by (metis surj_pair tree.exhaust_sel) |
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
608 |
|
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
609 |
have I1: "invar (rev ts\<^sub>1)" and I2: "invar ts\<^sub>2" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
610 |
using invar_get_min_rest[OF GM \<open>ts\<noteq>[]\<close> \<open>invar ts\<close>] invar_children |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
611 |
by auto |
66434
5d7e770c7d5d
added sorted_wrt to List; added Data_Structures/Binomial_Heap.thy
nipkow
parents:
diff
changeset
|
612 |
|
75667 | 613 |
define n\<^sub>1 where "n\<^sub>1 = size (mset_trees ts\<^sub>1)" |
614 |
define n\<^sub>2 where "n\<^sub>2 = size (mset_trees ts\<^sub>2)" |
|
67486 | 615 |
|
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
616 |
have "n\<^sub>1 \<le> n" "n\<^sub>1 + n\<^sub>2 \<le> n" unfolding n_def n\<^sub>1_def n\<^sub>2_def |
66522 | 617 |
using mset_get_min_rest[OF GM \<open>ts\<noteq>[]\<close>] |
75667 | 618 |
by (auto simp: mset_trees_def) |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
619 |
|
79138 | 620 |
have "T_del_min ts = real (T_get_min_rest ts) + real (T_rev ts\<^sub>1) + real (T_merge (rev ts\<^sub>1) ts\<^sub>2)" |
79666 | 621 |
unfolding T_del_min.simps GM |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
622 |
by simp |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
623 |
also have "T_get_min_rest ts \<le> log 2 (n+1)" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
624 |
using T_get_min_rest_bound[OF \<open>invar ts\<close> \<open>ts\<noteq>[]\<close>] unfolding n_def by simp |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
625 |
also have "T_rev ts\<^sub>1 \<le> 1 + log 2 (n\<^sub>1 + 1)" |
75667 | 626 |
unfolding T_rev_def n\<^sub>1_def using size_mset_trees[OF I1] by simp |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
627 |
also have "T_merge (rev ts\<^sub>1) ts\<^sub>2 \<le> 4*log 2 (n\<^sub>1 + n\<^sub>2 + 1) + 1" |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
628 |
unfolding n\<^sub>1_def n\<^sub>2_def using T_merge_bound[OF I1 I2] by (simp add: algebra_simps) |
79138 | 629 |
finally have "T_del_min ts \<le> log 2 (n+1) + log 2 (n\<^sub>1 + 1) + 4*log 2 (real (n\<^sub>1 + n\<^sub>2) + 1) + 2" |
72936
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
630 |
by (simp add: algebra_simps) |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
631 |
also note \<open>n\<^sub>1 + n\<^sub>2 \<le> n\<close> |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
632 |
also note \<open>n\<^sub>1 \<le> n\<close> |
1dc01c11aa86
simplified complexity proofs. Increased precision of T_del_min_bound. (though T_del_min might be be missing a +1)
Peter Lammich
parents:
72935
diff
changeset
|
633 |
finally show ?thesis by (simp add: algebra_simps) |
67486 | 634 |
qed |
635 |
||
72550
1d0ae7e578a0
renamed t_ functions to T_ (im Auftrag von T. Nipkow)
blanchet
parents:
70607
diff
changeset
|
636 |
end |