| changeset 73442 | 855a3c18b9c8 |
| parent 73411 | 1f1366966296 |
| child 73443 | 8948519e0a78 |
--- 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>