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