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--
Added AVL
     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