diff -r 2ffda850f844 -r c4531ddafe72 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Thu Mar 23 17:20:47 2017 +0100
+++ b/src/HOL/Library/Tree.thy	Fri Mar 31 17:21:36 2017 +0200
@@ -93,6 +93,15 @@
   (heap l \<and> heap r \<and> (\<forall>x \<in> set_tree l \<union> set_tree r. m \<le> x))"
 
 
+subsection \<open>@{const map_tree}\<close>
+
+lemma map_tree_Leaf[simp]: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf"
+by (rule tree.map_disc_iff)
+
+lemma Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
+
 subsection \<open>@{const size}\<close>
 
 lemma size1_simps[simp]:
@@ -103,15 +112,15 @@
 lemma size1_ge0[simp]: "0 < size1 t"
 by (simp add: size1_def)
 
-lemma size_0_iff_Leaf: "size t = 0 \<longleftrightarrow> t = Leaf"
+lemma size_0_iff_Leaf[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma Z_size_iff_Leaf[simp]: "0 = size t \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma neq_Leaf_iff: "(t \<noteq> \<langle>\<rangle>) = (\<exists>l a r. t = \<langle>l, a, r\<rangle>)"
 by (cases t) auto
 
-lemma finite_set_tree[simp]: "finite(set_tree t)"
-by(induction t) auto
-
 lemma size_map_tree[simp]: "size (map_tree f t) = size t"
 by (induction t) auto
 
@@ -119,6 +128,18 @@
 by (simp add: size1_def)
 
 
+subsection \<open>@{const set_tree}\<close>
+
+lemma set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
+lemma empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
+lemma finite_set_tree[simp]: "finite(set_tree t)"
+by(induction t) auto
+
+
 subsection \<open>@{const subtrees}\<close>
 
 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
@@ -133,7 +154,10 @@
 
 subsection \<open>@{const height} and @{const min_height}\<close>
 
-lemma height_0_iff_Leaf: "height t = 0 \<longleftrightarrow> t = Leaf"
+lemma height_0_iff_Leaf[simp]: "height t = 0 \<longleftrightarrow> t = Leaf"
+by(cases t) auto
+
+lemma Z_height_iff_Leaf[simp]: "0 = height t \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
@@ -370,6 +394,12 @@
 
 subsection "List of entries"
 
+lemma inorder_Nil_iff[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
+lemma Nil_inorder_iff[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
+by (cases t) auto
+
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
@@ -432,6 +462,9 @@
 lemma mirror_Leaf[simp]: "mirror t = \<langle>\<rangle> \<longleftrightarrow> t = \<langle>\<rangle>"
 by (induction t) simp_all
 
+lemma Leaf_mirror[simp]: "\<langle>\<rangle> = mirror t \<longleftrightarrow> t = \<langle>\<rangle>"
+using mirror_Leaf by fastforce
+
 lemma size_mirror[simp]: "size(mirror t) = size t"
 by (induction t) simp_all