src/HOL/ex/Tree23.thy
author huffman
Thu Nov 03 17:40:50 2011 +0100 (2011-11-03)
changeset 45332 ede9dc025150
parent 45325 26b6179b5a45
child 45333 04b21922ed68
permissions -rw-r--r--
ex/Tree23.thy: prove that deletion preserves balance
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
huffman@45325
   162
definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
huffman@45325
   163
  "opt_less x y = (case x of None \<Rightarrow> True | Some a \<Rightarrow> (case y of None \<Rightarrow> True | Some b \<Rightarrow> a < b))"
huffman@45325
   164
huffman@45325
   165
lemma opt_less_simps [simp]:
huffman@45325
   166
  "opt_less None y = True"
huffman@45325
   167
  "opt_less x None = True"
huffman@45325
   168
  "opt_less (Some a) (Some b) = (a < b)"
huffman@45325
   169
unfolding opt_less_def by (auto simp add: ord_def split: option.split)
huffman@45325
   170
huffman@45325
   171
fun ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
huffman@45325
   172
"ord' x Empty y = opt_less x y" |
huffman@45325
   173
"ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
huffman@45325
   174
"ord' x (Branch3 l p m q r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) m (Some (fst q)) & ord' (Some (fst q)) r y)"
huffman@45325
   175
huffman@45325
   176
lemma ord':
huffman@45325
   177
  "ord' x t y = (case x of None \<Rightarrow> (case y of None \<Rightarrow> ord0 t | Some y' \<Rightarrow> ordr t y')
huffman@45325
   178
    | Some x' \<Rightarrow> (case y of None \<Rightarrow> ordl x' t | Some y' \<Rightarrow> ordlr x' t y'))"
huffman@45325
   179
by (induct t arbitrary: x y, auto simp add: opt_less_def split: option.split)
huffman@45325
   180
nipkow@33436
   181
fun height :: "'a tree23 \<Rightarrow> nat" where
nipkow@33436
   182
"height Empty = 0" |
nipkow@33436
   183
"height (Branch2 l _ r) = Suc(max (height l) (height r))" |
nipkow@33436
   184
"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
nipkow@33436
   185
nipkow@33436
   186
text{* Is a tree balanced? *}
nipkow@33436
   187
fun bal :: "'a tree23 \<Rightarrow> bool" where
nipkow@33436
   188
"bal Empty = True" |
nipkow@33436
   189
"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
nipkow@33436
   190
"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
nipkow@33436
   191
huffman@45325
   192
text {* The @{term "add0"} function either preserves the height of the
huffman@45325
   193
tree, or increases it by one. The constructor returned by the @{term
huffman@45325
   194
"add"} function determines which: A return value of the form @{term
huffman@45325
   195
"Stay t"} indicates that the height will be the same. A value of the
huffman@45325
   196
form @{term "Sprout l p r"} indicates an increase in height. *}
huffman@45325
   197
huffman@45325
   198
fun gheight :: "'a growth \<Rightarrow> nat" where
huffman@45325
   199
"gheight (Stay t) = height t" |
huffman@45325
   200
"gheight (Sprout l p r) = max (height l) (height r)"
huffman@45325
   201
huffman@45325
   202
lemma gheight_add: "gheight (add k y t) = height t"
huffman@45325
   203
 apply (induct t)
huffman@45325
   204
   apply simp
huffman@45325
   205
  apply clarsimp
huffman@45325
   206
  apply (case_tac "ord k a")
huffman@45325
   207
    apply simp
huffman@45325
   208
    apply (case_tac "add k y t1", simp, simp)
huffman@45325
   209
   apply simp
huffman@45325
   210
  apply simp
huffman@45325
   211
  apply (case_tac "add k y t2", simp, simp)
huffman@45325
   212
 apply clarsimp
huffman@45325
   213
 apply (case_tac "ord k a")
huffman@45325
   214
   apply simp
huffman@45325
   215
   apply (case_tac "add k y t1", simp, simp)
huffman@45325
   216
  apply simp
huffman@45325
   217
 apply simp
huffman@45325
   218
 apply (case_tac "ord k aa")
huffman@45325
   219
   apply simp
