# HG changeset patch # User nipkow # Date 1257350062 -3600 # Node ID 0b5f07dd68f5350476d45977979daa79e77ed955 # Parent 6f825ec18b4999c2577184a557efe1ba3520343e New diff -r 6f825ec18b49 -r 0b5f07dd68f5 src/HOL/ex/ROOT.ML --- a/src/HOL/ex/ROOT.ML Wed Nov 04 10:17:58 2009 +0100 +++ b/src/HOL/ex/ROOT.ML Wed Nov 04 16:54:22 2009 +0100 @@ -40,6 +40,7 @@ "CTL", "Arith_Examples", "BT", + "Tree23", "MergeSort", "Lagrange", "Groebner_Examples", diff -r 6f825ec18b49 -r 0b5f07dd68f5 src/HOL/ex/Tree23.thy --- /dev/null Thu Jan 01 00:00:00 1970 +0000 +++ b/src/HOL/ex/Tree23.thy Wed Nov 04 16:54:22 2009 +0100 @@ -0,0 +1,193 @@ +(* Title: HOL/ex/Tree23.thy + Author: Tobias Nipkow, TU Muenchen +*) + +header {* 2-3 Trees *} + +theory Tree23 +imports Main +begin + +text{* This is a very direct translation of some of the functions in table.ML +in the Isabelle source code. That source is due to Makarius Wenzel and Stefan +Berghofer. + +So far this file contains only data types and functions, but no proofs. Feel +free to have a go at the latter! + +Note that because of complicated patterns and mutual recursion, these +function definitions take a few minutes and can also be seen as stress tests +for the function definition facility. *} + +types key = int -- {*for simplicity, should be a type class*} + +datatype ord = LESS | EQUAL | GREATER + +definition "ord i j = (if i 'a \ 'a tree23 \ 'a growth" where +"add key y Empty = Sprout Empty (key,y) Empty" | +"add key y (Branch2 left (k,x) right) = + (case ord key k of + LESS => + (case add key y left of + Stay left' => Stay (Branch2 left' (k,x) right) + | Sprout left1 q left2 + => Stay (Branch3 left1 q left2 (k,x) right)) + | EQUAL => Stay (Branch2 left (k,y) right) + | GREATER => + (case add key y right of + Stay right' => Stay (Branch2 left (k,x) right') + | Sprout right1 q right2 + => Stay (Branch3 left (k,x) right1 q right2)))" | +"add key y (Branch3 left (k1,x1) mid (k2,x2) right) = + (case ord key k1 of + LESS => + (case add key y left of + Stay left' => Stay (Branch3 left' (k1,x1) mid (k2,x2) right) + | Sprout left1 q left2 + => Sprout (Branch2 left1 q left2) (k1,x1) (Branch2 mid (k2,x2) right)) + | EQUAL => Stay (Branch3 left (k1,y) mid (k2,x2) right) + | GREATER => + (case ord key k2 of + LESS => + (case add key y mid of + Stay mid' => Stay (Branch3 left (k1,x1) mid' (k2,x2) right) + | Sprout mid1 q mid2 + => Sprout (Branch2 left (k1,x1) mid1) q (Branch2 mid2 (k2,x2) right)) + | EQUAL => Stay (Branch3 left (k1,x1) mid (k2,y) right) + | GREATER => + (case add key y right of + Stay right' => Stay (Branch3 left (k1,x1) mid (k2,x2) right') + | Sprout right1 q right2 + => Sprout (Branch2 left (k1,x1) mid) (k2,x2) (Branch2 right1 q right2))))" + +definition add0 :: "key \ 'a \ 'a tree23 \ 'a tree23" where +"add0 k y t = + (case add k y t of Stay t' => t' | Sprout l p r => Branch2 l p r)" + +value "add0 5 e (add0 4 d (add0 3 c (add0 2 b (add0 1 a Empty))))" + +fun compare where +"compare None (k2, _) = LESS" | +"compare (Some k1) (k2, _) = ord k1 k2" + +fun if_eq where +"if_eq EQUAL x y = x" | +"if_eq _ x y = y" + +fun del :: "key option \ 'a tree23 \ ((key * 'a) * bool * 'a tree23)option" +where +"del (Some k) Empty = None" | +"del None (Branch2 Empty p Empty) = Some(p, (True, Empty))" | +"del None (Branch3 Empty p Empty q Empty) = Some(p, (False, Branch2 Empty q Empty))" | +"del k (Branch2 Empty p Empty) = (case compare k p of + EQUAL => Some(p, (True, Empty)) | _ => None)" | +"del k (Branch3 Empty p Empty q Empty) = (case compare k p of + EQUAL => Some(p, (False, Branch2 Empty q Empty)) + | _ => (case compare k q of + EQUAL => Some(q, (False, Branch2 Empty p Empty)) + | _ => None))" | +"del k (Branch2 l p r) = (case compare k p of + LESS => (case del k l of None \ None | + Some(p', (False, l')) => Some(p', (False, Branch2 l' p r)) + | Some(p', (True, l')) => Some(p', case r of + Branch2 rl rp rr => (True, Branch3 l' p rl rp rr) + | Branch3 rl rp rm rq rr => (False, Branch2 + (Branch2 l' p rl) rp (Branch2 rm rq rr)))) + | or => (case del (if_eq or None k) r of None \ None | + Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r')) + | Some(p', (True, r')) => Some(p', case l of + Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r') + | Branch3 ll lp lm lq lr => (False, Branch2 + (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" | +"del k (Branch3 l p m q r) = (case compare k q of + LESS => (case compare k p of + LESS => (case del k l of None \ None | + Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r)) + | Some(p', (True, l')) => Some(p', (False, case (m, r) of + (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r + | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r + | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) => + Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr)))) + | or => (case del (if_eq or None k) m of None \ None | + Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r)) + | Some(p', (True, m')) => Some(p', (False, case (l, r) of + (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r + | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r + | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr))))) + | or => (case del (if_eq or None k) r of None \ None | + Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r')) + | Some(q', (True, r')) => Some(q', (False, case (l, m) of + (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r') + | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r') + | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) => + Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))" + +definition del0 :: "key \ 'a tree23 \ 'a tree23" where +"del0 k t = (case del (Some k) t of None \ t | Some(_,(_,t')) \ t')" + + +(* yes, this is rather slow *) +fun ord0 :: "'a tree23 \ bool" +and ordl :: "key \ 'a tree23 \ bool" +and ordr :: "'a tree23 \ key \ bool" +and ordlr :: "key \ 'a tree23 \ key \ bool" +where +"ord0 Empty = True" | +"ord0 (Branch2 l p r) = (ordr l (fst p) & ordl (fst p) r)" | +"ord0 (Branch3 l p m q r) = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | + +"ordl _ Empty = True" | +"ordl x (Branch2 l p r) = (ordlr x l (fst p) & ordl (fst p) r)" | +"ordl x (Branch3 l p m q r) = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" | + +"ordr Empty _ = True" | +"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" | +"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" | + +"ordlr x Empty y = (x < y)" | +"ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" | +"ordlr x (Branch3 l p m q r) y = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r y)" + +fun height :: "'a tree23 \ nat" where +"height Empty = 0" | +"height (Branch2 l _ r) = Suc(max (height l) (height r))" | +"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))" + +text{* Is a tree balanced? *} +fun bal :: "'a tree23 \ bool" where +"bal Empty = True" | +"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" | +"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)" + +text{* This is a little test harness and should be commented out once the +above functions have been proved correct. *} + +datatype 'a act = Add int 'a | Del int + +fun exec where +"exec [] t = t" | +"exec (Add k x # as) t = exec as (add0 k x t)" | +"exec (Del k # as) t = exec as (del0 k t)" + +text{* Some quick checks: *} + +lemma "ord0(exec as Empty)" +quickcheck +oops + +lemma "bal(exec as Empty)" +quickcheck +oops + +end \ No newline at end of file