diff -r 3fab5b28027d -r d4d34f552eec src/HOL/Library/Tree.thy
--- a/src/HOL/Library/Tree.thy	Sun Nov 17 21:20:26 2024 +0100
+++ b/src/HOL/Library/Tree.thy	Wed Nov 27 16:51:50 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