author | nipkow |
Thu, 23 Apr 2020 22:54:23 +0200 | |
changeset 71795 | 8ad9b2d3dd81 |
parent 71722 | 1cffe8f4d7b3 |
child 71801 | 49d8d8ad7e43 |
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 |
||
71795 | 6 |
subsection \<open>Invariant\<close> |
61232 | 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 |
71795 | 10 |
AVL_Set_Code |
66453
cc19f7ca2ed6
session-qualified theory imports: isabelle imports -U -i -d '~~/src/Benchmarks' -a;
wenzelm
parents:
63411
diff
changeset
|
11 |
"HOL-Number_Theory.Fib" |
61232 | 12 |
begin |
13 |
||
14 |
fun avl :: "'a avl_tree \<Rightarrow> bool" where |
|
15 |
"avl Leaf = True" | |
|
71466 | 16 |
"avl (Node l (a,n) r) = |
61232 | 17 |
((height l = height r \<or> height l = height r + 1 \<or> height r = height l + 1) \<and> |
71466 | 18 |
n = max (height l) (height r) + 1 \<and> avl l \<and> avl r)" |
61232 | 19 |
|
20 |
||
67406 | 21 |
subsubsection \<open>Insertion maintains AVL balance\<close> |
61232 | 22 |
|
23 |
declare Let_def [simp] |
|
24 |
||
70571 | 25 |
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
|
26 |
by (cases t rule: tree2_cases) simp_all |
61232 | 27 |
|
71635 | 28 |
text \<open>First, a fast but relatively manual proof with many lemmas:\<close> |
29 |
||
61581 | 30 |
lemma height_balL: |
71722 | 31 |
"\<lbrakk> avl l; avl r; height l = height r + 2 \<rbrakk> \<Longrightarrow> |
61581 | 32 |
height (balL l a r) = height r + 2 \<or> |
33 |
height (balL l a r) = height r + 3" |
|
34 |
by (cases l) (auto simp:node_def balL_def split:tree.split) |
|
61232 | 35 |
|
61581 | 36 |
lemma height_balR: |
71722 | 37 |
"\<lbrakk> avl l; avl r; height r = height l + 2 \<rbrakk> \<Longrightarrow> |
61581 | 38 |
height (balR l a r) = height l + 2 \<or> |
39 |
height (balR l a r) = height l + 3" |
|
40 |
by (cases r) (auto simp add:node_def balR_def split:tree.split) |
|
61232 | 41 |
|
70571 | 42 |
lemma height_node[simp]: "height(node l a r) = max (height l) (height r) + 1" |
61232 | 43 |
by (simp add: node_def) |
44 |
||
61581 | 45 |
lemma height_balL2: |
61232 | 46 |
"\<lbrakk> avl l; avl r; height l \<noteq> height r + 2 \<rbrakk> \<Longrightarrow> |
71722 | 47 |
height (balL l a r) = 1 + max (height l) (height r)" |
61581 | 48 |
by (cases l, cases r) (simp_all add: balL_def) |
61232 | 49 |
|
61581 | 50 |
lemma height_balR2: |
61232 | 51 |
"\<lbrakk> avl l; avl r; height r \<noteq> height l + 2 \<rbrakk> \<Longrightarrow> |
71722 | 52 |
height (balR l a r) = 1 + max (height l) (height r)" |
61581 | 53 |
by (cases l, cases r) (simp_all add: balR_def) |
61232 | 54 |
|
61581 | 55 |
lemma avl_balL: |
71722 | 56 |
"\<lbrakk> avl l; avl r; height r - 1 \<le> height l \<and> height l \<le> height r + 2 \<rbrakk> \<Longrightarrow> avl(balL l a r)" |
57 |
by(cases l, cases r) |
|
58 |
(auto simp: balL_def node_def split!: if_split tree.split) |
|
61232 | 59 |
|
61581 | 60 |
lemma avl_balR: |
71722 | 61 |
"\<lbrakk> avl l; avl r; height l - 1 \<le> height r \<and> height r \<le> height l + 2 \<rbrakk> \<Longrightarrow> avl(balR l a r)" |
62 |
by(cases r, cases l) |
|
63 |
(auto simp: balR_def node_def split!: if_split tree.split) |
|
61232 | 64 |
|
71635 | 65 |
text\<open>Insertion maintains the AVL property. Requires simultaneous proof.\<close> |
61232 | 66 |
|
68422 | 67 |
theorem avl_insert: |
61232 | 68 |
assumes "avl t" |
69 |
shows "avl(insert x t)" |
|
70 |
"(height (insert x t) = height t \<or> height (insert x t) = height t + 1)" |
|
71 |
using assms |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
72 |
proof (induction t rule: tree2_induct) |
71466 | 73 |
case (Node l a _ r) |
61232 | 74 |
case 1 |
68422 | 75 |
show ?case |
61232 | 76 |
proof(cases "x = a") |
68422 | 77 |
case True with Node 1 show ?thesis by simp |
61232 | 78 |
next |
79 |
case False |
|
68422 | 80 |
show ?thesis |
61232 | 81 |
proof(cases "x<a") |
68422 | 82 |
case True with Node 1 show ?thesis by (auto simp add:avl_balL) |
61232 | 83 |
next |
68422 | 84 |
case False with Node 1 \<open>x\<noteq>a\<close> show ?thesis by (auto simp add:avl_balR) |
61232 | 85 |
qed |
86 |
qed |
|
87 |
case 2 |
|
68422 | 88 |
show ?case |
61232 | 89 |
proof(cases "x = a") |
68422 | 90 |
case True with Node 1 show ?thesis by simp |
61232 | 91 |
next |
92 |
case False |
|
68422 | 93 |
show ?thesis |
94 |
proof(cases "x<a") |
|
61232 | 95 |
case True |
68422 | 96 |
show ?thesis |
61232 | 97 |
proof(cases "height (insert x l) = height r + 2") |
67406 | 98 |
case False with Node 2 \<open>x < a\<close> show ?thesis by (auto simp: height_balL2) |
61232 | 99 |
next |
100 |
case True |
|
61581 | 101 |
hence "(height (balL (insert x l) a r) = height r + 2) \<or> |
102 |
(height (balL (insert x l) a r) = height r + 3)" (is "?A \<or> ?B") |
|
103 |
using Node 2 by (intro height_balL) simp_all |
|
61232 | 104 |
thus ?thesis |
105 |
proof |
|
68422 | 106 |
assume ?A with 2 \<open>x < a\<close> show ?thesis by (auto) |
61232 | 107 |
next |
68422 | 108 |
assume ?B with True 1 Node(2) \<open>x < a\<close> show ?thesis by (simp) arith |
61232 | 109 |
qed |
110 |
qed |
|
111 |
next |
|
112 |
case False |
|
68422 | 113 |
show ?thesis |
61232 | 114 |
proof(cases "height (insert x r) = height l + 2") |
68422 | 115 |
case False with Node 2 \<open>\<not>x < a\<close> show ?thesis by (auto simp: height_balR2) |
61232 | 116 |
next |
117 |
case True |
|
61581 | 118 |
hence "(height (balR l a (insert x r)) = height l + 2) \<or> |
119 |
(height (balR l a (insert x r)) = height l + 3)" (is "?A \<or> ?B") |
|
120 |
using Node 2 by (intro height_balR) simp_all |
|
61232 | 121 |
thus ?thesis |
122 |
proof |
|
68422 | 123 |
assume ?A with 2 \<open>\<not>x < a\<close> show ?thesis by (auto) |
61232 | 124 |
next |
68422 | 125 |
assume ?B with True 1 Node(4) \<open>\<not>x < a\<close> show ?thesis by (simp) arith |
61232 | 126 |
qed |
127 |
qed |
|
128 |
qed |
|
129 |
qed |
|
130 |
qed simp_all |
|
131 |
||
71635 | 132 |
text \<open>Now an automatic proof without lemmas:\<close> |
133 |
||
134 |
theorem avl_insert_auto: "avl t \<Longrightarrow> |
|
135 |
avl(insert x t) \<and> height (insert x t) \<in> {height t, height t + 1}" |
|
136 |
apply (induction t rule: tree2_induct) |
|
71722 | 137 |
(* if you want to save a few secs: apply (auto split!: if_split) *) |
138 |
apply (auto simp: balL_def balR_def node_def max_absorb2 split!: if_split tree.split) |
|
71635 | 139 |
done |
140 |
||
61232 | 141 |
|
67406 | 142 |
subsubsection \<open>Deletion maintains AVL balance\<close> |
61232 | 143 |
|
68023 | 144 |
lemma avl_split_max: |
71722 | 145 |
"\<lbrakk> avl t; t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
146 |
avl (fst (split_max t)) \<and> |
|
147 |
height t \<in> {height(fst (split_max t)), height(fst (split_max t)) + 1}" |
|
148 |
by(induct t rule: split_max_induct) |
|
149 |
(auto simp: balL_def node_def max_absorb2 split!: prod.split if_split tree.split) |
|
61232 | 150 |
|
67406 | 151 |
text\<open>Deletion maintains the AVL property:\<close> |
61232 | 152 |
|
68422 | 153 |
theorem avl_delete: |
61232 | 154 |
assumes "avl t" |
155 |
shows "avl(delete x t)" and "height t = (height (delete x t)) \<or> height t = height (delete x t) + 1" |
|
156 |
using assms |
|
70755
3fb16bed5d6c
replaced new type ('a,'b) tree by old type ('a*'b) tree.
nipkow
parents:
70585
diff
changeset
|
157 |
proof (induct t rule: tree2_induct) |
71466 | 158 |
case (Node l a n r) |
61232 | 159 |
case 1 |
71722 | 160 |
thus ?case |
161 |
using Node avl_split_max[of l] by (auto simp: avl_balL avl_balR split: prod.split) |
|
61232 | 162 |
case 2 |
68422 | 163 |
show ?case |
71466 | 164 |
proof(cases "x = a") |
71636 | 165 |
case True then show ?thesis using 1 avl_split_max[of l] |
166 |
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split) |
|
61232 | 167 |
next |
168 |
case False |
|
68422 | 169 |
show ?thesis |
71466 | 170 |
proof(cases "x<a") |
61232 | 171 |
case True |
172 |
show ?thesis |
|
173 |
proof(cases "height r = height (delete x l) + 2") |
|
71466 | 174 |
case False with Node 1 \<open>x < a\<close> show ?thesis by(auto simp: balR_def) |
61232 | 175 |
next |
176 |
case True |
|
71466 | 177 |
hence "(height (balR (delete x l) a r) = height (delete x l) + 2) \<or> |
178 |
height (balR (delete x l) a r) = height (delete x l) + 3" (is "?A \<or> ?B") |
|
61581 | 179 |
using Node 2 by (intro height_balR) auto |
61232 | 180 |
thus ?thesis |
181 |
proof |
|
71466 | 182 |
assume ?A with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 183 |
next |
71466 | 184 |
assume ?B with \<open>x < a\<close> Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 185 |
qed |
186 |
qed |
|
187 |
next |
|
188 |
case False |
|
189 |
show ?thesis |
|
190 |
proof(cases "height l = height (delete x r) + 2") |
|
71466 | 191 |
case False with Node 1 \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> show ?thesis by(auto simp: balL_def) |
61232 | 192 |
next |
193 |
case True |
|
71466 | 194 |
hence "(height (balL l a (delete x r)) = height (delete x r) + 2) \<or> |
195 |
height (balL l a (delete x r)) = height (delete x r) + 3" (is "?A \<or> ?B") |
|
61581 | 196 |
using Node 2 by (intro height_balL) auto |
61232 | 197 |
thus ?thesis |
198 |
proof |
|
71466 | 199 |
assume ?A with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 200 |
next |
71466 | 201 |
assume ?B with \<open>\<not>x < a\<close> \<open>x \<noteq> a\<close> Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 202 |
qed |
203 |
qed |
|
204 |
qed |
|
205 |
qed |
|
206 |
qed simp_all |
|
207 |
||
71722 | 208 |
text \<open>A more automatic proof. |
209 |
Complete automation as for insertion seems hard due to resource requirements.\<close> |
|
210 |
||
211 |
theorem avl_delete_auto: |
|
212 |
assumes "avl t" |
|
213 |
shows "avl(delete x t)" and "height t \<in> {height (delete x t), height (delete x t) + 1}" |
|
214 |
using assms |
|
215 |
proof (induct t rule: tree2_induct) |
|
216 |
case (Node l a n r) |
|
217 |
case 1 |
|
218 |
show ?case |
|
219 |
proof(cases "x = a") |
|
220 |
case True thus ?thesis |
|
221 |
using 1 avl_split_max[of l] by (auto simp: avl_balR split: prod.split) |
|
222 |
next |
|
223 |
case False thus ?thesis |
|
224 |
using Node 1 by (auto simp: avl_balL avl_balR) |
|
225 |
qed |
|
226 |
case 2 |
|
227 |
show ?case |
|
228 |
proof(cases "x = a") |
|
229 |
case True thus ?thesis |
|
230 |
using 1 avl_split_max[of l] |
|
231 |
by(auto simp: balR_def max_absorb2 split!: if_splits prod.split tree.split) |
|
232 |
next |
|
233 |
case False thus ?thesis |
|
234 |
using height_balL[of l "delete x r" a] height_balR[of "delete x l" r a] Node 1 |
|
235 |
by(auto simp: balL_def balR_def split!: if_split) |
|
236 |
qed |
|
237 |
qed simp_all |
|
238 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
239 |
|
68422 | 240 |
subsection "Overall correctness" |
241 |
||
68440 | 242 |
interpretation S: Set_by_Ordered |
68431 | 243 |
where empty = empty and isin = isin and insert = insert and delete = delete |
68422 | 244 |
and inorder = inorder and inv = avl |
245 |
proof (standard, goal_cases) |
|
68431 | 246 |
case 1 show ?case by (simp add: empty_def) |
68422 | 247 |
next |
248 |
case 2 thus ?case by(simp add: isin_set_inorder) |
|
249 |
next |
|
250 |
case 3 thus ?case by(simp add: inorder_insert) |
|
251 |
next |
|
252 |
case 4 thus ?case by(simp add: inorder_delete) |
|
253 |
next |
|
68431 | 254 |
case 5 thus ?case by (simp add: empty_def) |
68422 | 255 |
next |
256 |
case 6 thus ?case by (simp add: avl_insert(1)) |
|
257 |
next |
|
258 |
case 7 thus ?case by (simp add: avl_delete(1)) |
|
259 |
qed |
|
260 |
||
261 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
262 |
subsection \<open>Height-Size Relation\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
263 |
|
71487 | 264 |
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
|
265 |
|
71466 | 266 |
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
|
267 |
|
71466 | 268 |
lemma avl_fib_bound: "avl t \<Longrightarrow> height t = n \<Longrightarrow> fib (n+2) \<le> size1 t" |
269 |
proof (induction n arbitrary: t rule: fib.induct) |
|
71487 | 270 |
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
|
271 |
next |
71487 | 272 |
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
|
273 |
next |
68313 | 274 |
case (3 h) |
275 |
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
|
276 |
[simp]: "t = Node l (a,Suc(Suc h)) r" "avl l" "avl r" |
68313 | 277 |
and C: " |
278 |
height r = Suc h \<and> height l = Suc h |
|
279 |
\<or> height r = Suc h \<and> height l = h |
|
280 |
\<or> height r = h \<and> height l = Suc h" (is "?C1 \<or> ?C2 \<or> ?C3") |
|
281 |
by (cases t) (simp, fastforce) |
|
282 |
{ |
|
283 |
assume ?C1 |
|
284 |
with "3.IH"(1) |
|
285 |
have "fib (h + 3) \<le> size1 l" "fib (h + 3) \<le> size1 r" |
|
286 |
by (simp_all add: eval_nat_numeral) |
|
287 |
hence ?case by (auto simp: eval_nat_numeral) |
|
288 |
} moreover { |
|
289 |
assume ?C2 |
|
290 |
hence ?case using "3.IH"(1)[of r] "3.IH"(2)[of l] by auto |
|
291 |
} moreover { |
|
292 |
assume ?C3 |
|
293 |
hence ?case using "3.IH"(1)[of l] "3.IH"(2)[of r] by auto |
|
294 |
} ultimately show ?case using C by blast |
|
295 |
qed |
|
296 |
||
69597 | 297 |
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
|
298 |
|
68313 | 299 |
lemma fib_lowerbound: |
300 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
71486 | 301 |
shows "real (fib(n+2)) \<ge> \<phi> ^ n" |
302 |
proof (induction n rule: fib.induct) |
|
303 |
case 1 |
|
304 |
then show ?case by simp |
|
305 |
next |
|
306 |
case 2 |
|
307 |
then show ?case by (simp add: \<phi>_def real_le_lsqrt) |
|
308 |
next |
|
309 |
case (3 n) term ?case |
|
310 |
have "\<phi> ^ Suc (Suc n) = \<phi> ^ 2 * \<phi> ^ n" |
|
311 |
by (simp add: field_simps power2_eq_square) |
|
312 |
also have "\<dots> = (\<phi> + 1) * \<phi> ^ n" |
|
313 |
by (simp_all add: \<phi>_def power2_eq_square field_simps) |
|
314 |
also have "\<dots> = \<phi> ^ Suc n + \<phi> ^ n" |
|
68313 | 315 |
by (simp add: field_simps) |
71486 | 316 |
also have "\<dots> \<le> real (fib (Suc n + 2)) + real (fib (n + 2))" |
317 |
by (intro add_mono "3.IH") |
|
318 |
finally show ?case by simp |
|
68313 | 319 |
qed |
320 |
||
321 |
text \<open>The size of an AVL tree is (at least) exponential in its height:\<close> |
|
322 |
||
68342 | 323 |
lemma avl_size_lowerbound: |
68313 | 324 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
325 |
assumes "avl t" |
|
68342 | 326 |
shows "\<phi> ^ (height t) \<le> size1 t" |
68313 | 327 |
proof - |
71486 | 328 |
have "\<phi> ^ height t \<le> fib (height t + 2)" |
329 |
unfolding \<phi>_def by(rule fib_lowerbound) |
|
68342 | 330 |
also have "\<dots> \<le> size1 t" |
68313 | 331 |
using avl_fib_bound[of t "height t"] assms by simp |
332 |
finally show ?thesis . |
|
333 |
qed |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
334 |
|
69597 | 335 |
text \<open>The height of an AVL tree is most \<^term>\<open>(1/log 2 \<phi>)\<close> \<open>\<approx> 1.44\<close> times worse |
336 |
than \<^term>\<open>log 2 (size1 t)\<close>:\<close> |
|
68342 | 337 |
|
338 |
lemma avl_height_upperbound: |
|
339 |
defines "\<phi> \<equiv> (1 + sqrt 5) / 2" |
|
340 |
assumes "avl t" |
|
341 |
shows "height t \<le> (1/log 2 \<phi>) * log 2 (size1 t)" |
|
342 |
proof - |
|
343 |
have "\<phi> > 0" "\<phi> > 1" by(auto simp: \<phi>_def pos_add_strict) |
|
344 |
hence "height t = log \<phi> (\<phi> ^ height t)" by(simp add: log_nat_power) |
|
345 |
also have "\<dots> \<le> log \<phi> (size1 t)" |
|
70350 | 346 |
using avl_size_lowerbound[OF assms(2), folded \<phi>_def] \<open>1 < \<phi>\<close> |
347 |
by (simp add: le_log_of_power) |
|
68342 | 348 |
also have "\<dots> = (1/log 2 \<phi>) * log 2 (size1 t)" |
349 |
by(simp add: log_base_change[of 2 \<phi>]) |
|
350 |
finally show ?thesis . |
|
351 |
qed |
|
352 |
||
61232 | 353 |
end |