2 |
2 |
3 section \<open>Creating Balanced Trees\<close> |
3 section \<open>Creating Balanced Trees\<close> |
4 |
4 |
5 theory Balance |
5 theory Balance |
6 imports |
6 imports |
7 Complex_Main |
7 "HOL-Library.Tree_Real" |
8 "HOL-Library.Tree" |
|
9 begin |
8 begin |
10 |
|
11 (* The following two lemmas should go into theory \<open>Tree\<close>, except that that |
|
12 theory would then depend on \<open>Complex_Main\<close>. *) |
|
13 |
|
14 lemma min_height_balanced: assumes "balanced t" |
|
15 shows "min_height t = nat(floor(log 2 (size1 t)))" |
|
16 proof cases |
|
17 assume *: "complete t" |
|
18 hence "size1 t = 2 ^ min_height t" |
|
19 by (simp add: complete_iff_height size1_if_complete) |
|
20 hence "size1 t = 2 powr min_height t" |
|
21 using * by (simp add: powr_realpow) |
|
22 hence "min_height t = log 2 (size1 t)" |
|
23 by simp |
|
24 thus ?thesis |
|
25 by linarith |
|
26 next |
|
27 assume *: "\<not> complete t" |
|
28 hence "height t = min_height t + 1" |
|
29 using assms min_height_le_height[of t] |
|
30 by(auto simp add: balanced_def complete_iff_height) |
|
31 hence "2 ^ min_height t \<le> size1 t \<and> size1 t < 2 ^ (min_height t + 1)" |
|
32 by (metis * min_height_size1 size1_height_if_incomplete) |
|
33 hence "2 powr min_height t \<le> size1 t \<and> size1 t < 2 powr (min_height t + 1)" |
|
34 by(simp only: powr_realpow) |
|
35 (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power) |
|
36 hence "min_height t \<le> log 2 (size1 t) \<and> log 2 (size1 t) < min_height t + 1" |
|
37 by(simp add: log_less_iff le_log_iff) |
|
38 thus ?thesis by linarith |
|
39 qed |
|
40 |
|
41 lemma height_balanced: assumes "balanced t" |
|
42 shows "height t = nat(ceiling(log 2 (size1 t)))" |
|
43 proof cases |
|
44 assume *: "complete t" |
|
45 hence "size1 t = 2 ^ height t" |
|
46 by (simp add: size1_if_complete) |
|
47 hence "size1 t = 2 powr height t" |
|
48 using * by (simp add: powr_realpow) |
|
49 hence "height t = log 2 (size1 t)" |
|
50 by simp |
|
51 thus ?thesis |
|
52 by linarith |
|
53 next |
|
54 assume *: "\<not> complete t" |
|
55 hence **: "height t = min_height t + 1" |
|
56 using assms min_height_le_height[of t] |
|
57 by(auto simp add: balanced_def complete_iff_height) |
|
58 hence 0: "2 ^ min_height t < size1 t \<and> size1 t \<le> 2 ^ (min_height t + 1)" |
|
59 by (metis "*" min_height_size1_if_incomplete size1_height) |
|
60 hence "2 powr min_height t < size1 t \<and> size1 t \<le> 2 powr (min_height t + 1)" |
|
61 by(simp only: powr_realpow) |
|
62 (metis of_nat_less_iff of_nat_le_iff of_nat_numeral of_nat_power) |
|
63 hence "min_height t < log 2 (size1 t) \<and> log 2 (size1 t) \<le> min_height t + 1" |
|
64 by(simp add: log_le_iff less_log_iff) |
|
65 thus ?thesis using ** by linarith |
|
66 qed |
|
67 |
9 |
68 (* mv *) |
10 (* mv *) |
69 |
11 |
70 text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized |
12 text \<open>The lemmas about \<open>floor\<close> and \<open>ceiling\<close> of \<open>log 2\<close> should be generalized |
71 from 2 to \<open>n\<close> and should be made executable. In the end they should be moved |
13 from 2 to \<open>n\<close> and should be made executable. In the end they should be moved |