author  nipkow 
Wed, 03 Oct 2018 20:55:59 +0200  
changeset 69115  919a1b23c192 
parent 68999  2af022252782 
child 69117  3d3e87835ae8 
permissions  rwrr 
57250  1 
(* Author: Tobias Nipkow *) 
64887  2 
(* Todo: minimal ipl of balanced trees *) 
57250  3 

60500  4 
section \<open>Binary Tree\<close> 
57250  5 

6 
theory Tree 

7 
imports Main 

8 
begin 

9 

58424  10 
datatype 'a tree = 
64887  11 
Leaf ("\<langle>\<rangle>")  
12 
Node "'a tree" (root_val: 'a) "'a tree" ("(1\<langle>_,/ _,/ _\<rangle>)") 

57569
e20a999f7161
register tree with datatype_compat ot support QuickCheck
hoelzl
parents:
57530
diff
changeset

13 
datatype_compat tree 
57250  14 

68998  15 
text\<open>Counting the number of leaves rather than nodes:\<close> 
58438  16 

68998  17 
fun size1 :: "'a tree \<Rightarrow> nat" where 
18 
"size1 \<langle>\<rangle> = 1"  

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

58438  20 

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

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

24 

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

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

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

28 

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

30 

31 
instantiation tree :: (type)height 

32 
begin 

33 

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

35 
"height Leaf = 0"  

68999  36 
"height (Node l a r) = max (height l) (height r) + 1" 
63861  37 

38 
instance .. 

39 

40 
end 

41 

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

43 
"min_height Leaf = 0"  

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

45 

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

47 
"complete Leaf = True"  

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

49 

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

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

52 

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

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

55 
"wbalanced Leaf = True"  

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

57 

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

64887  59 
fun ipl :: "'a tree \<Rightarrow> nat" where 
60 
"ipl Leaf = 0 "  

61 
"ipl (Node l _ r) = ipl l + size l + ipl r + size r" 

63861  62 

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

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

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

66 

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

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

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

70 

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

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

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

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

75 

64925  76 
fun postorder :: "'a tree \<Rightarrow> 'a list" where 
77 
"postorder \<langle>\<rangle> = []"  

78 
"postorder \<langle>l, x, r\<rangle> = postorder l @ postorder r @ [x]" 

79 

63861  80 
text\<open>Binary Search Tree:\<close> 
66606  81 
fun bst_wrt :: "('a \<Rightarrow> 'a \<Rightarrow> bool) \<Rightarrow> 'a tree \<Rightarrow> bool" where 
82 
"bst_wrt P \<langle>\<rangle> \<longleftrightarrow> True"  

83 
"bst_wrt P \<langle>l, a, r\<rangle> \<longleftrightarrow> 

84 
bst_wrt P l \<and> bst_wrt P r \<and> (\<forall>x\<in>set_tree l. P x a) \<and> (\<forall>x\<in>set_tree r. P a x)" 

63861  85 

66606  86 
abbreviation bst :: "('a::linorder) tree \<Rightarrow> bool" where 
67399  87 
"bst \<equiv> bst_wrt (<)" 
63861  88 

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

90 
"heap Leaf = True"  

91 
"heap (Node l m r) = 

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

93 

94 

65339  95 
subsection \<open>@{const map_tree}\<close> 
96 

65340  97 
lemma eq_map_tree_Leaf[simp]: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf" 
65339  98 
by (rule tree.map_disc_iff) 
99 

65340  100 
lemma eq_Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> t = Leaf" 
65339  101 
by (cases t) auto 
102 

103 

63861  104 
subsection \<open>@{const size}\<close> 
105 

68998  106 
lemma size1_size: "size1 t = size t + 1" 
107 
by (induction t) simp_all 

58438  108 

62650  109 
lemma size1_ge0[simp]: "0 < size1 t" 
68998  110 
by (simp add: size1_size) 
62650  111 

65340  112 
lemma eq_size_0[simp]: "size t = 0 \<longleftrightarrow> t = Leaf" 
65339  113 
by(cases t) auto 
114 

65340  115 
lemma eq_0_size[simp]: "0 = size t \<longleftrightarrow> t = Leaf" 
60505  116 
by(cases t) auto 
117 

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

57530  120 

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

123 

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

68998  125 
by (simp add: size1_size) 
59776  126 

127 

65339  128 
subsection \<open>@{const set_tree}\<close> 
129 

65340  130 
lemma eq_set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf" 
65339  131 
by (cases t) auto 
132 

65340  133 
lemma eq_empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> t = Leaf" 
65339  134 
by (cases t) auto 
135 

136 
lemma finite_set_tree[simp]: "finite(set_tree t)" 

137 
by(induction t) auto 

138 

139 

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

141 

65340  142 
lemma neq_subtrees_empty[simp]: "subtrees t \<noteq> {}" 
143 
by (cases t)(auto) 

144 

145 
lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t" 

146 
by (cases t)(auto) 

147 

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

59776  150 

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

59776  153 

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

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

156 

63861  157 

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

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

159 

65340  160 
lemma eq_height_0[simp]: "height t = 0 \<longleftrightarrow> t = Leaf" 
65339  161 
by(cases t) auto 
162 

65340  163 
lemma eq_0_height[simp]: "0 = height t \<longleftrightarrow> t = Leaf" 
63665  164 
by(cases t) auto 
165 

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

166 
lemma height_map_tree[simp]: "height (map_tree f t) = height t" 
59776  167 
by (induction t) auto 
168 

64414  169 
lemma height_le_size_tree: "height t \<le> size (t::'a tree)" 
170 
by (induction t) auto 

171 

64533  172 
lemma size1_height: "size1 t \<le> 2 ^ height (t::'a tree)" 
62202  173 
proof(induction t) 
174 
case (Node l a r) 

175 
show ?case 

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

177 
case True 

64533  178 
have "size1(Node l a r) = size1 l + size1 r" by simp 
64918  179 
also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith 
180 
also have "\<dots> \<le> 2 ^ height r + 2 ^ height r" using True by simp 

64922  181 
also have "\<dots> = 2 ^ height (Node l a r)" 
64918  182 
using True by (auto simp: max_def mult_2) 
183 
finally show ?thesis . 

62202  184 
next 
185 
case False 

64533  186 
have "size1(Node l a r) = size1 l + size1 r" by simp 
64918  187 
also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" using Node.IH by arith 
188 
also have "\<dots> \<le> 2 ^ height l + 2 ^ height l" using False by simp 

62202  189 
finally show ?thesis using False by (auto simp: max_def mult_2) 
190 
qed 

191 
qed simp 

192 

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

193 
corollary size_height: "size t \<le> 2 ^ height (t::'a tree)  1" 
68998  194 
using size1_height[of t, unfolded size1_size] by(arith) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

195 

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

57687  198 

63598  199 

64540  200 
lemma min_height_le_height: "min_height t \<le> height t" 
63598  201 
by(induction t) auto 
202 

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

204 
by (induction t) auto 

205 

64533  206 
lemma min_height_size1: "2 ^ min_height t \<le> size1 t" 
63598  207 
proof(induction t) 
208 
case (Node l a r) 

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

210 
by (simp add: min_def) 

64533  211 
also have "\<dots> \<le> size1(Node l a r)" using Node.IH by simp 
63598  212 
finally show ?case . 
213 
qed simp 

214 

215 

63861  216 
subsection \<open>@{const complete}\<close> 
63036  217 

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

218 
lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)" 
63598  219 
apply(induction t) 
220 
apply simp 

