src/HOL/ex/Tree23.thy
author bulwahn
Fri Oct 21 11:17:14 2011 +0200 (2011-10-21)
changeset 45231 d85a2fdc586c
parent 42463 f270e3e18be5
child 45325 26b6179b5a45
permissions -rw-r--r--
replacing code_inline by code_unfold, removing obsolete code_unfold, code_inline del now that the ancient code generator is removed
     1 (*  Title:      HOL/ex/Tree23.thy
     2     Author:     Tobias Nipkow, TU Muenchen
     3 *)
     4 
     5 header {* 2-3 Trees *}
     6 
     7 theory Tree23
     8 imports Main
     9 begin
    10 
    11 text{* This is a very direct translation of some of the functions in table.ML
    12 in the Isabelle source code. That source is due to Makarius Wenzel and Stefan
    13 Berghofer.
    14 
    15 So far this file contains only data types and functions, but no proofs. Feel
    16 free to have a go at the latter!
    17 
    18 Note that because of complicated patterns and mutual recursion, these
    19 function definitions take a few minutes and can also be seen as stress tests
    20 for the function definition facility.  *}
    21 
    22 type_synonym key = int -- {*for simplicity, should be a type class*}
    23 
    24 datatype ord = LESS | EQUAL | GREATER
    25 
    26 definition "ord i j = (if i<j then LESS else if i=j then EQUAL else GREATER)"
    27 
    28 datatype 'a tree23 =
    29   Empty |
    30   Branch2 "'a tree23" "key * 'a" "'a tree23" |
    31   Branch3 "'a tree23" "key * 'a" "'a tree23" "key * 'a" "'a tree23"
    32 
    33 datatype 'a growth =
    34   Stay "'a tree23" |
    35   Sprout "'a tree23" "key * 'a" "'a tree23"
    36 
    37 fun add :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a growth" where
    38 "add key y Empty = Sprout Empty (key,y) Empty" |
    39 "add key y (Branch2 left (k,x) right) =
    40    (case ord key k of
    41       LESS =>
    42         (case add key y left of
    43            Stay left' => Stay (Branch2 left' (k,x) right)
    44          | Sprout left1 q left2
    45            => Stay (Branch3 left1 q left2 (k,x) right))
    46     | EQUAL => Stay (Branch2 left (k,y) right)
    47     | GREATER =>
    48         (case add key y right of
    49            Stay right' => Stay (Branch2 left (k,x) right')
    50          | Sprout right1 q right2
    51            => Stay (Branch3 left (k,x) right1 q right2)))" |
    52 "add key y (Branch3 left (k1,x1) mid (k2,x2) right) =
    53    (case ord key k1 of
    54       LESS =>
    55         (case add key y left of
    56            Stay left' => Stay (Branch3 left' (k1,x1) mid (k2,x2) right)
    57          | Sprout left1 q left2
    58            => Sprout (Branch2 left1 q left2) (k1,x1) (Branch2 mid (k2,x2) right))
    59     | EQUAL => Stay (Branch3 left (k1,y) mid (k2,x2) right)
    60     | GREATER =>
    61         (case ord key k2 of
    62            LESS =>
    63              (case add key y mid of
    64                 Stay mid' => Stay (Branch3 left (k1,x1) mid' (k2,x2) right)
    65               | Sprout mid1 q mid2
    66                 => Sprout (Branch2 left (k1,x1) mid1) q (Branch2 mid2 (k2,x2) right))
    67          | EQUAL => Stay (Branch3 left (k1,x1) mid (k2,y) right)
    68          | GREATER =>
    69              (case add key y right of
    70                 Stay right' => Stay (Branch3 left (k1,x1) mid (k2,x2) right')
    71               | Sprout right1 q right2
    72                 => Sprout (Branch2 left (k1,x1) mid) (k2,x2) (Branch2 right1 q right2))))"
    73 
    74 definition add0 :: "key \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
    75 "add0 k y t =
    76   (case add k y t of Stay t' => t' | Sprout l p r => Branch2 l p r)"
    77 
    78 value "add0 5 e (add0 4 d (add0 3 c (add0 2 b (add0 1 a Empty))))"
    79 
    80 fun compare where
    81 "compare None (k2, _) = LESS" |
    82 "compare (Some k1) (k2, _) = ord k1 k2"
    83 
    84 fun if_eq where
    85 "if_eq EQUAL x y = x" |
    86 "if_eq _ x y = y"
    87 
    88 fun del :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> ((key * 'a) * bool * 'a tree23)option"
    89 where
    90 "del (Some k) Empty = None" |
    91 "del None (Branch2 Empty p Empty) = Some(p, (True, Empty))" |
    92 "del None (Branch3 Empty p Empty q Empty) = Some(p, (False, Branch2 Empty q Empty))" |
    93 "del k (Branch2 Empty p Empty) = (case compare k p of
    94       EQUAL => Some(p, (True, Empty)) | _ => None)" |
    95 "del k (Branch3 Empty p Empty q Empty) = (case compare k p of
    96       EQUAL => Some(p, (False, Branch2 Empty q Empty))
    97     | _ => (case compare k q of
    98         EQUAL => Some(q, (False, Branch2 Empty p Empty))
    99       | _ => None))" |
   100 "del k (Branch2 l p r) = (case compare k p of
   101       LESS => (case del k l of None \<Rightarrow> None |
   102         Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
   103       | Some(p', (True, l')) => Some(p', case r of
   104           Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
   105         | Branch3 rl rp rm rq rr => (False, Branch2
   106             (Branch2 l' p rl) rp (Branch2 rm rq rr))))
   107     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   108         Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
   109       | Some(p', (True, r')) => Some(p', case l of
   110           Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
   111         | Branch3 ll lp lm lq lr => (False, Branch2
   112             (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))" |
   113 "del k (Branch3 l p m q r) = (case compare k q of
   114       LESS => (case compare k p of
   115         LESS => (case del k l of None \<Rightarrow> None |
   116           Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
   117         | Some(p', (True, l')) => Some(p', (False, case (m, r) of
   118             (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
   119           | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
   120           | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
   121               Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
   122       | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
   123           Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
   124         | Some(p', (True, m')) => Some(p', (False, case (l, r) of
   125             (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
   126           | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
   127           | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
   128     | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
   129         Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
   130       | Some(q', (True, r')) => Some(q', (False, case (l, m) of
   131           (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
   132         | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
   133         | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
   134             Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
   135 
   136 definition del0 :: "key \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
   137 "del0 k t = (case del (Some k) t of None \<Rightarrow> t | Some(_,(_,t')) \<Rightarrow> t')"
   138 
   139 
   140 (* yes, this is rather slow *)
   141 fun ord0 :: "'a tree23 \<Rightarrow> bool"
   142 and ordl :: "key \<Rightarrow> 'a tree23 \<Rightarrow> bool"
   143 and ordr :: "'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   144 and ordlr :: "key \<Rightarrow> 'a tree23 \<Rightarrow> key \<Rightarrow> bool"
   145 where
   146 "ord0 Empty = True" |
   147 "ord0 (Branch2 l p r)  = (ordr l (fst p) & ordl (fst p) r)" |
   148 "ord0 (Branch3 l p m q r)  = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   149 
   150 "ordl _ Empty = True" |
   151 "ordl x (Branch2 l p r)  = (ordlr x l (fst p) & ordl (fst p) r)" |
   152 "ordl x (Branch3 l p m q r)  = (ordlr x l (fst p) & ordlr (fst p) m (fst q) & ordl (fst q) r)" |
   153 
   154 "ordr Empty _ = True" |
   155 "ordr (Branch2 l p r) x = (ordr l (fst p) & ordlr (fst p) r x)" |
   156 "ordr (Branch3 l p m q r) x = (ordr l (fst p) & ordlr (fst p) m (fst q) & ordlr (fst q) r x)" |
   157 
   158 "ordlr x Empty y = (x < y)" |
   159 "ordlr x (Branch2 l p r) y = (ordlr x l (fst p) & ordlr (fst p) r y)" |
   160 "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)"
   161 
   162 fun height :: "'a tree23 \<Rightarrow> nat" where
   163 "height Empty = 0" |
   164 "height (Branch2 l _ r) = Suc(max (height l) (height r))" |
   165 "height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
   166 
   167 text{* Is a tree balanced? *}
   168 fun bal :: "'a tree23 \<Rightarrow> bool" where
   169 "bal Empty = True" |
   170 "bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
   171 "bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
   172 
   173 text{* This is a little test harness and should be commented out once the
   174 above functions have been proved correct. *}
   175 
   176 datatype 'a act = Add int 'a | Del int
   177 
   178 fun exec where
   179 "exec [] t = t" |
   180 "exec (Add k x # as) t = exec as (add0 k x t)" |
   181 "exec (Del k # as) t = exec as (del0 k t)"
   182 
   183 text{* Some quick checks: *}
   184 
   185 lemma "ord0(exec as Empty)"
   186 quickcheck
   187 oops
   188 
   189 lemma "bal(exec as Empty)"
   190 quickcheck
   191 oops
   192 
   193 end