huffman@45325
   220
   apply (case_tac "add k y t2", simp, simp)
huffman@45325
   221
  apply simp
huffman@45325
   222
 apply simp
huffman@45325
   223
 apply (case_tac "add k y t3", simp, simp)
huffman@45325
   224
done
huffman@45325
   225
huffman@45325
   226
lemma add_eq_Stay_dest: "add k y t = Stay t' \<Longrightarrow> height t = height t'"
huffman@45325
   227
  using gheight_add [of k y t] by simp
huffman@45325
   228
huffman@45325
   229
lemma add_eq_Sprout_dest: "add k y t = Sprout l p r \<Longrightarrow> height t = max (height l) (height r)"
huffman@45325
   230
  using gheight_add [of k y t] by simp
huffman@45325
   231
huffman@45325
   232
definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
huffman@45325
   233
  "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
huffman@45325
   234
huffman@45325
   235
lemma gtree_simps [simp]:
huffman@45325
   236
  "gtree (Stay t) = t"
huffman@45325
   237
  "gtree (Sprout l p r) = Branch2 l p r"
huffman@45325
   238
unfolding gtree_def by simp_all
huffman@45325
   239
huffman@45325
   240
lemma add0: "add0 k y t = gtree (add k y t)"
huffman@45325
   241
  unfolding add0_def by (simp split: growth.split)
huffman@45325
   242
huffman@45325
   243
text {* The @{term "add0"} operation preserves balance. *}
huffman@45325
   244
huffman@45325
   245
lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
huffman@45325
   246
unfolding add0
huffman@45325
   247
 apply (induct t)
huffman@45325
   248
   apply simp
huffman@45325
   249
  apply clarsimp
huffman@45325
   250
  apply (case_tac "ord k a")
huffman@45325
   251
    apply simp
huffman@45325
   252
    apply (case_tac "add k y t1")
huffman@45325
   253
     apply (simp, drule add_eq_Stay_dest, simp)
huffman@45325
   254
    apply (simp, drule add_eq_Sprout_dest, simp)
huffman@45325
   255
   apply simp
huffman@45325
   256
  apply simp
huffman@45325
   257
  apply (case_tac "add k y t2")
huffman@45325
   258
   apply (simp, drule add_eq_Stay_dest, simp)
huffman@45325
   259
  apply (simp, drule add_eq_Sprout_dest, simp)
huffman@45325
   260
 apply clarsimp
huffman@45325
   261
 apply (case_tac "ord k a")
huffman@45325
   262
   apply simp
huffman@45325
   263
   apply (case_tac "add k y t1")
huffman@45325
   264
    apply (simp, drule add_eq_Stay_dest, simp)
huffman@45325
   265
   apply (simp, drule add_eq_Sprout_dest, simp)
huffman@45325
   266
  apply simp
huffman@45325
   267
 apply simp
huffman@45325
   268
 apply (case_tac "ord k aa")
huffman@45325
   269
   apply simp
huffman@45325
   270
   apply (case_tac "add k y t2")
huffman@45325
   271
    apply (simp, drule add_eq_Stay_dest, simp)
huffman@45325
   272
   apply (simp, drule add_eq_Sprout_dest, simp)
huffman@45325
   273
  apply simp
huffman@45325
   274
 apply simp
huffman@45325
   275
 apply (case_tac "add k y t3")
huffman@45325
   276
  apply (simp, drule add_eq_Stay_dest, simp)
huffman@45325
   277
 apply (simp, drule add_eq_Sprout_dest, simp)
huffman@45325
   278
done
huffman@45325
   279
huffman@45325
   280
text {* The @{term "add0"} operation preserves order. *}
huffman@45325
   281
huffman@45325
   282
lemma ord_cases:
huffman@45325
   283
  fixes a b :: int obtains
huffman@45325
   284
  "ord a b = LESS" and "a < b" |
huffman@45325
   285
  "ord a b = EQUAL" and "a = b" |
huffman@45325
   286
  "ord a b = GREATER" and "a > b"
huffman@45325
   287
unfolding ord_def by (rule linorder_cases [of a b]) auto
huffman@45325
   288
huffman@45325
   289
