src/HOL/ex/Tree23.thy
author wenzelm
Wed Jun 22 10:09:20 2016 +0200 (2016-06-22)
changeset 63343 fb5d8a50c641
parent 61933 cf58b5b794b2
child 69597 ff784d5a5bfb
permissions -rw-r--r--
bundle lifting_syntax;
nipkow@33436
     1
(*  Title:      HOL/ex/Tree23.thy
nipkow@33436
     2
    Author:     Tobias Nipkow, TU Muenchen
nipkow@33436
     3
*)
nipkow@33436
     4
wenzelm@61343
     5
section \<open>2-3 Trees\<close>
nipkow@33436
     6
nipkow@33436
     7
theory Tree23
nipkow@33436
     8
imports Main
nipkow@33436
     9
begin
nipkow@33436
    10
wenzelm@61343
    11
text\<open>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
wenzelm@61343
    20
for the function definition facility.\<close>
nipkow@33436
    21
wenzelm@61933
    22
type_synonym key = int \<comment> \<open>for simplicity, should be a type class\<close>
nipkow@33436
    23
blanchet@58310
    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
blanchet@58310
    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
blanchet@58310
    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
wenzelm@61343
   139
text \<open>Ordered trees\<close>
nipkow@33436
   140
huffman@45325
   141
definition opt_less :: "key option \<Rightarrow> key option \<Rightarrow> bool" where
huffman@45325
   142
  "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
   143
huffman@45325
   144
lemma opt_less_simps [simp]:
huffman@45325
   145
  "opt_less None y = True"
huffman@45325
   146
  "opt_less x None = True"
huffman@45325
   147
  "opt_less (Some a) (Some b) = (a < b)"
huffman@45325
   148
unfolding opt_less_def by (auto simp add: ord_def split: option.split)
huffman@45325
   149
huffman@45333
   150
primrec ord' :: "key option \<Rightarrow> 'a tree23 \<Rightarrow> key option \<Rightarrow> bool" where
huffman@45325
   151
"ord' x Empty y = opt_less x y" |
huffman@45325
   152
"ord' x (Branch2 l p r) y = (ord' x l (Some (fst p)) & ord' (Some (fst p)) r y)" |
huffman@45325
   153
"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
   154
huffman@45333
   155
definition ord0 :: "'a tree23 \<Rightarrow> bool" where
huffman@45333
   156
  "ord0 t = ord' None t None"
huffman@45325
   157
wenzelm@61343
   158
text \<open>Balanced trees\<close>
huffman@45334
   159
huffman@45334
   160
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
huffman@45334
   161
"full 0 Empty" |
huffman@45334
   162
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch2 l p r)" |
huffman@45334
   163
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Branch3 l p m q r)"
huffman@45334
   164
huffman@45334
   165
inductive_cases full_elims:
huffman@45334
   166
  "full n Empty"
huffman@45334
   167
  "full n (Branch2 l p r)"
huffman@45334
   168
  "full n (Branch3 l p m q r)"
huffman@45334
   169
huffman@45334
   170
inductive_cases full_0_elim: "full 0 t"
huffman@45334
   171
inductive_cases full_Suc_elim: "full (Suc n) t"
huffman@45334
   172
huffman@45334
   173
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Empty"
huffman@45334
   174
  by (auto elim: full_0_elim intro: full.intros)
huffman@45334
   175
huffman@45334
   176
lemma full_Empty_iff [simp]: "full n Empty \<longleftrightarrow> n = 0"
huffman@45334
   177
  by (auto elim: full_elims intro: full.intros)
huffman@45334
   178
huffman@45334
   179
lemma full_Suc_Branch2_iff [simp]:
huffman@45334
   180
  "full (Suc n) (Branch2 l p r) \<longleftrightarrow> full n l \<and> full n r"
huffman@45334
   181
  by (auto elim: full_elims intro: full.intros)
huffman@45334
   182
huffman@45334
   183
lemma full_Suc_Branch3_iff [simp]:
huffman@45334
   184
  "full (Suc n) (Branch3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
huffman@45334
   185
  by (auto elim: full_elims intro: full.intros)
huffman@45334
   186
nipkow@33436
   187
fun height :: "'a tree23 \<Rightarrow> nat" where
nipkow@33436
   188
"height Empty = 0" |
nipkow@33436
   189
"height (Branch2 l _ r) = Suc(max (height l) (height r))" |
nipkow@33436
   190
"height (Branch3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
nipkow@33436
   191
