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
```