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