wenzelm@61343
   192
text\<open>Is a tree balanced?\<close>
nipkow@33436
   193
fun bal :: "'a tree23 \<Rightarrow> bool" where
nipkow@33436
   194
"bal Empty = True" |
nipkow@33436
   195
"bal (Branch2 l _ r) = (bal l & bal r & height l = height r)" |
nipkow@33436
   196
"bal (Branch3 l _ m _ r) = (bal l & bal m & bal r & height l = height m & height m = height r)"
nipkow@33436
   197
huffman@45334
   198
lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
huffman@45334
   199
  by (induct set: full, simp_all)
huffman@45334
   200
huffman@45334
   201
lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
huffman@45334
   202
  by (induct set: full, auto dest: full_imp_height)
huffman@45334
   203
huffman@45334
   204
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
huffman@45334
   205
  by (induct t, simp_all)
huffman@45334
   206
huffman@45334
   207
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
huffman@45334
   208
  by (auto elim!: bal_imp_full full_imp_bal)
huffman@45334
   209
wenzelm@61343
   210
text \<open>The @{term "add0"} function either preserves the height of the
huffman@45325
   211
tree, or increases it by one. The constructor returned by the @{term
huffman@45325
   212
"add"} function determines which: A return value of the form @{term
huffman@45325
   213
"Stay t"} indicates that the height will be the same. A value of the
wenzelm@61343
   214
form @{term "Sprout l p r"} indicates an increase in height.\<close>
huffman@45325
   215
huffman@45334
   216
primrec gfull :: "nat \<Rightarrow> 'a growth \<Rightarrow> bool" where
huffman@45334
   217
"gfull n (Stay t) \<longleftrightarrow> full n t" |
huffman@45334
   218
"gfull n (Sprout l p r) \<longleftrightarrow> full n l \<and> full n r"
huffman@45325
   219
huffman@45334
   220
lemma gfull_add: "full n t \<Longrightarrow> gfull n (add k y t)"
huffman@45336
   221
by (induct set: full, auto split: ord.split growth.split)
huffman@45325
   222
wenzelm@61343
   223
text \<open>The @{term "add0"} operation preserves balance.\<close>
huffman@45325
   224
huffman@45334
   225
lemma bal_add0: "bal t \<Longrightarrow> bal (add0 k y t)"
huffman@45334
   226
unfolding bal_iff_full add0_def
huffman@45334
   227
apply (erule exE)
huffman@45334
   228
apply (drule gfull_add [of _ _ k y])
huffman@45334
   229
apply (cases "add k y t")
huffman@45334
   230
apply (auto intro: full.intros)
huffman@45334
   231
done
huffman@45334
   232
wenzelm@61343
   233
text \<open>The @{term "add0"} operation preserves order.\<close>
huffman@45334
   234
huffman@45334
   235
lemma ord_cases:
huffman@45334
   236
  fixes a b :: int obtains
huffman@45334
   237
  "ord a b = LESS" and "a < b" |
huffman@45334
   238
  "ord a b = EQUAL" and "a = b" |
huffman@45334
   239
  "ord a b = GREATER" and "a > b"
huffman@45334
   240
unfolding ord_def by (rule linorder_cases [of a b]) auto
huffman@45325
   241
huffman@45325
   242
definition gtree :: "'a growth \<Rightarrow> 'a tree23" where
huffman@45325
   243
  "gtree g = (case g of Stay t \<Rightarrow> t | Sprout l p r \<Rightarrow> Branch2 l p r)"
huffman@45325
   244
huffman@45325
   245
lemma gtree_simps [simp]:
huffman@45325
   246
  "gtree (Stay t) = t"
huffman@45325
   247
  "gtree (Sprout l p r) = Branch2 l p r"
huffman@45325
   248
unfolding gtree_def by simp_all
huffman@45325
   249
huffman@45325
   250
lemma add0: "add0 k y t = gtree (add k y t)"
huffman@45325
   251
  unfolding add0_def by (simp split: growth.split)
huffman@45325
   252
huffman@45325
   253
lemma ord'_add0:
huffman@45325
   254
  "\<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
   255
unfolding add0
huffman@45325
   256
 apply (induct t arbitrary: k1 k2)
huffman@45325
   257
   apply simp
huffman@45325
   258
  apply clarsimp
huffman@45325
   259
  apply (rule_tac a=k and b=a in ord_cases)
huffman@45325
   260
    apply simp
huffman@45325
   261
    apply (case_tac "add k y t1", simp, simp)
