94 show ?thesis by simp |
94 show ?thesis by simp |
95 qed |
95 qed |
96 |
96 |
97 (* end of mv *) |
97 (* end of mv *) |
98 |
98 |
99 fun bal :: "'a list \<Rightarrow> nat \<Rightarrow> 'a tree * 'a list" where |
99 fun bal :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree * 'a list" where |
100 "bal xs n = (if n=0 then (Leaf,xs) else |
100 "bal n xs = (if n=0 then (Leaf,xs) else |
101 (let m = n div 2; |
101 (let m = n div 2; |
102 (l, ys) = bal xs m; |
102 (l, ys) = bal m xs; |
103 (r, zs) = bal (tl ys) (n-1-m) |
103 (r, zs) = bal (n-1-m) (tl ys) |
104 in (Node l (hd ys) r, zs)))" |
104 in (Node l (hd ys) r, zs)))" |
105 |
105 |
106 declare bal.simps[simp del] |
106 declare bal.simps[simp del] |
107 |
107 |
|
108 definition bal_list :: "nat \<Rightarrow> 'a list \<Rightarrow> 'a tree" where |
|
109 "bal_list n xs = fst (bal n xs)" |
|
110 |
108 definition balance_list :: "'a list \<Rightarrow> 'a tree" where |
111 definition balance_list :: "'a list \<Rightarrow> 'a tree" where |
109 "balance_list xs = fst (bal xs (length xs))" |
112 "balance_list xs = bal_list (length xs) xs" |
|
113 |
|
114 definition bal_tree :: "nat \<Rightarrow> 'a tree \<Rightarrow> 'a tree" where |
|
115 "bal_tree n t = bal_list n (inorder t)" |
110 |
116 |
111 definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where |
117 definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where |
112 "balance_tree = balance_list o inorder" |
118 "balance_tree t = bal_tree (size t) t" |
113 |
119 |
114 lemma bal_simps: |
120 lemma bal_simps: |
115 "bal xs 0 = (Leaf, xs)" |
121 "bal 0 xs = (Leaf, xs)" |
116 "n > 0 \<Longrightarrow> |
122 "n > 0 \<Longrightarrow> |
117 bal xs n = |
123 bal n xs = |
118 (let m = n div 2; |
124 (let m = n div 2; |
119 (l, ys) = bal xs m; |
125 (l, ys) = bal m xs; |
120 (r, zs) = bal (tl ys) (n-1-m) |
126 (r, zs) = bal (n-1-m) (tl ys) |
121 in (Node l (hd ys) r, zs))" |
127 in (Node l (hd ys) r, zs))" |
122 by(simp_all add: bal.simps) |
128 by(simp_all add: bal.simps) |
123 |
129 |
124 text\<open>The following lemmas take advantage of the fact |
130 text\<open>Some of the following lemmas take advantage of the fact |
125 that \<open>bal xs n\<close> yields a result even if \<open>n > length xs\<close>.\<close> |
131 that \<open>bal xs n\<close> yields a result even if \<open>n > length xs\<close>.\<close> |
126 |
132 |
127 lemma size_bal: "bal xs n = (t,ys) \<Longrightarrow> size t = n" |
133 lemma size_bal: "bal n xs = (t,ys) \<Longrightarrow> size t = n" |
128 proof(induction xs n arbitrary: t ys rule: bal.induct) |
134 proof(induction n xs arbitrary: t ys rule: bal.induct) |
129 case (1 xs n) |
135 case (1 n xs) |
130 thus ?case |
136 thus ?case |
131 by(cases "n=0") |
137 by(cases "n=0") |
132 (auto simp add: bal_simps Let_def split: prod.splits) |
138 (auto simp add: bal_simps Let_def split: prod.splits) |
133 qed |
139 qed |
134 |
140 |
135 lemma bal_inorder: |
141 lemma bal_inorder: |
136 "\<lbrakk> bal xs n = (t,ys); n \<le> length xs \<rbrakk> |
142 "\<lbrakk> bal n xs = (t,ys); n \<le> length xs \<rbrakk> |
137 \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs" |
143 \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs" |
138 proof(induction xs n arbitrary: t ys rule: bal.induct) |
144 proof(induction n xs arbitrary: t ys rule: bal.induct) |
139 case (1 xs n) show ?case |
145 case (1 n xs) show ?case |
140 proof cases |
146 proof cases |
141 assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps) |
147 assume "n = 0" thus ?thesis using 1 by (simp add: bal_simps) |
142 next |
148 next |
143 assume [arith]: "n \<noteq> 0" |
149 assume [arith]: "n \<noteq> 0" |
144 let ?n1 = "n div 2" let ?n2 = "n - 1 - ?n1" |
150 let ?n1 = "n div 2" let ?n2 = "n - 1 - ?n1" |
145 from "1.prems" obtain l r xs' where |
151 from "1.prems" obtain l r xs' where |
146 b1: "bal xs ?n1 = (l,xs')" and |
152 b1: "bal ?n1 xs = (l,xs')" and |
147 b2: "bal (tl xs') ?n2 = (r,ys)" and |
153 b2: "bal ?n2 (tl xs') = (r,ys)" and |
148 t: "t = \<langle>l, hd xs', r\<rangle>" |
154 t: "t = \<langle>l, hd xs', r\<rangle>" |
149 by(auto simp: Let_def bal_simps split: prod.splits) |
155 by(auto simp: Let_def bal_simps split: prod.splits) |
150 have IH1: "inorder l = take ?n1 xs \<and> xs' = drop ?n1 xs" |
156 have IH1: "inorder l = take ?n1 xs \<and> xs' = drop ?n1 xs" |
151 using b1 "1.prems" by(intro "1.IH"(1)) auto |
157 using b1 "1.prems" by(intro "1.IH"(1)) auto |
152 have IH2: "inorder r = take ?n2 (tl xs') \<and> ys = drop ?n2 (tl xs')" |
158 have IH2: "inorder r = take ?n2 (tl xs') \<and> ys = drop ?n2 (tl xs')" |
160 hence "ys = drop n xs" using IH1 IH2 by (simp add: drop_Suc[symmetric]) |
166 hence "ys = drop n xs" using IH1 IH2 by (simp add: drop_Suc[symmetric]) |
161 thus ?thesis using * by blast |
167 thus ?thesis using * by blast |
162 qed |
168 qed |
163 qed |
169 qed |
164 |
170 |
165 corollary inorder_balance_list: "inorder(balance_list xs) = xs" |
171 corollary inorder_bal_list[simp]: |
166 using bal_inorder[of xs "length xs"] |
172 "n \<le> length xs \<Longrightarrow> inorder(bal_list n xs) = take n xs" |
167 by (metis balance_list_def order_refl prod.collapse take_all) |
173 unfolding bal_list_def by (metis bal_inorder eq_fst_iff) |
|
174 |
|
175 corollary inorder_balance_list[simp]: "inorder(balance_list xs) = xs" |
|
176 by(simp add: balance_list_def) |
|
177 |
|
178 corollary inorder_bal_tree: |
|
179 "n \<le> size t \<Longrightarrow> inorder(bal_tree n t) = take n (inorder t)" |
|
180 by(simp add: bal_tree_def) |
168 |
181 |
169 corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t" |
182 corollary inorder_balance_tree[simp]: "inorder(balance_tree t) = inorder t" |
170 by(simp add: balance_tree_def inorder_balance_list) |
183 by(simp add: balance_tree_def inorder_bal_tree) |
|
184 |
|
185 corollary size_bal_list[simp]: "size(bal_list n xs) = n" |
|
186 unfolding bal_list_def by (metis prod.collapse size_bal) |
171 |
187 |
172 corollary size_balance_list[simp]: "size(balance_list xs) = length xs" |
188 corollary size_balance_list[simp]: "size(balance_list xs) = length xs" |
173 by (metis inorder_balance_list length_inorder) |
189 by (simp add: balance_list_def) |
|
190 |
|
191 corollary size_bal_tree[simp]: "size(bal_tree n t) = n" |
|
192 by(simp add: bal_tree_def) |
174 |
193 |
175 corollary size_balance_tree[simp]: "size(balance_tree t) = size t" |
194 corollary size_balance_tree[simp]: "size(balance_tree t) = size t" |
176 by(simp add: balance_tree_def inorder_balance_list) |
195 by(simp add: balance_tree_def) |
177 |
196 |
178 lemma min_height_bal: |
197 lemma min_height_bal: |
179 "bal xs n = (t,ys) \<Longrightarrow> min_height t = nat(floor(log 2 (n + 1)))" |
198 "bal n xs = (t,ys) \<Longrightarrow> min_height t = nat(floor(log 2 (n + 1)))" |
180 proof(induction xs n arbitrary: t ys rule: bal.induct) |
199 proof(induction n xs arbitrary: t ys rule: bal.induct) |
181 case (1 xs n) show ?case |
200 case (1 n xs) show ?case |
182 proof cases |
201 proof cases |
183 assume "n = 0" thus ?thesis |
202 assume "n = 0" thus ?thesis |
184 using "1.prems" by (simp add: bal_simps) |
203 using "1.prems" by (simp add: bal_simps) |
185 next |
204 next |
186 assume [arith]: "n \<noteq> 0" |
205 assume [arith]: "n \<noteq> 0" |
187 from "1.prems" obtain l r xs' where |
206 from "1.prems" obtain l r xs' where |
188 b1: "bal xs (n div 2) = (l,xs')" and |
207 b1: "bal (n div 2) xs = (l,xs')" and |
189 b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and |
208 b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and |
190 t: "t = \<langle>l, hd xs', r\<rangle>" |
209 t: "t = \<langle>l, hd xs', r\<rangle>" |
191 by(auto simp: bal_simps Let_def split: prod.splits) |
210 by(auto simp: bal_simps Let_def split: prod.splits) |
192 let ?log1 = "nat (floor(log 2 (n div 2 + 1)))" |
211 let ?log1 = "nat (floor(log 2 (n div 2 + 1)))" |
193 let ?log2 = "nat (floor(log 2 (n - 1 - n div 2 + 1)))" |
212 let ?log2 = "nat (floor(log 2 (n - 1 - n div 2 + 1)))" |
194 have IH1: "min_height l = ?log1" using "1.IH"(1) b1 by simp |
213 have IH1: "min_height l = ?log1" using "1.IH"(1) b1 by simp |
209 finally show ?thesis . |
228 finally show ?thesis . |
210 qed |
229 qed |
211 qed |
230 qed |
212 |
231 |
213 lemma height_bal: |
232 lemma height_bal: |
214 "bal xs n = (t,ys) \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>" |
233 "bal n xs = (t,ys) \<Longrightarrow> height t = nat \<lceil>log 2 (n + 1)\<rceil>" |
215 proof(induction xs n arbitrary: t ys rule: bal.induct) |
234 proof(induction n xs arbitrary: t ys rule: bal.induct) |
216 case (1 xs n) show ?case |
235 case (1 n xs) show ?case |
217 proof cases |
236 proof cases |
218 assume "n = 0" thus ?thesis |
237 assume "n = 0" thus ?thesis |
219 using "1.prems" by (simp add: bal_simps) |
238 using "1.prems" by (simp add: bal_simps) |
220 next |
239 next |
221 assume [arith]: "n \<noteq> 0" |
240 assume [arith]: "n \<noteq> 0" |
222 from "1.prems" obtain l r xs' where |
241 from "1.prems" obtain l r xs' where |
223 b1: "bal xs (n div 2) = (l,xs')" and |
242 b1: "bal (n div 2) xs = (l,xs')" and |
224 b2: "bal (tl xs') (n - 1 - n div 2) = (r,ys)" and |
243 b2: "bal (n - 1 - n div 2) (tl xs') = (r,ys)" and |
225 t: "t = \<langle>l, hd xs', r\<rangle>" |
244 t: "t = \<langle>l, hd xs', r\<rangle>" |
226 by(auto simp: bal_simps Let_def split: prod.splits) |
245 by(auto simp: bal_simps Let_def split: prod.splits) |
227 let ?log1 = "nat \<lceil>log 2 (n div 2 + 1)\<rceil>" |
246 let ?log1 = "nat \<lceil>log 2 (n div 2 + 1)\<rceil>" |
228 let ?log2 = "nat \<lceil>log 2 (n - 1 - n div 2 + 1)\<rceil>" |
247 let ?log2 = "nat \<lceil>log 2 (n - 1 - n div 2 + 1)\<rceil>" |
229 have IH1: "height l = ?log1" using "1.IH"(1) b1 by simp |
248 have IH1: "height l = ?log1" using "1.IH"(1) b1 by simp |
240 finally show ?thesis . |
259 finally show ?thesis . |
241 qed |
260 qed |
242 qed |
261 qed |
243 |
262 |
244 lemma balanced_bal: |
263 lemma balanced_bal: |
245 assumes "bal xs n = (t,ys)" shows "balanced t" |
264 assumes "bal n xs = (t,ys)" shows "balanced t" |
246 unfolding balanced_def |
265 unfolding balanced_def |
247 using height_bal[OF assms] min_height_bal[OF assms] |
266 using height_bal[OF assms] min_height_bal[OF assms] |
248 by linarith |
267 by linarith |
249 |
268 |
|
269 lemma height_bal_list: |
|
270 "n \<le> length xs \<Longrightarrow> height (bal_list n xs) = nat \<lceil>log 2 (n + 1)\<rceil>" |
|
271 unfolding bal_list_def by (metis height_bal prod.collapse) |
|
272 |
250 lemma height_balance_list: |
273 lemma height_balance_list: |
251 "height (balance_list xs) = nat \<lceil>log 2 (length xs + 1)\<rceil>" |
274 "height (balance_list xs) = nat \<lceil>log 2 (length xs + 1)\<rceil>" |
252 by (metis balance_list_def height_bal prod.collapse) |
275 by (simp add: balance_list_def height_bal_list) |
|
276 |
|
277 corollary height_bal_tree: |
|
278 "n \<le> length xs \<Longrightarrow> height (bal_tree n t) = nat(ceiling(log 2 (n + 1)))" |
|
279 unfolding bal_list_def bal_tree_def |
|
280 using height_bal prod.exhaust_sel by blast |
253 |
281 |
254 corollary height_balance_tree: |
282 corollary height_balance_tree: |
255 "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))" |
283 "height (balance_tree t) = nat(ceiling(log 2 (size t + 1)))" |
256 by(simp add: balance_tree_def height_balance_list) |
284 by (simp add: bal_tree_def balance_tree_def height_bal_list) |
|
285 |
|
286 corollary balanced_bal_list[simp]: "balanced (bal_list n xs)" |
|
287 unfolding bal_list_def by (metis balanced_bal prod.collapse) |
257 |
288 |
258 corollary balanced_balance_list[simp]: "balanced (balance_list xs)" |
289 corollary balanced_balance_list[simp]: "balanced (balance_list xs)" |
259 by (metis balance_list_def balanced_bal prod.collapse) |
290 by (simp add: balance_list_def) |
|
291 |
|
292 corollary balanced_bal_tree[simp]: "balanced (bal_tree n t)" |
|
293 by (simp add: bal_tree_def) |
260 |
294 |
261 corollary balanced_balance_tree[simp]: "balanced (balance_tree t)" |
295 corollary balanced_balance_tree[simp]: "balanced (balance_tree t)" |
262 by (simp add: balance_tree_def) |
296 by (simp add: balance_tree_def) |
263 |
297 |
264 lemma wbalanced_bal: "bal xs n = (t,ys) \<Longrightarrow> wbalanced t" |
298 lemma wbalanced_bal: "bal n xs = (t,ys) \<Longrightarrow> wbalanced t" |
265 proof(induction xs n arbitrary: t ys rule: bal.induct) |
299 proof(induction n xs arbitrary: t ys rule: bal.induct) |
266 case (1 xs n) |
300 case (1 n xs) |
267 show ?case |
301 show ?case |
268 proof cases |
302 proof cases |
269 assume "n = 0" |
303 assume "n = 0" |
270 thus ?thesis |
304 thus ?thesis |
271 using "1.prems" by(simp add: bal_simps) |
305 using "1.prems" by(simp add: bal_simps) |
272 next |
306 next |
273 assume "n \<noteq> 0" |
307 assume "n \<noteq> 0" |
274 with "1.prems" obtain l ys r zs where |
308 with "1.prems" obtain l ys r zs where |
275 rec1: "bal xs (n div 2) = (l, ys)" and |
309 rec1: "bal (n div 2) xs = (l, ys)" and |
276 rec2: "bal (tl ys) (n - 1 - n div 2) = (r, zs)" and |
310 rec2: "bal (n - 1 - n div 2) (tl ys) = (r, zs)" and |
277 t: "t = \<langle>l, hd ys, r\<rangle>" |
311 t: "t = \<langle>l, hd ys, r\<rangle>" |
278 by(auto simp add: bal_simps Let_def split: prod.splits) |
312 by(auto simp add: bal_simps Let_def split: prod.splits) |
279 have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl rec1] . |
313 have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl rec1] . |
280 have "wbalanced r" using "1.IH"(2)[OF \<open>n\<noteq>0\<close> refl rec1[symmetric] refl rec2] . |
314 have "wbalanced r" using "1.IH"(2)[OF \<open>n\<noteq>0\<close> refl rec1[symmetric] refl rec2] . |
281 with l t size_bal[OF rec1] size_bal[OF rec2] |
315 with l t size_bal[OF rec1] size_bal[OF rec2] |
282 show ?thesis by auto |
316 show ?thesis by auto |
283 qed |
317 qed |
284 qed |
318 qed |
285 |
319 |
|
320 lemma wbalanced_bal_list[simp]: "wbalanced (bal_list n xs)" |
|
321 by(simp add: bal_list_def) (metis prod.collapse wbalanced_bal) |
|
322 |
|
323 lemma wbalanced_balance_list[simp]: "wbalanced (balance_list xs)" |
|
324 by(simp add: balance_list_def) |
|
325 |
|
326 lemma wbalanced_bal_tree[simp]: "wbalanced (bal_tree n t)" |
|
327 by(simp add: bal_tree_def) |
|
328 |
286 lemma wbalanced_balance_tree: "wbalanced (balance_tree t)" |
329 lemma wbalanced_balance_tree: "wbalanced (balance_tree t)" |
287 by(simp add: balance_tree_def balance_list_def) |
330 by (simp add: balance_tree_def) |
288 (metis prod.collapse wbalanced_bal) |
|
289 |
331 |
290 hide_const (open) bal |
332 hide_const (open) bal |
291 |
333 |
292 end |
334 end |