author  nipkow 
Thu, 19 Jan 2017 17:24:05 +0100  
changeset 64923  7c340dcbc323 
parent 64922  3fb4d7d00230 
child 64924  a410e8403957 
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 

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

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

18 
"size1 t = size t + 1" 

19 

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

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

23 

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

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

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

27 

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

29 

30 
instantiation tree :: (type)height 

31 
begin 

32 

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

34 
"height Leaf = 0"  

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

36 

37 
instance .. 

38 

39 
end 

40 

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

42 
"min_height Leaf = 0"  

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

44 

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

46 
"complete Leaf = True"  

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

48 

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

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

51 

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

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

54 
"wbalanced Leaf = True"  

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

56 

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

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

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

63861  61 

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

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

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

65 

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

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

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

69 

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

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

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

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

74 

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

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

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

78 
"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)" 

79 

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

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

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

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

84 
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)" 

85 

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

87 
"heap Leaf = True"  

88 
"heap (Node l m r) = 

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

90 

91 

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

93 

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

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

97 
by (simp_all add: size1_def) 

98 

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

101 

60507  102 
lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf" 
60505  103 
by(cases t) auto 
104 

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

57530  107 

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

110 

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

113 

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

115 
by (simp add: size1_def) 

116 

117 

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

119 

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

59776  122 

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

59776  125 

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

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

128 

63861  129 

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

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

131 

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

134 

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

135 
lemma height_map_tree[simp]: "height (map_tree f t) = height t" 
59776  136 
by (induction t) auto 
137 

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

140 

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

144 
show ?case 

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

146 
case True 

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

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

62202  153 
next 
154 
case False 

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

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

160 
qed simp 

161 

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

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

164 

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

57687  167 

63598  168 

64540  169 
lemma min_height_le_height: "min_height t \<le> height t" 
63598  170 
by(induction t) auto 
171 

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

173 
by (induction t) auto 

174 

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

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

179 
by (simp add: min_def) 

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

183 

184 

63861  185 
subsection \<open>@{const complete}\<close> 
63036  186 

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

187 
lemma complete_iff_height: "complete t \<longleftrightarrow> (min_height t = height t)" 
63598  188 
apply(induction t) 
189 
apply simp 

190 
apply (simp add: min_def max_def) 

64540  191 
by (metis le_antisym le_trans min_height_le_height) 
63598  192 

63770  193 
lemma size1_if_complete: "complete t \<Longrightarrow> size1 t = 2 ^ height t" 
63036  194 
by (induction t) auto 
195 

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

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

64533  199 
lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t" 
63770  200 
proof (induct "height t" arbitrary: t) 
64533  201 
case 0 thus ?case by (simp add: height_0_iff_Leaf) 
63770  202 
next 
203 
case (Suc h) 

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

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

206 
by (auto simp: neq_Leaf_iff) 

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

64533  208 
have 3: "\<not> height l < h" 
63770  209 
proof 
210 
assume 0: "height l < h" 

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

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

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

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

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

63770  220 
qed 
64918  221 
have 4: "\<not> height r < h" 
63770  222 
proof 
223 
assume 0: "height r < h" 

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

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

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

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

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

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

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

63770  237 
with * Suc(1) show ?case by simp 
238 
qed 

239 

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

242 
are used.\<close> 

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

243 

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

246 
case 0 thus ?case by (simp add: size_0_iff_Leaf size1_def) 

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

247 
next 
64533  248 
case (Suc h) 
249 
hence "t \<noteq> Leaf" by auto 

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

251 
by (auto simp: neq_Leaf_iff) 

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

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

254 
proof 

255 
assume 0: "h < min_height l" 

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

257 
also note min_height_size1[of l] 

258 
also(xtrans) note min_height_size1[of r] 

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

260 
using 0 by (simp add: diff_less_mono) 

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

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

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

264 
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

265 
qed 
64533  266 
have 4: "\<not> h < min_height r" 
267 
proof 