huffman@45325
   262
   apply simp
huffman@45325
   263
  apply simp
huffman@45325
   264
  apply (case_tac "add k y t2", simp, simp)
huffman@45325
   265
 apply clarsimp
huffman@45325
   266
 apply (rule_tac a=k and b=a in ord_cases)
huffman@45325
   267
   apply simp
huffman@45325
   268
   apply (case_tac "add k y t1", simp, simp)
huffman@45325
   269
  apply simp
huffman@45325
   270
 apply simp
huffman@45325
   271
 apply (rule_tac a=k and b=aa in ord_cases)
huffman@45325
   272
   apply simp
huffman@45325
   273
   apply (case_tac "add k y t2", simp, simp)
huffman@45325
   274
  apply simp
huffman@45325
   275
 apply simp
huffman@45325
   276
 apply (case_tac "add k y t3", simp, simp)
huffman@45325
   277
done
huffman@45325
   278
huffman@45325
   279
lemma ord0_add0: "ord0 t \<Longrightarrow> ord0 (add0 k y t)"
huffman@45333
   280
  by (simp add: ord0_def ord'_add0)
huffman@45325
   281
wenzelm@61343
   282
text \<open>The @{term "del"} function preserves balance.\<close>
huffman@45332
   283
huffman@45332
   284
lemma del_extra_simps:
huffman@45332
   285
"l \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
huffman@45332
   286
 del k (Branch2 l p r) = (case compare k p of
huffman@45332
   287
      LESS => (case del k l of None \<Rightarrow> None |
huffman@45332
   288
        Some(p', (False, l')) => Some(p', (False, Branch2 l' p r))
huffman@45332
   289
      | Some(p', (True, l')) => Some(p', case r of
huffman@45332
   290
          Branch2 rl rp rr => (True, Branch3 l' p rl rp rr)
huffman@45332
   291
        | Branch3 rl rp rm rq rr => (False, Branch2
huffman@45332
   292
            (Branch2 l' p rl) rp (Branch2 rm rq rr))))
huffman@45332
   293
    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
huffman@45332
   294
        Some(p', (False, r')) => Some(p', (False, Branch2 l (if_eq or p' p) r'))
huffman@45332
   295
      | Some(p', (True, r')) => Some(p', case l of
huffman@45332
   296
          Branch2 ll lp lr => (True, Branch3 ll lp lr (if_eq or p' p) r')
huffman@45332
   297
        | Branch3 ll lp lm lq lr => (False, Branch2
huffman@45332
   298
            (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) r')))))"
huffman@45332
   299
"l \<noteq> Empty \<or> m \<noteq> Empty \<or> r \<noteq> Empty \<Longrightarrow>
huffman@45332
   300
 del k (Branch3 l p m q r) = (case compare k q of
huffman@45332
   301
      LESS => (case compare k p of
huffman@45332
   302
        LESS => (case del k l of None \<Rightarrow> None |
huffman@45332
   303
          Some(p', (False, l')) => Some(p', (False, Branch3 l' p m q r))
huffman@45332
   304
        | Some(p', (True, l')) => Some(p', (False, case (m, r) of
huffman@45332
   305
            (Branch2 ml mp mr, Branch2 _ _ _) => Branch2 (Branch3 l' p ml mp mr) q r
huffman@45332
   306
          | (Branch3 ml mp mm mq mr, _) => Branch3 (Branch2 l' p ml) mp (Branch2 mm mq mr) q r
huffman@45332
   307
          | (Branch2 ml mp mr, Branch3 rl rp rm rq rr) =>
huffman@45332
   308
              Branch3 (Branch2 l' p ml) mp (Branch2 mr q rl) rp (Branch2 rm rq rr))))
huffman@45332
   309
      | or => (case del (if_eq or None k) m of None \<Rightarrow> None |
huffman@45332
   310
          Some(p', (False, m')) => Some(p', (False, Branch3 l (if_eq or p' p) m' q r))
huffman@45332
   311
        | Some(p', (True, m')) => Some(p', (False, case (l, r) of
huffman@45332
   312
            (Branch2 ll lp lr, Branch2 _ _ _) => Branch2 (Branch3 ll lp lr (if_eq or p' p) m') q r
huffman@45332
   313
          | (Branch3 ll lp lm lq lr, _) => Branch3 (Branch2 ll lp lm) lq (Branch2 lr (if_eq or p' p) m') q r
huffman@45332
   314
          | (_, Branch3 rl rp rm rq rr) => Branch3 l (if_eq or p' p) (Branch2 m' q rl) rp (Branch2 rm rq rr)))))
huffman@45332
   315
    | or => (case del (if_eq or None k) r of None \<Rightarrow> None |
huffman@45332
   316
        Some(q', (False, r')) => Some(q', (False, Branch3 l p m (if_eq or q' q) r'))
huffman@45332
   317
      | Some(q', (True, r')) => Some(q', (False, case (l, m) of
huffman@45332
   318
          (Branch2 _ _ _, Branch2 ml mp mr) => Branch2 l p (Branch3 ml mp mr (if_eq or q' q) r')
huffman@45332
   319
        | (_, Branch3 ml mp mm mq mr) => Branch3 l p (Branch2 ml mp mm) mq (Branch2 mr (if_eq or q' q) r')
huffman@45332
   320
        | (Branch3 ll lp lm lq lr, Branch2 ml mp mr) =>
huffman@45332
   321
            Branch3 (Branch2 ll lp lm) lq (Branch2 lr p ml) mp (Branch2 mr (if_eq or q' q) r')))))"
huffman@45332
   322
apply -
huffman@45332
   323
apply (cases l, cases r, simp_all only: del.simps, simp)
huffman@45332
   324
apply (cases l, cases m, cases r, simp_all only: del.simps, simp)
huffman@45332
   325
done
huffman@45332
   326
huffman@45335
   327
fun dfull where
huffman@45335
   328
"dfull n None \<longleftrightarrow> True" |
huffman@45335
   329
"dfull n (Some (p, (True, t'))) \<longleftrightarrow> full n t'" |
huffman@45335
   330
"dfull n (Some (p, (False, t'))) \<longleftrightarrow> full (Suc n) t'"
huffman@45332
   331
huffman@45335
   332
lemmas dfull_case_intros =
blanchet@55417
   333
  ord.exhaust [of y "dfull a (case_ord b c d y)"]
blanchet@55413
   334
  option.exhaust [of y "dfull a (case_option b c y)"]
blanchet@55414
   335
  prod.exhaust [of y "dfull a (case_prod b y)"]
blanchet@55414
   336
  bool.exhaust [of y "dfull a (case_bool b c y)"]
blanchet@55417
   337
  tree23.exhaust [of y "dfull a (Some (b, case_tree23 c d e y))"]
blanchet@55417
   338
  tree23.exhaust [of y "full a (case_tree23 b c d y)"]
wenzelm@45605
   339
  for a b c d e y
huffman@45332
   340
huffman@45335
   341
lemma dfull_del: "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
huffman@45332
   342
proof -
huffman@45332
   343
  { fix n :: "nat" and p :: "key \<times> 'a" and l r :: "'a tree23" and k
huffman@45335
   344
    assume "\<And>n. \<lbrakk>compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
huffman@45335
   345
    and "\<And>n. \<lbrakk>compare k p = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
huffman@45335
   346
    and "\<And>n. \<lbrakk>compare k p = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
huffman@45332
   347
    and "full (Suc n) (Branch2 l p r)"
huffman@45335
   348
    hence "dfull n (del k (Branch2 l p r))"
huffman@45332
   349
     apply clarsimp
huffman@45332
   350
     apply (cases n)
huffman@45332
   351
      apply (cases k)
huffman@45335
   352
       apply simp
huffman@45335
   353
      apply (simp split: ord.split)
huffman@45335
   354
     apply simp
huffman@45332
   355
     apply (subst del_extra_simps, force)
huffman@45336
   356
     (* This should work, but it is way too slow!
huffman@45336
   357
     apply (force split: ord.split option.split bool.split tree23.split) *)
huffman@45335
   358
     apply (simp | rule dfull_case_intros)+
huffman@45332
   359
     done
huffman@45332
   360
  } note A = this
huffman@45332
   361
  { fix n :: "nat" and p q :: "key \<times> 'a" and l m r :: "'a tree23" and k
huffman@45335
   362
    assume "\<And>n. \<lbrakk>compare k q = LESS; compare k p = LESS; full (Suc n) l\<rbrakk> \<Longrightarrow> dfull n (del k l)"
huffman@45335
   363
    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = EQUAL; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) m)"
huffman@45335
   364
    and "\<And>n. \<lbrakk>compare k q = LESS; compare k p = GREATER; full (Suc n) m\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) m)"
huffman@45335
   365
    and "\<And>n. \<lbrakk>compare k q = EQUAL; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq EQUAL None k) r)"
huffman@45335
   366
    and "\<And>n. \<lbrakk>compare k q = GREATER; full (Suc n) r\<rbrakk> \<Longrightarrow> dfull n (del (if_eq GREATER None k) r)"
huffman@45332
   367
    and "full (Suc n) (Branch3 l p m q r)"
huffman@45335
   368
    hence "dfull n (del k (Branch3 l p m q r))"
huffman@45332
   369
     apply clarsimp
huffman@45332
   370
     apply (cases n)
huffman@45332
   371
      apply (cases k)
huffman@45335
   372
       apply simp
huffman@45335
   373
      apply (simp split: ord.split)
huffman@45335
   374
     apply simp
huffman@45332
   375
     apply (subst del_extra_simps, force)
huffman@45335
   376
     apply (simp | rule dfull_case_intros)+
huffman@45332
   377
     done
huffman@45332
   378
  } note B = this
huffman@45335
   379
  show "full (Suc n) t \<Longrightarrow> dfull n (del k t)"
wenzelm@61166
   380
  proof (induct k t arbitrary: n rule: del.induct, goal_cases)
wenzelm@60580
   381
    case (1 k n)
wenzelm@60580
   382
    thus "dfull n (del (Some k) Empty)" by simp
wenzelm@60580
   383
  next
wenzelm@60580
   384
    case (2 p n)
wenzelm@60580
   385
    thus "dfull n (del None (Branch2 Empty p Empty))" by simp
wenzelm@60580
   386
  next
wenzelm@60580
   387
    case (3 p q n)
wenzelm@60580
   388
    thus "dfull n (del None (Branch3 Empty p Empty q Empty))" by simp
wenzelm@60580
   389
  next
wenzelm@60580
   390
    case (4 v p n)
wenzelm@60580
   391
    thus "dfull n (del (Some v) (Branch2 Empty p Empty))"
wenzelm@60580
   392
      by (simp split: ord.split)
wenzelm@60580
   393
  next
wenzelm@60580
   394
    case (5 v p q n)
wenzelm@60580
   395
    thus "dfull n (del (Some v) (Branch3 Empty p Empty q Empty))"
wenzelm@60580
   396
      by (simp split: ord.split)
wenzelm@60580
   397
  next
wenzelm@60580
   398
    case (26 n)
wenzelm@60580
   399
    thus ?case by simp
huffman@45332
   400
  qed (fact A | fact B)+
huffman@45332
   401
qed
huffman@45332
   402
huffman@45332
   403
lemma bal_del0: "bal t \<Longrightarrow> bal (del0 k t)"
huffman@45335
   404
unfolding bal_iff_full del0_def
huffman@45335
   405
apply (erule exE)
huffman@45335
   406
apply (case_tac n, simp, simp)
huffman@45335
   407
apply (frule dfull_del [where k="Some k"])
huffman@45335
   408
apply (cases "del (Some k) t", force)
blanchet@55417
   409
apply (rename_tac a, case_tac "a", rename_tac b t', case_tac "b", auto)
huffman@45335
   410
done
huffman@45332
   411
wenzelm@61343
   412
text\<open>This is a little test harness and should be commented out once the
wenzelm@61343
   413
above functions have been proved correct.\<close>
nipkow@33436
   414
blanchet@58310
   415
datatype 'a act = Add int 'a | Del int
nipkow@33436
   416
nipkow@33436
   417
fun exec where
nipkow@33436
   418
"exec [] t = t" |
nipkow@33436
   419
"exec (Add k x # as) t = exec as (add0 k x t)" |
nipkow@33436
   420
"exec (Del k # as) t = exec as (del0 k t)"
nipkow@33436
   421
wenzelm@61343
   422
text\<open>Some quick checks:\<close>
nipkow@33436
   423
huffman@45332
   424
lemma bal_exec: "bal t \<Longrightarrow> bal (exec as t)"
huffman@45332
   425
  by (induct as t arbitrary: t rule: exec.induct,
huffman@45332
   426
    simp_all add: bal_add0 bal_del0)
huffman@45332
   427
huffman@45332
   428
lemma "bal(exec as Empty)"
huffman@45332
   429
  by (simp add: bal_exec)
huffman@45332
   430
nipkow@33436
   431
lemma "ord0(exec as Empty)"
nipkow@33436
   432
quickcheck
nipkow@33436
   433
oops
nipkow@33436
   434
huffman@45332
   435
end