lemma ord'_add0:
huffman@45325
   290
  "\<lbrakk>ord' k1 t k2; opt_less k1 (Some k); opt_less (Some k) k2\<rbrakk> \<Longrightarrow> ord' k1 (add0 k y t) k2"
huffman@45325
   291
unfolding add0
huffman@45325
   292
 apply (induct t arbitrary: k1 k2)
huffman@45325
   293
   apply simp
huffman@45325
   294
  apply clarsimp
huffman@45325
   295
  apply (rule_tac a=k and b=a in ord_cases)
huffman@45325
   296
    apply simp
huffman@45325
   297
    apply (case_tac "add k y t1", simp, simp)
huffman@45325
   298
   apply simp
huffman@45325
   299
  apply simp
huffman@45325
   300
  apply (case_tac "add k y t2", simp, simp)
huffman@45325
   301
 apply clarsimp
huffman@45325
   302
 apply (rule_tac a=k and b=a in ord_cases)
huffman@45325
   303
   apply simp
huffman@45325
   304
   apply (case_tac "add k y t1", simp, simp)
huffman@45325
   305
  apply simp
huffman@45325
   306
 apply simp
huffman@45325
   307
 apply (rule_tac a=k and b=aa in ord_cases)
huffman@45325
   308
   apply simp
huffman@45325
   309
   apply (case_tac "add k y t2", simp, simp)
huffman@45325
   310
  apply simp
huffman@45325
   311
 apply simp
huffman@45325
   312
 apply (case_tac "add k y t3", simp, simp)
huffman@45325
   313
done
huffman@45325
   314
huffman@45325
   315
lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
huffman@45325
   316
using ord'_add0 [of None t None k y] by (simp add: ord')
huffman@45325
   317
huffman@45332
   318
text {* The @{term "del"} function preserves balance. *}
huffman@45332
   319
huffman@45332
   320
lemma del_extra_simps:
huffman@45332
   321
