author | nipkow |
Sun, 08 Apr 2018 09:46:33 +0200 | |
changeset 67964 | 08cc5ab18c84 |
parent 67929 | 30486b96274d |
child 67965 | aaa31cd0caef |
permissions | -rw-r--r-- |
61640 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
62130 | 3 |
section \<open>2-3-4 Tree Implementation of Sets\<close> |
61640 | 4 |
|
5 |
theory Tree234_Set |
|
6 |
imports |
|
7 |
Tree234 |
|
8 |
Cmp |
|
67964 | 9 |
"Set_Interfaces" |
61640 | 10 |
begin |
11 |
||
12 |
subsection \<open>Set operations on 2-3-4 trees\<close> |
|
13 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
14 |
fun isin :: "'a::linorder tree234 \<Rightarrow> 'a \<Rightarrow> bool" where |
61640 | 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))" | |
|
61703 | 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 |
|
61640 | 25 |
LT \<Rightarrow> isin t1 x | |
26 |
EQ \<Rightarrow> True | |
|
27 |
GT \<Rightarrow> isin t2 x) | |
|
61703 | 28 |
EQ \<Rightarrow> True | |
29 |
GT \<Rightarrow> |
|
30 |
(case cmp x c of |
|
61640 | 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" | |
|
61709 | 39 |
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" |
61640 | 40 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
41 |
fun ins :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>i" where |
61640 | 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))))" | |
|
61703 | 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))))" |
|
61640 | 91 |
|
92 |
hide_const insert |
|
93 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
94 |
definition insert :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where |
61640 | 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 |
|
61709 | 100 |
"tree\<^sub>d (T\<^sub>d t) = t" | |
101 |
"tree\<^sub>d (Up\<^sub>d t) = t" |
|
61640 | 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 del_min :: "'a tree234 \<Rightarrow> 'a * 'a up\<^sub>d" where |
|
158 |
"del_min (Node2 Leaf a Leaf) = (a, Up\<^sub>d Leaf)" | |
|
159 |
"del_min (Node3 Leaf a Leaf b Leaf) = (a, T\<^sub>d(Node2 Leaf b Leaf))" | |
|
160 |
"del_min (Node4 Leaf a Leaf b Leaf c Leaf) = (a, T\<^sub>d(Node3 Leaf b Leaf c Leaf))" | |
|
161 |
"del_min (Node2 l a r) = (let (x,l') = del_min l in (x, node21 l' a r))" | |
|
162 |
"del_min (Node3 l a m b r) = (let (x,l') = del_min l in (x, node31 l' a m b r))" | |
|
163 |
"del_min (Node4 l a m b n c r) = (let (x,l') = del_min l in (x, node41 l' a m b n c r))" |
|
164 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
165 |
fun del :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a up\<^sub>d" where |
61640 | 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) = del_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') = del_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') = del_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') = del_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') = del_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') = del_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 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
197 |
definition delete :: "'a::linorder \<Rightarrow> 'a tree234 \<Rightarrow> 'a tree234" where |
61640 | 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 |
||
67929 | 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) |
|
61640 | 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)" |
|
63636 | 213 |
by(induction t) (auto, auto simp: ins_list_simps split!: if_splits up\<^sub>i.splits) |
61640 | 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 del_minD: |
|
263 |
"del_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: del_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) |
|
63636 | 271 |
(auto simp: inorder_nodes del_list_simps del_minD split!: if_split prod.splits) |
272 |
(* 30 secs (2016) *) |
|
61640 | 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 |
||
67406 | 283 |
text\<open>First a standard proof that @{const ins} preserves @{const bal}.\<close> |
61640 | 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" |
|
63636 | 297 |
by (induct t) (auto split!: if_split up\<^sub>i.split) |
61640 | 298 |
|
299 |
||
67406 | 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> |
|
61640 | 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 |
||
67406 | 348 |
text \<open>The @{const "insert"} function either preserves the height of the |
61640 | 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 |
|
67406 | 352 |
form @{term "Up\<^sub>i l p r"} indicates an increase in height.\<close> |
61640 | 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 |
||
67406 | 361 |
text \<open>The @{const insert} operation preserves balance.\<close> |
61640 | 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_del_min: |
|
480 |
"del_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t" |
|
481 |
by(induct t arbitrary: x t' rule: del_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) |
|
63636 | 486 |
(auto simp add: heights height_del_min split!: if_split prod.split) |
61640 | 487 |
|
488 |
lemma bal_del_min: |
|
489 |
"\<lbrakk> del_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')" |
|
490 |
by(induct t arbitrary: x t' rule: del_min.induct) |
|
491 |
(auto simp: heights height_del_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) |
|
63636 | 495 |
(auto simp: bals bal_del_min height_del height_del_min split!: if_split prod.split) |
61640 | 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 |