author | nipkow |
Tue, 22 Sep 2015 08:38:25 +0200 | |
changeset 61224 | 759b5299a9f2 |
child 62160 | ff20b44b2fc8 |
permissions | -rw-r--r-- |
61224 | 1 |
theory Tree2 |
2 |
imports Main |
|
3 |
begin |
|
4 |
||
5 |
datatype ('a,'b) tree = |
|
6 |
Leaf ("\<langle>\<rangle>") | |
|
7 |
Node 'b "('a,'b)tree" 'a "('a,'b) tree" ("\<langle>_, _, _, _\<rangle>") |
|
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 |
||
17 |
end |