equal
deleted
inserted
replaced
|
1 (* Author: Tobias Nipkow *) |
|
2 |
|
3 section \<open>2-3 Trees\<close> |
|
4 |
|
5 theory Tree23 |
|
6 imports Main |
|
7 begin |
|
8 |
|
9 class height = |
|
10 fixes height :: "'a \<Rightarrow> nat" |
|
11 |
|
12 datatype 'a tree23 = |
|
13 Leaf | |
|
14 Node2 "'a tree23" 'a "'a tree23" | |
|
15 Node3 "'a tree23" 'a "'a tree23" 'a "'a tree23" |
|
16 |
|
17 fun 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 |
|
23 instantiation tree23 :: (type)height |
|
24 begin |
|
25 |
|
26 fun 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 |
|
31 instance .. |
|
32 |
|
33 end |
|
34 |
|
35 text \<open>Balanced:\<close> |
|
36 |
|
37 fun 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 |
|
43 end |