(*  Title:      HOL/ex/AVL.thy
    ID:         $Id: AVL_fragment2.thy,v 1.6 2010/02/03 10:55:41 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.

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   :: "'a => 'a tree => bool"
 isord  :: "('a::order) tree => bool" 
(* isbal  :: *)

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

primrec
"isin k Leaf = False"
"isin k (Node n l r) = (k=n | isin k l | isin k r)" 
  
primrec
"isord Leaf = True"
"isord (Node n l r) = ((! n'. isin n' l --> n' < n) &
                      (! n'. isin n' r --> n < n') &
                      isord l & isord 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