author  nipkow 
Fri, 20 Jan 2017 12:44:44 +0100  
changeset 64925  5eda89787621 
parent 64924  a410e8403957 
child 65339  c4531ddafe72 
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 

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

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

78 

63861  79 
text\<open>Binary Search Tree:\<close> 
80 
fun (in linorder) bst :: "'a tree \<Rightarrow> bool" where 

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

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

83 

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

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

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

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

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

89 

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

91 
"heap Leaf = True"  

92 
"heap (Node l m r) = 

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

94 

95 

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

97 

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

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

101 
by (simp_all add: size1_def) 

102 

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

105 

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

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

57530  111 

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

114 

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

117 

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

119 
by (simp add: size1_def) 

120 

121 

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

123 

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

59776  126 

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

59776  129 

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

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

132 

63861  133 

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

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

135 

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

138 

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

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

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

144 

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

148 
show ?case 

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

150 
case True 

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

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

62202  157 
next 
158 
case False 

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

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

164 
qed simp 

165 

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

166 
corollary size_height: "size t \<le> 2 ^ height (t::'a tree)  1" 
64533  167 
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

168 

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

57687  171 

63598  172 

64540  173 
lemma min_height_le_height: "min_height t \<le> height t" 
63598  174 
by(induction t) auto 
175 

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

177 
by (induction t) auto 

178 

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

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

183 
by (simp add: min_def) 

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

187 

188 

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

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

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

194 
apply (simp add: min_def max_def) 

64540  195 
by (metis le_antisym le_trans min_height_le_height) 
63598  196 

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

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

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

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

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

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

210 
by (auto simp: neq_Leaf_iff) 

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

64533  212 
have 3: "\<not> height l < h" 
63770  213 
proof 
214 
assume 0: "height l < h" 

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

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

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

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

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

63770  224 
qed 
64918  225 
have 4: "\<not> height r < h" 
63770  226 
proof 
227 
assume 0: "height r < h" 

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

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

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

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

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

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

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

63770  241 
with * Suc(1) show ?case by simp 
242 
qed 

243 

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

246 
are used.\<close> 

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

247 

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

250 
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

251 
next 
64533  252 
case (Suc h) 
253 
hence "t \<noteq> Leaf" by auto 

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

255 
by (auto simp: neq_Leaf_iff) 

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

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

258 
proof 

259 
assume 0: "h < min_height l" 

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

261 
also note min_height_size1[of l] 

262 
also(xtrans) note min_height_size1[of r] 

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

264 
using 0 by (simp add: diff_less_mono) 

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

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

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

268 
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

269 
qed 
64533  270 
have 4: "\<not> h < min_height r" 
271 
proof 

272 
assume 0: "h < min_height r" 

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

274 
also note min_height_size1[of l] 

275 
also(xtrans) note min_height_size1[of r] 

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

277 
using 0 by (simp add: diff_less_mono) 

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

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

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

281 
finally show False by (simp add: diff_le_mono) 

282 
qed 

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

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

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

286 
with * Suc(1) show ?case 

287 
by (simp add: complete_iff_height) 

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

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

289 

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

292 

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

294 

295 
lemma size1_height_if_incomplete: 

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

297 
by (meson antisym_conv complete_iff_size1 not_le size1_height) 

298 

299 
lemma min_height_size1_if_incomplete: 

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

301 
by (metis complete_if_size1_min_height le_less min_height_size1) 

302 

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

303 

63861  304 
subsection \<open>@{const balanced}\<close> 
305 

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

307 
by(simp add: balanced_def) 

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

308 

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

311 

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

313 
using [[simp_depth_limit=1]] 

314 
by(induction t arbitrary: s) 

315 
(auto simp add: balanced_subtreeL balanced_subtreeR) 

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

316 

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

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

318 

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

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

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

321 
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

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

323 
case True 
64924  324 
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

325 
proof  
64924  326 
have "2 ^ height t = size1 t" 
327 
using True by (simp add: complete_iff_height size1_if_complete) 

328 
also have "\<dots> \<le> size1 t'" using assms(2) by(simp add: size1_def) 

329 
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

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

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

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

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

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

336 
proof  
64533  337 
have "(2::nat) ^ min_height t < size1 t" 
338 
by(rule min_height_size1_if_incomplete[OF False]) 

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

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

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

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

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

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

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

349 
qed 
63036  350 

351 

63861  352 
subsection \<open>@{const wbalanced}\<close> 
353 

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

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

356 

357 

64887  358 
subsection \<open>@{const ipl}\<close> 
63413  359 

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

361 

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

364 
apply(induction t) 

365 
apply simp 

366 
apply simp 

367 
apply (simp add: algebra_simps size_if_complete of_nat_diff) 

368 
done 

63413  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 

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

381 

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

384 

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

386 
by (induction t) auto 

387 

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

390 

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

393 

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

395 
by (induction t) auto 

396 

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

399 

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

402 

57687  403 

63861  404 
subsection \<open>Binary Search Tree\<close> 
59561  405 

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

408 

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

411 
apply(simp) 

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

413 

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

416 
apply simp 

417 
apply(fastforce elim: order.asym) 

418 
done 

419 

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

421 
apply (induction t) 

422 
apply simp 

423 
apply(fastforce elim: order.asym) 

424 
done 

425 

59776  426 

63861  427 
subsection \<open>@{const heap}\<close> 
60505  428 

429 

63861  430 
subsection \<open>@{const mirror}\<close> 
59561  431 

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

433 
by (induction t) simp_all 

434 

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

436 
by (induction t) simp_all 

437 

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

439 
by (simp add: size1_def) 

440 

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

441 
lemma height_mirror[simp]: "height(mirror t) = height t" 
59776  442 
by (induction t) simp_all 
443 

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

445 
by (induction t) simp_all 

446 

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

448 
by (induction t) simp_all 

449 

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

452 

57250  453 
end 