(* 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