66510
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Tree_Real
|
|
4 |
imports
|
|
5 |
Complex_Main
|
|
6 |
Tree
|
|
7 |
begin
|
|
8 |
|
|
9 |
text \<open>This theory is separate from @{theory Tree} because the former is discrete and builds on
|
|
10 |
@{theory Main} whereas this theory builds on @{theory Complex_Main}.\<close>
|
|
11 |
|
|
12 |
|
|
13 |
lemma size1_height_log: "log 2 (size1 t) \<le> height t"
|
|
14 |
by (simp add: log2_of_power_le size1_height)
|
|
15 |
|
|
16 |
lemma min_height_size1_log: "min_height t \<le> log 2 (size1 t)"
|
|
17 |
by (simp add: le_log2_of_power min_height_size1)
|
|
18 |
|
|
19 |
lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
|
|
20 |
by (simp add: log2_of_power_eq size1_if_complete)
|
|
21 |
|
|
22 |
lemma min_height_size1_log_if_incomplete:
|
|
23 |
"\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
|
|
24 |
by (simp add: less_log2_of_power min_height_size1_if_incomplete)
|
|
25 |
|
|
26 |
|
|
27 |
lemma min_height_balanced: assumes "balanced t"
|
|
28 |
shows "min_height t = nat(floor(log 2 (size1 t)))"
|
|
29 |
proof cases
|
|
30 |
assume *: "complete t"
|
|
31 |
hence "size1 t = 2 ^ min_height t"
|
|
32 |
by (simp add: complete_iff_height size1_if_complete)
|
|
33 |
from log2_of_power_eq[OF this] show ?thesis by linarith
|
|
34 |
next
|
|
35 |
assume *: "\<not> complete t"
|
|
36 |
hence "height t = min_height t + 1"
|
|
37 |
using assms min_height_le_height[of t]
|
|
38 |
by(auto simp add: balanced_def complete_iff_height)
|
|
39 |
hence "size1 t < 2 ^ (min_height t + 1)"
|
|
40 |
by (metis * size1_height_if_incomplete)
|
|
41 |
hence "log 2 (size1 t) < min_height t + 1"
|
|
42 |
using log2_of_power_less size1_ge0 by blast
|
|
43 |
thus ?thesis using min_height_size1_log[of t] by linarith
|
|
44 |
qed
|
|
45 |
|
|
46 |
lemma height_balanced: assumes "balanced t"
|
|
47 |
shows "height t = nat(ceiling(log 2 (size1 t)))"
|
|
48 |
proof cases
|
|
49 |
assume *: "complete t"
|
|
50 |
hence "size1 t = 2 ^ height t"
|
|
51 |
by (simp add: size1_if_complete)
|
|
52 |
from log2_of_power_eq[OF this] show ?thesis
|
|
53 |
by linarith
|
|
54 |
next
|
|
55 |
assume *: "\<not> complete t"
|
|
56 |
hence **: "height t = min_height t + 1"
|
|
57 |
using assms min_height_le_height[of t]
|
|
58 |
by(auto simp add: balanced_def complete_iff_height)
|
|
59 |
hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
|
|
60 |
from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
|
|
61 |
show ?thesis by linarith
|
|
62 |
qed
|
|
63 |
|
|
64 |
end |