221 
apply (simp add: min_def max_def) 

64540  222 
by (metis le_antisym le_trans min_height_le_height) 
63598  223 

63770  224 
lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t" 
63036  225 
by (induction t) auto 
226 

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

227 
lemma size_if_complete: "complete t \<Longrightarrow> size t = 2 ^ height t  1" 
68998  228 
using size1_if_complete[simplified size1_size] by fastforce 
63770  229 

64533  230 
lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t" 
63770  231 
proof (induct "height t" arbitrary: t) 
65340  232 
case 0 thus ?case by (simp) 
63770  233 
next 
234 
case (Suc h) 

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

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

237 
by (auto simp: neq_Leaf_iff) 

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

64533  239 
have 3: "\<not> height l < h" 
63770  240 
proof 
241 
assume 0: "height l < h" 

64533  242 
have "size1 t = size1 l + size1 r" by simp 
64918  243 
also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" 
244 
using size1_height[of l] size1_height[of r] by arith 

245 
also have " \<dots> < 2 ^ h + 2 ^ height r" using 0 by (simp) 

246 
also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 2 by (simp) 

247 
also have "\<dots> = 2 ^ (Suc h)" by (simp) 

64533  248 
also have "\<dots> = size1 t" using Suc(2,3) by simp 
64918  249 
finally have "size1 t < size1 t" . 
250 
thus False by (simp) 

63770  251 
qed 
64918  252 
have 4: "\<not> height r < h" 
63770  253 
proof 
254 
assume 0: "height r < h" 

64533  255 
have "size1 t = size1 l + size1 r" by simp 
64918  256 
also have "\<dots> \<le> 2 ^ height l + 2 ^ height r" 
257 
using size1_height[of l] size1_height[of r] by arith 

258 
also have " \<dots> < 2 ^ height l + 2 ^ h" using 0 by (simp) 

259 
also have " \<dots> \<le> 2 ^ h + 2 ^ h" using 1 by (simp) 

