src/HOL/Data_Structures/Tree23_Set.thy
author nipkow
Thu Nov 09 09:08:14 2017 +0100 (17 months ago)
changeset 67038 db3e2240f830
parent 63636 6f38b7abb648
child 67406 23307fd33906
permissions -rw-r--r--
tuned
nipkow@61640
     1
(* Author: Tobias Nipkow *)
nipkow@61640
     2
nipkow@62130
     3
section \<open>2-3 Tree Implementation of Sets\<close>
nipkow@61640
     4
nipkow@61640
     5
theory Tree23_Set
nipkow@61640
     6
imports
nipkow@61640
     7
  Tree23
nipkow@61640
     8
  Cmp
nipkow@61640
     9
  Set_by_Ordered
nipkow@61640
    10
begin
nipkow@61640
    11
nipkow@63411
    12
fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where
nipkow@61640
    13
"isin Leaf x = False" |
nipkow@61640
    14
"isin (Node2 l a r) x =
nipkow@61678
    15
  (case cmp x a of
nipkow@61678
    16
     LT \<Rightarrow> isin l x |
nipkow@61678
    17
     EQ \<Rightarrow> True |
nipkow@61678
    18
     GT \<Rightarrow> isin r x)" |
nipkow@61640
    19
"isin (Node3 l a m b r) x =
nipkow@61678
    20
  (case cmp x a of
nipkow@61678
    21
     LT \<Rightarrow> isin l x |
nipkow@61678
    22
     EQ \<Rightarrow> True |
nipkow@61678
    23
     GT \<Rightarrow>
nipkow@61678
    24
       (case cmp x b of
nipkow@61678
    25
          LT \<Rightarrow> isin m x |
nipkow@61678
    26
          EQ \<Rightarrow> True |
nipkow@61678
    27
          GT \<Rightarrow> isin r x))"
nipkow@61640
    28
nipkow@61640
    29
datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23"
nipkow@61640
    30
nipkow@61640
    31
fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where
nipkow@61640
    32
"tree\<^sub>i (T\<^sub>i t) = t" |
nipkow@61709
    33
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r"
nipkow@61640
    34
nipkow@63411
    35
fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where
nipkow@61640
    36
"ins x Leaf = Up\<^sub>i Leaf x Leaf" |
nipkow@61640
    37
"ins x (Node2 l a r) =
nipkow@61640
    38
   (case cmp x a of
nipkow@61678
    39
      LT \<Rightarrow>
nipkow@61678
    40
        (case ins x l of
nipkow@61678
    41
           T\<^sub>i l' => T\<^sub>i (Node2 l' a r) |
nipkow@61678
    42
           Up\<^sub>i l1 b l2 => T\<^sub>i (Node3 l1 b l2 a r)) |
nipkow@61640
    43
      EQ \<Rightarrow> T\<^sub>i (Node2 l x r) |
nipkow@61678
    44
      GT \<Rightarrow>
nipkow@61678
    45
        (case ins x r of
nipkow@61678
    46
           T\<^sub>i r' => T\<^sub>i (Node2 l a r') |
nipkow@61678
    47
           Up\<^sub>i r1 b r2 => T\<^sub>i (Node3 l a r1 b r2)))" |
nipkow@61640
    48
"ins x (Node3 l a m b r) =
nipkow@61640
    49
   (case cmp x a of
nipkow@61678
    50
      LT \<Rightarrow>
nipkow@61678
    51
        (case ins x l of
nipkow@61678
    52
           T\<^sub>i l' => T\<^sub>i (Node3 l' a m b r) |
nipkow@61678
    53
           Up\<^sub>i l1 c l2 => Up\<^sub>i (Node2 l1 c l2) a (Node2 m b r)) |
nipkow@61640
    54
      EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
nipkow@61678
    55
      GT \<Rightarrow>
nipkow@61678
    56
        (case cmp x b of
nipkow@61678
    57
           GT \<Rightarrow>
nipkow@61678
    58
             (case ins x r of
nipkow@61678
    59
                T\<^sub>i r' => T\<^sub>i (Node3 l a m b r') |
nipkow@61678
    60
                Up\<^sub>i r1 c r2 => Up\<^sub>i (Node2 l a m) b (Node2 r1 c r2)) |
