1(* Author: Tobias Nipkow *)
2
3section \<open>2-3 Trees\<close>
4
5theory Tree23
6imports Main
7begin
8
9class height =
10fixes height :: "'a \<Rightarrow> nat"
11
12datatype 'a tree23 =
13  Leaf ("\<langle>\<rangle>") |
14  Node2 "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _\<rangle>") |
15  Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23"  ("\<langle>_, _, _, _, _\<rangle>")
16
17fun inorder :: "'a tree23 \<Rightarrow> 'a list" where
18"inorder Leaf = []" |
19"inorder(Node2 l a r) = inorder l @ a # inorder r" |
20"inorder(Node3 l a m b r) = inorder l @ a # inorder m @ b # inorder r"
21
22
23instantiation tree23 :: (type)height
24begin
25
26fun height_tree23 :: "'a tree23 \<Rightarrow> nat" where
27"height Leaf = 0" |
28"height (Node2 l _ r) = Suc(max (height l) (height r))" |
29"height (Node3 l _ m _ r) = Suc(max (height l) (max (height m) (height r)))"
30
31instance ..
32
33end
34
35text \<open>Balanced:\<close>
36
37fun bal :: "'a tree23 \<Rightarrow> bool" where
38"bal Leaf = True" |
39"bal (Node2 l _ r) = (bal l & bal r & height l = height r)" |
40"bal (Node3 l _ m _ r) =
41  (bal l & bal m & bal r & height l = height m & height m = height r)"
42
43lemma ht_sz_if_bal: "bal t \<Longrightarrow> 2 ^ height t \<le> size t + 1"
44by (induction t) auto
45
46end
47