| changeset 62650 | 7e6bb43e7217 |
| parent 62202 | e5bc7cbb0bcc |
| child 63036 | 1ba3aacfa4d3 |
--- a/src/HOL/Library/Tree.thy Fri Mar 18 08:32:37 2016 +0100 +++ b/src/HOL/Library/Tree.thy Fri Mar 18 10:14:56 2016 +0100 @@ -24,6 +24,9 @@ "size1 \<langle>l, x, r\<rangle> = size1 l + size1 r" by (simp_all add: size1_def) +lemma size1_ge0[simp]: "0 < size1 t" +by (simp add: size1_def) + lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf" by(cases t) auto