src/HOL/ex/Tree23.thy
changeset 33436 0b5f07dd68f5
child 42463 f270e3e18be5
     1.1 --- /dev/null	Thu Jan 01 00:00:00 1970 +0000
     1.2 +++ b/src/HOL/ex/Tree23.thy	Wed Nov 04 16:54:22 2009 +0100
     1.3 @@ -0,0 +1,193 @@
     1.4 +(*  Title:      HOL/ex/Tree23.thy
     1.5 +    Author:     Tobias Nipkow, TU Muenchen
     1.6 +*)
     1.7 +
     1.8 +header {* 2-3 Trees *}
     1.9 +
    1.10 +theory Tree23
    1.11 +imports Main
    1.12 +begin
    1.13 +
    1.14 +text{* This is a very direct translation of some of the functions in table.ML
    1.15 +in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
    1.16 +Berghofer.
    1.17 +
    1.18 +So far this file contains only data types and functions, but no proofs. Feel
    1.19 +free to have a go at the latter!
    1.20 +
    1.21 +Note that because of complicated patterns and mutual recursion, these
    1.22 +function definitions take a few minutes and can also be seen as stress tests
    1.23 +for the function definition facility.  *}
    1.24 +
    1.25 +types key = int -- {*for simplicity, should be a type class*}
    1.26 +
    1.27 +datatype ord = LESS | EQUAL | GREATER
    1.28 +
    1.29 +definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
    1.30 +
    1.31 +datatype 'a tree23 =
    1.32 +  Empty |
    1.33 +  Branch2 "'a tree23" "key * 'a" "'a tree23" |
    1.34 +  Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
    1.35 +
    1.36 +datatype 'a growth =
    1.37 +  Stay "'a tree23" |
    1.38 +  Sprout "'a tree23" "key * 'a" "'a tree23"
    1.39 +
    1.40 +fun add :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a growth" where
    1.41 +"add key y Empty = Sprout Empty (key,y) Empty" |
    1.42 +"add key y (Branch2 left (k,x) right) =
    1.43 +   (case ord key k of
    1.44 +      LESS =>
    1.45 +        (case add key y left of
    1.46 +           Stay left' => Stay (Branch2 left' (k,x) right)
    1.47 +         | Sprout left1 q left2
    1.48 +           => Stay (Branch3 left1 q left2 (k,x) right))
    1.49 +    | EQUAL => Stay (Branch2 left (k,y) right)
    1.50 +    | GREATER =>
    1.51 +        (case add key y right of
    1.52 +           Stay right' => Stay (Branch2 left (k,x) right')
    1.53 +         | Sprout right1 q right2
    1.54 +           => Stay (Branch3 left (k,x) right1 q right2)))" |
    1.55 +"add key y (Branch3 left (k1,x1) mid (k2,x2) right) =
    1.56 +   (case ord key k1 of
    1.57 +      LESS =>
    1.58 +        (case add key y left of
    1.59 +           Stay left' => Stay (Branch3 left' (k1,x1) mid (k2,x2) right)
    1.60 +         | Sprout left1 q left2
    1.61 +           => Sprout (Branch2 left1 q left2) (k1,x1) (Branch2 mid (k2,x2) right))
    1.62 +    | EQUAL => Stay (Branch3 left (k1,y) mid (k2,x2) right)
    1.63 +    | GREATER =>
    1.64 +        (case ord key k2 of
    1.65 +           LESS =>
    1.66 +             (case add key y mid of
    1.67 +                Stay mid' => Stay (Branch3 left (k1,x1) mid' (k2,x2) right)
    1.68 +              | Sprout mid1 q mid2
    1.69 +                => Sprout (Branch2 left (k1,x1) mid1) q (Branch2 mid2 (k2,x2) right))
    1.70 +         | EQUAL => Stay (Branch3 left (k1,x1) mid (k2,y) right)
    1.71 +         | GREATER =>
    1.72 +             (case add key y right of
    1.73 +                Stay right' => Stay (Branch3 left (k1,x1) mid (k2,x2) right')
    1.74 +              | Sprout right1 q right2
    1.75 +                => Sprout (Branch2 left (k1,x1) mid) (k2,x2) (Branch2 right1 q right2))))"
    1.76 +
    1.77 +definition add0 :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    1.78 +"add0 k y t =
    1.79 +  (case add k y t of Stay t' => t' | Sprout l p r => Branch2 l p r)"
    1.80 +
    1.81 +value "add0 5 e (add0 4 d (add0 3 c (add0 2 b (add0 1 a Empty))))"
    1.82 +
    1.83 +fun compare where
    1.84 +"compare None (k2, _) = LESS" |
    1.85 +"compare (Some k1) (k2, _) = ord k1 k2"
    1.86 +
    1.87 +fun if_eq where
    1.88 +"if_eq EQUAL x y = x" |
    1.89 +"if_eq _ x y = y"
    1.90 +
    1.91 +fun del :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> ((key * 'a) * bool * 'a tree23)option"
    1.92 +where
    1.93 +"del (Some k) Empty = None" |
    1.94 +"del None (Branch2 Empty p Empty) = Some(p, (True, Empty))" |
    1.95 +"del None (Branch3 Empty p Empty q Empty) = Some(p, (False, Branch2 Empty q Empty))" |
    1.96 +"del k (Branch2 Empty p Empty) = (case compare k p of
    1.97 +      EQUAL => Some(p, (True, Empty)) | _ => None)" |
    1.98 +"del k (Branch3 Empty p Empty q Empty) = (case compare k p of
    1.99 +      EQUAL => Some(p, (False, Branch2 Empty q Empty))
   1.100 +    | _ => (case compare k q of
   1.101 +        EQUAL => Some(q, (False, Branch2 Empty p Empty))
   1.102 +      | _ => None))" |
   1.103 +"del k (Branch2 l p r) = (case compare k p of
   1.104 +      LESS => (case del k l of None \<Rightarrow> None |
   1.105 +        Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   1.106 +      | Some(p', (True, l')) => Some(p', case r of
   1.107 +          Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   1.108 +        | Branch3 rl rp rm rq rr => (False, Branch2
   1.109 +            (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   1.110 +    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   1.111 +        Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   1.112 +      | Some(p', (True, r')) => Some(p', case l of
   1.113 +          Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   1.114 +        | Branch3 ll lp lm lq lr => (False, Branch2
   1.115 +            (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" |
   1.116 +"del k (Branch3 l p m q r) = (case compare k q of
   1.117 +      LESS => (case compare k p of
   1.118 +        LESS => (case del k l of None \<Rightarrow> None |
   1.119 +          Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   1.120 +        | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   1.121 +            (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   1.122 +          | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   1.123 +          | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   1.124 +              Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   1.125 +      | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   1.126 +          Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   1.127 +        | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   1.128 +            (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   1.129 +          | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   1.130 +          | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   1.131 +    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   1.132 +        Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   1.133 +      | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   1.134 +          (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   1.135 +        | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   1.136 +        | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   1.137 +            Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   1.138 +
   1.139 +definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   1.140 +"del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
   1.141 +
   1.142 +
   1.143 +(* yes, this is rather slow *)
   1.144 +fun ord0 :: "'a tree23 \<Rightarrow> bool"
   1.145 +and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
   1.146 +and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   1.147 +and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   1.148 +where
   1.149 +"ord0 Empty = True" |
   1.150 +"ord0 (Branch2 l p r)  = (ordr l (fst p) & ordl (fst p) r)" |
   1.151 +"ord0 (Branch3 l p m q r)  = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   1.152 +
   1.153 +"ordl _ Empty = True" |
   1.154 +"ordl x (Branch2 l p r)  = (ordlr x l (fst p) & ordl (fst p) r)" |
   1.155 +"ordl x (Branch3 l p m q r)  = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   1.156 +
   1.157 +"ordr Empty _ = True" |
   1.158 +"ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" |
   1.159 +"ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" |
   1.160 +
   1.161 +"ordlr x Empty y = (x < y)" |
   1.162 +"ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
   1.163 +"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)"
   1.164 +
   1.165 +fun height :: "'a tree23 \<Rightarrow> nat" where
   1.166 +"height Empty = 0" |
   1.167 +"height (Branch2 l _ r) = Suc(max (height l) (height r))" |
   1.168 +"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
   1.169 +
   1.170 +text{* Is a tree balanced? *}
   1.171 +fun bal :: "'a tree23 \<Rightarrow> bool" where
   1.172 +"bal Empty = True" |
   1.173 +"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
   1.174 +"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
   1.175 +
   1.176 +text{* This is a little test harness and should be commented out once the
   1.177 +above functions have been proved correct. *}
   1.178 +
   1.179 +datatype 'a act = Add int 'a | Del int
   1.180 +
   1.181 +fun exec where
   1.182 +"exec [] t = t" |
   1.183 +"exec (Add k x # as) t = exec as (add0 k x t)" |
   1.184 +"exec (Del k # as) t = exec as (del0 k t)"
   1.185 +
   1.186 +text{* Some quick checks: *}
   1.187 +
   1.188 +lemma "ord0(exec as Empty)"
   1.189 +quickcheck
   1.190 +oops
   1.191 +
   1.192 +lemma "bal(exec as Empty)"
   1.193 +quickcheck
   1.194 +oops
   1.195 +
   1.196 +end
   1.197 \ No newline at end of file