equal
deleted
inserted
replaced
12 |
12 |
13 fun height :: "('a,'b) tree \<Rightarrow> nat" where |
13 fun height :: "('a,'b) tree \<Rightarrow> nat" where |
14 "height Leaf = 0" | |
14 "height Leaf = 0" | |
15 "height (Node _ l a r) = max (height l) (height r) + 1" |
15 "height (Node _ l a r) = max (height l) (height r) + 1" |
16 |
16 |
|
17 definition size1 :: "('a,'b) tree \<Rightarrow> nat" where |
|
18 "size1 t = size t + 1" |
|
19 |
|
20 lemma size1_simps[simp]: |
|
21 "size1 \<langle>\<rangle> = 1" |
|
22 "size1 \<langle>u, l, x, r\<rangle> = size1 l + size1 r" |
|
23 by (simp_all add: size1_def) |
|
24 |
|
25 lemma size1_ge0[simp]: "0 < size1 t" |
|
26 by (simp add: size1_def) |
|
27 |
17 end |
28 end |