src/HOL/Data_Structures/Tree234_Set.thy
author nipkow
Wed Jun 13 15:24:20 2018 +0200 (10 months ago)
changeset 68440 6826718f732d
parent 68431 b294e095f64c
child 69597 ff784d5a5bfb
permissions -rw-r--r--
qualify interpretations to avoid clashes
nipkow@61640
     1
(* Author: Tobias Nipkow *)
nipkow@61640
     2
nipkow@62130
     3
section \<open>2-3-4 Tree Implementation of Sets\<close>
nipkow@61640
     4
nipkow@61640
     5
theory Tree234_Set
nipkow@61640
     6
imports
nipkow@61640
     7
  Tree234
nipkow@61640
     8
  Cmp
nipkow@67965
     9
  Set_Specs
nipkow@61640
    10
begin
nipkow@61640
    11
nipkow@68109
    12
declare sorted_wrt.simps(2)[simp del]
nipkow@68109
    13
nipkow@61640
    14
subsection \<open>Set operations on 2-3-4 trees\<close>
nipkow@61640
    15
nipkow@68431
    16
definition empty :: "'a tree234" where
nipkow@68431
    17
"empty = Leaf"
nipkow@68431
    18
nipkow@63411
    19
fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where
nipkow@61640
    20
"isin Leaf x = False" |
nipkow@61640
    21
"isin (Node2 l a r) x =
nipkow@61640
    22
  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x)" |
nipkow@61640
    23
"isin (Node3 l a m b r) x =
nipkow@61640
    24
  (case cmp x a of LT \<Rightarrow> isin l x | EQ \<Rightarrow> True | GT \<Rightarrow> (case cmp x b of
nipkow@61640
    25
   LT \<Rightarrow> isin m x | EQ \<Rightarrow> True | GT \<Rightarrow> isin r x))" |
nipkow@61703
    26
"isin (Node4 t1 a t2 b t3 c t4) x =
nipkow@61703
    27
  (case cmp x b of
nipkow@61703
    28
     LT \<Rightarrow>
nipkow@61703
    29
       (case cmp x a of
nipkow@61640
    30
          LT \<Rightarrow> isin t1 x |
nipkow@61640
    31
          EQ \<Rightarrow> True |
nipkow@61640
    32
          GT \<Rightarrow> isin t2 x) |
nipkow@61703
    33
     EQ \<Rightarrow> True |
nipkow@61703
    34
     GT \<Rightarrow>
nipkow@61703
    35
       (case cmp x c of
nipkow@61640
    36
          LT \<Rightarrow> isin t3 x |
nipkow@61640
    37
          EQ \<Rightarrow> True |
nipkow@61640
    38
          GT \<Rightarrow> isin t4 x))"
nipkow@61640
    39
nipkow@61640
    40
datatype 'a up\<^sub>i = T\<^sub>i "'a tree234" | Up\<^sub>i "'a tree234" 'a "'a tree234"
nipkow@61640
    41
nipkow@61640
    42
fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree234" where
nipkow@61640
    43
"tree\<^sub>i (T\<^sub>i t) = t" |
nipkow@61709
    44
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
nipkow@61640
    45
nipkow@63411
    46
fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where
nipkow@61640
    47
"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
nipkow@61640
    48
