# HG changeset patch
# User nipkow
# Date 1491026740 -7200
# Node ID 8ec91f7eca37e1d0675f498dc393a55136ad0dce
# Parent  c4531ddafe7253be146086b57479d72ec7fd1c08
tuned

diff -r c4531ddafe72 -r 8ec91f7eca37 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Mar 31 17:21:36 2017 +0200
+++ b/src/HOL/Library/Tree.thy	Sat Apr 01 08:05:40 2017 +0200
@@ -95,10 +95,10 @@
 
 subsection \<open>@{const map_tree}\<close>
 
-lemma map_tree_Leaf[simp]: "map_tree f t = Leaf \<longleftrightarrow> t = Leaf"
+lemma eq_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"
+lemma eq_Leaf_map_tree[simp]: "Leaf = map_tree f t \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 
@@ -112,10 +112,10 @@
 lemma size1_ge0[simp]: "0 < size1 t"
 by (simp add: size1_def)
 
-lemma size_0_iff_Leaf[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
+lemma eq_size_0[simp]: "size t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
-lemma Z_size_iff_Leaf[simp]: "0 = size t \<longleftrightarrow> t = Leaf"
+lemma eq_0_size[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>)"
@@ -130,10 +130,10 @@
 
 subsection \<open>@{const set_tree}\<close>
 
-lemma set_tree_empty[simp]: "set_tree t = {} \<longleftrightarrow> t = Leaf"
+lemma eq_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"
+lemma eq_empty_set_tree[simp]: "{} = set_tree t \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma finite_set_tree[simp]: "finite(set_tree t)"
@@ -142,6 +142,12 @@
 
 subsection \<open>@{const subtrees}\<close>
 
+lemma neq_subtrees_empty[simp]: "subtrees t \<noteq> {}"
+by (cases t)(auto)
+
+lemma neq_empty_subtrees[simp]: "{} \<noteq> subtrees t"
+by (cases t)(auto)
+
 lemma set_treeE: "a \<in> set_tree t \<Longrightarrow> \<exists>l r. \<langle>l, a, r\<rangle> \<in> subtrees t"
 by (induction t)(auto)
 
@@ -154,10 +160,10 @@
 
 subsection \<open>@{const height} and @{const min_height}\<close>
 
-lemma height_0_iff_Leaf[simp]: "height t = 0 \<longleftrightarrow> t = Leaf"
+lemma eq_height_0[simp]: "height t = 0 \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
-lemma Z_height_iff_Leaf[simp]: "0 = height t \<longleftrightarrow> t = Leaf"
+lemma eq_0_height[simp]: "0 = height t \<longleftrightarrow> t = Leaf"
 by(cases t) auto
 
 lemma height_map_tree[simp]: "height (map_tree f t) = height t"
@@ -226,7 +232,7 @@
 
 lemma complete_if_size1_height: "size1 t = 2 ^ height t \<Longrightarrow> complete t"
 proof (induct "height t" arbitrary: t)
-  case 0 thus ?case by (simp add: height_0_iff_Leaf)
+  case 0 thus ?case by (simp)
 next
   case (Suc h)
   hence "t \<noteq> Leaf" by auto
@@ -271,7 +277,7 @@
 
 lemma complete_if_size1_min_height: "size1 t = 2 ^ min_height t \<Longrightarrow> complete t"
 proof (induct "min_height t" arbitrary: t)
-  case 0 thus ?case by (simp add: size_0_iff_Leaf size1_def)
+  case 0 thus ?case by (simp add: size1_def)
 next
   case (Suc h)
   hence "t \<noteq> Leaf" by auto
@@ -394,10 +400,10 @@
 
 subsection "List of entries"
 
-lemma inorder_Nil_iff[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
+lemma eq_inorder_Nil[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
-lemma Nil_inorder_iff[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
+lemma eq_Nil_inorder[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"