(*  Title:      HOL/ex/AVL_completion2.thy
    ID:         $Id: AVL_completion3.thy,v 1.8 2009/05/01 12:24:50 flopom 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)"

Completion of AVL_completion2.thy (note that there is no AVL_fragment3.thy!
Thus the version of AVL.thy after exercise sheet 15 has been done.
This goes beyond the version by Pusch and Nipkow!

*)

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" 
(*Efficient isin. Sheet 15 Exercise 1*)
 isin_eff   :: "('a::order) => 'a tree => bool"

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

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.*)
  
(*Sheet 15 Exercise 1*)
primrec
isin_eff_empty "isin_eff k Leaf = False"
isin_eff_branch "isin_eff k (Node n l r) = (if k = n then True
                          else (if k<n then (isin_eff k l)
                                else (isin_eff k r)))"
(*Note: Essentially, the machinery of primrec etc. ensures that
  logically, the above (just like other function definitions) is
  a faithful embedding of functional programming language code in
  Isabelle. Whether or not such code is EFFICIENT is a different matter
  and depends on the implementation. The above uses if-then-else which
  should be efficient in any sensible implementation, in that only one
  of the two branches is evaluated. One could define isin_eff as
  follows instead:

primrec
  isin_eff_empty "isin_eff k Leaf = False"
  isin_eff_branch "isin_eff k (Node n l r) = ((k=n) | ((k<n) & (isin_eff k l)) | ((n<k) & (isin_eff k r)))"

If"and" and "or" are implemented in a non-strict way and Boolean
  expressions are evaluated left-to-right, then this is also
  efficient. This is typically the case in existing implementations,
  but one could imagine deviations from this, for which reason 
  the if-then-else may be preferable. *)
  
  
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"

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

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

(*Sheet 15, Exercise 3*)
datatype 'a etree = ELeaf | ENode bal 'a ('a etree) ('a etree)

consts
(*Sheet 15, Exercise 4*)
  prune :: "'a etree => 'a tree"
(*prune means: throw away the balancing labels*)  
(*Exercise 5*)
 correct :: "'a etree => bool"
(*correct means: the balancing arguments are correct*) 

(*Exercise 4*)
primrec
prune_empty  "prune ELeaf = Leaf" 
prune_branch "prune (ENode b n l r) =
		         Node n (prune l) (prune r)"

(*Exercise 5*)
primrec
correct_empty  "correct ELeaf = True"
correct_branch "correct (ENode b n l r) =
	         (b = bal (Node n (prune l) (prune r)) & correct l & correct r)" 

(*Exercise 7*)
consts
 label :: "'a tree => 'a etree"
(*label means: add correct balancing labels*)

(*Exercise 7*)
primrec
label_empty "label Leaf = ELeaf"
label_branch "label (Node n l r) =
	                 ENode (bal (Node n l r)) n (label l)
	                                              (label r)"

end