| author | paulson <lp15@cam.ac.uk> |
| Fri, 02 Oct 2015 15:07:41 +0100 | |
| changeset 61306 | 9dd394c866fc |
| parent 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 |