author  nipkow 
Tue, 13 Sep 2016 11:31:30 +0200  
changeset 63861  90360390a916 
parent 63829  6a05c8cbf7de 
child 64414  f8be2208e99c 
permissions  rwrr 
57250  1 
(* Author: Tobias Nipkow *) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

2 
(* Todo: 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

3 
(min_)height of balanced trees via floorlog 
63770  4 
minimal path_len of balanced trees 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

5 
*) 
57250  6 

60500  7 
section \<open>Binary Tree\<close> 
57250  8 

9 
theory Tree 

10 
imports Main 

11 
begin 

12 

58424  13 
datatype 'a tree = 
62160  14 
is_Leaf: Leaf ("\<langle>\<rangle>")  
15 
Node (left: "'a tree") (val: 'a) (right: "'a tree") ("(1\<langle>_,/ _,/ _\<rangle>)") 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

16 
where 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

17 
"left Leaf = Leaf" 
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

18 
 "right Leaf = Leaf" 
57569
e20a999f7161
register tree with datatype_compat ot support QuickCheck
hoelzl
parents:
57530
diff
changeset

19 
datatype_compat tree 
57250  20 

60500  21 
text\<open>Can be seen as counting the number of leaves rather than nodes:\<close> 
58438  22 

23 
definition size1 :: "'a tree \<Rightarrow> nat" where 

24 
"size1 t = size t + 1" 

25 

63861  26 
fun subtrees :: "'a tree \<Rightarrow> 'a tree set" where 
27 
"subtrees \<langle>\<rangle> = {\<langle>\<rangle>}"  

28 
"subtrees (\<langle>l, a, r\<rangle>) = insert \<langle>l, a, r\<rangle> (subtrees l \<union> subtrees r)" 

29 

30 
fun mirror :: "'a tree \<Rightarrow> 'a tree" where 

31 
"mirror \<langle>\<rangle> = Leaf"  

32 
"mirror \<langle>l,x,r\<rangle> = \<langle>mirror r, x, mirror l\<rangle>" 

33 

34 
class height = fixes height :: "'a \<Rightarrow> nat" 

35 

36 
instantiation tree :: (type)height 

37 
begin 

38 

39 
fun height_tree :: "'a tree => nat" where 

40 
"height Leaf = 0"  

41 
"height (Node t1 a t2) = max (height t1) (height t2) + 1" 

42 

43 
instance .. 

44 

45 
end 

46 

47 
fun min_height :: "'a tree \<Rightarrow> nat" where 

48 
"min_height Leaf = 0"  

49 
"min_height (Node l _ r) = min (min_height l) (min_height r) + 1" 

50 

51 
fun complete :: "'a tree \<Rightarrow> bool" where 

52 
"complete Leaf = True"  

53 
"complete (Node l x r) = (complete l \<and> complete r \<and> height l = height r)" 

54 

55 
definition balanced :: "'a tree \<Rightarrow> bool" where 

56 
"balanced t = (height t  min_height t \<le> 1)" 

57 

58 
text \<open>Weight balanced:\<close> 

59 
fun wbalanced :: "'a tree \<Rightarrow> bool" where 

60 
"wbalanced Leaf = True"  

61 
"wbalanced (Node l x r) = (abs(int(size l)  int(size r)) \<le> 1 \<and> wbalanced l \<and> wbalanced r)" 

62 

63 
text \<open>Internal path length:\<close> 

64 
fun path_len :: "'a tree \<Rightarrow> nat" where 

65 
"path_len Leaf = 0 "  

66 
"path_len (Node l _ r) = path_len l + size l + path_len r + size r" 

67 

68 
fun preorder :: "'a tree \<Rightarrow> 'a list" where 

69 
"preorder \<langle>\<rangle> = []"  

70 
"preorder \<langle>l, x, r\<rangle> = x # preorder l @ preorder r" 

71 

72 
fun inorder :: "'a tree \<Rightarrow> 'a list" where 

73 
"inorder \<langle>\<rangle> = []"  

74 
"inorder \<langle>l, x, r\<rangle> = inorder l @ [x] @ inorder r" 

75 

76 
text\<open>A linear version avoiding append:\<close> 

77 
fun inorder2 :: "'a tree \<Rightarrow> 'a list \<Rightarrow> 'a list" where 

78 
"inorder2 \<langle>\<rangle> xs = xs"  

79 
"inorder2 \<langle>l, x, r\<rangle> xs = inorder2 l (x # inorder2 r xs)" 

80 

81 
text\<open>Binary Search Tree:\<close> 

82 
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where 

83 
"bst \<langle>\<rangle> \<longleftrightarrow> True"  

84 
"bst \<langle>l, a, r\<rangle> \<longleftrightarrow> bst l \<and> bst r \<and> (\<forall>x\<in>set_tree l. x < a) \<and> (\<forall>x\<in>set_tree r. a < x)" 

85 

86 
text\<open>Binary Search Tree with duplicates:\<close> 

87 
fun (in linorder) bst_eq :: "'a tree \<Rightarrow> bool" where 

88 
"bst_eq \<langle>\<rangle> \<longleftrightarrow> True"  

89 
"bst_eq \<langle>l,a,r\<rangle> \<longleftrightarrow> 

90 
bst_eq l \<and> bst_eq r \<and> (\<forall>x\<in>set_tree l. x \<le> a) \<and> (\<forall>x\<in>set_tree r. a \<le> x)" 

91 

92 
fun (in linorder) heap :: "'a tree \<Rightarrow> bool" where 

93 
"heap Leaf = True"  

94 
"heap (Node l m r) = 

95 
(heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))" 

