author | nipkow |
Mon, 11 Jun 2018 16:29:27 +0200 | |
changeset 68413 | b56ed5010e69 |
parent 68342 | b80734daf7ed |
child 68422 | 0a3a36fa1d63 |
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 |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
3 |
Largely derived from 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 |
||
15 |
type_synonym 'a avl_tree = "('a,nat) tree" |
|
16 |
||
67406 | 17 |
text \<open>Invariant:\<close> |
61232 | 18 |
|
19 |
fun avl :: "'a avl_tree \<Rightarrow> bool" where |
|
20 |
"avl Leaf = True" | |
|
68413 | 21 |
"avl (Node l a h r) = |
61232 | 22 |
((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> |
23 |
h = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
|
24 |
||
25 |
fun ht :: "'a avl_tree \<Rightarrow> nat" where |
|
26 |
"ht Leaf = 0" | |
|
68413 | 27 |
"ht (Node l a h r) = h" |
61232 | 28 |
|
29 |
definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
68413 | 30 |
"node l a r = Node l a (max (ht l) (ht r) + 1) r" |
61232 | 31 |
|
61581 | 32 |
definition balL :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
61678 | 33 |
"balL l a r = |
34 |
(if ht l = ht r + 2 then |
|
35 |
case l of |
|
68413 | 36 |
Node bl b _ br \<Rightarrow> |
61678 | 37 |
if ht bl < ht br then |
38 |
case br of |
|
68413 | 39 |
Node cl c _ cr \<Rightarrow> node (node bl b cl) c (node cr a r) |
61678 | 40 |
else node bl b (node br a r) |
41 |
else node l a r)" |
|
61232 | 42 |
|
61581 | 43 |
definition balR :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
61678 | 44 |
"balR l a r = |
45 |
(if ht r = ht l + 2 then |
|
46 |
case r of |
|
68413 | 47 |
Node bl b _ br \<Rightarrow> |
61678 | 48 |
if ht bl > ht br then |
49 |
case bl of |
|
68413 | 50 |
Node cl c _ cr \<Rightarrow> node (node l a cl) c (node cr b br) |
61678 | 51 |
else node (node l a bl) b br |
61232 | 52 |
else node l a r)" |
53 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
54 |
fun insert :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
68413 | 55 |
"insert x Leaf = Node Leaf x 1 Leaf" | |
56 |
"insert x (Node l a h r) = (case cmp x a of |
|
57 |
EQ \<Rightarrow> Node l a h r | |
|
61581 | 58 |
LT \<Rightarrow> balL (insert x l) a r | |
59 |
GT \<Rightarrow> balR l a (insert x r))" |
|
61232 | 60 |
|
68023 | 61 |
fun split_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
68413 | 62 |
"split_max (Node l a _ r) = |
68023 | 63 |
(if r = Leaf then (l,a) else let (r',a') = split_max r in (balL l a r', a'))" |
61232 | 64 |
|
68023 | 65 |
lemmas split_max_induct = split_max.induct[case_names Node Leaf] |
61232 | 66 |
|
61647 | 67 |
fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where |
68413 | 68 |
"del_root (Node Leaf a h r) = r" | |
69 |
"del_root (Node l a h Leaf) = l" | |
|
70 |
"del_root (Node l a h r) = (let (l', a') = split_max l in balR l' a' r)" |
|
61232 | 71 |
|
61647 | 72 |
lemmas del_root_cases = del_root.cases[case_names Leaf_t Node_Leaf Node_Node] |
61232 | 73 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
74 |
fun delete :: "'a::linorder \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
61232 | 75 |
"delete _ Leaf = Leaf" | |
68413 | 76 |
"delete x (Node l a h r) = |
61678 | 77 |
(case cmp x a of |
68413 | 78 |
EQ \<Rightarrow> del_root (Node l a h r) | |
61678 | 79 |
LT \<Rightarrow> balR (delete x l) a r | |
80 |
GT \<Rightarrow> balL l a (delete x r))" |
|
61232 | 81 |
|
82 |
||
67406 | 83 |
subsection \<open>Functional Correctness Proofs\<close> |
61232 | 84 |
|
67406 | 85 |
text\<open>Very different from the AFP/AVL proofs\<close> |
61232 | 86 |
|
87 |
||
88 |
subsubsection "Proofs for insert" |
|
89 |
||
61581 | 90 |
lemma inorder_balL: |
91 |
"inorder (balL l a r) = inorder l @ a # inorder r" |
|
92 |
by (auto simp: node_def balL_def split:tree.splits) |
|
61232 | 93 |
|
61581 | 94 |
lemma inorder_balR: |
95 |
"inorder (balR l a r) = inorder l @ a # inorder r" |
|
96 |
by (auto simp: node_def balR_def split:tree.splits) |
|
61232 | 97 |
|
98 |
theorem inorder_insert: |
|
99 |
"sorted(inorder t) \<Longrightarrow> inorder(insert x t) = ins_list x (inorder t)" |
|
100 |
by (induct t) |
|
61581 | 101 |
(auto simp: ins_list_simps inorder_balL inorder_balR) |
61232 | 102 |
|
103 |
||
104 |
subsubsection "Proofs for delete" |
|
105 |
||
68023 | 106 |
lemma inorder_split_maxD: |
107 |
"\<lbrakk> split_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
|
61232 | 108 |
inorder t' @ [a] = inorder t" |
68023 | 109 |
by(induction t arbitrary: t' rule: split_max.induct) |
61647 | 110 |
(auto simp: inorder_balL split: if_splits prod.splits tree.split) |
61232 | 111 |
|
61647 | 112 |
lemma inorder_del_root: |
68413 | 113 |
"inorder (del_root (Node l a h r)) = inorder l @ inorder r" |
114 |
by(cases "Node l a h r" rule: del_root.cases) |
|
68023 | 115 |
(auto simp: inorder_balL inorder_balR inorder_split_maxD split: if_splits prod.splits) |
61232 | 116 |
|
117 |
theorem inorder_delete: |
|
118 |
"sorted(inorder t) \<Longrightarrow> inorder (delete x t) = del_list x (inorder t)" |
|
119 |
by(induction t) |
|
61581 | 120 |
(auto simp: del_list_simps inorder_balL inorder_balR |
68023 | 121 |
inorder_del_root inorder_split_maxD split: prod.splits) |
61232 | 122 |
|
123 |
||
124 |
subsubsection "Overall functional correctness" |
|
125 |
||
126 |
interpretation Set_by_Ordered |
|
127 |
where empty = Leaf and isin = isin and insert = insert and delete = delete |
|
61588 | 128 |
and inorder = inorder and inv = "\<lambda>_. True" |
61232 | 129 |
proof (standard, goal_cases) |
130 |
case 1 show ?case by simp |
|
131 |
next |
|
67967 | 132 |
case 2 thus ?case by(simp add: isin_set_inorder) |
61232 | 133 |
next |
134 |
case 3 thus ?case by(simp add: inorder_insert) |
|
135 |
next |
|
136 |
case 4 thus ?case by(simp add: inorder_delete) |
|
61428 | 137 |
qed (rule TrueI)+ |
61232 | 138 |
|
139 |
||
67406 | 140 |
subsection \<open>AVL invariants\<close> |
61232 | 141 |
|
67406 | 142 |
text\<open>Essentially the AFP/AVL proofs\<close> |
61232 | 143 |
|
144 |
||
67406 | 145 |
subsubsection \<open>Insertion maintains AVL balance\<close> |
61232 | 146 |
|
147 |
declare Let_def [simp] |
|
148 |
||
149 |
lemma [simp]: "avl t \<Longrightarrow> ht t = height t" |
|
150 |
by (induct t) simp_all |
|
151 |
||
61581 | 152 |
lemma height_balL: |
61232 | 153 |
"\<lbrakk> height l = height r + 2; avl l; avl r \<rbrakk> \<Longrightarrow> |
61581 | 154 |
height (balL l a r) = height r + 2 \<or> |
155 |
height (balL l a r) = height r + 3" |
|
156 |
by (cases l) (auto simp:node_def balL_def split:tree.split) |
|
61232 | 157 |
|
61581 | 158 |
lemma height_balR: |
61232 | 159 |
"\<lbrakk> height r = height l + 2; avl l; avl r \<rbrakk> \<Longrightarrow> |
61581 | 160 |
height (balR l a r) = height l + 2 \<or> |
161 |
height (balR l a r) = height l + 3" |
|
162 |
by (cases r) (auto simp add:node_def balR_def split:tree.split) |
|
61232 | 163 |
|
164 |
lemma [simp]: "height(node l a r) = max (height l) (height r) + 1" |
|
165 |
by (simp add: node_def) |
|
166 |
||
167 |
lemma avl_node: |
|
168 |
"\<lbrakk> avl l; avl r; |
|
169 |
height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1 |
|
170 |
\<rbrakk> \<Longrightarrow> avl(node l a r)" |
|
171 |
by (auto simp add:max_def node_def) |
|
172 |
||
61581 | 173 |
lemma height_balL2: |
61232 | 174 |
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow> |
61581 | 175 |
height (balL l a r) = (1 + max (height l) (height r))" |
176 |
by (cases l, cases r) (simp_all add: balL_def) |
|
61232 | 177 |
|
61581 | 178 |
lemma height_balR2: |
61232 | 179 |
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow> |
61581 | 180 |
height (balR l a r) = (1 + max (height l) (height r))" |
181 |
by (cases l, cases r) (simp_all add: balR_def) |
|
61232 | 182 |
|
61581 | 183 |
lemma avl_balL: |
61232 | 184 |
assumes "avl l" "avl r" and "height l = height r \<or> height l = height r + 1 |
185 |
\<or> height r = height l + 1 \<or> height l = height r + 2" |
|
61581 | 186 |
shows "avl(balL l a r)" |
61232 | 187 |
proof(cases l) |
188 |
case Leaf |
|
61581 | 189 |
with assms show ?thesis by (simp add: node_def balL_def) |
61232 | 190 |
next |
68413 | 191 |
case Node |
61232 | 192 |
with assms show ?thesis |
193 |
proof(cases "height l = height r + 2") |
|
194 |
case True |
|
195 |
from True Node assms show ?thesis |
|
61581 | 196 |
by (auto simp: balL_def intro!: avl_node split: tree.split) arith+ |
61232 | 197 |
next |
198 |
case False |
|
61581 | 199 |
with assms show ?thesis by (simp add: avl_node balL_def) |
61232 | 200 |
qed |
201 |
qed |
|
202 |
||
61581 | 203 |
lemma avl_balR: |
61232 | 204 |
assumes "avl l" and "avl r" and "height l = height r \<or> height l = height r + 1 |
205 |
\<or> height r = height l + 1 \<or> height r = height l + 2" |
|
61581 | 206 |
shows "avl(balR l a r)" |
61232 | 207 |
proof(cases r) |
208 |
case Leaf |
|
61581 | 209 |
with assms show ?thesis by (simp add: node_def balR_def) |
61232 | 210 |
next |
68413 | 211 |
case Node |
61232 | 212 |
with assms show ?thesis |
213 |
proof(cases "height r = height l + 2") |
|
214 |
case True |
|
215 |
from True Node assms show ?thesis |
|
61581 | 216 |
by (auto simp: balR_def intro!: avl_node split: tree.split) arith+ |
61232 | 217 |
next |
218 |
case False |
|
61581 | 219 |
with assms show ?thesis by (simp add: balR_def avl_node) |
61232 | 220 |
qed |
221 |
qed |
|
222 |
||
223 |
(* It appears that these two properties need to be proved simultaneously: *) |
|
224 |
||
67406 | 225 |
text\<open>Insertion maintains the AVL property:\<close> |
61232 | 226 |
|
227 |
theorem avl_insert_aux: |
|
228 |
assumes "avl t" |
|
229 |
shows "avl(insert x t)" |
|
230 |
"(height (insert x t) = height t \<or> height (insert x t) = height t + 1)" |
|
231 |
using assms |
|
232 |
proof (induction t) |
|
68413 | 233 |
case (Node l a h r) |
61232 | 234 |
case 1 |
235 |
with Node show ?case |
|
236 |
proof(cases "x = a") |
|
237 |
case True |
|
238 |
with Node 1 show ?thesis by simp |
|
239 |
next |
|
240 |
case False |
|
241 |
with Node 1 show ?thesis |
|
242 |
proof(cases "x<a") |
|
243 |
case True |
|
61581 | 244 |
with Node 1 show ?thesis by (auto simp add:avl_balL) |
61232 | 245 |
next |
246 |
case False |
|
67406 | 247 |
with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR) |
61232 | 248 |
qed |
249 |
qed |
|
250 |
case 2 |
|
251 |
from 2 Node show ?case |
|
252 |
proof(cases "x = a") |
|
253 |
case True |
|
254 |
with Node 1 show ?thesis by simp |
|
255 |
next |
|
256 |
case False |
|
257 |
with Node 1 show ?thesis |
|
258 |
proof(cases "x<a") |
|
259 |
case True |
|
260 |
with Node 2 show ?thesis |
|
261 |
proof(cases "height (insert x l) = height r + 2") |
|
67406 | 262 |
case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) |
61232 | 263 |
next |
264 |
case True |
|
61581 | 265 |
hence "(height (balL (insert x l) a r) = height r + 2) \<or> |
266 |
(height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B") |
|
267 |
using Node 2 by (intro height_balL) simp_all |
|
61232 | 268 |
thus ?thesis |
269 |
proof |
|
270 |
assume ?A |
|
67406 | 271 |
with 2 \<open>x < a\<close> show ?thesis by (auto) |
61232 | 272 |
next |
273 |
assume ?B |
|
67406 | 274 |
with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith |
61232 | 275 |
qed |
276 |
qed |
|
277 |
next |
|
278 |
case False |
|
279 |
with Node 2 show ?thesis |
|
280 |
proof(cases "height (insert x r) = height l + 2") |
|
281 |
case False |
|
67406 | 282 |
with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) |
61232 | 283 |
next |
284 |
case True |
|
61581 | 285 |
hence "(height (balR l a (insert x r)) = height l + 2) \<or> |
286 |
(height (balR l a (insert x r)) = height l + 3)" (is "?A \<or> ?B") |
|
287 |
using Node 2 by (intro height_balR) simp_all |
|
61232 | 288 |
thus ?thesis |
289 |
proof |
|
290 |
assume ?A |
|
67406 | 291 |
with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) |
61232 | 292 |
next |
293 |
assume ?B |
|
67406 | 294 |
with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith |
61232 | 295 |
qed |
296 |
qed |
|
297 |
qed |
|
298 |
qed |
|
299 |
qed simp_all |
|
300 |
||
301 |
||
67406 | 302 |
subsubsection \<open>Deletion maintains AVL balance\<close> |
61232 | 303 |
|
68023 | 304 |
lemma avl_split_max: |
61232 | 305 |
assumes "avl x" and "x \<noteq> Leaf" |
68023 | 306 |
shows "avl (fst (split_max x))" "height x = height(fst (split_max x)) \<or> |
307 |
height x = height(fst (split_max x)) + 1" |
|
61232 | 308 |
using assms |
68023 | 309 |
proof (induct x rule: split_max_induct) |
68413 | 310 |
case (Node l a h r) |
61232 | 311 |
case 1 |
61647 | 312 |
thus ?case using Node |
313 |
by (auto simp: height_balL height_balL2 avl_balL |
|
61232 | 314 |
linorder_class.max.absorb1 linorder_class.max.absorb2 |
315 |
split:prod.split) |
|
316 |
next |
|
68413 | 317 |
case (Node l a h r) |
61232 | 318 |
case 2 |
68023 | 319 |
let ?r' = "fst (split_max r)" |
67406 | 320 |
from \<open>avl x\<close> Node 2 have "avl l" and "avl r" by simp_all |
61581 | 321 |
thus ?case using Node 2 height_balL[of l ?r' a] height_balL2[of l ?r' a] |
61232 | 322 |
apply (auto split:prod.splits simp del:avl.simps) by arith+ |
323 |
qed auto |
|
324 |
||
61647 | 325 |
lemma avl_del_root: |
61232 | 326 |
assumes "avl t" and "t \<noteq> Leaf" |
61647 | 327 |
shows "avl(del_root t)" |
61232 | 328 |
using assms |
61647 | 329 |
proof (cases t rule:del_root_cases) |
68413 | 330 |
case (Node_Node ll ln lh lr n h rl rn rh rr) |
331 |
let ?l = "Node ll ln lh lr" |
|
332 |
let ?r = "Node rl rn rh rr" |
|
68023 | 333 |
let ?l' = "fst (split_max ?l)" |
67406 | 334 |
from \<open>avl t\<close> and Node_Node have "avl ?r" by simp |
335 |
from \<open>avl t\<close> and Node_Node have "avl ?l" by simp |
|
61232 | 336 |
hence "avl(?l')" "height ?l = height(?l') \<or> |
68023 | 337 |
height ?l = height(?l') + 1" by (rule avl_split_max,simp)+ |
67406 | 338 |
with \<open>avl t\<close> Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1 |
61232 | 339 |
\<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce |
68023 | 340 |
with \<open>avl ?l'\<close> \<open>avl ?r\<close> have "avl(balR ?l' (snd(split_max ?l)) ?r)" |
61581 | 341 |
by (rule avl_balR) |
61232 | 342 |
with Node_Node show ?thesis by (auto split:prod.splits) |
343 |
qed simp_all |
|
344 |
||
61647 | 345 |
lemma height_del_root: |
61232 | 346 |
assumes "avl t" and "t \<noteq> Leaf" |
61647 | 347 |
shows "height t = height(del_root t) \<or> height t = height(del_root t) + 1" |
61232 | 348 |
using assms |
61647 | 349 |
proof (cases t rule: del_root_cases) |
68413 | 350 |
case (Node_Node ll ln lh lr n h rl rn rh rr) |
351 |
let ?l = "Node ll ln lh lr" |
|
352 |
let ?r = "Node rl rn rh rr" |
|
68023 | 353 |
let ?l' = "fst (split_max ?l)" |
354 |
let ?t' = "balR ?l' (snd(split_max ?l)) ?r" |
|
67406 | 355 |
from \<open>avl t\<close> and Node_Node have "avl ?r" by simp |
356 |
from \<open>avl t\<close> and Node_Node have "avl ?l" by simp |
|
68023 | 357 |
hence "avl(?l')" by (rule avl_split_max,simp) |
358 |
have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using \<open>avl ?l\<close> by (intro avl_split_max) auto |
|
67406 | 359 |
have t_height: "height t = 1 + max (height ?l) (height ?r)" using \<open>avl t\<close> Node_Node by simp |
360 |
have "height t = height ?t' \<or> height t = height ?t' + 1" using \<open>avl t\<close> Node_Node |
|
61232 | 361 |
proof(cases "height ?r = height ?l' + 2") |
362 |
case False |
|
67406 | 363 |
show ?thesis using l'_height t_height False by (subst height_balR2[OF \<open>avl ?l'\<close> \<open>avl ?r\<close> False])+ arith |
61232 | 364 |
next |
365 |
case True |
|
366 |
show ?thesis |
|
68023 | 367 |
proof(cases rule: disjE[OF height_balR[OF True \<open>avl ?l'\<close> \<open>avl ?r\<close>, of "snd (split_max ?l)"]]) |
61232 | 368 |
case 1 |
369 |
thus ?thesis using l'_height t_height True by arith |
|
370 |
next |
|
371 |
case 2 |
|
372 |
thus ?thesis using l'_height t_height True by arith |
|
373 |
qed |
|
374 |
qed |
|
375 |
thus ?thesis using Node_Node by (auto split:prod.splits) |
|
376 |
qed simp_all |
|
377 |
||
67406 | 378 |
text\<open>Deletion maintains the AVL property:\<close> |
61232 | 379 |
|
380 |
theorem avl_delete_aux: |
|
381 |
assumes "avl t" |
|
382 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" |
|
383 |
using assms |
|
384 |
proof (induct t) |
|
68413 | 385 |
case (Node l n h r) |
61232 | 386 |
case 1 |
387 |
with Node show ?case |
|
388 |
proof(cases "x = n") |
|
389 |
case True |
|
61647 | 390 |
with Node 1 show ?thesis by (auto simp:avl_del_root) |
61232 | 391 |
next |
392 |
case False |
|
393 |
with Node 1 show ?thesis |
|
394 |
proof(cases "x<n") |
|
395 |
case True |
|
61581 | 396 |
with Node 1 show ?thesis by (auto simp add:avl_balR) |
61232 | 397 |
next |
398 |
case False |
|
67406 | 399 |
with Node 1 \<open>x\<noteq>n\<close> show ?thesis by (auto simp add:avl_balL) |
61232 | 400 |
qed |
401 |
qed |
|
402 |
case 2 |
|
403 |
with Node show ?case |
|
404 |
proof(cases "x = n") |
|
405 |
case True |
|
68413 | 406 |
with 1 have "height (Node l n h r) = height(del_root (Node l n h r)) |
407 |
\<or> height (Node l n h r) = height(del_root (Node l n h r)) + 1" |
|
61647 | 408 |
by (subst height_del_root,simp_all) |
61232 | 409 |
with True show ?thesis by simp |
410 |
next |
|
411 |
case False |
|
412 |
with Node 1 show ?thesis |
|
413 |
proof(cases "x<n") |
|
414 |
case True |
|
415 |
show ?thesis |
|
416 |
proof(cases "height r = height (delete x l) + 2") |
|
67406 | 417 |
case False with Node 1 \<open>x < n\<close> show ?thesis by(auto simp: balR_def) |
61232 | 418 |
next |
419 |
case True |
|
61581 | 420 |
hence "(height (balR (delete x l) n r) = height (delete x l) + 2) \<or> |
421 |
height (balR (delete x l) n r) = height (delete x l) + 3" (is "?A \<or> ?B") |
|
422 |
using Node 2 by (intro height_balR) auto |
|
61232 | 423 |
thus ?thesis |
424 |
proof |
|
425 |
assume ?A |
|
67406 | 426 |
with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 427 |
next |
428 |
assume ?B |
|
67406 | 429 |
with \<open>x < n\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 430 |
qed |
431 |
qed |
|
432 |
next |
|
433 |
case False |
|
434 |
show ?thesis |
|
435 |
proof(cases "height l = height (delete x r) + 2") |
|
67406 | 436 |
case False with Node 1 \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> show ?thesis by(auto simp: balL_def) |
61232 | 437 |
next |
438 |
case True |
|
61581 | 439 |
hence "(height (balL l n (delete x r)) = height (delete x r) + 2) \<or> |
440 |
height (balL l n (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B") |
|
441 |
using Node 2 by (intro height_balL) auto |
|
61232 | 442 |
thus ?thesis |
443 |
proof |
|
444 |
assume ?A |
|
67406 | 445 |
with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 446 |
next |
447 |
assume ?B |
|
67406 | 448 |
with \<open>\<not>x < n\<close> \<open>x \<noteq> n\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 449 |
qed |
450 |
qed |
|
451 |
qed |
|
452 |
qed |
|
453 |
qed simp_all |
|
454 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
455 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
456 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
457 |
|
68342 | 458 |
text \<open>Based on theorems by Daniel St\"uwe, Manuel Eberl and Peter Lammich.\<close> |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
459 |
|
68313 | 460 |
lemma height_invers: |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
461 |
"(height t = 0) = (t = Leaf)" |
68413 | 462 |
"avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node l a (Suc h) r)" |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
463 |
by (induction t) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
464 |
|
68313 | 465 |
text \<open>Any AVL tree of height \<open>h\<close> has at least \<open>fib (h+2)\<close> leaves:\<close> |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
466 |
|
68313 | 467 |
lemma avl_fib_bound: "avl t \<Longrightarrow> height t = h \<Longrightarrow> fib (h+2) \<le> size1 t" |
468 |
proof (induction h arbitrary: t rule: fib.induct) |
|
469 |
case 1 thus ?case by (simp add: height_invers) |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
470 |
next |
68313 | 471 |
case 2 thus ?case by (cases t) (auto simp: height_invers) |
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
472 |
next |
68313 | 473 |
case (3 h) |
474 |
from "3.prems" obtain l a r where |
|
68413 | 475 |
[simp]: "t = Node l a (Suc(Suc h)) r" "avl l" "avl r" |
68313 | 476 |
and C: " |
477 |
height r = Suc h \<and> height l = Suc h |
|
478 |
\<or> height r = Suc h \<and> height l = h |
|
479 |
\<or> height r = h \<and> height l = Suc h" (is "?C1 \<or> ?C2 \<or> ?C3") |
|
480 |
by (cases t) (simp, fastforce) |
|
481 |
{ |
|
482 |
assume ?C1 |
|
483 |
with "3.IH"(1) |
|
484 |
have "fib (h + 3) \<le> size1 l" "fib (h + 3) \<le> size1 r" |
|
485 |
by (simp_all add: eval_nat_numeral) |
|
486 |
hence ?case by (auto simp: eval_nat_numeral) |
|
487 |
} moreover { |
|
488 |
assume ?C2 |
|
489 |
hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto |
|
490 |
} moreover { |
|
491 |
assume ?C3 |
|
492 |
hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto |
|
493 |
} ultimately show ?case using C by blast |
|
494 |
qed |
|
495 |
||
496 |
lemma fib_alt_induct [consumes 1, case_names 1 2 rec]: |
|
497 |
assumes "n > 0" "P 1" "P 2" "\<And>n. n > 0 \<Longrightarrow> P n \<Longrightarrow> P (Suc n) \<Longrightarrow> P (Suc (Suc n))" |
|
498 |
shows "P n" |
|
499 |
using assms(1) |
|
500 |
proof (induction n rule: fib.induct) |
|
501 |
case (3 n) |
|
502 |
thus ?case using assms by (cases n) (auto simp: eval_nat_numeral) |
|
503 |
qed (insert assms, auto) |
|
504 |
||
505 |
text \<open>An exponential lower bound for @{const fib}:\<close> |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
506 |
|
68313 | 507 |
lemma fib_lowerbound: |
508 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
509 |
defines "c \<equiv> 1 / \<phi> ^ 2" |
|
510 |
assumes "n > 0" |
|
511 |
shows "real (fib n) \<ge> c * \<phi> ^ n" |
|
512 |
proof - |
|
513 |
have "\<phi> > 1" by (simp add: \<phi>_def) |
|
514 |
hence "c > 0" by (simp add: c_def) |
|
515 |
from \<open>n > 0\<close> show ?thesis |
|
516 |
proof (induction n rule: fib_alt_induct) |
|
517 |
case (rec n) |
|
518 |
have "c * \<phi> ^ Suc (Suc n) = \<phi> ^ 2 * (c * \<phi> ^ n)" |
|
519 |
by (simp add: field_simps power2_eq_square) |
|
520 |
also have "\<dots> \<le> (\<phi> + 1) * (c * \<phi> ^ n)" |
|
521 |
by (rule mult_right_mono) (insert \<open>c > 0\<close>, simp_all add: \<phi>_def power2_eq_square field_simps) |
|
522 |
also have "\<dots> = c * \<phi> ^ Suc n + c * \<phi> ^ n" |
|
523 |
by (simp add: field_simps) |
|
524 |
also have "\<dots> \<le> real (fib (Suc n)) + real (fib n)" |
|
525 |
by (intro add_mono rec.IH) |
|
526 |
finally show ?case by simp |
|
527 |
qed (insert \<open>\<phi> > 1\<close>, simp_all add: c_def power2_eq_square eval_nat_numeral) |
|
528 |
qed |
|
529 |
||
530 |
text \<open>The size of an AVL tree is (at least) exponential in its height:\<close> |
|
531 |
||
68342 | 532 |
lemma avl_size_lowerbound: |
68313 | 533 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
534 |
assumes "avl t" |
|
68342 | 535 |
shows "\<phi> ^ (height t) \<le> size1 t" |
68313 | 536 |
proof - |
537 |
have "\<phi> > 0" by(simp add: \<phi>_def add_pos_nonneg) |
|
538 |
hence "\<phi> ^ height t = (1 / \<phi> ^ 2) * \<phi> ^ (height t + 2)" |
|
539 |
by(simp add: field_simps power2_eq_square) |
|
68342 | 540 |
also have "\<dots> \<le> fib (height t + 2)" |
68313 | 541 |
using fib_lowerbound[of "height t + 2"] by(simp add: \<phi>_def) |
68342 | 542 |
also have "\<dots> \<le> size1 t" |
68313 | 543 |
using avl_fib_bound[of t "height t"] assms by simp |
544 |
finally show ?thesis . |
|
545 |
qed |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
546 |
|
68342 | 547 |
text \<open>The height of an AVL tree is most @{term "(1/log 2 \<phi>)"} \<open>\<approx> 1.44\<close> times worse |
548 |
than @{term "log 2 (size1 t)"}:\<close> |
|
549 |
||
550 |
lemma avl_height_upperbound: |
|
551 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
552 |
assumes "avl t" |
|
553 |
shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" |
|
554 |
proof - |
|
555 |
have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) |
|
556 |
hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) |
|
557 |
also have "\<dots> \<le> log \<phi> (size1 t)" |
|
558 |
using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> by simp |
|
559 |
also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" |
|
560 |
by(simp add: log_base_change[of 2 \<phi>]) |
|
561 |
finally show ?thesis . |
|
562 |
qed |
|
563 |
||
61232 | 564 |
end |