"ins x (Node2 l a r) =
nipkow@61640
    49
   (case cmp x a of
nipkow@61640
    50
      LT \<Rightarrow> (case ins x l of
nipkow@61640
    51
              T\<^sub>i l' => T\<^sub>i (Node2 l' a r)
nipkow@61640
    52
            | Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
nipkow@61640
    53
      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
nipkow@61640
    54
      GT \<Rightarrow> (case ins x r of
nipkow@61640
    55
              T\<^sub>i r' => T\<^sub>i (Node2 l a r')
nipkow@61640
    56
            | Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
nipkow@61640
    57
"ins x (Node3 l a m b r) =
nipkow@61640
    58
   (case cmp x a of
nipkow@61640
    59
      LT \<Rightarrow> (case ins x l of
nipkow@61640
    60
              T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r)
nipkow@61640
    61
            | Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
nipkow@61640
    62
      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
nipkow@61640
    63
      GT \<Rightarrow> (case cmp x b of
nipkow@61640
    64
               GT \<Rightarrow> (case ins x r of
nipkow@61640
    65
                       T\<^sub>i r' => T\<^sub>i (Node3 l a m b r')
nipkow@61640
    66
                     | Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
nipkow@61640
    67
               EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
nipkow@61640
    68
               LT \<Rightarrow> (case ins x m of
nipkow@61640
    69
                       T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r)
nipkow@61640
    70
                     | Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))" |
nipkow@61703
    71
"ins x (Node4 t1 a t2 b t3 c t4) =
nipkow@61703
    72
  (case cmp x b of
nipkow@61703
    73
     LT \<Rightarrow>
nipkow@61703
    74
       (case cmp x a of
nipkow@61703
    75
          LT \<Rightarrow>
nipkow@61703
    76
            (case ins x t1 of
nipkow@61703
    77
               T\<^sub>i t => T\<^sub>i (Node4 t a t2 b t3 c t4) |
nipkow@61703
    78
               Up\<^sub>i l y r => Up\<^sub>i (Node2 l y r) a (Node3 t2 b t3 c t4)) |
nipkow@61703
    79
          EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
nipkow@61703
    80
          GT \<Rightarrow>
nipkow@61703
    81
            (case ins x t2 of
nipkow@61703
    82
               T\<^sub>i t => T\<^sub>i (Node4 t1 a t b t3 c t4) |
nipkow@61703
    83
               Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a l) y (Node3 r b t3 c t4))) |
nipkow@61703
    84
     EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
nipkow@61703
    85
     GT \<Rightarrow>
nipkow@61703
    86
       (case cmp x c of
nipkow@61703
    87
          LT \<Rightarrow>
nipkow@61703
    88
            (case ins x t3 of
nipkow@61703
    89
              T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t c t4) |
nipkow@61703
    90
              Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 l y r c t4)) |
nipkow@61703
    91
          EQ \<Rightarrow> T\<^sub>i (Node4 t1 a t2 b t3 c t4) |
nipkow@61703
    92
          GT \<Rightarrow>
nipkow@61703
    93
            (case ins x t4 of
nipkow@61703
    94
              T\<^sub>i t => T\<^sub>i (Node4 t1 a t2 b t3 c t) |
nipkow@61703
    95
              Up\<^sub>i l y r => Up\<^sub>i (Node2 t1 a t2) b (Node3 t3 c l y r))))"
nipkow@61640
    96
nipkow@61640
    97
hide_const insert
nipkow@61640
    98
nipkow@63411
    99
definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
nipkow@61640
   100
"insert x t = tree\<^sub>i(ins x t)"
nipkow@61640
   101
nipkow@61640
   102
datatype 'a up\<^sub>d = T\<^sub>d "'a tree234" | Up\<^sub>d "'a tree234"
nipkow@61640
   103
nipkow@61640
   104
fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree234" where
nipkow@61709
   105
"tree\<^sub>d (T\<^sub>d t) = t" |
nipkow@61709
   106
"tree\<^sub>d (Up\<^sub>d t) = t"
nipkow@61640
   107
nipkow@61640
   108
fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   109
"node21 (T\<^sub>d l) a r = T\<^sub>d(Node2 l a r)" |
nipkow@61640
   110
"node21 (Up\<^sub>d l) a (Node2 lr b rr) = Up\<^sub>d(Node3 l a lr b rr)" |
nipkow@61640
   111
"node21 (Up\<^sub>d l) a (Node3 lr b mr c rr) = T\<^sub>d(Node2 (Node2 l a lr) b (Node2 mr c rr))" |
nipkow@61640
   112
"node21 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
nipkow@61640
   113
nipkow@61640
   114
fun node22 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   115
"node22 l a (T\<^sub>d r) = T\<^sub>d(Node2 l a r)" |
nipkow@61640
   116
"node22 (Node2 ll b rl) a (Up\<^sub>d r) = Up\<^sub>d(Node3 ll b rl a r)" |
nipkow@61640
   117
"node22 (Node3 ll b ml c rl) a (Up\<^sub>d r) = T\<^sub>d(Node2 (Node2 ll b ml) c (Node2 rl a r))" |
nipkow@61640
   118
"node22 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node3 t3 c t4 d t5))"
nipkow@61640
   119
nipkow@61640
   120
fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   121
"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
nipkow@61640
   122
"node31 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 = T\<^sub>d(Node2 (Node3 t1 a t2 b t3) c t4)" |
nipkow@61640
   123
"node31 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node2 t3 c t4) d t5)" |
nipkow@61640
   124
"node31 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 = T\<^sub>d(Node3 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6)"
nipkow@61640
   125
nipkow@61640
   126
