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