|
1 (* Title: HOL/ex/AVL.ML |
|
2 ID: $Id$ |
|
3 Author: Cornelia Pusch and Tobias Nipkow |
|
4 Copyright 1998 TUM |
|
5 *) |
|
6 |
|
7 (****************************** isbal **********************************) |
|
8 |
|
9 Addsimps[Let_def]; |
|
10 |
|
11 (* rotations preserve isbal property *) |
|
12 |
|
13 Goalw [bal_def] |
|
14 "height l = Suc(Suc(height r)) --> bal l = Right --> isbal l --> isbal r \ |
|
15 \ --> isbal (lr_rot (n, l, r))"; |
|
16 by (case_tac "l" 1); |
|
17 by (Asm_simp_tac 1); |
|
18 by (case_tac "tree2" 1); |
|
19 by (Asm_simp_tac 1); |
|
20 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
21 by (arith_tac 1); |
|
22 qed_spec_mp "isbal_lr_rot"; |
|
23 |
|
24 |
|
25 Goalw [bal_def] |
|
26 "height l = Suc(Suc(height r)) --> bal l ~= Right --> isbal l --> isbal r \ |
|
27 \ --> isbal (r_rot (n, l, r))"; |
|
28 by (case_tac "l" 1); |
|
29 by (Asm_simp_tac 1); |
|
30 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
31 qed_spec_mp "isbal_r_rot"; |
|
32 |
|
33 |
|
34 Goalw [bal_def] |
|
35 "height r = Suc(Suc(height l)) --> bal r = Left --> isbal l --> isbal r \ |
|
36 \ --> isbal (rl_rot (n, l, r))"; |
|
37 by (case_tac "r" 1); |
|
38 by (Asm_simp_tac 1); |
|
39 by (case_tac "tree1" 1); |
|
40 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
41 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
42 by (arith_tac 1); |
|
43 qed_spec_mp "isbal_rl_rot"; |
|
44 |
|
45 |
|
46 Goalw [bal_def] |
|
47 "height r = Suc(Suc(height l)) --> bal r ~= Left --> isbal l --> isbal r \ |
|
48 \ --> isbal (l_rot (n, l, r))"; |
|
49 by (case_tac "r" 1); |
|
50 by (Asm_simp_tac 1); |
|
51 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
52 qed_spec_mp "isbal_l_rot"; |
|
53 |
|
54 |
|
55 (* lemmas about height after rotation *) |
|
56 |
|
57 Goalw [bal_def] |
|
58 "bal l = Right --> height l = Suc(Suc(height r)) \ |
|
59 \ --> Suc(height (lr_rot (n, l, r))) = height (MKT n l r) "; |
|
60 by (case_tac "l" 1); |
|
61 by (Asm_simp_tac 1); |
|
62 by (case_tac "tree2" 1); |
|
63 by (Asm_simp_tac 1); |
|
64 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
65 qed_spec_mp "height_lr_rot"; |
|
66 |
|
67 |
|
68 Goalw [bal_def] |
|
69 "height l = Suc(Suc(height r)) --> bal l ~= Right \ |
|
70 \ --> Suc(height (r_rot (n, l, r))) = height (MKT n l r) | \ |
|
71 \ height (r_rot (n, l, r)) = height (MKT n l r)"; |
|
72 by (case_tac "l" 1); |
|
73 by (Asm_simp_tac 1); |
|
74 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
75 qed_spec_mp "height_r_rot"; |
|
76 |
|
77 |
|
78 Goalw [l_bal_def] |
|
79 "height l = Suc(Suc(height r)) \ |
|
80 \ --> Suc(height (l_bal n l r)) = height (MKT n l r) | \ |
|
81 \ height (l_bal n l r) = height (MKT n l r)"; |
|
82 by (case_tac "bal l = Right" 1); |
|
83 by (fast_tac (claset() addDs [height_lr_rot] addss simpset()) 1); |
|
84 by (fast_tac (claset() addDs [height_r_rot] addss simpset()) 1); |
|
85 qed_spec_mp "height_l_bal"; |
|
86 |
|
87 |
|
88 Goalw [bal_def] |
|
89 "height r = Suc(Suc(height l)) --> bal r = Left \ |
|
90 \ --> Suc(height (rl_rot (n, l, r))) = height (MKT n l r)"; |
|
91 by (case_tac "r" 1); |
|
92 by (Asm_simp_tac 1); |
|
93 by (case_tac "tree1" 1); |
|
94 by (Asm_simp_tac 1); |
|
95 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
96 by (arith_tac 1); |
|
97 qed_spec_mp "height_rl_rot"; |
|
98 |
|
99 |
|
100 Goalw [bal_def] |
|
101 "height r = Suc(Suc(height l)) --> bal r ~= Left \ |
|
102 \ --> Suc(height (l_rot (n, l, r))) = height (MKT n l r) | \ |
|
103 \ height (l_rot (n, l, r)) = height (MKT n l r)"; |
|
104 by (case_tac "r" 1); |
|
105 by (Asm_simp_tac 1); |
|
106 by (asm_simp_tac (simpset() addsimps [max_def]) 1); |
|
107 qed_spec_mp "height_l_rot"; |
|
108 |
|
109 |
|
110 Goalw [r_bal_def] |
|
111 "height r = Suc(Suc(height l)) \ |
|
112 \ --> Suc(height (r_bal n l r)) = height (MKT n l r) | \ |
|
113 \ height (r_bal n l r) = height (MKT n l r)"; |
|
114 by (case_tac "bal r = Left" 1); |
|
115 by (fast_tac (claset() addDs [height_rl_rot] addss simpset()) 1); |
|
116 by (fast_tac (claset() addDs [height_l_rot] addss simpset()) 1); |
|
117 qed_spec_mp "height_r_bal"; |
|
118 |
|
119 |
|
120 (* lemma about height after insert *) |
|
121 Goal |
|
122 "isbal t \ |
|
123 \ --> height (insert x t) = height t | height (insert x t) = Suc(height t)"; |
|
124 by (induct_tac "t" 1); |
|
125 by (Simp_tac 1); |
|
126 by (case_tac "x=nat" 1); |
|
127 by (Asm_simp_tac 1); |
|
128 by (case_tac "x<nat" 1); |
|
129 by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1); |
|
130 by (forw_inst_tac [("n","nat")] height_l_bal 1); |
|
131 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1); |
|
132 by(fast_tac (claset() addss simpset()) 1); |
|
133 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1); |
|
134 by(fast_tac (claset() addss simpset()) 1); |
|
135 by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1); |
|
136 by (forw_inst_tac [("n","nat")] height_r_bal 1); |
|
137 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1); |
|
138 by(fast_tac (claset() addss simpset()) 1); |
|
139 by (asm_full_simp_tac (simpset() addsimps [max_def]) 1); |
|
140 by(fast_tac (claset() addss simpset()) 1); |
|
141 qed_spec_mp "height_insert"; |
|
142 |
|
143 |
|
144 Goal |
|
145 "!!x. [| height (insert x l) ~= Suc(Suc(height r)); isbal (insert x l); isbal (MKT n l r) |] \ |
|
146 \ ==> isbal (MKT n (insert x l) r)"; |
|
147 by (cut_inst_tac [("x","x"),("t","l")] height_insert 1); |
|
148 by (Asm_full_simp_tac 1); |
|
149 by (fast_tac (claset() addss simpset()) 1); |
|
150 qed "isbal_insert_left"; |
|
151 |
|
152 |
|
153 Goal |
|
154 "!!x. [| height (insert x r) ~= Suc(Suc(height l)); isbal (insert x r); isbal (MKT n l r) |] \ |
|
155 \ ==> isbal (MKT n l (insert x r))"; |
|
156 by (cut_inst_tac [("x","x"),("t","r")] height_insert 1); |
|
157 by (Asm_full_simp_tac 1); |
|
158 by (fast_tac (claset() addss simpset()) 1); |
|
159 qed "isbal_insert_right"; |
|
160 |
|
161 (* insert-operation preserves isbal property *) |
|
162 |
|
163 Goal |
|
164 "isbal t --> isbal(insert x t)"; |
|
165 by (induct_tac "t" 1); |
|
166 by (Simp_tac 1); |
|
167 by (case_tac "x=nat" 1); |
|
168 by (Asm_simp_tac 1); |
|
169 by (case_tac "x<nat" 1); |
|
170 by (case_tac "height (insert x tree1) = Suc (Suc (height tree2))" 1); |
|
171 by (case_tac "bal (insert x tree1) = Right" 1); |
|
172 by (fast_tac (claset() addIs [isbal_lr_rot] addss (simpset() |
|
173 addsimps [l_bal_def])) 1); |
|
174 by (fast_tac (claset() addIs [isbal_r_rot] addss (simpset() |
|
175 addsimps [l_bal_def])) 1); |
|
176 by (Clarify_tac 1); |
|
177 by (forward_tac [isbal_insert_left] 1); |
|
178 by (Asm_full_simp_tac 1); |
|
179 ba 1; |
|
180 by (Asm_full_simp_tac 1); |
|
181 by (case_tac "height (insert x tree2) = Suc (Suc (height tree1))" 1); |
|
182 by (case_tac "bal (insert x tree2) = Left" 1); |
|
183 by (fast_tac (claset() addIs [isbal_rl_rot] addss (simpset() |
|
184 addsimps [r_bal_def])) 1); |
|
185 by (fast_tac (claset() addIs [isbal_l_rot] addss (simpset() |
|
186 addsimps [r_bal_def])) 1); |
|
187 by (Clarify_tac 1); |
|
188 by (forward_tac [isbal_insert_right] 1); |
|
189 by (Asm_full_simp_tac 1); |
|
190 ba 1; |
|
191 by (Asm_full_simp_tac 1); |
|
192 qed_spec_mp "isbal_insert"; |
|
193 |
|
194 |
|
195 (****************************** isin **********************************) |
|
196 |
|
197 |
|
198 (* rotations preserve isin property *) |
|
199 |
|
200 Goalw [bal_def] |
|
201 "height l = Suc(Suc(height r)) --> bal l = Right \ |
|
202 \ --> isin x (lr_rot (n, l, r)) = isin x (MKT n l r)"; |
|
203 by (case_tac "l" 1); |
|
204 by (Asm_simp_tac 1); |
|
205 by (case_tac "tree2" 1); |
|
206 by (Asm_simp_tac 1); |
|
207 by (fast_tac (claset() addss simpset()) 1); |
|
208 qed_spec_mp "isin_lr_rot"; |
|
209 |
|
210 |
|
211 Goalw [bal_def] |
|
212 "height l = Suc(Suc(height r)) --> bal l ~= Right \ |
|
213 \ --> isin x (r_rot (n, l, r)) = isin x (MKT n l r)"; |
|
214 by (case_tac "l" 1); |
|
215 by (Asm_simp_tac 1); |
|
216 by (fast_tac (claset() addss simpset()) 1); |
|
217 qed_spec_mp "isin_r_rot"; |
|
218 |
|
219 |
|
220 Goalw [bal_def] |
|
221 "height r = Suc(Suc(height l)) --> bal r = Left \ |
|
222 \ --> isin x (rl_rot (n, l, r)) = isin x (MKT n l r)"; |
|
223 by (case_tac "r" 1); |
|
224 by (Asm_simp_tac 1); |
|
225 by (case_tac "tree1" 1); |
|
226 by (asm_simp_tac (simpset() addsimps [max_def,le_def]) 1); |
|
227 by (fast_tac (claset() addss simpset()) 1); |
|
228 qed_spec_mp "isin_rl_rot"; |
|
229 |
|
230 |
|
231 Goalw [bal_def] |
|
232 "height r = Suc(Suc(height l)) --> bal r ~= Left \ |
|
233 \ --> isin x (l_rot (n, l, r)) = isin x (MKT n l r)"; |
|
234 by (case_tac "r" 1); |
|
235 by (Asm_simp_tac 1); |
|
236 by (fast_tac (claset() addss simpset()) 1); |
|
237 qed_spec_mp "isin_l_rot"; |
|
238 |
|
239 |
|
240 (* isin insert *) |
|
241 |
|
242 Goal |
|
243 "isin y (insert x t) = (y=x | isin y t)"; |
|
244 by (induct_tac "t" 1); |
|
245 by (Asm_simp_tac 1); |
|
246 by(asm_simp_tac (simpset() addsimps [l_bal_def,isin_lr_rot,isin_r_rot, |
|
247 r_bal_def,isin_rl_rot,isin_l_rot]) 1); |
|
248 by(Blast_tac 1); |
|
249 qed "isin_insert"; |
|
250 |
|
251 |
|
252 (****************************** isord **********************************) |
|
253 |
|
254 (* rotations preserve isord property *) |
|
255 |
|
256 Goalw [bal_def] |
|
257 "height l = Suc(Suc(height r)) --> bal l = Right --> isord (MKT n l r) \ |
|
258 \ --> isord (lr_rot (n, l, r))"; |
|
259 by (case_tac "l" 1); |
|
260 by (Asm_simp_tac 1); |
|
261 by (case_tac "tree2" 1); |
|
262 by (Asm_simp_tac 1); |
|
263 by (Asm_simp_tac 1); |
|
264 by(blast_tac (claset() addIs [less_trans])1); |
|
265 qed_spec_mp "isord_lr_rot"; |
|
266 |
|
267 |
|
268 Goalw [bal_def] |
|
269 "height l = Suc(Suc(height r)) --> bal l ~= Right --> isord (MKT n l r) \ |
|
270 \ --> isord (r_rot (n, l, r))"; |
|
271 by (case_tac "l" 1); |
|
272 by (Asm_simp_tac 1); |
|
273 by (auto_tac (claset() addIs [less_trans],simpset())); |
|
274 qed_spec_mp "isord_r_rot"; |
|
275 |
|
276 |
|
277 Goalw [bal_def] |
|
278 "height r = Suc(Suc(height l)) --> bal r = Left --> isord (MKT n l r) \ |
|
279 \ --> isord (rl_rot (n, l, r))"; |
|
280 by (case_tac "r" 1); |
|
281 by (Asm_simp_tac 1); |
|
282 by (case_tac "tree1" 1); |
|
283 by (asm_simp_tac (simpset() addsimps [le_def]) 1); |
|
284 by (Asm_simp_tac 1); |
|
285 by(blast_tac (claset() addIs [less_trans])1); |
|
286 qed_spec_mp "isord_rl_rot"; |
|
287 |
|
288 |
|
289 Goalw [bal_def] |
|
290 "height r = Suc(Suc(height l)) --> bal r ~= Left --> isord (MKT n l r) \ |
|
291 \ --> isord (l_rot (n, l, r))"; |
|
292 by (case_tac "r" 1); |
|
293 by (Asm_simp_tac 1); |
|
294 by (Asm_simp_tac 1); |
|
295 by(blast_tac (claset() addIs [less_trans])1); |
|
296 qed_spec_mp "isord_l_rot"; |
|
297 |
|
298 (* insert operation presreves isord property *) |
|
299 |
|
300 Goal |
|
301 "isord t --> isord(insert x t)"; |
|
302 by (induct_tac "t" 1); |
|
303 by (Simp_tac 1); |
|
304 by (cut_inst_tac [("m","x"),("n","nat")] less_linear 1); |
|
305 by (fast_tac (claset() addss (simpset() addsimps [l_bal_def,isord_lr_rot, |
|
306 isord_r_rot,r_bal_def,isord_l_rot,isord_rl_rot,isin_insert])) 1); |
|
307 qed_spec_mp "isord_insert"; |