fun node32 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   127
"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
nipkow@61640
   128
"node32 t1 a (Up\<^sub>d t2) b (Node2 t3 c t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
nipkow@61640
   129
"node32 t1 a (Up\<^sub>d t2) b (Node3 t3 c t4 d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
nipkow@61640
   130
"node32 t1 a (Up\<^sub>d t2) b (Node4 t3 c t4 d t5 e t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
nipkow@61640
   131
nipkow@61640
   132
fun node33 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   133
"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
nipkow@61640
   134
"node33 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) = T\<^sub>d(Node2 t1 a (Node3 t2 b t3 c t4))" |
nipkow@61640
   135
"node33 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node2 t4 d t5))" |
nipkow@61640
   136
"node33 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node3 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6))"
nipkow@61640
   137
nipkow@61640
   138
fun node41 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   139
"node41 (T\<^sub>d t1) a t2 b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
nipkow@61640
   140
"node41 (Up\<^sub>d t1) a (Node2 t2 b t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
nipkow@61640
   141
"node41 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
nipkow@61640
   142
"node41 (Up\<^sub>d t1) a (Node4 t2 b t3 c t4 d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
nipkow@61640
   143
nipkow@61640
   144
fun node42 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   145
"node42 t1 a (T\<^sub>d t2) b t3 c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
nipkow@61640
   146
"node42 (Node2 t1 a t2) b (Up\<^sub>d t3) c t4 d t5 = T\<^sub>d(Node3 (Node3 t1 a t2 b t3) c t4 d t5)" |
nipkow@61640
   147
"node42 (Node3 t1 a t2 b t3) c (Up\<^sub>d t4) d t5 e t6 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node2 t3 c t4) d t5 e t6)" |
nipkow@61640
   148
"node42 (Node4 t1 a t2 b t3 c t4) d (Up\<^sub>d t5) e t6 f t7 = T\<^sub>d(Node4 (Node2 t1 a t2) b (Node3 t3 c t4 d t5) e t6 f t7)"
nipkow@61640
   149
nipkow@61640
   150
fun node43 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   151
"node43 t1 a t2 b (T\<^sub>d t3) c t4 = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
nipkow@61640
   152
"node43 t1 a (Node2 t2 b t3) c (Up\<^sub>d t4) d t5 = T\<^sub>d(Node3 t1 a (Node3 t2 b t3 c t4) d t5)" |
nipkow@61640
   153
"node43 t1 a (Node3 t2 b t3 c t4) d (Up\<^sub>d t5) e t6 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node2 t4 d t5) e t6)" |
nipkow@61640
   154
"node43 t1 a (Node4 t2 b t3 c t4 d t5) e (Up\<^sub>d t6) f t7 = T\<^sub>d(Node4 t1 a (Node2 t2 b t3) c (Node3 t4 d t5 e t6) f t7)"
nipkow@61640
   155
nipkow@61640
   156
fun node44 :: "'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a tree234 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   157
"node44 t1 a t2 b t3 c (T\<^sub>d t4) = T\<^sub>d(Node4 t1 a t2 b t3 c t4)" |
nipkow@61640
   158
"node44 t1 a t2 b (Node2 t3 c t4) d (Up\<^sub>d t5) = T\<^sub>d(Node3 t1 a t2 b (Node3 t3 c t4 d t5))" |
nipkow@61640
   159
"node44 t1 a t2 b (Node3 t3 c t4 d t5) e (Up\<^sub>d t6) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node2 t5 e t6))" |
nipkow@61640
   160
"node44 t1 a t2 b (Node4 t3 c t4 d t5 e t6) f (Up\<^sub>d t7) = T\<^sub>d(Node4 t1 a t2 b (Node2 t3 c t4) d (Node3 t5 e t6 f t7))"
nipkow@61640
   161
nipkow@68020
   162
fun split_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where
nipkow@68020
   163
"split_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
nipkow@68020
   164
"split_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
nipkow@68020
   165
"split_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" |
nipkow@68020
   166
"split_min (Node2 l a r) = (let (x,l') = split_min l in (x, node21 l' a r))" |
nipkow@68020
   167
"split_min (Node3 l a m b r) = (let (x,l') = split_min l in (x, node31 l' a m b r))" |
nipkow@68020
   168
"split_min (Node4 l a m b n c r) = (let (x,l') = split_min l in (x, node41 l' a m b n c r))"
nipkow@61640
   169
nipkow@63411
   170
fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   171
"del k Leaf = T\<^sub>d Leaf" |
nipkow@61640
   172
"del k (Node2 Leaf p Leaf) = (if k=p then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf p Leaf))" |
nipkow@61640
   173
"del k (Node3 Leaf p Leaf q Leaf) = T\<^sub>d(if k=p then Node2 Leaf q Leaf
nipkow@61640
   174
  else if k=q then Node2 Leaf p Leaf else Node3 Leaf p Leaf q Leaf)" |
nipkow@61640
   175
"del k (Node4 Leaf a Leaf b Leaf c Leaf) =
nipkow@61640
   176
  T\<^sub>d(if k=a then Node3 Leaf b Leaf c Leaf else
nipkow@61640
   177
     if k=b then Node3 Leaf a Leaf c Leaf else
nipkow@61640
   178
     if k=c then Node3 Leaf a Leaf b Leaf
nipkow@61640
   179
     else Node4 Leaf a Leaf b Leaf c Leaf)" |
nipkow@61640
   180
"del k (Node2 l a r) = (case cmp k a of
nipkow@61640
   181
  LT \<Rightarrow> node21 (del k l) a r |
nipkow@61640
   182
  GT \<Rightarrow> node22 l a (del k r) |
nipkow@68020
   183
  EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" |
nipkow@61640
   184
"del k (Node3 l a m b r) = (case cmp k a of
nipkow@61640
   185
  LT \<Rightarrow> node31 (del k l) a m b r |
nipkow@68020
   186
  EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r |
nipkow@61640
   187
  GT \<Rightarrow> (case cmp k b of
nipkow@61640
   188
           LT \<Rightarrow> node32 l a (del k m) b r |
nipkow@68020
   189
           EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' |
nipkow@61640
   190
           GT \<Rightarrow> node33 l a m b (del k r)))" |
nipkow@61640
   191
"del k (Node4 l a m b n c r) = (case cmp k b of
nipkow@61640
   192
  LT \<Rightarrow> (case cmp k a of
nipkow@61640
   193
          LT \<Rightarrow> node41 (del k l) a m b n c r |
nipkow@68020
   194
          EQ \<Rightarrow> let (a',m') = split_min m in node42 l a' m' b n c r |
nipkow@61640
   195
          GT \<Rightarrow> node42 l a (del k m) b n c r) |
nipkow@68020
   196
  EQ \<Rightarrow> let (b',n') = split_min n in node43 l a m b' n' c r |
nipkow@61640
   197
  GT \<Rightarrow> (case cmp k c of
nipkow@61640
   198
           LT \<Rightarrow> node43 l a m b (del k n) c r |
nipkow@68020
   199
           EQ \<Rightarrow> let (c',r') = split_min r in node44 l a m b n c' r' |
nipkow@61640
   200
           GT \<Rightarrow> node44 l a m b n c (del k r)))"
nipkow@61640
   201
nipkow@63411
   202
definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where
nipkow@61640
   203
"delete x t = tree\<^sub>d(del x t)"
nipkow@61640
   204
nipkow@61640
   205
nipkow@61640
   206
subsection "Functional correctness"
nipkow@61640
   207
nipkow@61640
   208
subsubsection \<open>Functional correctness of isin:\<close>
nipkow@61640
   209
nipkow@67929
   210
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))"
nipkow@67929
   211
by (induction t) (auto simp: isin_simps ball_Un)
nipkow@61640
   212
nipkow@61640
   213
nipkow@61640
   214
subsubsection \<open>Functional correctness of insert:\<close>
nipkow@61640
   215
nipkow@61640
   216
lemma inorder_ins:
nipkow@61640
   217
  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
nipkow@63636
   218
by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits)
nipkow@61640
   219
nipkow@61640
   220
lemma inorder_insert:
nipkow@61640
   221
  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
nipkow@61640
   222
by(simp add: insert_def inorder_ins)
nipkow@61640
   223
nipkow@61640
   224
nipkow@61640
   225
subsubsection \<open>Functional correctness of delete\<close>
nipkow@61640
   226
nipkow@61640
   227
lemma inorder_node21: "height r > 0 \<Longrightarrow>
nipkow@61640
   228
  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
nipkow@61640
   229
