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