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