21 "balance_list xs = fst (bal xs (length xs))" |
21 "balance_list xs = fst (bal xs (length xs))" |
22 |
22 |
23 definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where |
23 definition balance_tree :: "'a tree \<Rightarrow> 'a tree" where |
24 "balance_tree = balance_list o inorder" |
24 "balance_tree = balance_list o inorder" |
25 |
25 |
26 |
|
27 lemma bal_simps: |
26 lemma bal_simps: |
28 "bal xs 0 = (Leaf, xs)" |
27 "bal xs 0 = (Leaf, xs)" |
29 "n > 0 \<Longrightarrow> |
28 "n > 0 \<Longrightarrow> |
30 bal xs n = |
29 bal xs n = |
31 (let m = n div 2; |
30 (let m = n div 2; |
32 (l, ys) = Balance.bal xs m; |
31 (l, ys) = Balance.bal xs m; |
33 (r, zs) = Balance.bal (tl ys) (n-1-m) |
32 (r, zs) = Balance.bal (tl ys) (n-1-m) |
34 in (Node l (hd ys) r, zs))" |
33 in (Node l (hd ys) r, zs))" |
35 by(simp_all add: bal.simps) |
34 by(simp_all add: bal.simps) |
|
35 |
|
36 text\<open>The following lemmas take advantage of the fact |
|
37 that \<open>bal xs n\<close> yields a result even if \<open>n > length xs\<close>.\<close> |
|
38 |
|
39 lemma size_bal: "bal xs n = (t,ys) \<Longrightarrow> size t = n" |
|
40 proof(induction xs n arbitrary: t ys rule: bal.induct) |
|
41 case (1 xs n) |
|
42 thus ?case |
|
43 by(cases "n=0") |
|
44 (auto simp add: bal_simps Let_def split: prod.splits) |
|
45 qed |
36 |
46 |
37 lemma bal_inorder: |
47 lemma bal_inorder: |
38 "\<lbrakk> bal xs n = (t,ys); n \<le> length xs \<rbrakk> |
48 "\<lbrakk> bal xs n = (t,ys); n \<le> length xs \<rbrakk> |
39 \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs" |
49 \<Longrightarrow> inorder t = take n xs \<and> ys = drop n xs" |
40 proof(induction xs n arbitrary: t ys rule: bal.induct) |
50 proof(induction xs n arbitrary: t ys rule: bal.induct) |
154 by (simp add: balance_tree_def) |
164 by (simp add: balance_tree_def) |
155 |
165 |
156 lemma height_balance_tree: "height(balance_tree t) = floorlog 2 (size t)" |
166 lemma height_balance_tree: "height(balance_tree t) = floorlog 2 (size t)" |
157 by(simp add: balance_tree_def height_balance_list) |
167 by(simp add: balance_tree_def height_balance_list) |
158 |
168 |
|
169 lemma wbalanced_bal: "bal xs n = (t,ys) \<Longrightarrow> wbalanced t" |
|
170 proof(induction xs n arbitrary: t ys rule: bal.induct) |
|
171 case (1 xs n) |
|
172 show ?case |
|
173 proof cases |
|
174 assume "n = 0" |
|
175 thus ?thesis |
|
176 using "1.prems" by(simp add: bal_simps) |
|
177 next |
|
178 assume "n \<noteq> 0" |
|
179 with "1.prems" obtain l ys r zs where |
|
180 rec1: "bal xs (n div 2) = (l, ys)" and |
|
181 rec2: "bal (tl ys) (n - 1 - n div 2) = (r, zs)" and |
|
182 t: "t = \<langle>l, hd ys, r\<rangle>" |
|
183 by(auto simp add: bal_simps Let_def split: prod.splits) |
|
184 have l: "wbalanced l" using "1.IH"(1)[OF \<open>n\<noteq>0\<close> refl rec1] . |
|
185 have "wbalanced r" using "1.IH"(2)[OF \<open>n\<noteq>0\<close> refl rec1[symmetric] refl rec2] . |
|
186 with l t size_bal[OF rec1] size_bal[OF rec2] |
|
187 show ?thesis by auto |
|
188 qed |
|
189 qed |
|
190 |
|
191 lemma wbalanced_balance_tree: "wbalanced (balance_tree t)" |
|
192 by(simp add: balance_tree_def balance_list_def) |
|
193 (metis prod.collapse wbalanced_bal) |
|
194 |
159 hide_const (open) bal |
195 hide_const (open) bal |
160 |
196 |
161 end |
197 end |