author | nipkow |
Wed, 01 Apr 2020 21:48:39 +0200 | |
changeset 71636 | 9d8fb1dbc368 |
parent 71635 | b36f07d28867 |
child 71722 | 1cffe8f4d7b3 |
permissions | -rw-r--r-- |
61232 | 1 |
(* |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
2 |
Author: Tobias Nipkow, Daniel Stüwe |
71635 | 3 |
Based on the AFP entry AVL. |
61232 | 4 |
*) |
5 |
||
6 |
section "AVL Tree Implementation of Sets" |
|
7 |
||
8 |
theory AVL_Set |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
9 |
imports |
67964 | 10 |
Cmp |
11 |
Isin2 |
|
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63411
diff
changeset
|
12 |
"HOL-Number_Theory.Fib" |
61232 | 13 |
begin |
14 |
||
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
15 |
type_synonym 'a avl_tree = "('a*nat) tree" |
61232 | 16 |
|
68431 | 17 |
definition empty :: "'a avl_tree" where |
18 |
"empty = Leaf" |
|
19 |
||
67406 | 20 |
text \<open>Invariant:\<close> |
61232 | 21 |
|
22 |
fun avl :: "'a avl_tree \<Rightarrow> bool" where |
|
23 |
"avl Leaf = True" | |
|
71466 | 24 |
"avl (Node l (a,n) r) = |
61232 | 25 |
((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> |
71466 | 26 |
n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
61232 | 27 |
|
28 |
fun ht :: "'a avl_tree \<Rightarrow> nat" where |
|
29 |
"ht Leaf = 0" | |
|
71466 | 30 |
"ht (Node l (a,n) r) = n" |
61232 | 31 |
|
32 |
definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
33 |
"node l a r = Node l (a, max (ht l) (ht r) + 1) r" |
61232 | 34 |
|
61581 | 35 |
definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
71635 | 36 |
"balL AB b C = |
37 |
(if ht AB = ht C + 2 then |
|
38 |
case AB of |
|
39 |
Node A (a, _) B \<Rightarrow> |
|
40 |
if ht A \<ge> ht B then node A a (node B b C) |
|
41 |
else |
|
42 |
case B of |
|
43 |
Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C) |
|
44 |
else node AB b C)" |
|
61232 | 45 |
|
61581 | 46 |
definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
71635 | 47 |
"balR A a BC = |
48 |
(if ht BC = ht A + 2 then |
|
49 |
case BC of |
|
50 |
Node B (b, _) C \<Rightarrow> |
|
51 |
if ht B \<le> ht C then node (node A a B) b C |
|
52 |
else |
|
53 |
case B of |
|
54 |
Node B\<^sub>1 (ab, _) B\<^sub>2 \<Rightarrow> node (node A a B\<^sub>1) ab (node B\<^sub>2 b C) |
|
55 |
else node A a BC)" |
|
61232 | 56 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
57 |
fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
58 |
"insert x Leaf = Node Leaf (x, 1) Leaf" | |
71466 | 59 |
"insert x (Node l (a, n) r) = (case cmp x a of |
60 |
EQ \<Rightarrow> Node l (a, n) r | |
|
61581 | 61 |
LT \<Rightarrow> balL (insert x l) a r | |
62 |
GT \<Rightarrow> balR l a (insert x r))" |
|
61232 | 63 |
|
68023 | 64 |
fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
65 |
"split_max (Node l (a, _) r) = |
68023 | 66 |
(if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))" |
61232 | 67 |
|
68023 | 68 |
lemmas split_max_induct = split_max.induct[case_names Node Leaf] |
61232 | 69 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
70 |
fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
61232 | 71 |
"delete _ Leaf = Leaf" | |
71466 | 72 |
"delete x (Node l (a, n) r) = |
61678 | 73 |
(case cmp x a of |
71636 | 74 |
EQ \<Rightarrow> if l = Leaf then r |
75 |
else let (l', a') = split_max l in balR l' a' r | |
|
61678 | 76 |
LT \<Rightarrow> balR (delete x l) a r | |
77 |
GT \<Rightarrow> balL l a (delete x r))" |
|
61232 | 78 |
|
79 |
||
67406 | 80 |
subsection \<open>Functional Correctness Proofs\<close> |
61232 | 81 |
|
67406 | 82 |
text\<open>Very different from the AFP/AVL proofs\<close> |
61232 | 83 |
|
84 |
||
85 |
subsubsection "Proofs for insert" |
|
86 |
||
61581 | 87 |
lemma inorder_balL: |
88 |
"inorder (balL l a r) = inorder l @ a # inorder r" |
|
89 |
by (auto simp: node_def balL_def split:tree.splits) |
|
61232 | 90 |
|
61581 | 91 |
lemma inorder_balR: |
92 |
"inorder (balR l a r) = inorder l @ a # inorder r" |
|
93 |
by (auto simp: node_def balR_def split:tree.splits) |
|
61232 | 94 |
|
95 |
theorem inorder_insert: |
|
96 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
|
97 |
by (induct t) |
|
61581 | 98 |
(auto simp: ins_list_simps inorder_balL inorder_balR) |
61232 | 99 |
|
100 |
||
101 |
subsubsection "Proofs for delete" |
|
102 |
||
68023 | 103 |
lemma inorder_split_maxD: |
104 |
"\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
|
61232 | 105 |
inorder t' @ [a] = inorder t" |
68023 | 106 |
by(induction t arbitrary: t' rule: split_max.induct) |
61647 | 107 |
(auto simp: inorder_balL split: if_splits prod.splits tree.split) |
61232 | 108 |
|
109 |
theorem inorder_delete: |
|
110 |
"sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
|
111 |
by(induction t) |
|
71636 | 112 |
(auto simp: del_list_simps inorder_balL inorder_balR inorder_split_maxD split: prod.splits) |
61232 | 113 |
|
114 |
||
67406 | 115 |
subsection \<open>AVL invariants\<close> |
61232 | 116 |
|
67406 | 117 |
text\<open>Essentially the AFP/AVL proofs\<close> |
61232 | 118 |
|
119 |
||
67406 | 120 |
subsubsection \<open>Insertion maintains AVL balance\<close> |
61232 | 121 |
|
122 |
declare Let_def [simp] |
|
123 |
||
70571 | 124 |
lemma ht_height[simp]: "avl t \<Longrightarrow> ht t = height t" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
125 |
by (cases t rule: tree2_cases) simp_all |
61232 | 126 |
|
71635 | 127 |
text \<open>First, a fast but relatively manual proof with many lemmas:\<close> |
128 |
||
61581 | 129 |
lemma height_balL: |
61232 | 130 |
"\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow> |
61581 | 131 |
height (balL l a r) = height r + 2 \<or> |
132 |
height (balL l a r) = height r + 3" |
|
133 |
by (cases l) (auto simp:node_def balL_def split:tree.split) |
|
61232 | 134 |
|
61581 | 135 |
lemma height_balR: |
61232 | 136 |
"\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow> |
61581 | 137 |
height (balR l a r) = height l + 2 \<or> |
138 |
height (balR l a r) = height l + 3" |
|
139 |
by (cases r) (auto simp add:node_def balR_def split:tree.split) |
|
61232 | 140 |
|
70571 | 141 |
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1" |
61232 | 142 |
by (simp add: node_def) |
143 |
||
144 |
lemma avl_node: |
|
145 |
"\<lbrakk> avl l; avl r; |
|
146 |
height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1 |
|
147 |
\<rbrakk> \<Longrightarrow> avl(node l a r)" |
|
148 |
by (auto simp add:max_def node_def) |
|
149 |
||
61581 | 150 |
lemma height_balL2: |
61232 | 151 |
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow> |
61581 | 152 |
height (balL l a r) = (1 + max (height l) (height r))" |
153 |
by (cases l, cases r) (simp_all add: balL_def) |
|
61232 | 154 |
|
61581 | 155 |
lemma height_balR2: |
61232 | 156 |
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow> |
61581 | 157 |
height (balR l a r) = (1 + max (height l) (height r))" |
158 |
by (cases l, cases r) (simp_all add: balR_def) |
|
61232 | 159 |
|
61581 | 160 |
lemma avl_balL: |
61232 | 161 |
assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1 |
162 |
\<or> height r = height l + 1 \<or> height l = height r + 2" |
|
61581 | 163 |
shows "avl(balL l a r)" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
164 |
proof(cases l rule: tree2_cases) |
61232 | 165 |
case Leaf |
61581 | 166 |
with assms show ?thesis by (simp add: node_def balL_def) |
61232 | 167 |
next |
68413 | 168 |
case Node |
61232 | 169 |
with assms show ?thesis |
170 |
proof(cases "height l = height r + 2") |
|
171 |
case True |
|
172 |
from True Node assms show ?thesis |
|
61581 | 173 |
by (auto simp: balL_def intro!: avl_node split: tree.split) arith+ |
61232 | 174 |
next |
175 |
case False |
|
61581 | 176 |
with assms show ?thesis by (simp add: avl_node balL_def) |
61232 | 177 |
qed |
178 |
qed |
|
179 |
||
61581 | 180 |
lemma avl_balR: |
61232 | 181 |
assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1 |
182 |
\<or> height r = height l + 1 \<or> height r = height l + 2" |
|
61581 | 183 |
shows "avl(balR l a r)" |
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
184 |
proof(cases r rule: tree2_cases) |
61232 | 185 |
case Leaf |
61581 | 186 |
with assms show ?thesis by (simp add: node_def balR_def) |
61232 | 187 |
next |
68413 | 188 |
case Node |
61232 | 189 |
with assms show ?thesis |
190 |
proof(cases "height r = height l + 2") |
|
191 |
case True |
|
192 |
from True Node assms show ?thesis |
|
61581 | 193 |
by (auto simp: balR_def intro!: avl_node split: tree.split) arith+ |
61232 | 194 |
next |
195 |
case False |
|
61581 | 196 |
with assms show ?thesis by (simp add: balR_def avl_node) |
61232 | 197 |
qed |
198 |
qed |
|
199 |
||
71635 | 200 |
text\<open>Insertion maintains the AVL property. Requires simultaneous proof.\<close> |
61232 | 201 |
|
68422 | 202 |
theorem avl_insert: |
61232 | 203 |
assumes "avl t" |
204 |
shows "avl(insert x t)" |
|
205 |
"(height (insert x t) = height t \<or> height (insert x t) = height t + 1)" |
|
206 |
using assms |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
207 |
proof (induction t rule: tree2_induct) |
71466 | 208 |
case (Node l a _ r) |
61232 | 209 |
case 1 |
68422 | 210 |
show ?case |
61232 | 211 |
proof(cases "x = a") |
68422 | 212 |
case True with Node 1 show ?thesis by simp |
61232 | 213 |
next |
214 |
case False |
|
68422 | 215 |
show ?thesis |
61232 | 216 |
proof(cases "x<a") |
68422 | 217 |
case True with Node 1 show ?thesis by (auto simp add:avl_balL) |
61232 | 218 |
next |
68422 | 219 |
case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR) |
61232 | 220 |
qed |
221 |
qed |
|
222 |
case 2 |
|
68422 | 223 |
show ?case |
61232 | 224 |
proof(cases "x = a") |
68422 | 225 |
case True with Node 1 show ?thesis by simp |
61232 | 226 |
next |
227 |
case False |
|
68422 | 228 |
show ?thesis |
229 |
proof(cases "x<a") |
|
61232 | 230 |
case True |
68422 | 231 |
show ?thesis |
61232 | 232 |
proof(cases "height (insert x l) = height r + 2") |
67406 | 233 |
case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) |
61232 | 234 |
next |
235 |
case True |
|
61581 | 236 |
hence "(height (balL (insert x l) a r) = height r + 2) \<or> |
237 |
(height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B") |
|
238 |
using Node 2 by (intro height_balL) simp_all |
|
61232 | 239 |
thus ?thesis |
240 |
proof |
|
68422 | 241 |
assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) |
61232 | 242 |
next |
68422 | 243 |
assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith |
61232 | 244 |
qed |
245 |
qed |
|
246 |
next |
|
247 |
case False |
|
68422 | 248 |
show ?thesis |
61232 | 249 |
proof(cases "height (insert x r) = height l + 2") |
68422 | 250 |
case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) |
61232 | 251 |
next |
252 |
case True |
|
61581 | 253 |
hence "(height (balR l a (insert x r)) = height l + 2) \<or> |
254 |
(height (balR l a (insert x r)) = height l + 3)" (is "?A \<or> ?B") |
|
255 |
using Node 2 by (intro height_balR) simp_all |
|
61232 | 256 |
thus ?thesis |
257 |
proof |
|
68422 | 258 |
assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) |
61232 | 259 |
next |
68422 | 260 |
assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith |
61232 | 261 |
qed |
262 |
qed |
|
263 |
qed |
|
264 |
qed |
|
265 |
qed simp_all |
|
266 |
||
71635 | 267 |
text \<open>Now an automatic proof without lemmas:\<close> |
268 |
||
269 |
theorem avl_insert_auto: "avl t \<Longrightarrow> |
|
270 |
avl(insert x t) \<and> height (insert x t) \<in> {height t, height t + 1}" |
|
271 |
apply (induction t rule: tree2_induct) |
|
272 |
apply (auto split!: if_splits) |
|
273 |
apply (auto simp: balL_def balR_def node_def max_absorb2 split!: tree.splits) |
|
274 |
done |
|
275 |
||
61232 | 276 |
|
67406 | 277 |
subsubsection \<open>Deletion maintains AVL balance\<close> |
61232 | 278 |
|
68023 | 279 |
lemma avl_split_max: |
61232 | 280 |
assumes "avl x" and "x \<noteq> Leaf" |
68023 | 281 |
shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \<or> |
282 |
height x = height(fst (split_max x)) + 1" |
|
61232 | 283 |
using assms |
68023 | 284 |
proof (induct x rule: split_max_induct) |
71466 | 285 |
case Node |
61232 | 286 |
case 1 |
61647 | 287 |
thus ?case using Node |
68422 | 288 |
by (auto simp: height_balL height_balL2 avl_balL split:prod.split) |
61232 | 289 |
next |
71466 | 290 |
case (Node l a _ r) |
61232 | 291 |
case 2 |
68023 | 292 |
let ?r' = "fst (split_max r)" |
67406 | 293 |
from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all |
61581 | 294 |
thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] |
61232 | 295 |
apply (auto split:prod.splits simp del:avl.simps) by arith+ |
296 |
qed auto |
|
297 |
||
67406 | 298 |
text\<open>Deletion maintains the AVL property:\<close> |
61232 | 299 |
|
68422 | 300 |
theorem avl_delete: |
61232 | 301 |
assumes "avl t" |
302 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" |
|
303 |
using assms |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
304 |
proof (induct t rule: tree2_induct) |
71466 | 305 |
case (Node l a n r) |
61232 | 306 |
case 1 |
68422 | 307 |
show ?case |
71466 | 308 |
proof(cases "x = a") |
71636 | 309 |
case True with Node 1 show ?thesis |
310 |
using avl_split_max[of l] by (auto simp: avl_balR split: prod.split) |
|
61232 | 311 |
next |
312 |
case False |
|
68422 | 313 |
show ?thesis |
71466 | 314 |
proof(cases "x<a") |
68422 | 315 |
case True with Node 1 show ?thesis by (auto simp add:avl_balR) |
61232 | 316 |
next |
71466 | 317 |
case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balL) |
61232 | 318 |
qed |
319 |
qed |
|
320 |
case 2 |
|
68422 | 321 |
show ?case |
71466 | 322 |
proof(cases "x = a") |
71636 | 323 |
case True then show ?thesis using 1 avl_split_max[of l] |
324 |
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split) |
|
61232 | 325 |
next |
326 |
case False |
|
68422 | 327 |
show ?thesis |
71466 | 328 |
proof(cases "x<a") |
61232 | 329 |
case True |
330 |
show ?thesis |
|
331 |
proof(cases "height r = height (delete x l) + 2") |
|
71466 | 332 |
case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def) |
61232 | 333 |
next |
334 |
case True |
|
71466 | 335 |
hence "(height (balR (delete x l) a r) = height (delete x l) + 2) \<or> |
336 |
height (balR (delete x l) a r) = height (delete x l) + 3" (is "?A \<or> ?B") |
|
61581 | 337 |
using Node 2 by (intro height_balR) auto |
61232 | 338 |
thus ?thesis |
339 |
proof |
|
71466 | 340 |
assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 341 |
next |
71466 | 342 |
assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 343 |
qed |
344 |
qed |
|
345 |
next |
|
346 |
case False |
|
347 |
show ?thesis |
|
348 |
proof(cases "height l = height (delete x r) + 2") |
|
71466 | 349 |
case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def) |
61232 | 350 |
next |
351 |
case True |
|
71466 | 352 |
hence "(height (balL l a (delete x r)) = height (delete x r) + 2) \<or> |
353 |
height (balL l a (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B") |
|
61581 | 354 |
using Node 2 by (intro height_balL) auto |
61232 | 355 |
thus ?thesis |
356 |
proof |
|
71466 | 357 |
assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 358 |
next |
71466 | 359 |
assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 360 |
qed |
361 |
qed |
|
362 |
qed |
|
363 |
qed |
|
364 |
qed simp_all |
|
365 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
366 |
|
68422 | 367 |
subsection "Overall correctness" |
368 |
||
68440 | 369 |
interpretation S: Set_by_Ordered |
68431 | 370 |
where empty = empty and isin = isin and insert = insert and delete = delete |
68422 | 371 |
and inorder = inorder and inv = avl |
372 |
proof (standard, goal_cases) |
|
68431 | 373 |
case 1 show ?case by (simp add: empty_def) |
68422 | 374 |
next |
375 |
case 2 thus ?case by(simp add: isin_set_inorder) |
|
376 |
next |
|
377 |
case 3 thus ?case by(simp add: inorder_insert) |
|
378 |
next |
|
379 |
case 4 thus ?case by(simp add: inorder_delete) |
|
380 |
next |
|
68431 | 381 |
case 5 thus ?case by (simp add: empty_def) |
68422 | 382 |
next |
383 |
case 6 thus ?case by (simp add: avl_insert(1)) |
|
384 |
next |
|
385 |
case 7 thus ?case by (simp add: avl_delete(1)) |
|
386 |
qed |
|
387 |
||
388 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
389 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
390 |
|
71487 | 391 |
text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich, much simplified.\<close> |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
392 |
|
71466 | 393 |
text \<open>Any AVL tree of height \<open>n\<close> has at least \<open>fib (n+2)\<close> leaves:\<close> |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
394 |
|
71466 | 395 |
lemma avl_fib_bound: "avl t \<Longrightarrow> height t = n \<Longrightarrow> fib (n+2) \<le> size1 t" |
396 |
proof (induction n arbitrary: t rule: fib.induct) |
|
71487 | 397 |
case 1 thus ?case by (simp) |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
398 |
next |
71487 | 399 |
case 2 thus ?case by (cases t) (auto) |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
400 |
next |
68313 | 401 |
case (3 h) |
402 |
from "3.prems" obtain l a r where |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
403 |
[simp]: "t = Node l (a,Suc(Suc h)) r" "avl l" "avl r" |
68313 | 404 |
and C: " |
405 |
height r = Suc h \<and> height l = Suc h |
|
406 |
\<or> height r = Suc h \<and> height l = h |
|
407 |
\<or> height r = h \<and> height l = Suc h" (is "?C1 \<or> ?C2 \<or> ?C3") |
|
408 |
by (cases t) (simp, fastforce) |
|
409 |
{ |
|
410 |
assume ?C1 |
|
411 |
with "3.IH"(1) |
|
412 |
have "fib (h + 3) \<le> size1 l" "fib (h + 3) \<le> size1 r" |
|
413 |
by (simp_all add: eval_nat_numeral) |
|
414 |
hence ?case by (auto simp: eval_nat_numeral) |
|
415 |
} moreover { |
|
416 |
assume ?C2 |
|
417 |
hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto |
|
418 |
} moreover { |
|
419 |
assume ?C3 |
|
420 |
hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto |
|
421 |
} ultimately show ?case using C by blast |
|
422 |
qed |
|
423 |
||
69597 | 424 |
text \<open>An exponential lower bound for \<^const>\<open>fib\<close>:\<close> |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
425 |
|
68313 | 426 |
lemma fib_lowerbound: |
427 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
71486 | 428 |
shows "real (fib(n+2)) \<ge> \<phi> ^ n" |
429 |
proof (induction n rule: fib.induct) |
|
430 |
case 1 |
|
431 |
then show ?case by simp |
|
432 |
next |
|
433 |
case 2 |
|
434 |
then show ?case by (simp add: \<phi>_def real_le_lsqrt) |
|
435 |
next |
|
436 |
case (3 n) term ?case |
|
437 |
have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n" |
|
438 |
by (simp add: field_simps power2_eq_square) |
|
439 |
also have "\<dots> = (\<phi> + 1) * \<phi> ^ n" |
|
440 |
by (simp_all add: \<phi>_def power2_eq_square field_simps) |
|
441 |
also have "\<dots> = \<phi> ^ Suc n + \<phi> ^ n" |
|
68313 | 442 |
by (simp add: field_simps) |
71486 | 443 |
also have "\<dots> \<le> real (fib (Suc n + 2)) + real (fib (n + 2))" |
444 |
by (intro add_mono "3.IH") |
|
445 |
finally show ?case by simp |
|
68313 | 446 |
qed |
447 |
||
448 |
text \<open>The size of an AVL tree is (at least) exponential in its height:\<close> |
|
449 |
||
68342 | 450 |
lemma avl_size_lowerbound: |
68313 | 451 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
452 |
assumes "avl t" |
|
68342 | 453 |
shows "\<phi> ^ (height t) \<le> size1 t" |
68313 | 454 |
proof - |
71486 | 455 |
have "\<phi> ^ height t \<le> fib (height t + 2)" |
456 |
unfolding \<phi>_def by(rule fib_lowerbound) |
|
68342 | 457 |
also have "\<dots> \<le> size1 t" |
68313 | 458 |
using avl_fib_bound[of t "height t"] assms by simp |
459 |
finally show ?thesis . |
|
460 |
qed |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
461 |
|
69597 | 462 |
text \<open>The height of an AVL tree is most \<^term>\<open>(1/log 2 \<phi>)\<close> \<open>\<approx> 1.44\<close> times worse |
463 |
than \<^term>\<open>log 2 (size1 t)\<close>:\<close> |
|
68342 | 464 |
|
465 |
lemma avl_height_upperbound: |
|
466 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
467 |
assumes "avl t" |
|
468 |
shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" |
|
469 |
proof - |
|
470 |
have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) |
|
471 |
hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) |
|
472 |
also have "\<dots> \<le> log \<phi> (size1 t)" |
|
70350 | 473 |
using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> |
474 |
by (simp add: le_log_of_power) |
|
68342 | 475 |
also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" |
476 |
by(simp add: log_base_change[of 2 \<phi>]) |
|
477 |
finally show ?thesis . |
|
478 |
qed |
|
479 |
||
61232 | 480 |
end |