author | nipkow |
Fri, 12 Aug 2016 18:08:40 +0200 | |
changeset 63665 | 15f48ce7ec23 |
parent 63664 | 9ddc48a8635e |
child 63682 | 67cffbbca84d |
--- a/src/HOL/Library/Tree.thy Fri Aug 12 09:57:09 2016 +0200 +++ b/src/HOL/Library/Tree.thy Fri Aug 12 18:08:40 2016 +0200 @@ -58,6 +58,9 @@ end +lemma height_0_iff_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf" +by(cases t) auto + lemma height_map_tree[simp]: "height (map_tree f t) = height t" by (induction t) auto