(*  Title:      HOL/ex/AVL.thy
    ID:         $Id: AVL_completion1.thy,v 1.9 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.

Completion of AVL_fragment1.thy.
Thus the version of AVL.thy after exercise sheet 13 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" (*for exercise 5*)
 isord  :: "('a::order) tree => bool" (*for exercise 6*)

primrec
"height Leaf = 0"
"height (Node n l r) = Suc(max (height l) (height r))"
  
(*Exercise 5*)
primrec
"isin k Leaf = False"
"isin k (Node n l r) = (k=n | isin k l | isin k r)" 


(*Exercise 6*)  
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)"


end
