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