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