(*  Title:      HOL/ex/AVL.thy
    ID:         $Id: AVL_fragment.thy,v 1.1 2004/02/02 11:55:04 smaus Exp $
    Author:     Cornelia Pusch and Tobias Nipkow
                modified by B. Wolff
    Copyright   1998  TUM

AVL trees: at the moment only insertion.
This version works exclusively with nat.
Balance check could be simplified by working with int:
"isbal (Node n l r) = (abs(int(height l) - int(height r)) <= #1 &
                      isbal l & isbal r)"

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

It is part of exercise sheet 14.

*)

AVL = Main +

datatype 'a tree = Leaf | Node 'a ('a tree) ('a tree)

consts
 height :: "'a tree => nat"
 isin   :: 
 isord  :: 
 isbal  :: 

primrec
"height Leaf = 0"
"height (Node n l r) = Suc(max (height l) (height r))"


(***********************************************
  Some more chunks you will need

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')"
  

*******************************************************)



  

end