66510
|
1 |
(* Author: Tobias Nipkow *)
|
|
2 |
|
|
3 |
theory Tree_Real
|
|
4 |
imports
|
|
5 |
Complex_Main
|
|
6 |
Tree
|
|
7 |
begin
|
|
8 |
|
68484
|
9 |
text \<open>
|
69593
|
10 |
This theory is separate from \<^theory>\<open>HOL-Library.Tree\<close> because the former is discrete and
|
|
11 |
builds on \<^theory>\<open>Main\<close> whereas this theory builds on \<^theory>\<open>Complex_Main\<close>.
|
68484
|
12 |
\<close>
|
66510
|
13 |
|
|
14 |
|
|
15 |
lemma size1_height_log: "log 2 (size1 t) \<le> height t"
|
|
16 |
by (simp add: log2_of_power_le size1_height)
|
|
17 |
|
|
18 |
lemma min_height_size1_log: "min_height t \<le> log 2 (size1 t)"
|
|
19 |
by (simp add: le_log2_of_power min_height_size1)
|
|
20 |
|
|
21 |
lemma size1_log_if_complete: "complete t \<Longrightarrow> height t = log 2 (size1 t)"
|
70350
|
22 |
by (simp add: size1_if_complete)
|
66510
|
23 |
|
|
24 |
lemma min_height_size1_log_if_incomplete:
|
|
25 |
"\<not> complete t \<Longrightarrow> min_height t < log 2 (size1 t)"
|
|
26 |
by (simp add: less_log2_of_power min_height_size1_if_incomplete)
|
|
27 |
|
|
28 |
|
|
29 |
lemma min_height_balanced: assumes "balanced t"
|
|
30 |
shows "min_height t = nat(floor(log 2 (size1 t)))"
|
|
31 |
proof cases
|
|
32 |
assume *: "complete t"
|
|
33 |
hence "size1 t = 2 ^ min_height t"
|
|
34 |
by (simp add: complete_iff_height size1_if_complete)
|
|
35 |
from log2_of_power_eq[OF this] show ?thesis by linarith
|
|
36 |
next
|
|
37 |
assume *: "\<not> complete t"
|
|
38 |
hence "height t = min_height t + 1"
|
|
39 |
using assms min_height_le_height[of t]
|
69117
|
40 |
by(auto simp: balanced_def complete_iff_height)
|
|
41 |
hence "size1 t < 2 ^ (min_height t + 1)" by (metis * size1_height_if_incomplete)
|
|
42 |
from floor_log_nat_eq_if[OF min_height_size1 this] show ?thesis by simp
|
66510
|
43 |
qed
|
|
44 |
|
|
45 |
lemma height_balanced: assumes "balanced t"
|
|
46 |
shows "height t = nat(ceiling(log 2 (size1 t)))"
|
|
47 |
proof cases
|
|
48 |
assume *: "complete t"
|
69117
|
49 |
hence "size1 t = 2 ^ height t" by (simp add: size1_if_complete)
|
|
50 |
from log2_of_power_eq[OF this] show ?thesis by linarith
|
66510
|
51 |
next
|
|
52 |
assume *: "\<not> complete t"
|
|
53 |
hence **: "height t = min_height t + 1"
|
|
54 |
using assms min_height_le_height[of t]
|
|
55 |
by(auto simp add: balanced_def complete_iff_height)
|
|
56 |
hence "size1 t \<le> 2 ^ (min_height t + 1)" by (metis size1_height)
|
69117
|
57 |
from log2_of_power_le[OF this size1_ge0] min_height_size1_log_if_incomplete[OF *] **
|
66510
|
58 |
show ?thesis by linarith
|
|
59 |
qed
|
|
60 |
|
66515
|
61 |
lemma balanced_Node_if_wbal1:
|
|
62 |
assumes "balanced l" "balanced r" "size l = size r + 1"
|
|
63 |
shows "balanced \<langle>l, x, r\<rangle>"
|
|
64 |
proof -
|
68998
|
65 |
from assms(3) have [simp]: "size1 l = size1 r + 1" by(simp add: size1_size)
|
66515
|
66 |
have "nat \<lceil>log 2 (1 + size1 r)\<rceil> \<ge> nat \<lceil>log 2 (size1 r)\<rceil>"
|
|
67 |
by(rule nat_mono[OF ceiling_mono]) simp
|
|
68 |
hence 1: "height(Node l x r) = nat \<lceil>log 2 (1 + size1 r)\<rceil> + 1"
|
|
69 |
using height_balanced[OF assms(1)] height_balanced[OF assms(2)]
|
|
70 |
by (simp del: nat_ceiling_le_eq add: max_def)
|
|
71 |
have "nat \<lfloor>log 2 (1 + size1 r)\<rfloor> \<ge> nat \<lfloor>log 2 (size1 r)\<rfloor>"
|
|
72 |
by(rule nat_mono[OF floor_mono]) simp
|
|
73 |
hence 2: "min_height(Node l x r) = nat \<lfloor>log 2 (size1 r)\<rfloor> + 1"
|
|
74 |
using min_height_balanced[OF assms(1)] min_height_balanced[OF assms(2)]
|
|
75 |
by (simp)
|
68998
|
76 |
have "size1 r \<ge> 1" by(simp add: size1_size)
|
66515
|
77 |
then obtain i where i: "2 ^ i \<le> size1 r" "size1 r < 2 ^ (i + 1)"
|
|
78 |
using ex_power_ivl1[of 2 "size1 r"] by auto
|
|
79 |
hence i1: "2 ^ i < size1 r + 1" "size1 r + 1 \<le> 2 ^ (i + 1)" by auto
|
|
80 |
from 1 2 floor_log_nat_eq_if[OF i] ceiling_log_nat_eq_if[OF i1]
|
|
81 |
show ?thesis by(simp add:balanced_def)
|
|
82 |
qed
|
|
83 |
|
|
84 |
lemma balanced_sym: "balanced \<langle>l, x, r\<rangle> \<Longrightarrow> balanced \<langle>r, y, l\<rangle>"
|
|
85 |
by(auto simp: balanced_def)
|
|
86 |
|
|
87 |
lemma balanced_Node_if_wbal2:
|
|
88 |
assumes "balanced l" "balanced r" "abs(int(size l) - int(size r)) \<le> 1"
|
|
89 |
shows "balanced \<langle>l, x, r\<rangle>"
|
|
90 |
proof -
|
|
91 |
have "size l = size r \<or> (size l = size r + 1 \<or> size r = size l + 1)" (is "?A \<or> ?B")
|
|
92 |
using assms(3) by linarith
|
|
93 |
thus ?thesis
|
|
94 |
proof
|
|
95 |
assume "?A"
|
|
96 |
thus ?thesis using assms(1,2)
|
|
97 |
apply(simp add: balanced_def min_def max_def)
|
|
98 |
by (metis assms(1,2) balanced_optimal le_antisym le_less)
|
|
99 |
next
|
|
100 |
assume "?B"
|
|
101 |
thus ?thesis
|
|
102 |
by (meson assms(1,2) balanced_sym balanced_Node_if_wbal1)
|
|
103 |
qed
|
|
104 |
qed
|
|
105 |
|
|
106 |
lemma balanced_if_wbalanced: "wbalanced t \<Longrightarrow> balanced t"
|
|
107 |
proof(induction t)
|
|
108 |
case Leaf show ?case by (simp add: balanced_def)
|
|
109 |
next
|
|
110 |
case (Node l x r)
|
|
111 |
thus ?case by(simp add: balanced_Node_if_wbal2)
|
|
112 |
qed
|
|
113 |
|
67399
|
114 |
end
|