nipkow@61678
    61
           EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) |
nipkow@61678
    62
           LT \<Rightarrow>
nipkow@61678
    63
             (case ins x m of
nipkow@61678
    64
                T\<^sub>i m' => T\<^sub>i (Node3 l a m' b r) |
nipkow@61678
    65
                Up\<^sub>i m1 c m2 => Up\<^sub>i (Node2 l a m1) c (Node2 m2 b r))))"
nipkow@61640
    66
nipkow@61640
    67
hide_const insert
nipkow@61640
    68
nipkow@63411
    69
definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
nipkow@61640
    70
"insert x t = tree\<^sub>i(ins x t)"
nipkow@61640
    71
nipkow@61640
    72
datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23"
nipkow@61640
    73
nipkow@61640
    74
fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where
nipkow@61709
    75
"tree\<^sub>d (T\<^sub>d t) = t" |
nipkow@61709
    76
"tree\<^sub>d (Up\<^sub>d t) = t"
nipkow@61640
    77
nipkow@61640
    78
(* Variation: return None to signal no-change *)
nipkow@61640
    79
nipkow@61640
    80
fun node21 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
    81
"node21 (T\<^sub>d t1) a t2 = T\<^sub>d(Node2 t1 a t2)" |
nipkow@61640
    82
"node21 (Up\<^sub>d t1) a (Node2 t2 b t3) = Up\<^sub>d(Node3 t1 a t2 b t3)" |
nipkow@61640
    83
"node21 (Up\<^sub>d t1) a (Node3 t2 b t3 c t4) = T\<^sub>d(Node2 (Node2 t1 a t2) b (Node2 t3 c t4))"
nipkow@61640
    84
nipkow@61640
    85
fun node22 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
    86
"node22 t1 a (T\<^sub>d t2) = T\<^sub>d(Node2 t1 a t2)" |
nipkow@61640
    87
"node22 (Node2 t1 b t2) a (Up\<^sub>d t3) = Up\<^sub>d(Node3 t1 b t2 a t3)" |
nipkow@61640
    88
"node22 (Node3 t1 b t2 c t3) a (Up\<^sub>d t4) = T\<^sub>d(Node2 (Node2 t1 b t2) c (Node2 t3 a t4))"
nipkow@61640
    89
nipkow@61640
    90
fun node31 :: "'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
    91
"node31 (T\<^sub>d t1) a t2 b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
nipkow@61640
    92
"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
    93
"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
    94
nipkow@61640
    95
fun node32 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
    96
"node32 t1 a (T\<^sub>d t2) b t3 = T\<^sub>d(Node3 t1 a t2 b t3)" |
nipkow@61640
    97
"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
    98
"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
    99
nipkow@61640
   100
fun node33 :: "'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a tree23 \<Rightarrow> 'a \<Rightarrow> 'a up\<^sub>d \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   101
"node33 l a m b (T\<^sub>d r) = T\<^sub>d(Node3 l a m b r)" |
nipkow@61640
   102
"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
   103
"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
   104
nipkow@61640
   105
fun del_min :: "'a tree23 \<Rightarrow> 'a * 'a up\<^sub>d" where
nipkow@61640
   106
"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" |
nipkow@61640
   107
"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" |
nipkow@61640
   108
"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" |
nipkow@61640
   109
"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))"
nipkow@61640
   110
nipkow@67038
   111
text \<open>In the base cases of \<open>del_min\<close> and \<open>del\<close> it is enough to check if one subtree is a \<open>Leaf\<close>,
nipkow@67038
   112
in which case balancedness implies that so are the others. Exercise.\<close>
nipkow@67038
   113
nipkow@63411
   114
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where
nipkow@61640
   115
"del x Leaf = T\<^sub>d Leaf" |
nipkow@61678
   116
"del x (Node2 Leaf a Leaf) =
nipkow@61678
   117
  (if x = a then Up\<^sub>d Leaf else T\<^sub>d(Node2 Leaf a Leaf))" |
nipkow@61678
   118
