added lemma
authornipkow
Fri, 12 Aug 2016 18:08:40 +0200
changeset 63665 15f48ce7ec23
parent 63664 9ddc48a8635e
child 63682 67cffbbca84d
added lemma
src/HOL/Library/Tree.thy
--- 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