260 
also have "\<dots> = 2 ^ (Suc h)" by (simp) 

64533  261 
also have "\<dots> = size1 t" using Suc(2,3) by simp 
64918  262 
finally have "size1 t < size1 t" . 
263 
thus False by (simp) 

63770  264 
qed 
265 
from 1 2 3 4 have *: "height l = h" "height r = h" by linarith+ 

64533  266 
hence "size1 l = 2 ^ height l" "size1 r = 2 ^ height r" 
267 
using Suc(3) size1_height[of l] size1_height[of r] by (auto) 

63770  268 
with * Suc(1) show ?case by simp 
269 
qed 

270 

64533  271 
text\<open>The following proof involves \<open>\<ge>\<close>/\<open>>\<close> chains rather than the standard 
272 
\<open>\<le>\<close>/\<open><\<close> chains. To chain the elements together the transitivity rules \<open>xtrans\<close> 

273 
are used.\<close> 

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

274 

64533  275 
lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t" 
276 
proof (induct "min_height t" arbitrary: t) 

68998  277 
case 0 thus ?case by (simp add: size1_size) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

278 
next 
64533  279 
case (Suc h) 
280 
hence "t \<noteq> Leaf" by auto 

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

282 
by (auto simp: neq_Leaf_iff) 

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

284 
have 3: "\<not> h < min_height l" 

285 
proof 

286 
assume 0: "h < min_height l" 

287 
have "size1 t = size1 l + size1 r" by simp 

288 
also note min_height_size1[of l] 

289 
also(xtrans) note min_height_size1[of r] 

290 
also(xtrans) have "(2::nat) ^ min_height l > 2 ^ h" 

291 
using 0 by (simp add: diff_less_mono) 

292 
also(xtrans) have "(2::nat) ^ min_height r \<ge> 2 ^ h" using 2 by simp 

293 
also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp) 

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

295 
finally show False by (simp add: diff_le_mono) 

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

296 
qed 
64533  297 
have 4: "\<not> h < min_height r" 
298 
proof 

299 
assume 0: "h < min_height r" 

300 
have "size1 t = size1 l + size1 r" by simp 

301 
also note min_height_size1[of l] 

302 
also(xtrans) note min_height_size1[of r] 

303 
also(xtrans) have "(2::nat) ^ min_height r > 2 ^ h" 

304 
using 0 by (simp add: diff_less_mono) 

305 
also(xtrans) have "(2::nat) ^ min_height l \<ge> 2 ^ h" using 1 by simp 

306 
also(xtrans) have "(2::nat) ^ h + 2 ^ h = 2 ^ (Suc h)" by (simp) 

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

308 
finally show False by (simp add: diff_le_mono) 

309 
qed 

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

311 
hence "size1 l = 2 ^ min_height l" "size1 r = 2 ^ min_height r" 

312 
using Suc(3) min_height_size1[of l] min_height_size1[of r] by (auto) 

313 
with * Suc(1) show ?case 

314 
by (simp add: complete_iff_height) 

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

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

316 

64533  317 
lemma complete_iff_size1: "complete t \<longleftrightarrow> size1 t = 2 ^ height t" 
318 
using complete_if_size1_height size1_if_complete by blast 

319 

320 
text\<open>Better bounds for incomplete trees:\<close> 

321 

322 
lemma size1_height_if_incomplete: 

323 
"\<not> complete t \<Longrightarrow> size1 t < 2 ^ height t" 

324 
by (meson antisym_conv complete_iff_size1 not_le size1_height) 

325 

326 
lemma min_height_size1_if_incomplete: 

327 
"\<not> complete t \<Longrightarrow> 2 ^ min_height t < size1 t" 

328 
by (metis complete_if_size1_min_height le_less min_height_size1) 

329 

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

330 

63861  331 
subsection \<open>@{const balanced}\<close> 
332 

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

334 
by(simp add: balanced_def) 

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

335 

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

338 

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

340 
using [[simp_depth_limit=1]] 

341 
by(induction t arbitrary: s) 

342 
(auto simp add: balanced_subtreeL balanced_subtreeR) 

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

343 

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

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

345 

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

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

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

348 
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

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

350 
case True 
64924  351 
have "(2::nat) ^ height t \<le> 2 ^ height t'" 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

352 
proof  
64924  353 
have "2 ^ height t = size1 t" 
69115  354 
using True by (simp add: size1_if_complete) 
68998  355 
also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_size) 
64924  356 
also have "\<dots> \<le> 2 ^ height t'" by (rule size1_height) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

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

358 
qed 
64924  359 
thus ?thesis by (simp) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

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

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

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

363 
proof  
64533  364 
have "(2::nat) ^ min_height t < size1 t" 
365 
by(rule min_height_size1_if_incomplete[OF False]) 

