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