author | wenzelm |
Sat, 05 Jan 2019 17:24:33 +0100 | |
changeset 69597 | ff784d5a5bfb |
parent 68440 | 6826718f732d |
child 70272 | 1d564a895296 |
permissions | -rw-r--r-- |
61640 | 1 |
(* Author: Tobias Nipkow *) |
2 |
||
62130 | 3 |
section \<open>2-3 Tree Implementation of Sets\<close> |
61640 | 4 |
|
5 |
theory Tree23_Set |
|
6 |
imports |
|
7 |
Tree23 |
|
8 |
Cmp |
|
67965 | 9 |
Set_Specs |
61640 | 10 |
begin |
11 |
||
68109 | 12 |
declare sorted_wrt.simps(2)[simp del] |
13 |
||
68431 | 14 |
definition empty :: "'a tree23" where |
15 |
"empty = Leaf" |
|
16 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
17 |
fun isin :: "'a::linorder tree23 \<Rightarrow> 'a \<Rightarrow> bool" where |
61640 | 18 |
"isin Leaf x = False" | |
19 |
"isin (Node2 l a r) x = |
|
61678 | 20 |
(case cmp x a of |
21 |
LT \<Rightarrow> isin l x | |
|
22 |
EQ \<Rightarrow> True | |
|
23 |
GT \<Rightarrow> isin r x)" | |
|
61640 | 24 |
"isin (Node3 l a m b r) x = |
61678 | 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))" |
|
61640 | 33 |
|
34 |
datatype 'a up\<^sub>i = T\<^sub>i "'a tree23" | Up\<^sub>i "'a tree23" 'a "'a tree23" |
|
35 |
||
36 |
fun tree\<^sub>i :: "'a up\<^sub>i \<Rightarrow> 'a tree23" where |
|
37 |
"tree\<^sub>i (T\<^sub>i t) = t" | |
|
61709 | 38 |
"tree\<^sub>i (Up\<^sub>i l a r) = Node2 l a r" |
61640 | 39 |
|
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
40 |
fun ins :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>i" where |
61640 | 41 |
"ins x Leaf = Up\<^sub>i Leaf x Leaf" | |
42 |
"ins x (Node2 l a r) = |
|
43 |
(case cmp x a of |
|
61678 | 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)) | |
|
61640 | 48 |
EQ \<Rightarrow> T\<^sub>i (Node2 l x r) | |
61678 | 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)))" | |
|
61640 | 53 |
"ins x (Node3 l a m b r) = |
54 |
(case cmp x a of |
|
61678 | 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)) | |
|
61640 | 59 |
EQ \<Rightarrow> T\<^sub>i (Node3 l a m b r) | |
61678 | 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))))" |
|
61640 | 71 |
|
72 |
hide_const insert |
|
73 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
74 |
definition insert :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where |
61640 | 75 |
"insert x t = tree\<^sub>i(ins x t)" |
76 |
||
77 |
datatype 'a up\<^sub>d = T\<^sub>d "'a tree23" | Up\<^sub>d "'a tree23" |
|
78 |
||
79 |
fun tree\<^sub>d :: "'a up\<^sub>d \<Rightarrow> 'a tree23" where |
|
61709 | 80 |
"tree\<^sub>d (T\<^sub>d t) = t" | |
81 |
"tree\<^sub>d (Up\<^sub>d t) = t" |
|
61640 | 82 |
|
83 |
(* Variation: return None to signal no-change *) |
|
84 |
||
85 |
fun 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 |
||
90 |
fun 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 |
||
95 |
fun 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 |
||
100 |
fun 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 |
||
105 |
fun 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 |
||
68020 | 110 |
fun 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))" |
|
61640 | 115 |
|
68020 | 116 |
text \<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>, |
67038 | 117 |
in which case balancedness implies that so are the others. Exercise.\<close> |
118 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
119 |
fun del :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a up\<^sub>d" where |
61640 | 120 |
"del x Leaf = T\<^sub>d Leaf" | |
61678 | 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) | |
|
68020 | 131 |
EQ \<Rightarrow> let (a',t) = split_min r in node22 l a' t)" | |
61678 | 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 | |
|
68020 | 135 |
EQ \<Rightarrow> let (a',m') = split_min m in node32 l a' m' b r | |
61678 | 136 |
GT \<Rightarrow> |
137 |
(case cmp x b of |
|
61640 | 138 |
LT \<Rightarrow> node32 l a (del x m) b r | |
68020 | 139 |
EQ \<Rightarrow> let (b',r') = split_min r in node33 l a m b' r' | |
61640 | 140 |
GT \<Rightarrow> node33 l a m b (del x r)))" |
141 |
||
63411
e051eea34990
got rid of class cmp; added height-size proofs by Daniel Stuewe
nipkow
parents:
62130
diff
changeset
|
142 |
definition delete :: "'a::linorder \<Rightarrow> 'a tree23 \<Rightarrow> 'a tree23" where |
61640 | 143 |
"delete x t = tree\<^sub>d(del x t)" |
144 |
||
145 |
||
146 |
subsection "Functional Correctness" |
|
147 |
||
148 |
subsubsection "Proofs for isin" |
|
149 |
||
67929 | 150 |
lemma isin_set: "sorted(inorder t) \<Longrightarrow> isin t x = (x \<in> set (inorder t))" |
151 |
by (induction t) (auto simp: isin_simps ball_Un) |
|
61640 | 152 |
|
153 |
||
154 |
subsubsection "Proofs for insert" |
|
155 |
||
156 |
lemma inorder_ins: |
|
157 |
"sorted(inorder t) \<Longrightarrow> inorder(tree\<^sub>i(ins x t)) = ins_list x (inorder t)" |
|
158 |
by(induction t) (auto simp: ins_list_simps split: up\<^sub>i.splits) |
|
159 |
||
160 |
lemma inorder_insert: |
|
161 |
"sorted(inorder t) \<Longrightarrow> inorder(insert a t) = ins_list a (inorder t)" |
|
162 |
by(simp add: insert_def inorder_ins) |
|
163 |
||
164 |
||
165 |
subsubsection "Proofs for delete" |
|
166 |
||
167 |
lemma inorder_node21: "height r > 0 \<Longrightarrow> |
|
168 |
inorder (tree\<^sub>d (node21 l' a r)) = inorder (tree\<^sub>d l') @ a # inorder r" |
|
169 |
by(induct l' a r rule: node21.induct) auto |
|
170 |
||
171 |
lemma inorder_node22: "height l > 0 \<Longrightarrow> |
|
172 |
inorder (tree\<^sub>d (node22 l a r')) = inorder l @ a # inorder (tree\<^sub>d r')" |
|
173 |
by(induct l a r' rule: node22.induct) auto |
|
174 |
||
175 |
lemma 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" |
|
177 |
by(induct l' a m b r rule: node31.induct) auto |
|
178 |
||
179 |
lemma 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" |
|
181 |
by(induct l a m' b r rule: node32.induct) auto |
|
182 |
||
183 |
lemma 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')" |
|
185 |
by(induct l a m b r' rule: node33.induct) auto |
|
186 |
||
187 |
lemmas inorder_nodes = inorder_node21 inorder_node22 |
|
188 |
inorder_node31 inorder_node32 inorder_node33 |
|
189 |
||
68020 | 190 |
lemma split_minD: |
191 |
"split_min t = (x,t') \<Longrightarrow> bal t \<Longrightarrow> height t > 0 \<Longrightarrow> |
|
61640 | 192 |
x # inorder(tree\<^sub>d t') = inorder t" |
68020 | 193 |
by(induction t arbitrary: t' rule: split_min.induct) |
61640 | 194 |
(auto simp: inorder_nodes split: prod.splits) |
195 |
||
196 |
lemma inorder_del: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> |
|
197 |
inorder(tree\<^sub>d (del x t)) = del_list x (inorder t)" |
|
198 |
by(induction t rule: del.induct) |
|
68020 | 199 |
(auto simp: del_list_simps inorder_nodes split_minD split!: if_split prod.splits) |
61640 | 200 |
|
201 |
lemma inorder_delete: "\<lbrakk> bal t ; sorted(inorder t) \<rbrakk> \<Longrightarrow> |
|
202 |
inorder(delete x t) = del_list x (inorder t)" |
|
203 |
by(simp add: delete_def inorder_del) |
|
204 |
||
205 |
||
206 |
subsection \<open>Balancedness\<close> |
|
207 |
||
208 |
||
209 |
subsubsection "Proofs for insert" |
|
210 |
||
69597 | 211 |
text\<open>First a standard proof that \<^const>\<open>ins\<close> preserves \<^const>\<open>bal\<close>.\<close> |
61640 | 212 |
|
213 |
instantiation up\<^sub>i :: (type)height |
|
214 |
begin |
|
215 |
||
216 |
fun 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 |
||
220 |
instance .. |
|
221 |
||
222 |
end |
|
223 |
||
224 |
lemma bal_ins: "bal t \<Longrightarrow> bal (tree\<^sub>i(ins a t)) \<and> height(ins a t) = height t" |
|
63636 | 225 |
by (induct t) (auto split!: if_split up\<^sub>i.split) (* 15 secs in 2015 *) |
61640 | 226 |
|
67406 | 227 |
text\<open>Now an alternative proof (by Brian Huffman) that runs faster because |
228 |
two properties (balance and height) are combined in one predicate.\<close> |
|
61640 | 229 |
|
230 |
inductive 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 |
||
235 |
inductive_cases full_elims: |
|
236 |
"full n Leaf" |
|
237 |
"full n (Node2 l p r)" |
|
238 |
"full n (Node3 l p m q r)" |
|
239 |
||
240 |
inductive_cases full_0_elim: "full 0 t" |
|
241 |
inductive_cases full_Suc_elim: "full (Suc n) t" |
|
242 |
||
243 |
lemma full_0_iff [simp]: "full 0 t \<longleftrightarrow> t = Leaf" |
|
244 |
by (auto elim: full_0_elim intro: full.intros) |
|
245 |
||
246 |
lemma full_Leaf_iff [simp]: "full n Leaf \<longleftrightarrow> n = 0" |
|
247 |
by (auto elim: full_elims intro: full.intros) |
|
248 |
||
249 |
lemma 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 |
||
253 |
lemma 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 |
||
257 |
lemma full_imp_height: "full n t \<Longrightarrow> height t = n" |
|
258 |
by (induct set: full, simp_all) |
|
259 |
||
260 |
lemma full_imp_bal: "full n t \<Longrightarrow> bal t" |
|
261 |
by (induct set: full, auto dest: full_imp_height) |
|
262 |
||
263 |
lemma bal_imp_full: "bal t \<Longrightarrow> full (height t) t" |
|
264 |
by (induct t, simp_all) |
|
265 |
||
266 |
lemma bal_iff_full: "bal t \<longleftrightarrow> (\<exists>n. full n t)" |
|
267 |
by (auto elim!: bal_imp_full full_imp_bal) |
|
268 |
||
69597 | 269 |
text \<open>The \<^const>\<open>insert\<close> function either preserves the height of the |
270 |
tree, or increases it by one. The constructor returned by the \<^term>\<open>insert\<close> function determines which: A return value of the form \<^term>\<open>T\<^sub>i t\<close> indicates that the height will be the same. A value of the |
|
271 |
form \<^term>\<open>Up\<^sub>i l p r\<close> indicates an increase in height.\<close> |
|
61640 | 272 |
|
273 |
fun full\<^sub>i :: "nat \<Rightarrow> 'a up\<^sub>i \<Rightarrow> bool" where |
|
274 |
"full\<^sub>i n (T\<^sub>i t) \<longleftrightarrow> full n t" | |
|
275 |
"full\<^sub>i n (Up\<^sub>i l p r) \<longleftrightarrow> full n l \<and> full n r" |
|
276 |
||
277 |
lemma full\<^sub>i_ins: "full n t \<Longrightarrow> full\<^sub>i n (ins a t)" |
|
278 |
by (induct rule: full.induct) (auto split: up\<^sub>i.split) |
|
279 |
||
69597 | 280 |
text \<open>The \<^const>\<open>insert\<close> operation preserves balance.\<close> |
61640 | 281 |
|
282 |
lemma bal_insert: "bal t \<Longrightarrow> bal (insert a t)" |
|
283 |
unfolding bal_iff_full insert_def |
|
284 |
apply (erule exE) |
|
285 |
apply (drule full\<^sub>i_ins [of _ _ a]) |
|
286 |
apply (cases "ins a t") |
|
287 |
apply (auto intro: full.intros) |
|
288 |
done |
|
289 |
||
290 |
||
291 |
subsection "Proofs for delete" |
|
292 |
||
293 |
instantiation up\<^sub>d :: (type)height |
|
294 |
begin |
|
295 |
||
296 |
fun height_up\<^sub>d :: "'a up\<^sub>d \<Rightarrow> nat" where |
|
297 |
"height (T\<^sub>d t) = height t" | |
|
298 |
"height (Up\<^sub>d t) = height t + 1" |
|
299 |
||
300 |
instance .. |
|
301 |
||
302 |
end |
|
303 |
||
304 |
lemma bal_tree\<^sub>d_node21: |
|
305 |
"\<lbrakk>bal r; bal (tree\<^sub>d l'); height r = height l' \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node21 l' a r))" |
|
306 |
by(induct l' a r rule: node21.induct) auto |
|
307 |
||
308 |
lemma bal_tree\<^sub>d_node22: |
|
309 |
"\<lbrakk>bal(tree\<^sub>d r'); bal l; height r' = height l \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d (node22 l a r'))" |
|
310 |
by(induct l a r' rule: node22.induct) auto |
|
311 |
||
312 |
lemma bal_tree\<^sub>d_node31: |
|
313 |
"\<lbrakk> bal (tree\<^sub>d l'); bal m; bal r; height l' = height r; height m = height r \<rbrakk> |
|
314 |
\<Longrightarrow> bal (tree\<^sub>d (node31 l' a m b r))" |
|
315 |
by(induct l' a m b r rule: node31.induct) auto |
|
316 |
||
317 |
lemma bal_tree\<^sub>d_node32: |
|
318 |
"\<lbrakk> bal l; bal (tree\<^sub>d m'); bal r; height l = height r; height m' = height r \<rbrakk> |
|
319 |
\<Longrightarrow> bal (tree\<^sub>d (node32 l a m' b r))" |
|
320 |
by(induct l a m' b r rule: node32.induct) auto |
|
321 |
||
322 |
lemma bal_tree\<^sub>d_node33: |
|
323 |
"\<lbrakk> bal l; bal m; bal(tree\<^sub>d r'); height l = height r'; height m = height r' \<rbrakk> |
|
324 |
\<Longrightarrow> bal (tree\<^sub>d (node33 l a m b r'))" |
|
325 |
by(induct l a m b r' rule: node33.induct) auto |
|
326 |
||
327 |
lemmas bals = bal_tree\<^sub>d_node21 bal_tree\<^sub>d_node22 |
|
328 |
bal_tree\<^sub>d_node31 bal_tree\<^sub>d_node32 bal_tree\<^sub>d_node33 |
|
329 |
||
330 |
lemma height'_node21: |
|
331 |
"height r > 0 \<Longrightarrow> height(node21 l' a r) = max (height l') (height r) + 1" |
|
332 |
by(induct l' a r rule: node21.induct)(simp_all) |
|
333 |
||
334 |
lemma height'_node22: |
|
335 |
"height l > 0 \<Longrightarrow> height(node22 l a r') = max (height l) (height r') + 1" |
|
336 |
by(induct l a r' rule: node22.induct)(simp_all) |
|
337 |
||
338 |
lemma height'_node31: |
|
339 |
"height m > 0 \<Longrightarrow> height(node31 l a m b r) = |
|
340 |
max (height l) (max (height m) (height r)) + 1" |
|
341 |
by(induct l a m b r rule: node31.induct)(simp_all add: max_def) |
|
342 |
||
343 |
lemma height'_node32: |
|
344 |
"height r > 0 \<Longrightarrow> height(node32 l a m b r) = |
|
345 |
max (height l) (max (height m) (height r)) + 1" |
|
346 |
by(induct l a m b r rule: node32.induct)(simp_all add: max_def) |
|
347 |
||
348 |
lemma height'_node33: |
|
349 |
"height m > 0 \<Longrightarrow> height(node33 l a m b r) = |
|
350 |
max (height l) (max (height m) (height r)) + 1" |
|
351 |
by(induct l a m b r rule: node33.induct)(simp_all add: max_def) |
|
352 |
||
353 |
lemmas heights = height'_node21 height'_node22 |
|
354 |
height'_node31 height'_node32 height'_node33 |
|
355 |
||
68020 | 356 |
lemma height_split_min: |
357 |
"split_min t = (x, t') \<Longrightarrow> height t > 0 \<Longrightarrow> bal t \<Longrightarrow> height t' = height t" |
|
358 |
by(induct t arbitrary: x t' rule: split_min.induct) |
|
61640 | 359 |
(auto simp: heights split: prod.splits) |
360 |
||
361 |
lemma height_del: "bal t \<Longrightarrow> height(del x t) = height t" |
|
362 |
by(induction x t rule: del.induct) |
|
68020 | 363 |
(auto simp: heights max_def height_split_min split: prod.splits) |
61640 | 364 |
|
68020 | 365 |
lemma bal_split_min: |
366 |
"\<lbrakk> split_min t = (x, t'); bal t; height t > 0 \<rbrakk> \<Longrightarrow> bal (tree\<^sub>d t')" |
|
367 |
by(induct t arbitrary: x t' rule: split_min.induct) |
|
368 |
(auto simp: heights height_split_min bals split: prod.splits) |
|
61640 | 369 |
|
370 |
lemma bal_tree\<^sub>d_del: "bal t \<Longrightarrow> bal(tree\<^sub>d(del x t))" |
|
371 |
by(induction x t rule: del.induct) |
|
68020 | 372 |
(auto simp: bals bal_split_min height_del height_split_min split: prod.splits) |
61640 | 373 |
|
374 |
corollary bal_delete: "bal t \<Longrightarrow> bal(delete x t)" |
|
375 |
by(simp add: delete_def bal_tree\<^sub>d_del) |
|
376 |
||
377 |
||
378 |
subsection \<open>Overall Correctness\<close> |
|
379 |
||
68440 | 380 |
interpretation S: Set_by_Ordered |
68431 | 381 |
where empty = empty and isin = isin and insert = insert and delete = delete |
61640 | 382 |
and inorder = inorder and inv = bal |
383 |
proof (standard, goal_cases) |
|
384 |
case 2 thus ?case by(simp add: isin_set) |
|
385 |
next |
|
386 |
case 3 thus ?case by(simp add: inorder_insert) |
|
387 |
next |
|
388 |
case 4 thus ?case by(simp add: inorder_delete) |
|
389 |
next |
|
390 |
case 6 thus ?case by(simp add: bal_insert) |
|
391 |
next |
|
392 |
case 7 thus ?case by(simp add: bal_delete) |
|
68431 | 393 |
qed (simp add: empty_def)+ |
61640 | 394 |
|
395 |
end |