96 

97 

98 
subsection \<open>@{const size}\<close> 

99 

58438  100 
lemma size1_simps[simp]: 
101 
"size1 \<langle>\<rangle> = 1" 

102 
"size1 \<langle>l, x, r\<rangle> = size1 l + size1 r" 

103 
by (simp_all add: size1_def) 

104 

62650  105 
lemma size1_ge0[simp]: "0 < size1 t" 
106 
by (simp add: size1_def) 

107 

60507  108 
lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf" 
60505  109 
by(cases t) auto 
110 

58424  111 
lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)" 
112 
by (cases t) auto 

57530  113 

57687  114 
lemma finite_set_tree[simp]: "finite(set_tree t)" 
115 
by(induction t) auto 

116 

59776  117 
lemma size_map_tree[simp]: "size (map_tree f t) = size t" 
118 
by (induction t) auto 

119 

120 
lemma size1_map_tree[simp]: "size1 (map_tree f t) = size1 t" 

121 
by (simp add: size1_def) 

122 

123 

63861  124 
subsection \<open>@{const subtrees}\<close> 
60808
fd26519b1a6a
depth > height; removed del_rightmost (too specifi)
nipkow
parents:
60507
diff
changeset

125 

63861  126 
lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t" 
127 
by (induction t)(auto) 

59776  128 

63861  129 
lemma Node_notin_subtrees_if[simp]: "a \<notin> set_tree t \<Longrightarrow> Node l a r \<notin> subtrees t" 
130 
by (induction t) auto 

59776  131 

63861  132 
lemma in_set_tree_if: "\<langle>l, a, r\<rangle> \<in> subtrees t \<Longrightarrow> a \<in> set_tree t" 
133 
by (metis Node_notin_subtrees_if) 

60808
fd26519b1a6a
depth > height; removed del_rightmost (too specifi)
nipkow
parents:
60507
diff
changeset

134 

63861  135 

136 
subsection \<open>@{const height} and @{const min_height}\<close> 

60808
fd26519b1a6a
depth > height; removed del_rightmost (too specifi)
nipkow
parents:
60507
diff
changeset

137 

63665  138 
lemma height_0_iff_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf" 
139 
by(cases t) auto 

140 

60808
fd26519b1a6a
depth > height; removed del_rightmost (too specifi)
nipkow
parents:
60507
diff
changeset

141 
lemma height_map_tree[simp]: "height (map_tree f t) = height t" 
59776  142 
by (induction t) auto 
143 

62202  144 
lemma size1_height: "size t + 1 \<le> 2 ^ height (t::'a tree)" 
145 
proof(induction t) 

146 
case (Node l a r) 

147 
show ?case 

148 
proof (cases "height l \<le> height r") 

149 
case True 

150 
have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp 

151 
also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1)) 

152 
also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2)) 

153 
also have "(2::nat) ^ height l \<le> 2 ^ height r" using True by simp 

154 
finally show ?thesis using True by (auto simp: max_def mult_2) 

155 
next 

156 
case False 

157 
have "size(Node l a r) + 1 = (size l + 1) + (size r + 1)" by simp 

158 
also have "size l + 1 \<le> 2 ^ height l" by(rule Node.IH(1)) 

159 
also have "size r + 1 \<le> 2 ^ height r" by(rule Node.IH(2)) 

160 
also have "(2::nat) ^ height r \<le> 2 ^ height l" using False by simp 

