(*

This is a fragment for the AVL.thy file as received by Smaus from
Wolff.

It is part of exercise sheet 14.

*)


(**********************************************************************)
datatype bal = Just | Left | Right

constdefs
 bal :: "'a tree => bal"
"bal t == case t of Leaf => Just
 | (Node n l r) => if height l = height r then Just
                  else if height l < height r then Right else Left"

consts
 r_rot,l_rot,lr_rot,rl_rot :: "'a * 'a tree * 'a tree => 'a tree"

recdef r_rot "{}"
"r_rot (n, Node ln ll lr, r) = Node ln ll (Node n lr r)"

recdef l_rot "{}"
"l_rot(n, l, Node rn rl rr) = Node rn (Node n l rl) rr"


(**********************************************************************)  
constdefs
 l_bal :: "'a => 'a tree => 'a tree => 'a tree"
"l_bal n l r == if 
                then 
                else             "

(**********************************************************************)
  consts
 insert :: "'a::order => 'a tree => 'a tree"
primrec
"insert x Leaf = Node x Leaf Leaf"
"insert x (Node n l r) =
   (if x=n
    then Node n l r
    else if x<n
         then let l' = insert x l
              in if height l' = Suc(Suc(height r))
                 then l_bal n l' r
                 else Node n l' r
         else let r' = insert x r
              in if height r' = Suc(Suc(height l))
                 then r_bal n l r'
                 else Node n l r')"