src/HOL/ex/AVL.thy
 author nipkow Fri May 05 12:51:33 2000 +0200 (2000-05-05) changeset 8797 b55e2354d71e child 11701 3d51fbf81c17 permissions -rw-r--r--
```     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
```