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