"del x (Node3 Leaf a Leaf b Leaf) =
nipkow@61678
   119
  T\<^sub>d(if x = a then Node2 Leaf b Leaf else
nipkow@61678
   120
     if x = b then Node2 Leaf a Leaf
nipkow@61678
   121
     else Node3 Leaf a Leaf b Leaf)" |
nipkow@61678
   122
"del x (Node2 l a r) =
nipkow@61678
   123
  (case cmp x a of
nipkow@61678
   124
     LT \<Rightarrow> node21 (del x l) a r |
nipkow@61678
   125
     GT \<Rightarrow> node22 l a (del x r) |
nipkow@61678
   126
     EQ \<Rightarrow> let (a',t) = del_min r in node22 l a' t)" |
nipkow@61678
   127
"del x (Node3 l a m b r) =
nipkow@61678
   128
  (case cmp x a of
nipkow@61678
   129
     LT \<Rightarrow> node31 (del x l) a m b r |
nipkow@61678
   130
     EQ \<Rightarrow> let (a',m') = del_min m in node32 l a' m' b r |
nipkow@61678
   131
     GT \<Rightarrow>
nipkow@61678
   132
       (case cmp x b of
nipkow@61640
   133
          LT \<Rightarrow> node32 l a (del x m) b r |
nipkow@61640
   134
          EQ \<Rightarrow> let (b',r') = del_min r in node33 l a m b' r' |
nipkow@61640
   135
          GT \<Rightarrow> node33 l a m b (del x r)))"
nipkow@61640
   136
nipkow@63411
   137
definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where
nipkow@61640
   138
"delete x t = tree\<^sub>d(del x t)"
nipkow@61640
   139
nipkow@61640
   140
nipkow@61640
   141
subsection "Functional Correctness"
nipkow@61640
   142
nipkow@61640
   143
subsubsection "Proofs for isin"
nipkow@61640
   144
nipkow@61640
   145
lemma "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
nipkow@61640
   146
by (induction t) (auto simp: elems_simps1 ball_Un)
nipkow@61640
   147
nipkow@61640
   148
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> elems (inorder t))"
nipkow@61640
   149
by (induction t) (auto simp: elems_simps2)
nipkow@61640
   150
nipkow@61640
   151
nipkow@61640
   152
subsubsection "Proofs for insert"
nipkow@61640
   153
nipkow@61640
   154
lemma inorder_ins:
nipkow@61640
   155
  "sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)"
nipkow@61640
   156
by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits)
nipkow@61640
   157
nipkow@61640
   158
lemma inorder_insert:
nipkow@61640
   159
  "sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)"
nipkow@61640
   160
by(simp add: insert_def inorder_ins)
nipkow@61640
   161
nipkow@61640
   162
nipkow@61640
   163
subsubsection "Proofs for delete"
nipkow@61640
   164
nipkow@61640
   165
lemma inorder_node21: "height r > 0 \<Longrightarrow>
nipkow@61640
   166
  inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r"
nipkow@61640
   167
