# HG changeset patch
# User nipkow
# Date 1732722724 -3600
# Node ID 25978a474603a92a2a66d5b290cccfa0d1202358
# Parent  60696404b40a29d6011ecc6a1b5afc3a21740ee8# Parent  d4d34f552eec63eaa4da4bc84790fc03e062564c
merged

diff -r 60696404b40a -r 25978a474603 src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Fri Nov 22 20:21:36 2024 +0100
+++ b/src/HOL/Library/Tree.thy	Wed Nov 27 16:52:04 2024 +0100
@@ -363,12 +363,22 @@
 lemma eq_inorder_Nil[simp]: "inorder t = [] \<longleftrightarrow> t = Leaf"
 by (cases t) auto
 
-lemma eq_Nil_inorder[simp]: "[] = inorder t \<longleftrightarrow> t = Leaf"
-by (cases t) auto
+lemmas eq_Nil_inorder[simp] = eq_inorder_Nil[THEN eq_iff_swap]
 
 lemma set_inorder[simp]: "set (inorder t) = set_tree t"
 by (induction t) auto
 
+lemma preorder_eq_Nil_iff[simp]: "(preorder t = []) = (t = \<langle>\<rangle>)"
+by (cases t) auto
+
+lemmas Nil_eq_preorder_iff [simp] = preorder_eq_Nil_iff[THEN eq_iff_swap]
+
+lemma preorder_eq_Cons_iff:
+  "preorder t = x # xs \<longleftrightarrow> (\<exists> l r. t = \<langle>l, x, r\<rangle> \<and> xs = preorder l @ preorder r)"
+by (cases t) auto
+
+lemmas Cons_eq_preorder_iff = preorder_eq_Cons_iff[THEN eq_iff_swap]
+
 lemma set_preorder[simp]: "set (preorder t) = set_tree t"
 by (induction t) auto