161 
finally show ?thesis using False by (auto simp: max_def mult_2) 

162 
qed 

163 
qed simp 

164 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

165 
corollary size_height: "size t \<le> 2 ^ height (t::'a tree)  1" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

166 
using size1_height[of t] by(arith) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

167 

63861  168 
lemma height_subtrees: "s \<in> subtrees t \<Longrightarrow> height s \<le> height t" 
169 
by (induction t) auto 

57687  170 

63598  171 

172 
lemma min_hight_le_height: "min_height t \<le> height t" 

173 
by(induction t) auto 

174 

175 
lemma min_height_map_tree[simp]: "min_height (map_tree f t) = min_height t" 

176 
by (induction t) auto 

177 

178 
lemma min_height_le_size1: "2 ^ min_height t \<le> size t + 1" 

179 
proof(induction t) 

180 
case (Node l a r) 

181 
have "(2::nat) ^ min_height (Node l a r) \<le> 2 ^ min_height l + 2 ^ min_height r" 

182 
by (simp add: min_def) 

183 
also have "\<dots> \<le> size(Node l a r) + 1" using Node.IH by simp 

184 
finally show ?case . 

185 
qed simp 

186 

187 

63861  188 
subsection \<open>@{const complete}\<close> 
63036  189 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

190 
lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)" 
63598  191 
apply(induction t) 
192 
apply simp 

193 
apply (simp add: min_def max_def) 

194 
by (metis le_antisym le_trans min_hight_le_height) 

195 

63770  196 
lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t" 
63036  197 
by (induction t) auto 
198 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

199 
lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t  1" 
63770  200 
using size1_if_complete[simplified size1_def] by fastforce 
201 

202 
lemma complete_if_size: "size t = 2 ^ height t  1 \<Longrightarrow> complete t" 

203 
proof (induct "height t" arbitrary: t) 

204 
case 0 thus ?case by (simp add: size_0_iff_Leaf) 

205 
next 

206 
case (Suc h) 

207 
hence "t \<noteq> Leaf" by auto 

208 
then obtain l a r where [simp]: "t = Node l a r" 

209 
by (auto simp: neq_Leaf_iff) 

210 
have 1: "height l \<le> h" and 2: "height r \<le> h" using Suc(2) by(auto) 

211 
have 3: "~ height l < h" 

212 
proof 

213 
assume 0: "height l < h" 

214 
have "size t = size l + (size r + 1)" by simp 

215 
also note size_height[of l] 

216 
also note size1_height[of r] 

217 
also have "(2::nat) ^ height l  1 < 2 ^ h  1" 

218 
using 0 by (simp add: diff_less_mono) 

219 
also have "(2::nat) ^ height r \<le> 2 ^ h" using 2 by simp 

220 
also have "(2::nat) ^ h  1 + 2 ^ h = 2 ^ (Suc h)  1" by (simp) 

221 
also have "\<dots> = size t" using Suc(2,3) by simp 

222 
finally show False by (simp add: diff_le_mono) 

223 
qed 

224 
have 4: "~ height r < h" 

225 
proof 

226 
assume 0: "height r < h" 

227 
have "size t = (size l + 1) + size r" by simp 

228 
also note size_height[of r] 

229 
also note size1_height[of l] 

230 
also have "(2::nat) ^ height r  1 < 2 ^ h  1" 

231 
using 0 by (simp add: diff_less_mono) 

232 
also have "(2::nat) ^ height l \<le> 2 ^ h" using 1 by simp 

233 
also have "(2::nat) ^ h + (2 ^ h  1) = 2 ^ (Suc h)  1" by (simp) 

234 
also have "\<dots> = size t" using Suc(2,3) by simp 

235 
finally show False by (simp add: diff_le_mono) 

236 
qed 

237 
from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+ 

238 
hence "size l = 2 ^ height l  1" "size r = 2 ^ height r  1" 

239 
using Suc(3) size_height[of l] size_height[of r] by (auto) 

240 
with * Suc(1) show ?case by simp 

241 
qed 

242 

243 
lemma complete_iff_size: "complete t \<longleftrightarrow> size t = 2 ^ height t  1" 

244 
using complete_if_size size_if_complete by blast 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

245 

182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

246 
text\<open>A better lower bound for incomplete trees:\<close> 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

247 

182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

248 
lemma min_height_le_size_if_incomplete: 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

249 
"\<not> complete t \<Longrightarrow> 2 ^ min_height t \<le> size t" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

250 
proof(induction t) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

