# HG changeset patch
# User nipkow
# Date 1615845500 -3600
# Node ID 855a3c18b9c8b2fdf61bd0f50e2022a370b7a427
# Parent  f2167948157ea3d9c25cf5a87b4b49ea8d7152b0
added lemma

diff -r f2167948157e -r 855a3c18b9c8 src/HOL/List.thy
--- a/src/HOL/List.thy	Mon Mar 15 11:50:58 2021 +0100
+++ b/src/HOL/List.thy	Mon Mar 15 22:58:20 2021 +0100
@@ -4371,6 +4371,10 @@
 lemma remove1_idem: "x \<notin> set xs \<Longrightarrow> remove1 x xs = xs"
 by (induct xs) simp_all
 
+lemma remove1_split:
+  "a \<in> set xs \<Longrightarrow> \<exists>ls rs. xs = ls @ a # rs \<and> remove1 a xs = ls @ rs"
+by (metis remove1.simps(2) remove1_append split_list_first)
+
 
 subsubsection \<open>\<^const>\<open>removeAll\<close>\<close>