68998  366 
also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_size) 
64918  367 
also have "\<dots> \<le> 2 ^ height t'" by(rule size1_height) 
368 
finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" . 

64924  369 
thus ?thesis . 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

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

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

372 
have "min_height t + 1 = height t" 
64540  373 
using min_height_le_height[of t] assms(1) False 
63829  374 
by (simp add: complete_iff_height balanced_def) 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

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

376 
qed 
63036  377 

378 

63861  379 
subsection \<open>@{const wbalanced}\<close> 
380 

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

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

383 

384 

64887  385 
subsection \<open>@{const ipl}\<close> 
63413  386 

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

388 

64923  389 
lemma ipl_if_complete_int: 
390 
"complete t \<Longrightarrow> int(ipl t) = (int(height t)  2) * 2^(height t) + 2" 

391 
apply(induction t) 

392 
apply simp 

393 
apply simp 

394 
apply (simp add: algebra_simps size_if_complete of_nat_diff) 

395 
done 

63413  396 

397 

59776  398 
subsection "List of entries" 
399 

65340  400 
lemma eq_inorder_Nil[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf" 
65339  401 
by (cases t) auto 
402 

65340  403 
lemma eq_Nil_inorder[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf" 
65339  404 
by (cases t) auto 
405 

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

406 
lemma set_inorder[simp]: "set (inorder t) = set_tree t" 
58424  407 
by (induction t) auto 
57250  408 

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

411 

64925  412 
lemma set_postorder[simp]: "set (postorder t) = set_tree t" 
413 
by (induction t) auto 

414 

59776  415 
lemma length_preorder[simp]: "length (preorder t) = size t" 
416 
by (induction t) auto 

417 

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

419 
by (induction t) auto 

420 

64925  421 
lemma length_postorder[simp]: "length (postorder t) = size t" 
422 
by (induction t) auto 

423 

59776  424 
lemma preorder_map: "preorder (map_tree f t) = map f (preorder t)" 
425 
by (induction t) auto 

426 

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

428 
by (induction t) auto 

429 

64925  430 
lemma postorder_map: "postorder (map_tree f t) = map f (postorder t)" 
431 
by (induction t) auto 

432 

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

435 

57687  436 

63861  437 
subsection \<open>Binary Search Tree\<close> 
59561  438 

66606  439 
lemma bst_wrt_mono: "(\<And>x y. P x y \<Longrightarrow> Q x y) \<Longrightarrow> bst_wrt P t \<Longrightarrow> bst_wrt Q t" 
59928  440 
by (induction t) (auto) 
441 

67399  442 
lemma bst_wrt_le_if_bst: "bst t \<Longrightarrow> bst_wrt (\<le>) t" 
66606  443 
using bst_wrt_mono less_imp_le by blast 
444 

67399  445 
lemma bst_wrt_le_iff_sorted: "bst_wrt (\<le>) t \<longleftrightarrow> sorted (inorder t)" 
59561  446 
apply (induction t) 
447 
apply(simp) 

68109  448 
by (fastforce simp: sorted_append intro: less_imp_le less_trans) 
59561  449 

67399  450 
lemma bst_iff_sorted_wrt_less: "bst t \<longleftrightarrow> sorted_wrt (<) (inorder t)" 
59928  451 
apply (induction t) 
452 
apply simp 

68109  453 
apply (fastforce simp: sorted_wrt_append) 
59928  454 
done 
455 

59776  456 

63861  457 
subsection \<open>@{const heap}\<close> 
60505  458 

459 

63861  460 
subsection \<open>@{const mirror}\<close> 
59561  461 

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

463 
by (induction t) simp_all 

464 

65339  465 
lemma Leaf_mirror[simp]: "\<langle>\<rangle> = mirror t \<longleftrightarrow> t = \<langle>\<rangle>" 
466 
using mirror_Leaf by fastforce 

467 

59561  468 
lemma size_mirror[simp]: "size(mirror t) = size t" 
469 
by (induction t) simp_all 

470 

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

68998  472 
by (simp add: size1_size) 
59561  473 

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

474 
lemma height_mirror[simp]: "height(mirror t) = height t" 
59776  475 
by (induction t) simp_all 
476 

66659  477 
lemma min_height_mirror [simp]: "min_height (mirror t) = min_height t" 
478 
by (induction t) simp_all 

479 

480 
lemma ipl_mirror [simp]: "ipl (mirror t) = ipl t" 

481 
by (induction t) simp_all 

482 

59776  483 
lemma inorder_mirror: "inorder(mirror t) = rev(inorder t)" 
484 
by (induction t) simp_all 

485 

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

487 
by (induction t) simp_all 

488 

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

491 

57250  492 
end 