by(induct l' a r rule: node21.induct) auto
nipkow@61640
   230
nipkow@61640
   231
lemma inorder_node22: "height l > 0 \<Longrightarrow>
nipkow@61640
   232
  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
nipkow@61640
   233
by(induct l a r' rule: node22.induct) auto
nipkow@61640
   234
nipkow@61640
   235
lemma inorder_node31: "height m > 0 \<Longrightarrow>
nipkow@61640
   236
  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
nipkow@61640
   237
by(induct l' a m b r rule: node31.induct) auto
nipkow@61640
   238
nipkow@61640
   239
lemma inorder_node32: "height r > 0 \<Longrightarrow>
nipkow@61640
   240
  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
nipkow@61640
   241
by(induct l a m' b r rule: node32.induct) auto
nipkow@61640
   242
nipkow@61640
   243
lemma inorder_node33: "height m > 0 \<Longrightarrow>
nipkow@61640
   244
  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
nipkow@61640
   245
by(induct l a m b r' rule: node33.induct) auto
nipkow@61640
   246
nipkow@61640
   247
lemma inorder_node41: "height m > 0 \<Longrightarrow>
nipkow@61640
   248
  inorder (tree\<^sub>d (node41 l' a m b n c r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder n @ c # inorder r"
nipkow@61640
   249
by(induct l' a m b n c r rule: node41.induct) auto
nipkow@61640
   250
nipkow@61640
   251
lemma inorder_node42: "height l > 0 \<Longrightarrow>
nipkow@61640
   252
  inorder (tree\<^sub>d (node42 l a m b n c r)) = inorder l @ a # inorder (tree\<^sub>d m) @ b # inorder n @ c # inorder r"
nipkow@61640
   253
by(induct l a m b n c r rule: node42.induct) auto
nipkow@61640
   254
nipkow@61640
   255
lemma inorder_node43: "height m > 0 \<Longrightarrow>
nipkow@61640
   256
  inorder (tree\<^sub>d (node43 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder(tree\<^sub>d n) @ c # inorder r"
nipkow@61640
   257
by(induct l a m b n c r rule: node43.induct) auto
nipkow@61640
   258
nipkow@61640
   259
lemma inorder_node44: "height n > 0 \<Longrightarrow>
nipkow@61640
   260
  inorder (tree\<^sub>d (node44 l a m b n c r)) = inorder l @ a # inorder m @ b # inorder n @ c # inorder (tree\<^sub>d r)"
nipkow@61640
   261
by(induct l a m b n c r rule: node44.induct) auto
nipkow@61640
   262
nipkow@61640
   263
lemmas inorder_nodes = inorder_node21 inorder_node22
nipkow@61640
   264
  inorder_node31 inorder_node32 inorder_node33
nipkow@61640
   265
  inorder_node41 inorder_node42 inorder_node43 inorder_node44
nipkow@61640
   266
nipkow@68020
   267
lemma split_minD:
nipkow@68020
   268
  "split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
nipkow@61640
   269
  x # inorder(tree\<^sub>d t') = inorder t"
nipkow@68020
   270
by(induction t arbitrary: t' rule: split_min.induct)
nipkow@61640
   271
  (auto simp: inorder_nodes split: prod.splits)
nipkow@61640
   272
nipkow@61640
   273
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
nipkow@61640
   274
  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
nipkow@61640
   275
by(induction t rule: del.induct)
nipkow@68020
   276
  (auto simp: inorder_nodes del_list_simps split_minD split!: if_split prod.splits)
nipkow@63636
   277
  (* 30 secs (2016) *)
nipkow@61640
   278
nipkow@61640
   279
lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
nipkow@61640
   280
  inorder(delete x t) = del_list x (inorder t)"
nipkow@61640
   281
by(simp add: delete_def inorder_del)
nipkow@61640
   282
nipkow@61640
   283
nipkow@61640
   284
subsection \<open>Balancedness\<close>
nipkow@61640
   285
nipkow@61640
   286
subsubsection "Proofs for insert"
nipkow@61640
   287
wenzelm@67406
   288
text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close>
nipkow@61640
   289
nipkow@61640
   290
instantiation up\<^sub>i :: (type)height
nipkow@61640
   291
begin
nipkow@61640
   292
nipkow@61640
   293
fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
nipkow@61640
   294
"height (T\<^sub>i t) = height t" |
nipkow@61640
   295
"height (Up\<^sub>i l a r) = height l"
nipkow@61640
   296
nipkow@61640
   297
instance ..
nipkow@61640
   298
nipkow@61640
   299
end
nipkow@61640
   300
nipkow@61640
   301
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
nipkow@63636
   302
by (induct t) (auto split!: if_split up\<^sub>i.split)
nipkow@61640
   303
nipkow@61640
   304
wenzelm@67406
   305
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because
wenzelm@67406
   306
two properties (balance and height) are combined in one predicate.\<close>
nipkow@61640
   307
nipkow@61640
   308
inductive full :: "nat \<Rightarrow> 'a tree234 \<Rightarrow> bool" where
nipkow@61640
   309
"full 0 Leaf" |
nipkow@61640
   310
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
nipkow@61640
   311
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)" |
nipkow@61640
   312
"\<lbrakk>full n l; full n m; full n m'; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node4 l p m q m' q' r)"
nipkow@61640
   313
nipkow@61640
   314
inductive_cases full_elims:
nipkow@61640
   315
  "full n Leaf"
nipkow@61640
   316
  "full n (Node2 l p r)"
nipkow@61640
   317
  "full n (Node3 l p m q r)"
nipkow@61640
   318
  "full n (Node4 l p m q m' q' r)"
nipkow@61640
   319
nipkow@61640
   320
inductive_cases full_0_elim: "full 0 t"
nipkow@61640
   321
inductive_cases full_Suc_elim: "full (Suc n) t"
nipkow@61640
   322
nipkow@61640
   323
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
nipkow@61640
   324
  by (auto elim: full_0_elim intro: full.intros)
nipkow@61640
   325
nipkow@61640
   326
lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
nipkow@61640
   327
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   328
nipkow@61640
   329
lemma full_Suc_Node2_iff [simp]:
nipkow@61640
   330
  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
nipkow@61640
   331
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   332
nipkow@61640
   333
lemma full_Suc_Node3_iff [simp]:
nipkow@61640
   334
  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
nipkow@61640
   335
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   336
nipkow@61640
   337
lemma full_Suc_Node4_iff [simp]:
nipkow@61640
   338
  "full (Suc n) (Node4 l p m q m' q' r) \<longleftrightarrow> full n l \<and> full n m \<and> full n m' \<and> full n r"
nipkow@61640
   339
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   340
nipkow@61640
   341
lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
nipkow@61640
   342
  by (induct set: full, simp_all)
nipkow@61640
   343
nipkow@61640
   344
lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
nipkow@61640
   345
  by (induct set: full, auto dest: full_imp_height)
nipkow@61640
   346
nipkow@61640
   347
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
nipkow@61640
   348
  by (induct t, simp_all)
nipkow@61640
   349
nipkow@61640
   350
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
nipkow@61640
   351
  by (auto elim!: bal_imp_full full_imp_bal)
nipkow@61640
   352
wenzelm@67406
   353
text \<open>The @{const "insert"} function either preserves the height of the
nipkow@61640
   354
tree, or increases it by one. The constructor returned by the @{term
nipkow@61640
   355
"insert"} function determines which: A return value of the form @{term
nipkow@61640
   356
"T\<^sub>i t"} indicates that the height will be the same. A value of the
wenzelm@67406
   357
form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close>
nipkow@61640
   358
nipkow@61640
   359
primrec full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
nipkow@61640
   360
"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
nipkow@61640
   361
"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
nipkow@61640
   362
nipkow@61640
   363
lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
nipkow@61640
   364
by (induct rule: full.induct) (auto, auto split: up\<^sub>i.split)
nipkow@61640
   365
wenzelm@67406
   366
text \<open>The @{const insert} operation preserves balance.\<close>
nipkow@61640
   367
nipkow@61640
   368
lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
nipkow@61640
   369
unfolding bal_iff_full insert_def
nipkow@61640
   370
apply (erule exE)
nipkow@61640
   371
apply (drule full\<^sub>i_ins [of _ _ a])
nipkow@61640
   372
apply (cases "ins a t")
nipkow@61640
   373
apply (auto intro: full.intros)
nipkow@61640
   374
done
nipkow@61640
   375
nipkow@61640
   376
nipkow@61640
   377
subsubsection "Proofs for delete"
nipkow@61640
   378
nipkow@61640
   379
instantiation up\<^sub>d :: (type)height
nipkow@61640
   380
begin
nipkow@61640
   381
nipkow@61640
   382
fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
nipkow@61640
   383
"height (T\<^sub>d t) = height t" |
nipkow@61640
   384
"height (Up\<^sub>d t) = height t + 1"
nipkow@61640
   385
nipkow@61640
   386
instance ..
nipkow@61640
   387
nipkow@61640
   388
end
nipkow@61640
   389
nipkow@61640
   390
lemma bal_tree\<^sub>d_node21:
nipkow@61640
   391
  "\<lbrakk>bal r; bal (tree\<^sub>d l); height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l a r))"
nipkow@61640
   392
by(induct l a r rule: node21.induct) auto
nipkow@61640
   393
nipkow@61640
   394
lemma bal_tree\<^sub>d_node22:
nipkow@61640
   395
  "\<lbrakk>bal(tree\<^sub>d r); bal l; height r = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r))"
nipkow@61640
   396
by(induct l a r rule: node22.induct) auto
nipkow@61640
   397
nipkow@61640
   398
lemma bal_tree\<^sub>d_node31:
nipkow@61640
   399
  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal r; height l = height r; height m = height r \<rbrakk>
nipkow@61640
   400
  \<Longrightarrow> bal (tree\<^sub>d (node31 l a m b r))"
nipkow@61640
   401
by(induct l a m b r rule: node31.induct) auto
nipkow@61640
   402
nipkow@61640
   403
lemma bal_tree\<^sub>d_node32:
nipkow@61640
   404
  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal r; height l = height r; height m = height r \<rbrakk>
nipkow@61640
   405
  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m b r))"
nipkow@61640
   406
by(induct l a m b r rule: node32.induct) auto
nipkow@61640
   407
nipkow@61640
   408
lemma bal_tree\<^sub>d_node33:
nipkow@61640
   409
  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r); height l = height r; height m = height r \<rbrakk>
nipkow@61640
   410
  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r))"
nipkow@61640
   411
by(induct l a m b r rule: node33.induct) auto
nipkow@61640
   412
nipkow@61640
   413
lemma bal_tree\<^sub>d_node41:
nipkow@61640
   414
  "\<lbrakk> bal (tree\<^sub>d l); bal m; bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
nipkow@61640
   415
  \<Longrightarrow> bal (tree\<^sub>d (node41 l a m b n c r))"
nipkow@61640
   416
by(induct l a m b n c r rule: node41.induct) auto
nipkow@61640
   417
nipkow@61640
   418
lemma bal_tree\<^sub>d_node42:
nipkow@61640
   419
  "\<lbrakk> bal l; bal (tree\<^sub>d m); bal n; bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
nipkow@61640
   420
  \<Longrightarrow> bal (tree\<^sub>d (node42 l a m b n c r))"
nipkow@61640
   421
by(induct l a m b n c r rule: node42.induct) auto
nipkow@61640
   422
nipkow@61640
   423
lemma bal_tree\<^sub>d_node43:
nipkow@61640
   424
  "\<lbrakk> bal l; bal m; bal (tree\<^sub>d n); bal r; height l = height r; height m = height r; height n = height r \<rbrakk>
nipkow@61640
   425
  \<Longrightarrow> bal (tree\<^sub>d (node43 l a m b n c r))"
nipkow@61640
   426
by(induct l a m b n c r rule: node43.induct) auto
nipkow@61640
   427
nipkow@61640
   428
lemma bal_tree\<^sub>d_node44:
nipkow@61640
   429
  "\<lbrakk> bal l; bal m; bal n; bal (tree\<^sub>d r); height l = height r; height m = height r; height n = height r \<rbrakk>
nipkow@61640
   430
  \<Longrightarrow> bal (tree\<^sub>d (node44 l a m b n c r))"
nipkow@61640
   431
by(induct l a m b n c r rule: node44.induct) auto
nipkow@61640
   432
nipkow@61640
   433
lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
nipkow@61640
   434
  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
nipkow@61640
   435
  bal_tree\<^sub>d_node41 bal_tree\<^sub>d_node42 bal_tree\<^sub>d_node43 bal_tree\<^sub>d_node44
nipkow@61640
   436
nipkow@61640
   437
lemma height_node21:
nipkow@61640
   438
   "height r > 0 \<Longrightarrow> height(node21 l a r) = max (height l) (height r) + 1"
nipkow@61640
   439
by(induct l a r rule: node21.induct)(simp_all add: max.assoc)
nipkow@61640
   440
nipkow@61640
   441
lemma height_node22:
nipkow@61640
   442
   "height l > 0 \<Longrightarrow> height(node22 l a r) = max (height l) (height r) + 1"
nipkow@61640
   443
by(induct l a r rule: node22.induct)(simp_all add: max.assoc)
nipkow@61640
   444
nipkow@61640
   445
lemma height_node31:
nipkow@61640
   446
  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
nipkow@61640
   447
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   448
by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
nipkow@61640
   449
nipkow@61640
   450
lemma height_node32:
nipkow@61640
   451
  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
nipkow@61640
   452
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   453
by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
nipkow@61640
   454
nipkow@61640
   455
lemma height_node33:
nipkow@61640
   456
  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
nipkow@61640
   457
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   458
by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
nipkow@61640
   459
nipkow@61640
   460
lemma height_node41:
nipkow@61640
   461
  "height m > 0 \<Longrightarrow> height(node41 l a m b n c r) =
nipkow@61640
   462
   max (height l) (max (height m) (max (height n) (height r))) + 1"
nipkow@61640
   463
by(induct l a m b n c r rule: node41.induct)(simp_all add: max_def)
nipkow@61640
   464
nipkow@61640
   465
lemma height_node42:
nipkow@61640
   466
  "height l > 0 \<Longrightarrow> height(node42 l a m b n c r) =
nipkow@61640
   467
   max (height l) (max (height m) (max (height n) (height r))) + 1"
nipkow@61640
   468
by(induct l a m b n c r rule: node42.induct)(simp_all add: max_def)
nipkow@61640
   469
nipkow@61640
   470
lemma height_node43:
nipkow@61640
   471
  "height m > 0 \<Longrightarrow> height(node43 l a m b n c r) =
nipkow@61640
   472
   max (height l) (max (height m) (max (height n) (height r))) + 1"
nipkow@61640
   473
by(induct l a m b n c r rule: node43.induct)(simp_all add: max_def)
nipkow@61640
   474
nipkow@61640
   475
lemma height_node44:
nipkow@61640
   476
  "height n > 0 \<Longrightarrow> height(node44 l a m b n c r) =
nipkow@61640
   477
   max (height l) (max (height m) (max (height n) (height r))) + 1"
nipkow@61640
   478
by(induct l a m b n c r rule: node44.induct)(simp_all add: max_def)
nipkow@61640
   479
nipkow@61640
   480
lemmas heights = height_node21 height_node22
nipkow@61640
   481
  height_node31 height_node32 height_node33
nipkow@61640
   482
  height_node41 height_node42 height_node43 height_node44
nipkow@61640
   483
nipkow@68020
   484
lemma height_split_min:
nipkow@68020
   485
  "split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
nipkow@68020
   486
by(induct t arbitrary: x t' rule: split_min.induct)
nipkow@61640
   487
  (auto simp: heights split: prod.splits)
nipkow@61640
   488
nipkow@61640
   489
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
nipkow@61640
   490
by(induction x t rule: del.induct)
nipkow@68020
   491
  (auto simp add: heights height_split_min split!: if_split prod.split)
nipkow@61640
   492
nipkow@68020
   493
lemma bal_split_min:
nipkow@68020
   494
  "\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
nipkow@68020
   495
by(induct t arbitrary: x t' rule: split_min.induct)
nipkow@68020
   496
  (auto simp: heights height_split_min bals split: prod.splits)
nipkow@61640
   497
nipkow@61640
   498
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
nipkow@61640
   499
by(induction x t rule: del.induct)
nipkow@68020
   500
  (auto simp: bals bal_split_min height_del height_split_min split!: if_split prod.split)
nipkow@61640
   501
nipkow@61640
   502
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
nipkow@61640
   503
by(simp add: delete_def bal_tree\<^sub>d_del)
nipkow@61640
   504
nipkow@61640
   505
subsection \<open>Overall Correctness\<close>
nipkow@61640
   506
nipkow@68440
   507
interpretation S: Set_by_Ordered
nipkow@68431
   508
where empty = empty and isin = isin and insert = insert and delete = delete
nipkow@61640
   509
and inorder = inorder and inv = bal
nipkow@61640
   510
proof (standard, goal_cases)
nipkow@61640
   511
  case 2 thus ?case by(simp add: isin_set)
nipkow@61640
   512
next
nipkow@61640
   513
  case 3 thus ?case by(simp add: inorder_insert)
nipkow@61640
   514
next
nipkow@61640
   515
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@61640
   516
next
nipkow@61640
   517
  case 6 thus ?case by(simp add: bal_insert)
nipkow@61640
   518
next
nipkow@61640
   519
  case 7 thus ?case by(simp add: bal_delete)
nipkow@68431
   520
qed (simp add: empty_def)+
nipkow@61640
   521
nipkow@61640
   522
end