251 
case Leaf thus ?case by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

252 
next 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

253 
case (Node l a r) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

254 
show ?case (is "?l \<le> ?r") 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

255 
proof (cases "complete l") 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

256 
case l: True thus ?thesis 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

257 
proof (cases "complete r") 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

258 
case r: True 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

259 
have "height l \<noteq> height r" using Node.prems l r by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

260 
hence "?l < 2 ^ min_height l + 2 ^ min_height r" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

261 
using l r by (simp add: min_def complete_iff_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

262 
also have "\<dots> = (size l + 1) + (size r + 1)" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

263 
using l r size_if_complete[where ?'a = 'a] 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

264 
by (simp add: complete_iff_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

265 
also have "\<dots> \<le> ?r + 1" by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

266 
finally show ?thesis by arith 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

267 
next 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

268 
case r: False 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

269 
have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

270 
also have "\<dots> \<le> size l + 1 + size r" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

271 
using Node.IH(2)[OF r] l size_if_complete[where ?'a = 'a] 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

272 
by (simp add: complete_iff_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

273 
also have "\<dots> = ?r" by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

274 
finally show ?thesis . 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

275 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

276 
next 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

277 
case l: False thus ?thesis 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

278 
proof (cases "complete r") 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

279 
case r: True 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

280 
have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" by (simp add: min_def) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

281 
also have "\<dots> \<le> size l + (size r + 1)" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

282 
using Node.IH(1)[OF l] r size_if_complete[where ?'a = 'a] 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

283 
by (simp add: complete_iff_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

284 
also have "\<dots> = ?r" by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

285 
finally show ?thesis . 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

286 
next 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

287 
case r: False 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

288 
have "?l \<le> 2 ^ min_height l + 2 ^ min_height r" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

289 
by (simp add: min_def) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

290 
also have "\<dots> \<le> size l + size r" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

291 
using Node.IH(1)[OF l] Node.IH(2)[OF r] by (simp) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

292 
also have "\<dots> \<le> ?r" by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

293 
finally show ?thesis . 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

294 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

295 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

296 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

297 

182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

298 

63861  299 
subsection \<open>@{const balanced}\<close> 
300 

301 
lemma balanced_subtreeL: "balanced (Node l x r) \<Longrightarrow> balanced l" 

302 
by(simp add: balanced_def) 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

303 

63861  304 
lemma balanced_subtreeR: "balanced (Node l x r) \<Longrightarrow> balanced r" 
305 
by(simp add: balanced_def) 

306 

307 
lemma balanced_subtrees: "\<lbrakk> balanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> balanced s" 

308 
using [[simp_depth_limit=1]] 

309 
by(induction t arbitrary: s) 

310 
(auto simp add: balanced_subtreeL balanced_subtreeR) 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

311 

182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

312 
text\<open>Balanced trees have optimal height:\<close> 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

313 

182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

314 
lemma balanced_optimal: 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

315 
fixes t :: "'a tree" and t' :: "'b tree" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

316 
assumes "balanced t" "size t \<le> size t'" shows "height t \<le> height t'" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

317 
proof (cases "complete t") 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

318 
case True 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

319 
have "(2::nat) ^ height t  1 \<le> 2 ^ height t'  1" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

320 
proof  
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

321 
have "(2::nat) ^ height t  1 = size t" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

322 
using True by (simp add: complete_iff_height size_if_complete) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

323 
also note assms(2) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

324 
also have "size t' \<le> 2 ^ height t'  1" by (rule size_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

325 
finally show ?thesis . 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

326 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

327 
thus ?thesis by (simp add: le_diff_iff) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

328 
next 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

329 
case False 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

330 
have "(2::nat) ^ min_height t < 2 ^ height t'" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

331 
proof  
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

332 
have "(2::nat) ^ min_height t \<le> size t" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

333 
by(rule min_height_le_size_if_incomplete[OF False]) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

334 
also note assms(2) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

335 
also have "size t' \<le> 2 ^ height t'  1" by(rule size_height) 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

336 
finally show ?thesis 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

337 
using power_eq_0_iff[of "2::nat" "height t'"] by linarith 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

338 
qed 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

339 
hence *: "min_height t < height t'" by simp 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

340 
have "min_height t + 1 = height t" 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

341 
using min_hight_le_height[of t] assms(1) False 
63829  342 
by (simp add: complete_iff_height balanced_def) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

343 
with * show ?thesis by arith 
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

344 
qed 
63036  345 

346 

63861  347 
subsection \<open>@{const wbalanced}\<close> 
348 

349 
lemma wbalanced_subtrees: "\<lbrakk> wbalanced t; s \<in> subtrees t \<rbrakk> \<Longrightarrow> wbalanced s" 

350 
using [[simp_depth_limit=1]] by(induction t arbitrary: s) auto 

351 

352 
(* show wbalanced \<Longrightarrow> balanced and use that in Balanced.thy *) 

353 

354 

355 
subsection \<open>@{const path_len}\<close> 

63413  356 

357 
text \<open>The internal path length of a tree:\<close> 

358 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

359 
lemma path_len_if_bal: "complete t 
63413  360 
\<Longrightarrow> path_len t = (let n = height t in 2 + n*2^n  2^(n+1))" 
361 
proof(induction t) 

362 
case (Node l x r) 

363 
have *: "2^(n+1) \<le> 2 + n*2^n" for n :: nat 

364 
by(induction n) auto 

365 
have **: "(0::nat) < 2^n" for n :: nat by simp 

366 
let ?h = "height r" 

63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

367 
show ?case using Node *[of ?h] **[of ?h] by (simp add: size_if_complete Let_def) 
63413  368 
qed simp 
369 

370 

59776  371 
subsection "List of entries" 
372 

57449
f81da03b9ebd
Library/Tree: use datatype_new, bst is an inductive predicate
hoelzl
parents:
57250
diff
changeset

373 
lemma set_inorder[simp]: "set (inorder t) = set_tree t" 
58424  374 
by (induction t) auto 
57250  375 

59776  376 
lemma set_preorder[simp]: "set (preorder t) = set_tree t" 
377 
by (induction t) auto 

378 

379 
lemma length_preorder[simp]: "length (preorder t) = size t" 

380 
by (induction t) auto 

381 

382 
lemma length_inorder[simp]: "length (inorder t) = size t" 

383 
by (induction t) auto 

384 

385 
lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)" 

386 
by (induction t) auto 

387 

388 
lemma inorder_map: "inorder (map_tree f t) = map f (inorder t)" 

389 
by (induction t) auto 

390 

63765  391 
lemma inorder2_inorder: "inorder2 t xs = inorder t @ xs" 
392 
by (induction t arbitrary: xs) auto 

393 

57687  394 

63861  395 
subsection \<open>Binary Search Tree\<close> 
59561  396 

59928  397 
lemma (in linorder) bst_eq_if_bst: "bst t \<Longrightarrow> bst_eq t" 
398 
by (induction t) (auto) 

399 

59561  400 
lemma (in linorder) bst_eq_imp_sorted: "bst_eq t \<Longrightarrow> sorted (inorder t)" 
401 
apply (induction t) 

402 
apply(simp) 

403 
by (fastforce simp: sorted_append sorted_Cons intro: less_imp_le less_trans) 

404 

59928  405 
lemma (in linorder) distinct_preorder_if_bst: "bst t \<Longrightarrow> distinct (preorder t)" 
406 
apply (induction t) 

407 
apply simp 

408 
apply(fastforce elim: order.asym) 

409 
done 

410 

411 
lemma (in linorder) distinct_inorder_if_bst: "bst t \<Longrightarrow> distinct (inorder t)" 

412 
apply (induction t) 

413 
apply simp 

414 
apply(fastforce elim: order.asym) 

415 
done 

416 

59776  417 

63861  418 
subsection \<open>@{const heap}\<close> 
60505  419 

420 

63861  421 
subsection \<open>@{const mirror}\<close> 
59561  422 

423 
lemma mirror_Leaf[simp]: "mirror t = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>" 

424 
by (induction t) simp_all 

425 

426 
lemma size_mirror[simp]: "size(mirror t) = size t" 

427 
by (induction t) simp_all 

428 

429 
lemma size1_mirror[simp]: "size1(mirror t) = size1 t" 

430 
by (simp add: size1_def) 

431 

60808
fd26519b1a6a
depth > height; removed del_rightmost (too specifi)
nipkow
parents:
60507
diff
changeset

432 
lemma height_mirror[simp]: "height(mirror t) = height t" 
59776  433 
by (induction t) simp_all 
434 

435 
lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)" 

436 
by (induction t) simp_all 

437 

438 
lemma map_mirror: "map_tree f (mirror t) = mirror (map_tree f t)" 

439 
by (induction t) simp_all 

440 

59561  441 
lemma mirror_mirror[simp]: "mirror(mirror t) = t" 
442 
by (induction t) simp_all 

443 

57250  444 
end 