| author | nipkow |
| Tue, 23 Feb 2016 16:25:08 +0100 | |
| changeset 62390 | 842917225d56 |
| parent 62160 | ff20b44b2fc8 |
| child 62650 | 7e6bb43e7217 |
| permissions | -rw-r--r-- |
| 61224 | 1 |
theory Tree2 |
2 |
imports Main |
|
3 |
begin |
|
4 |
||
5 |
datatype ('a,'b) tree =
|
|
6 |
Leaf ("\<langle>\<rangle>") |
|
|
| 62160 | 7 |
Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("(1\<langle>_,/ _,/ _,/ _\<rangle>)")
|
| 61224 | 8 |
|
9 |
fun inorder :: "('a,'b)tree \<Rightarrow> 'a list" where
|
|
10 |
"inorder Leaf = []" | |
|
11 |
"inorder (Node _ l a r) = inorder l @ a # inorder r" |
|
12 |
||
13 |
fun height :: "('a,'b) tree \<Rightarrow> nat" where
|
|
14 |
"height Leaf = 0" | |
|
15 |
"height (Node _ l a r) = max (height l) (height r) + 1" |
|
16 |
||
| 62390 | 17 |
end |