"l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
huffman@45332
   322
 del k (Branch2 l p r) = (case compare k p of
huffman@45332
   323
      LESS => (case del k l of None \<Rightarrow> None |
huffman@45332
   324
        Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
huffman@45332
   325
      | Some(p', (True, l')) => Some(p', case r of
huffman@45332
   326
          Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
huffman@45332
   327
        | Branch3 rl rp rm rq rr => (False, Branch2
huffman@45332
   328
            (Branch2 l' p rl) rp (Branch2 rm rq rr))))
huffman@45332
   329
    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
huffman@45332
   330
        Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
huffman@45332
   331
      | Some(p', (True, r')) => Some(p', case l of
huffman@45332
   332
          Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
huffman@45332
   333
        | Branch3 ll lp lm lq lr => (False, Branch2
huffman@45332
   334
            (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
huffman@45332
   335
"l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
huffman@45332
   336
 del k (Branch3 l p m q r) = (case compare k q of
huffman@45332
   337
      LESS => (case compare k p of
huffman@45332
   338
        LESS => (case del k l of None \<Rightarrow> None |
huffman@45332
   339
          Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
huffman@45332
   340
        | Some(p', (True, l')) => Some(p', (False, case (m, r) of
huffman@45332
   341
            (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
huffman@45332
   342
          | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
huffman@45332
   343
          | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
huffman@45332
   344
              Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
huffman@45332
   345
      | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
huffman@45332
   346
          Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
huffman@45332
   347
        | Some(p', (True, m')) => Some(p', (False, case (l, r) of
huffman@45332
   348
            (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
huffman@45332
   349
          | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
huffman@45332
   350
          | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
huffman@45332
   351
    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
huffman@45332
   352
        Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
huffman@45332
   353
      | Some(q', (True, r')) => Some(q', (False, case (l, m) of
huffman@45332
   354
          (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
huffman@45332
   355
        | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
huffman@45332
   356
        | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
huffman@45332
   357
            Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
huffman@45332
   358
apply -
huffman@45332
   359
apply (cases l, cases r, simp_all only: del.simps, simp)
huffman@45332
   360
apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
huffman@45332
   361
done
huffman@45332
   362
huffman@45332
   363
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
huffman@45332
   364
"full 0 Empty" |
huffman@45332
   365
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
huffman@45332
   366
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
huffman@45332
   367
huffman@45332
   368
inductive_cases full_elims:
huffman@45332
   369
  "full n Empty"
huffman@45332
   370
  "full n (Branch2 l p r)"
huffman@45332
   371
  "full n (Branch3 l p m q r)"
huffman@45332
   372
huffman@45332
   373
inductive_cases full_0_elim: "full 0 t"
huffman@45332
   374
inductive_cases full_Suc_elim: "full (Suc n) t"
huffman@45332
   375
huffman@45332
   376
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
huffman@45332
   377
  by (auto elim: full_0_elim intro: full.intros)
huffman@45332
   378
huffman@45332
   379
lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
huffman@45332
   380
  by (auto elim: full_elims intro: full.intros)
huffman@45332
   381
huffman@45332
   382
lemma full_Suc_Branch2_iff [simp]:
huffman@45332
   383
  "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
huffman@45332
   384
  by (auto elim: full_elims intro: full.intros)
huffman@45332
   385
huffman@45332
   386
lemma full_Suc_Branch3_iff [simp]:
huffman@45332
   387
  "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
huffman@45332
   388
  by (auto elim: full_elims intro: full.intros)
huffman@45332
   389
huffman@45332
   390
definition
huffman@45332
   391
  "full_del n k t = (case del k t of None \<Rightarrow> True | Some (p, b, t') \<Rightarrow> full (if b then n else Suc n) t')"
huffman@45332
   392
huffman@45332
   393
lemmas ord_case = ord.exhaust [where y=y and P="ord_case a b c y", standard]
huffman@45332
   394
lemmas option_ord_case = ord.exhaust [where y=y and P="option_case a b (ord_case d e f y)", standard]
huffman@45332
   395
lemmas option_option_case = option.exhaust [where y=y and P="option_case a b (option_case d e y)", standard]
huffman@45332
   396
lemmas option_prod_case = prod.exhaust [where y=y and P="option_case a b (prod_case c y)", standard]
huffman@45332
   397
lemmas option_bool_case = bool.exhaust [where y=y and P="option_case a b (bool_case c d y)", standard]
huffman@45332
   398
lemmas prod_tree23_case = tree23.exhaust [where y=y and P="prod_case a (tree23_case b c d y)", standard]
huffman@45332
   399
lemmas option_case = option.exhaust [where y=y and P="option_case a b y", standard]
huffman@45332
   400
lemmas full_tree23_case = tree23.exhaust [where y=y and P="full a (tree23_case b c d y)", standard]
huffman@45332
   401
huffman@45332
   402
lemmas case_intros =
huffman@45332
   403
  option_ord_case option_option_case option_prod_case option_bool_case prod_tree23_case option_case
huffman@45332
   404
  full_tree23_case
huffman@45332
   405
huffman@45332
   406
lemma full_del: "full (Suc n) t \<Longrightarrow> full_del n k t"
huffman@45332
   407
proof -
huffman@45332
   408
  { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
huffman@45332
   409
    assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
huffman@45332
   410
    and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
huffman@45332
   411
    and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
huffman@45332
   412
    and "full (Suc n) (Branch2 l p r)"
huffman@45332
   413
    hence "full_del n k (Branch2 l p r)"
huffman@45332
   414
     apply clarsimp
huffman@45332
   415
     apply (cases n)
huffman@45332
   416
      apply (cases k)
huffman@45332
   417
       apply (simp add: full_del_def)
huffman@45332
   418
      apply (simp add: full_del_def split: ord.split)
huffman@45332
   419
     apply (simp add: full_del_def)
huffman@45332
   420
     apply (subst del_extra_simps, force)
huffman@45332
   421
     apply (simp | rule case_intros)+
huffman@45332
   422
     done
huffman@45332
   423
  } note A = this
huffman@45332
   424
  { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
huffman@45332
   425
    assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> full_del n k l"
huffman@45332
   426
    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) m"
huffman@45332
   427
    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) m"
huffman@45332
   428
    and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq EQUAL None k) r"
huffman@45332
   429
    and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> full_del n (if_eq GREATER None k) r"
huffman@45332
   430
    and "full (Suc n) (Branch3 l p m q r)"
huffman@45332
   431
    hence "full_del n k (Branch3 l p m q r)"
huffman@45332
   432
     apply clarsimp
huffman@45332
   433
     apply (cases n)
huffman@45332
   434
      apply (cases k)
huffman@45332
   435
       apply (simp add: full_del_def)
huffman@45332
   436
      apply (simp add: full_del_def split: ord.split)
huffman@45332
   437
     apply (simp add: full_del_def)
huffman@45332
   438
     apply (subst del_extra_simps, force)
huffman@45332
   439
     apply (simp | rule case_intros)+
huffman@45332
   440
     done
huffman@45332
   441
  } note B = this
huffman@45332
   442
  show "full (Suc n) t \<Longrightarrow> full_del n k t"
huffman@45332
   443
  proof (induct k t arbitrary: n rule: del.induct)
huffman@45332
   444
    { case goal1 thus "full_del n (Some k) Empty"
huffman@45332
   445
        by simp }
huffman@45332
   446
    { case goal2 thus "full_del n None (Branch2 Empty p Empty)"
huffman@45332
   447
        unfolding full_del_def by auto }
huffman@45332
   448
    { case goal3 thus "full_del n None (Branch3 Empty p Empty q Empty)"
huffman@45332
   449
        unfolding full_del_def by auto }
huffman@45332
   450
    { case goal4 thus "full_del n (Some v) (Branch2 Empty p Empty)"
huffman@45332
   451
        unfolding full_del_def by (auto split: ord.split) }
huffman@45332
   452
    { case goal5 thus "full_del n (Some v) (Branch3 Empty p Empty q Empty)"
huffman@45332
   453
        unfolding full_del_def by (auto split: ord.split) }
huffman@45332
   454
    { case goal26 thus ?case by simp }
huffman@45332
   455
  qed (fact A | fact B)+
huffman@45332
   456
qed
huffman@45332
   457
huffman@45332
   458
lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
huffman@45332
   459
  by (induct set: full, simp_all)
huffman@45332
   460
huffman@45332
   461
lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
huffman@45332
   462
  by (induct set: full, auto dest: full_imp_height)
huffman@45332
   463
huffman@45332
   464
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
huffman@45332
   465
  by (induct t, simp_all)
huffman@45332
   466
huffman@45332
   467
lemma bal_iff_full: "bal t \<longleftrightarrow> full (height t) t"
huffman@45332
   468
  using bal_imp_full full_imp_bal ..
huffman@45332
   469
huffman@45332
   470
lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
huffman@45332
   471
  unfolding del0_def
huffman@45332
   472
  apply (drule bal_imp_full)
huffman@45332
   473
  apply (case_tac "height t", simp, simp)
huffman@45332
   474
  apply (frule full_del [where k="Some k"])
huffman@45332
   475
  apply (simp add: full_del_def)
huffman@45332
   476
  apply (auto split: option.split elim: full_imp_bal)
huffman@45332
   477
  done
huffman@45332
   478
nipkow@33436
   479
text{* This is a little test harness and should be commented out once the
nipkow@33436
   480
above functions have been proved correct. *}
nipkow@33436
   481
nipkow@33436
   482
datatype 'a act = Add int 'a | Del int
nipkow@33436
   483
nipkow@33436
   484
fun exec where
nipkow@33436
   485
"exec [] t = t" |
nipkow@33436
   486
"exec (Add k x # as) t = exec as (add0 k x t)" |
nipkow@33436
   487
"exec (Del k # as) t = exec as (del0 k t)"
nipkow@33436
   488
nipkow@33436
   489
text{* Some quick checks: *}
nipkow@33436
   490
huffman@45332
   491
lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
huffman@45332
   492
  by (induct as t arbitrary: t rule: exec.induct,
huffman@45332
   493
    simp_all add: bal_add0 bal_del0)
huffman@45332
   494
huffman@45332
   495
lemma "bal(exec as Empty)"
huffman@45332
   496
  by (simp add: bal_exec)
huffman@45332
   497
nipkow@33436
   498
lemma "ord0(exec as Empty)"
nipkow@33436
   499
quickcheck
nipkow@33436
   500
oops
nipkow@33436
   501
huffman@45332
   502
end