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