|
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: |
|
9 "isbal (MKT n l r) = (abs(int(height l) - int(height r)) <= #1 & |
|
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 |