(*  Title:      HOL/ex/AVL_completion2.thy
    ID:         $Id: AVL_completion2.thy,v 1.8 2008/02/11 15:29:14 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.

Completion of AVL_fragment2.thy
Thus the version of AVL.thy after exercise sheet 14 has been done.

*)

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  :: "'a tree => bool" 

(*Sheet 14 Ex.5*)  
primrec
height_empty "height Leaf = 0"
height_branch "height (Node n l r) = Suc(max (height l) (height r))"

primrec
isin_empty "isin k Leaf = False"
isin_branch "isin k (Node n l r) = (k=n | isin k l | isin k r)" 

primrec
isord_empty "isord Leaf = True"
isord_branch "isord (Node n l r) = ((! n'. isin n' l --> n' < n) &
                      (! n'. isin n' r --> n < n') &
                      isord l & isord r)"

(*Sheet 14 Ex.1*)
primrec
isbal_empty  "isbal Leaf = True"
isbal_branch "isbal (Node n l r) = ((height l = height r |
                       height l = Suc(height r) |
                       Suc(height l) = height r) &
                      isbal l & isbal r)"
(*It was discovered by Christoph Sprunk that it is crucial for the
  automatic proofs that all above equations have the "l" part on the
  lhs and the "r" part on the rhs.*)
  
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"

(*Sheet 14 Ex.3*)  
recdef lr_rot "{}"
"lr_rot(n, Node ln ll (Node lrn lrl lrr), r) = Node lrn (Node ln ll lrl) (Node n lrr r)"

recdef rl_rot "{}"
"rl_rot(n, l, Node rn (Node rln rll rlr) rr) = Node rln (Node n l rll) (Node rn rlr rr)"


(*Sheet 14 Ex.4*)  
constdefs
 l_bal :: "'a => 'a tree => 'a tree => 'a tree"
"l_bal n l r == if bal l = Right
                then lr_rot (n, l, r)
                else r_rot (n, l, r)"

 r_bal :: "'a => 'a tree => 'a tree => 'a tree"
"r_bal n l r == if bal r = Left
                then rl_rot (n, l, r)
                else l_rot (n, l, r)"
  
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