src/HOL/ex/AVL.thy
changeset 8797 b55e2354d71e
child 11701 3d51fbf81c17
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/AVL.thy	Fri May 05 12:51:33 2000 +0200
     1.3 @@ -0,0 +1,97 @@
     1.4 +(*  Title:      HOL/ex/AVL.thy
     1.5 +    ID:         $Id$
     1.6 +    Author:     Cornelia Pusch and Tobias Nipkow
     1.7 +    Copyright   1998  TUM
     1.8 +
     1.9 +AVL trees: at the moment only insertion.
    1.10 +This version works exclusively with nat.
    1.11 +Balance check could be simplified by working with int:
    1.12 +"isbal (MKT n l r) = (abs(int(height l) - int(height r)) <= #1 &
    1.13 +                      isbal l & isbal r)"
    1.14 +*)
    1.15 +
    1.16 +AVL = Main +
    1.17 +
    1.18 +datatype tree = ET | MKT nat tree tree
    1.19 +
    1.20 +consts
    1.21 + height :: "tree => nat"
    1.22 + isin   :: "nat => tree => bool"
    1.23 + isord  :: "tree => bool"
    1.24 + isbal  :: "tree => bool"
    1.25 +
    1.26 +primrec
    1.27 +"height ET = 0"
    1.28 +"height (MKT n l r) = Suc(max (height l) (height r))"
    1.29 +
    1.30 +primrec
    1.31 +"isin k ET = False"
    1.32 +"isin k (MKT n l r) = (k=n | isin k l | isin k r)"
    1.33 +
    1.34 +primrec
    1.35 +"isord ET = True"
    1.36 +"isord (MKT n l r) = ((! n'. isin n' l --> n' < n) &
    1.37 +                      (! n'. isin n' r --> n < n') &
    1.38 +                      isord l & isord r)"
    1.39 +
    1.40 +primrec
    1.41 +"isbal ET = True"
    1.42 +"isbal (MKT n l r) = ((height l = height r | 
    1.43 +                       height l = Suc(height r) | 
    1.44 +                       height r = Suc(height l)) & 
    1.45 +                      isbal l & isbal r)"
    1.46 +
    1.47 +
    1.48 +datatype bal = Just | Left | Right
    1.49 +
    1.50 +constdefs
    1.51 + bal :: "tree => bal"
    1.52 +"bal t == case t of ET => Just
    1.53 + | (MKT n l r) => if height l = height r then Just
    1.54 +                  else if height l < height r then Right else Left"
    1.55 +
    1.56 +consts
    1.57 + r_rot,l_rot,lr_rot,rl_rot :: "nat * tree * tree => tree"
    1.58 +
    1.59 +recdef r_rot "{}"
    1.60 +"r_rot (n, MKT ln ll lr, r) = MKT ln ll (MKT n lr r)"
    1.61 +
    1.62 +recdef l_rot "{}"
    1.63 +"l_rot(n, l, MKT rn rl rr) = MKT rn (MKT n l rl) rr"
    1.64 +
    1.65 +recdef lr_rot "{}"
    1.66 +"lr_rot(n, MKT ln ll (MKT lrn lrl lrr), r) = MKT lrn (MKT ln ll lrl) (MKT n lrr r)"
    1.67 +
    1.68 +recdef rl_rot "{}"
    1.69 +"rl_rot(n, l, MKT rn (MKT rln rll rlr) rr) = MKT rln (MKT n l rll) (MKT rn rlr rr)"
    1.70 +
    1.71 +
    1.72 +constdefs 
    1.73 + l_bal :: "nat => tree => tree => tree"
    1.74 +"l_bal n l r == if bal l = Right 
    1.75 +                then lr_rot (n, l, r)
    1.76 +                else r_rot (n, l, r)"
    1.77 +
    1.78 + r_bal :: "nat => tree => tree => tree"
    1.79 +"r_bal n l r == if bal r = Left
    1.80 +                then rl_rot (n, l, r)
    1.81 +                else l_rot (n, l, r)"
    1.82 +
    1.83 +consts
    1.84 + insert :: "nat => tree => tree"
    1.85 +primrec
    1.86 +"insert x ET = MKT x ET ET"
    1.87 +"insert x (MKT n l r) = 
    1.88 +   (if x=n
    1.89 +    then MKT n l r
    1.90 +    else if x<n
    1.91 +         then let l' = insert x l
    1.92 +              in if height l' = Suc(Suc(height r))
    1.93 +                 then l_bal n l' r
    1.94 +                 else MKT n l' r
    1.95 +         else let r' = insert x r
    1.96 +              in if height r' = Suc(Suc(height l))
    1.97 +                 then r_bal n l r'
    1.98 +                 else MKT n l r')"
    1.99 +
   1.100 +end