8797
|
1 |
(* Title: HOL/ex/AVL.thy
|
|
2 |
ID: $Id$
|
|
3 |
Author: Cornelia Pusch and Tobias Nipkow
|
|
4 |
Copyright 1998 TUM
|
|
5 |
|
|
6 |
AVL trees: at the moment only insertion.
|
|
7 |
This version works exclusively with nat.
|
|
8 |
Balance check could be simplified by working with int:
|
11908
|
9 |
"isbal (MKT n l r) = (abs(int(height l) - int(height r)) <= 1 &
|
8797
|
10 |
isbal l & isbal r)"
|
|
11 |
*)
|
|
12 |
|
|
13 |
AVL = Main +
|
|
14 |
|
|
15 |
datatype tree = ET | MKT nat tree tree
|
|
16 |
|
|
17 |
consts
|
|
18 |
height :: "tree => nat"
|
|
19 |
isin :: "nat => tree => bool"
|
|
20 |
isord :: "tree => bool"
|
|
21 |
isbal :: "tree => bool"
|
|
22 |
|
|
23 |
primrec
|
|
24 |
"height ET = 0"
|
|
25 |
"height (MKT n l r) = Suc(max (height l) (height r))"
|
|
26 |
|
|
27 |
primrec
|
|
28 |
"isin k ET = False"
|
|
29 |
"isin k (MKT n l r) = (k=n | isin k l | isin k r)"
|
|
30 |
|
|
31 |
primrec
|
|
32 |
"isord ET = True"
|
|
33 |
"isord (MKT n l r) = ((! n'. isin n' l --> n' < n) &
|
|
34 |
(! n'. isin n' r --> n < n') &
|
|
35 |
isord l & isord r)"
|
|
36 |
|
|
37 |
primrec
|
|
38 |
"isbal ET = True"
|
|
39 |
"isbal (MKT n l r) = ((height l = height r |
|
|
40 |
height l = Suc(height r) |
|
|
41 |
height r = Suc(height l)) &
|
|
42 |
isbal l & isbal r)"
|
|
43 |
|
|
44 |
|
|
45 |
datatype bal = Just | Left | Right
|
|
46 |
|
|
47 |
constdefs
|
|
48 |
bal :: "tree => bal"
|
|
49 |
"bal t == case t of ET => Just
|
|
50 |
| (MKT n l r) => if height l = height r then Just
|
|
51 |
else if height l < height r then Right else Left"
|
|
52 |
|
|
53 |
consts
|
|
54 |
r_rot,l_rot,lr_rot,rl_rot :: "nat * tree * tree => tree"
|
|
55 |
|
|
56 |
recdef r_rot "{}"
|
|
57 |
"r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
|
|
58 |
|
|
59 |
recdef l_rot "{}"
|
|
60 |
"l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
|
|
61 |
|
|
62 |
recdef lr_rot "{}"
|
|
63 |
"lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
|
|
64 |
|
|
65 |
recdef rl_rot "{}"
|
|
66 |
"rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
|
|
67 |
|
|
68 |
|
|
69 |
constdefs
|
|
70 |
l_bal :: "nat => tree => tree => tree"
|
|
71 |
"l_bal n l r == if bal l = Right
|
|
72 |
then lr_rot (n, l, r)
|
|
73 |
else r_rot (n, l, r)"
|
|
74 |
|
|
75 |
r_bal :: "nat => tree => tree => tree"
|
|
76 |
"r_bal n l r == if bal r = Left
|
|
77 |
then rl_rot (n, l, r)
|
|
78 |
else l_rot (n, l, r)"
|
|
79 |
|
|
80 |
consts
|
|
81 |
insert :: "nat => tree => tree"
|
|
82 |
primrec
|
|
83 |
"insert x ET = MKT x ET ET"
|
|
84 |
"insert x (MKT n l r) =
|
|
85 |
(if x=n
|
|
86 |
then MKT n l r
|
|
87 |
else if x<n
|
|
88 |
then let l' = insert x l
|
|
89 |
in if height l' = Suc(Suc(height r))
|
|
90 |
then l_bal n l' r
|
|
91 |
else MKT n l' r
|
|
92 |
else let r' = insert x r
|
|
93 |
in if height r' = Suc(Suc(height l))
|
|
94 |
then r_bal n l r'
|
|
95 |
else MKT n l r')"
|
|
96 |
|
|
97 |
end
|