by(induct l' a r rule: node21.induct) auto
nipkow@61640
   168
nipkow@61640
   169
lemma inorder_node22: "height l > 0 \<Longrightarrow>
nipkow@61640
   170
  inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')"
nipkow@61640
   171
by(induct l a r' rule: node22.induct) auto
nipkow@61640
   172
nipkow@61640
   173
lemma inorder_node31: "height m > 0 \<Longrightarrow>
nipkow@61640
   174
  inorder (tree\<^sub>d (node31 l' a m b r)) = inorder (tree\<^sub>d l') @ a # inorder m @ b # inorder r"
nipkow@61640
   175
by(induct l' a m b r rule: node31.induct) auto
nipkow@61640
   176
nipkow@61640
   177
lemma inorder_node32: "height r > 0 \<Longrightarrow>
nipkow@61640
   178
  inorder (tree\<^sub>d (node32 l a m' b r)) = inorder l @ a # inorder (tree\<^sub>d m') @ b # inorder r"
nipkow@61640
   179
by(induct l a m' b r rule: node32.induct) auto
nipkow@61640
   180
nipkow@61640
   181
lemma inorder_node33: "height m > 0 \<Longrightarrow>
nipkow@61640
   182
  inorder (tree\<^sub>d (node33 l a m b r')) = inorder l @ a # inorder m @ b # inorder (tree\<^sub>d r')"
nipkow@61640
   183
by(induct l a m b r' rule: node33.induct) auto
nipkow@61640
   184
nipkow@61640
   185
lemmas inorder_nodes = inorder_node21 inorder_node22
nipkow@61640
   186
  inorder_node31 inorder_node32 inorder_node33
nipkow@61640
   187
nipkow@61640
   188
lemma del_minD:
nipkow@61640
   189
  "del_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow>
nipkow@61640
   190
  x # inorder(tree\<^sub>d t') = inorder t"
nipkow@61640
   191
by(induction t arbitrary: t' rule: del_min.induct)
nipkow@61640
   192
  (auto simp: inorder_nodes split: prod.splits)
nipkow@61640
   193
nipkow@61640
   194
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
nipkow@61640
   195
  inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)"
nipkow@61640
   196
by(induction t rule: del.induct)
nipkow@63636
   197
  (auto simp: del_list_simps inorder_nodes del_minD split!: if_split prod.splits)
nipkow@61640
   198
nipkow@61640
   199
lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow>
nipkow@61640
   200
  inorder(delete x t) = del_list x (inorder t)"
nipkow@61640
   201
by(simp add: delete_def inorder_del)
nipkow@61640
   202
nipkow@61640
   203
nipkow@61640
   204
subsection \<open>Balancedness\<close>
nipkow@61640
   205
nipkow@61640
   206
nipkow@61640
   207
subsubsection "Proofs for insert"
nipkow@61640
   208
nipkow@61640
   209
text{* First a standard proof that @{const ins} preserves @{const bal}. *}
nipkow@61640
   210
nipkow@61640
   211
instantiation up\<^sub>i :: (type)height
nipkow@61640
   212
begin
nipkow@61640
   213
nipkow@61640
   214
fun height_up\<^sub>i :: "'a up\<^sub>i \<Rightarrow> nat" where
nipkow@61640
   215
"height (T\<^sub>i t) = height t" |
nipkow@61640
   216
"height (Up\<^sub>i l a r) = height l"
nipkow@61640
   217
nipkow@61640
   218
instance ..
nipkow@61640
   219
nipkow@61640
   220
end
nipkow@61640
   221
nipkow@61640
   222
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t"
nipkow@63636
   223
by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *)
nipkow@61640
   224
nipkow@61640
   225
text{* Now an alternative proof (by Brian Huffman) that runs faster because
nipkow@61640
   226
two properties (balance and height) are combined in one predicate. *}
nipkow@61640
   227
nipkow@61640
   228
inductive full :: "nat \<Rightarrow> 'a tree23 \<Rightarrow> bool" where
nipkow@61640
   229
"full 0 Leaf" |
nipkow@61640
   230
"\<lbrakk>full n l; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node2 l p r)" |
nipkow@61640
   231
"\<lbrakk>full n l; full n m; full n r\<rbrakk> \<Longrightarrow> full (Suc n) (Node3 l p m q r)"
nipkow@61640
   232
nipkow@61640
   233
inductive_cases full_elims:
nipkow@61640
   234
  "full n Leaf"
nipkow@61640
   235
  "full n (Node2 l p r)"
nipkow@61640
   236
  "full n (Node3 l p m q r)"
nipkow@61640
   237
nipkow@61640
   238
inductive_cases full_0_elim: "full 0 t"
nipkow@61640
   239
inductive_cases full_Suc_elim: "full (Suc n) t"
nipkow@61640
   240
nipkow@61640
   241
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf"
nipkow@61640
   242
  by (auto elim: full_0_elim intro: full.intros)
nipkow@61640
   243
nipkow@61640
   244
lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0"
nipkow@61640
   245
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   246
nipkow@61640
   247
lemma full_Suc_Node2_iff [simp]:
nipkow@61640
   248
  "full (Suc n) (Node2 l p r) \<longleftrightarrow> full n l \<and> full n r"
nipkow@61640
   249
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   250
nipkow@61640
   251
lemma full_Suc_Node3_iff [simp]:
nipkow@61640
   252
  "full (Suc n) (Node3 l p m q r) \<longleftrightarrow> full n l \<and> full n m \<and> full n r"
nipkow@61640
   253
  by (auto elim: full_elims intro: full.intros)
nipkow@61640
   254
nipkow@61640
   255
lemma full_imp_height: "full n t \<Longrightarrow> height t = n"
nipkow@61640
   256
  by (induct set: full, simp_all)
nipkow@61640
   257
nipkow@61640
   258
lemma full_imp_bal: "full n t \<Longrightarrow> bal t"
nipkow@61640
   259
  by (induct set: full, auto dest: full_imp_height)
nipkow@61640
   260
nipkow@61640
   261
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t"
nipkow@61640
   262
  by (induct t, simp_all)
nipkow@61640
   263
nipkow@61640
   264
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)"
nipkow@61640
   265
  by (auto elim!: bal_imp_full full_imp_bal)
nipkow@61640
   266
nipkow@61640
   267
text {* The @{const "insert"} function either preserves the height of the
nipkow@61640
   268
tree, or increases it by one. The constructor returned by the @{term
nipkow@61640
   269
"insert"} function determines which: A return value of the form @{term
nipkow@61640
   270
"T\<^sub>i t"} indicates that the height will be the same. A value of the
nipkow@61640
   271
form @{term "Up\<^sub>i l p r"} indicates an increase in height. *}
nipkow@61640
   272
nipkow@61640
   273
fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where
nipkow@61640
   274
"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" |
nipkow@61640
   275
"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r"
nipkow@61640
   276
nipkow@61640
   277
lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)"
nipkow@61640
   278
by (induct rule: full.induct) (auto split: up\<^sub>i.split)
nipkow@61640
   279
nipkow@61640
   280
text {* The @{const insert} operation preserves balance. *}
nipkow@61640
   281
nipkow@61640
   282
lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)"
nipkow@61640
   283
unfolding bal_iff_full insert_def
nipkow@61640
   284
apply (erule exE)
nipkow@61640
   285
apply (drule full\<^sub>i_ins [of _ _ a])
nipkow@61640
   286
apply (cases "ins a t")
nipkow@61640
   287
apply (auto intro: full.intros)
nipkow@61640
   288
done
nipkow@61640
   289
nipkow@61640
   290
nipkow@61640
   291
subsection "Proofs for delete"
nipkow@61640
   292
nipkow@61640
   293
instantiation up\<^sub>d :: (type)height
nipkow@61640
   294
begin
nipkow@61640
   295
nipkow@61640
   296
fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where
nipkow@61640
   297
"height (T\<^sub>d t) = height t" |
nipkow@61640
   298
"height (Up\<^sub>d t) = height t + 1"
nipkow@61640
   299
nipkow@61640
   300
instance ..
nipkow@61640
   301
nipkow@61640
   302
end
nipkow@61640
   303
nipkow@61640
   304
lemma bal_tree\<^sub>d_node21:
nipkow@61640
   305
  "\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))"
nipkow@61640
   306
by(induct l' a r rule: node21.induct) auto
nipkow@61640
   307
nipkow@61640
   308
lemma bal_tree\<^sub>d_node22:
nipkow@61640
   309
  "\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))"
nipkow@61640
   310
by(induct l a r' rule: node22.induct) auto
nipkow@61640
   311
nipkow@61640
   312
lemma bal_tree\<^sub>d_node31:
nipkow@61640
   313
  "\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk>
nipkow@61640
   314
  \<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))"
nipkow@61640
   315
by(induct l' a m b r rule: node31.induct) auto
nipkow@61640
   316
nipkow@61640
   317
lemma bal_tree\<^sub>d_node32:
nipkow@61640
   318
  "\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk>
nipkow@61640
   319
  \<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))"
nipkow@61640
   320
by(induct l a m' b r rule: node32.induct) auto
nipkow@61640
   321
nipkow@61640
   322
lemma bal_tree\<^sub>d_node33:
nipkow@61640
   323
  "\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk>
nipkow@61640
   324
  \<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))"
nipkow@61640
   325
by(induct l a m b r' rule: node33.induct) auto
nipkow@61640
   326
nipkow@61640
   327
lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22
nipkow@61640
   328
  bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33
nipkow@61640
   329
nipkow@61640
   330
lemma height'_node21:
nipkow@61640
   331
   "height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1"
nipkow@61640
   332
by(induct l' a r rule: node21.induct)(simp_all)
nipkow@61640
   333
nipkow@61640
   334
lemma height'_node22:
nipkow@61640
   335
   "height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1"
nipkow@61640
   336
by(induct l a r' rule: node22.induct)(simp_all)
nipkow@61640
   337
nipkow@61640
   338
lemma height'_node31:
nipkow@61640
   339
  "height m > 0 \<Longrightarrow> height(node31 l a m b r) =
nipkow@61640
   340
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   341
by(induct l a m b r rule: node31.induct)(simp_all add: max_def)
nipkow@61640
   342
nipkow@61640
   343
lemma height'_node32:
nipkow@61640
   344
  "height r > 0 \<Longrightarrow> height(node32 l a m b r) =
nipkow@61640
   345
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   346
by(induct l a m b r rule: node32.induct)(simp_all add: max_def)
nipkow@61640
   347
nipkow@61640
   348
lemma height'_node33:
nipkow@61640
   349
  "height m > 0 \<Longrightarrow> height(node33 l a m b r) =
nipkow@61640
   350
   max (height l) (max (height m) (height r)) + 1"
nipkow@61640
   351
by(induct l a m b r rule: node33.induct)(simp_all add: max_def)
nipkow@61640
   352
nipkow@61640
   353
lemmas heights = height'_node21 height'_node22
nipkow@61640
   354
  height'_node31 height'_node32 height'_node33
nipkow@61640
   355
nipkow@61640
   356
lemma height_del_min:
nipkow@61640
   357
  "del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t"
nipkow@61640
   358
by(induct t arbitrary: x t' rule: del_min.induct)
nipkow@61640
   359
  (auto simp: heights split: prod.splits)
nipkow@61640
   360
nipkow@61640
   361
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t"
nipkow@61640
   362
by(induction x t rule: del.induct)
nipkow@61640
   363
  (auto simp: heights max_def height_del_min split: prod.splits)
nipkow@61640
   364
nipkow@61640
   365
lemma bal_del_min:
nipkow@61640
   366
  "\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')"
nipkow@61640
   367
by(induct t arbitrary: x t' rule: del_min.induct)
nipkow@61640
   368
  (auto simp: heights height_del_min bals split: prod.splits)
nipkow@61640
   369
nipkow@61640
   370
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))"
nipkow@61640
   371
by(induction x t rule: del.induct)
nipkow@61640
   372
  (auto simp: bals bal_del_min height_del height_del_min split: prod.splits)
nipkow@61640
   373
nipkow@61640
   374
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)"
nipkow@61640
   375
by(simp add: delete_def bal_tree\<^sub>d_del)
nipkow@61640
   376
nipkow@61640
   377
nipkow@61640
   378
subsection \<open>Overall Correctness\<close>
nipkow@61640
   379
nipkow@61640
   380
interpretation Set_by_Ordered
nipkow@61640
   381
where empty = Leaf and isin = isin and insert = insert and delete = delete
nipkow@61640
   382
and inorder = inorder and inv = bal
nipkow@61640
   383
proof (standard, goal_cases)
nipkow@61640
   384
  case 2 thus ?case by(simp add: isin_set)
nipkow@61640
   385
next
nipkow@61640
   386
  case 3 thus ?case by(simp add: inorder_insert)
nipkow@61640
   387
next
nipkow@61640
   388
  case 4 thus ?case by(simp add: inorder_delete)
nipkow@61640
   389
next
nipkow@61640
   390
  case 6 thus ?case by(simp add: bal_insert)
nipkow@61640
   391
next
nipkow@61640
   392
  case 7 thus ?case by(simp add: bal_delete)
nipkow@61640
   393
qed simp+
nipkow@61640
   394
nipkow@61640
   395
end