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