268 
assume 0: "h < min_height r" 

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

270 
also note min_height_size1[of l] 

271 
also(xtrans) note min_height_size1[of r] 

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

273 
using 0 by (simp add: diff_less_mono) 

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

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

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

277 
finally show False by (simp add: diff_le_mono) 

278 
qed 

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

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

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

282 
with * Suc(1) show ?case 

283 
by (simp add: complete_iff_height) 

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

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

285 

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

288 

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

290 

291 
lemma size1_height_if_incomplete: 

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

293 
by (meson antisym_conv complete_iff_size1 not_le size1_height) 

294 

295 
lemma min_height_size1_if_incomplete: 

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

297 
by (metis complete_if_size1_min_height le_less min_height_size1) 

298 

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

299 

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

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

303 
by(simp add: balanced_def) 

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

304 

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

307 

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

309 
using [[simp_depth_limit=1]] 

310 
by(induction t arbitrary: s) 

311 
(auto simp add: balanced_subtreeL balanced_subtreeR) 

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

312 

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

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

314 

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

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

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

317 
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

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

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

320 
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

321 
proof  
64918  322 
have "2 ^ height t  1 = size t" 
63755
182c111190e5
Renamed balanced to complete; added balanced; more about both
nipkow
parents:
63665
diff
changeset

323 
using True by (simp add: complete_iff_height size_if_complete) 
64918  324 
also have "\<dots> \<le> size t'" by(rule assms(2)) 
325 
also have "\<dots> \<le> 2 ^ height t'  1" by (rule size_height) 

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

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

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

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

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

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

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

332 
proof  
64533  333 
have "(2::nat) ^ min_height t < size1 t" 
334 
by(rule min_height_size1_if_incomplete[OF False]) 

64918  335 
also have "\<dots> \<le> size1 t'" using assms(2) by (simp add: size1_def) 
336 
also have "\<dots> \<le> 2 ^ height t'" by(rule size1_height) 

337 
finally have "(2::nat) ^ min_height t < (2::nat) ^ height t'" . 

338 
thus ?thesis 

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

339 
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

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

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

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

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

346 
qed 
63036  347 

348 

63861  349 
subsection \<open>@{const wbalanced}\<close> 
350 

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

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

353 

354 

64887  355 
subsection \<open>@{const ipl}\<close> 
63413  356 

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

358 

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

361 
apply(induction t) 

362 
apply simp 

363 
apply simp 

364 
apply (simp add: algebra_simps size_if_complete of_nat_diff) 

365 
done 

63413  366 

367 

59776  368 
subsection "List of entries" 
369 

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

370 
lemma set_inorder[simp]: "set (inorder t) = set_tree t" 
58424  371 
by (induction t) auto 
57250  372 

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

375 

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

377 
by (induction t) auto 

378 

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

380 
by (induction t) auto 

381 

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

383 
by (induction t) auto 

384 

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

386 
by (induction t) auto 

387 

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

390 

57687  391 

63861  392 
subsection \<open>Binary Search Tree\<close> 
59561  393 

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

396 

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

399 
apply(simp) 

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

401 

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

404 
apply simp 

405 
apply(fastforce elim: order.asym) 

406 
done 

407 

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

409 
apply (induction t) 

410 
apply simp 

411 
apply(fastforce elim: order.asym) 

412 
done 

413 

59776  414 

63861  415 
subsection \<open>@{const heap}\<close> 
60505  416 

417 

63861  418 
subsection \<open>@{const mirror}\<close> 
59561  419 

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

421 
by (induction t) simp_all 

422 

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

424 
by (induction t) simp_all 

425 

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

427 
by (simp add: size1_def) 

428 

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

429 
lemma height_mirror[simp]: "height(mirror t) = height t" 
59776  430 
by (induction t) simp_all 
431 

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

433 
by (induction t) simp_all 

434 

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

436 
by (induction t) simp_all 

437 

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

440 

57250  441 
end 