author | wenzelm |
Fri, 18 Aug 2017 20:47:47 +0200 | |
changeset 66453 | cc19f7ca2ed6 |
parent 63411 | e051eea34990 |
child 67406 | 23307fd33906 |
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 |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
10 |
Cmp |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
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 |
||
17 |
text {* Invariant: *} |
|
18 |
||
19 |
fun avl :: "'a avl_tree \<Rightarrow> bool" where |
|
20 |
"avl Leaf = True" | |
|
21 |
"avl (Node h l a r) = |
|
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" | |
|
27 |
"ht (Node h l a r) = h" |
|
28 |
||
29 |
definition node :: "'a avl_tree \<Rightarrow> 'a \<Rightarrow> 'a avl_tree \<Rightarrow> 'a avl_tree" where |
|
30 |
"node l a r = Node (max (ht l) (ht r) + 1) l a r" |
|
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 |
|
36 |
Node _ bl b br \<Rightarrow> |
|
37 |
if ht bl < ht br then |
|
38 |
case br of |
|
39 |
Node _ cl c cr \<Rightarrow> node (node bl b cl) c (node cr a r) |
|
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 |
|
47 |
Node _ bl b br \<Rightarrow> |
|
48 |
if ht bl > ht br then |
|
49 |
case bl of |
|
50 |
Node _ cl c cr \<Rightarrow> node (node l a cl) c (node cr b br) |
|
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 |
61232 | 55 |
"insert x Leaf = Node 1 Leaf x Leaf" | |
61581 | 56 |
"insert x (Node h l a r) = (case cmp x a of |
57 |
EQ \<Rightarrow> Node h l a r | |
|
58 |
LT \<Rightarrow> balL (insert x l) a r | |
|
59 |
GT \<Rightarrow> balR l a (insert x r))" |
|
61232 | 60 |
|
61647 | 61 |
fun del_max :: "'a avl_tree \<Rightarrow> 'a avl_tree * 'a" where |
61678 | 62 |
"del_max (Node _ l a r) = |
63 |
(if r = Leaf then (l,a) else let (r',a') = del_max r in (balL l a r', a'))" |
|
61232 | 64 |
|
61647 | 65 |
lemmas del_max_induct = del_max.induct[case_names Node Leaf] |
61232 | 66 |
|
61647 | 67 |
fun del_root :: "'a avl_tree \<Rightarrow> 'a avl_tree" where |
68 |
"del_root (Node h Leaf a r) = r" | |
|
69 |
"del_root (Node h l a Leaf) = l" | |
|
70 |
"del_root (Node h l a r) = (let (l', a') = del_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" | |
61678 | 76 |
"delete x (Node h l a r) = |
77 |
(case cmp x a of |
|
78 |
EQ \<Rightarrow> del_root (Node h l a r) | |
|
79 |
LT \<Rightarrow> balR (delete x l) a r | |
|
80 |
GT \<Rightarrow> balL l a (delete x r))" |
|
61232 | 81 |
|
82 |
||
83 |
subsection {* Functional Correctness Proofs *} |
|
84 |
||
85 |
text{* Very different from the AFP/AVL proofs *} |
|
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 |
||
61647 | 106 |
lemma inorder_del_maxD: |
107 |
"\<lbrakk> del_max t = (t',a); t \<noteq> Leaf \<rbrakk> \<Longrightarrow> |
|
61232 | 108 |
inorder t' @ [a] = inorder t" |
61647 | 109 |
by(induction t arbitrary: t' rule: del_max.induct) |
110 |
(auto simp: inorder_balL split: if_splits prod.splits tree.split) |
|
61232 | 111 |
|
61647 | 112 |
lemma inorder_del_root: |
113 |
"inorder (del_root (Node h l a r)) = inorder l @ inorder r" |
|
62526 | 114 |
by(cases "Node h l a r" rule: del_root.cases) |
61647 | 115 |
(auto simp: inorder_balL inorder_balR inorder_del_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 |
61647 | 121 |
inorder_del_root inorder_del_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 |
|
132 |
case 2 thus ?case by(simp add: isin_set) |
|
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 |
||
140 |
subsection {* AVL invariants *} |
|
141 |
||
142 |
text{* Essentially the AFP/AVL proofs *} |
|
143 |
||
144 |
||
145 |
subsubsection {* Insertion maintains AVL balance *} |
|
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 |
191 |
case (Node ln ll lr lh) |
|
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 |
211 |
case (Node rn rl rr rh) |
|
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 |
||
225 |
text{* Insertion maintains the AVL property: *} |
|
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) |
|
233 |
case (Node h l a r) |
|
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 |
|
61581 | 247 |
with Node 1 `x\<noteq>a` 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") |
|
61581 | 262 |
case False with Node 2 `x < a` 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 |
|
271 |
with 2 `x < a` show ?thesis by (auto) |
|
272 |
next |
|
273 |
assume ?B |
|
274 |
with True 1 Node(2) `x < a` show ?thesis by (simp) arith |
|
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 |
|
61581 | 282 |
with Node 2 `\<not>x < a` 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 |
|
291 |
with 2 `\<not>x < a` show ?thesis by (auto) |
|
292 |
next |
|
293 |
assume ?B |
|
294 |
with True 1 Node(4) `\<not>x < a` show ?thesis by (simp) arith |
|
295 |
qed |
|
296 |
qed |
|
297 |
qed |
|
298 |
qed |
|
299 |
qed simp_all |
|
300 |
||
301 |
||
302 |
subsubsection {* Deletion maintains AVL balance *} |
|
303 |
||
61647 | 304 |
lemma avl_del_max: |
61232 | 305 |
assumes "avl x" and "x \<noteq> Leaf" |
61647 | 306 |
shows "avl (fst (del_max x))" "height x = height(fst (del_max x)) \<or> |
307 |
height x = height(fst (del_max x)) + 1" |
|
61232 | 308 |
using assms |
61647 | 309 |
proof (induct x rule: del_max_induct) |
310 |
case (Node h l a 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 |
|
61647 | 317 |
case (Node h l a r) |
61232 | 318 |
case 2 |
61647 | 319 |
let ?r' = "fst (del_max r)" |
320 |
from `avl x` 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) |
61232 | 330 |
case (Node_Node h lh ll ln lr n rh rl rn rr) |
331 |
let ?l = "Node lh ll ln lr" |
|
332 |
let ?r = "Node rh rl rn rr" |
|
61647 | 333 |
let ?l' = "fst (del_max ?l)" |
61232 | 334 |
from `avl t` and Node_Node have "avl ?r" by simp |
335 |
from `avl t` and Node_Node have "avl ?l" by simp |
|
336 |
hence "avl(?l')" "height ?l = height(?l') \<or> |
|
61647 | 337 |
height ?l = height(?l') + 1" by (rule avl_del_max,simp)+ |
61232 | 338 |
with `avl t` Node_Node have "height ?l' = height ?r \<or> height ?l' = height ?r + 1 |
339 |
\<or> height ?r = height ?l' + 1 \<or> height ?r = height ?l' + 2" by fastforce |
|
61647 | 340 |
with `avl ?l'` `avl ?r` have "avl(balR ?l' (snd(del_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) |
61232 | 350 |
case (Node_Node h lh ll ln lr n rh rl rn rr) |
351 |
let ?l = "Node lh ll ln lr" |
|
352 |
let ?r = "Node rh rl rn rr" |
|
61647 | 353 |
let ?l' = "fst (del_max ?l)" |
354 |
let ?t' = "balR ?l' (snd(del_max ?l)) ?r" |
|
61232 | 355 |
from `avl t` and Node_Node have "avl ?r" by simp |
356 |
from `avl t` and Node_Node have "avl ?l" by simp |
|
61647 | 357 |
hence "avl(?l')" by (rule avl_del_max,simp) |
358 |
have l'_height: "height ?l = height ?l' \<or> height ?l = height ?l' + 1" using `avl ?l` by (intro avl_del_max) auto |
|
61232 | 359 |
have t_height: "height t = 1 + max (height ?l) (height ?r)" using `avl t` Node_Node by simp |
360 |
have "height t = height ?t' \<or> height t = height ?t' + 1" using `avl t` Node_Node |
|
361 |
proof(cases "height ?r = height ?l' + 2") |
|
362 |
case False |
|
61581 | 363 |
show ?thesis using l'_height t_height False by (subst height_balR2[OF `avl ?l'` `avl ?r` False])+ arith |
61232 | 364 |
next |
365 |
case True |
|
366 |
show ?thesis |
|
61647 | 367 |
proof(cases rule: disjE[OF height_balR[OF True `avl ?l'` `avl ?r`, of "snd (del_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 |
||
378 |
text{* Deletion maintains the AVL property: *} |
|
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) |
|
385 |
case (Node h l n r) |
|
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 |
|
61581 | 399 |
with Node 1 `x\<noteq>n` 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 |
|
61647 | 406 |
with 1 have "height (Node h l n r) = height(del_root (Node h l n r)) |
407 |
\<or> height (Node h l n r) = height(del_root (Node h l n r)) + 1" |
|
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") |
|
61581 | 417 |
case False with Node 1 `x < n` 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 |
|
61581 | 426 |
with `x < n` Node 2 show ?thesis by(auto simp: balR_def) |
61232 | 427 |
next |
428 |
assume ?B |
|
61581 | 429 |
with `x < n` 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") |
|
61581 | 436 |
case False with Node 1 `\<not>x < n` `x \<noteq> n` 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 |
|
61581 | 445 |
with `\<not>x < n` `x \<noteq> n` Node 2 show ?thesis by(auto simp: balL_def) |
61232 | 446 |
next |
447 |
assume ?B |
|
61581 | 448 |
with `\<not>x < n` `x \<noteq> n` 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 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
458 |
text \<open>By Daniel St\"uwe\<close> |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
459 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
460 |
fun fib_tree :: "nat \<Rightarrow> unit avl_tree" where |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
461 |
"fib_tree 0 = Leaf" | |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
462 |
"fib_tree (Suc 0) = Node 1 Leaf () Leaf" | |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
463 |
"fib_tree (Suc(Suc n)) = Node (Suc(Suc(n))) (fib_tree (Suc n)) () (fib_tree n)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
464 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
465 |
lemma [simp]: "ht (fib_tree h) = h" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
466 |
by (induction h rule: "fib_tree.induct") auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
467 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
468 |
lemma [simp]: "height (fib_tree h) = h" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
469 |
by (induction h rule: "fib_tree.induct") auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
470 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
471 |
lemma "avl(fib_tree h)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
472 |
by (induction h rule: "fib_tree.induct") auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
473 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
474 |
lemma fib_tree_size1: "size1 (fib_tree h) = fib (h+2)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
475 |
by (induction h rule: fib_tree.induct) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
476 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
477 |
lemma height_invers[simp]: |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
478 |
"(height t = 0) = (t = Leaf)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
479 |
"avl t \<Longrightarrow> (height t = Suc h) = (\<exists> l a r . t = Node (Suc h) l a r)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
480 |
by (induction t) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
481 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
482 |
lemma fib_Suc_lt: "fib n \<le> fib (Suc n)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
483 |
by (induction n rule: fib.induct) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
484 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
485 |
lemma fib_mono: "n \<le> m \<Longrightarrow> fib n \<le> fib m" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
486 |
proof (induction n arbitrary: m rule: fib.induct ) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
487 |
case (2 m) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
488 |
thus ?case using fib_neq_0_nat[of m] by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
489 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
490 |
case (3 n m) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
491 |
from 3 obtain m' where "m = Suc (Suc m')" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
492 |
by (metis le_Suc_ex plus_nat.simps(2)) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
493 |
thus ?case using 3(1)[of "Suc m'"] 3(2)[of m'] 3(3) by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
494 |
qed simp |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
495 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
496 |
lemma size1_fib_tree_mono: |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
497 |
assumes "n \<le> m" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
498 |
shows "size1 (fib_tree n) \<le> size1 (fib_tree m)" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
499 |
using fib_tree_size1 fib_mono[OF assms] fib_mono[of "Suc n"] add_le_mono assms by fastforce |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
500 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
501 |
lemma fib_tree_minimal: "avl t \<Longrightarrow> size1 (fib_tree (ht t)) \<le> size1 t" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
502 |
proof (induction "ht t" arbitrary: t rule: fib_tree.induct) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
503 |
case (2 t) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
504 |
from 2 obtain l a r where "t = Node (Suc 0) l a r" by (cases t) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
505 |
with 2 show ?case by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
506 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
507 |
case (3 h t) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
508 |
note [simp] = 3(3)[symmetric] |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
509 |
from 3 obtain l a r where [simp]: "t = Node (Suc (Suc h)) l a r" by (cases t) auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
510 |
show ?case proof (cases rule: linorder_cases[of "ht l" "ht r"]) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
511 |
case equal |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
512 |
with 3(3,4) have ht: "ht l = Suc h" "ht r = Suc h" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
513 |
with 3 have "size1 (fib_tree (ht l)) \<le> size1 l" by auto moreover |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
514 |
from 3(1)[of r] 3(3,4) ht(2) have "size1 (fib_tree (ht r)) \<le> size1 r" by auto ultimately |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
515 |
show ?thesis using ht size1_fib_tree_mono[of h "Suc h"] by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
516 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
517 |
case greater |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
518 |
with 3(3,4) have ht: "ht l = Suc h" "ht r = h" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
519 |
from ht 3(1,2,4) have "size1 (fib_tree (Suc h)) \<le> size1 l" by auto moreover |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
520 |
from ht 3(1,2,4) have "size1 (fib_tree h) \<le> size1 r" by auto ultimately |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
521 |
show ?thesis by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
522 |
next |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
523 |
case less (* analogously *) |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
524 |
with 3 have ht: "ht l = h" "Suc h = ht r" by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
525 |
from ht 3 have "size1 (fib_tree h) \<le> size1 l" by auto moreover |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
526 |
from ht 3 have "size1 (fib_tree (Suc h)) \<le> size1 r" by auto ultimately |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
527 |
show ?thesis by auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
528 |
qed |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
529 |
qed auto |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
530 |
|
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
531 |
theorem avl_size_bound: "avl t \<Longrightarrow> fib(height t + 2) \<le> size1 t" |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
532 |
using fib_tree_minimal fib_tree_size1 by fastforce |
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62526
diff
changeset
|
533 |
|
61232 | 534 |
end |