## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] A lemma about remove1

#### Email Gateway (Mar 15 2021 at 13:37):

Hello,

I have proven the following lemma, which splits the result of remove1
into the items before and after the removed element. I feel like it
might be generally useful.

lemma remove1_split:
assumes "a ∈ set xs"
shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r"
using assms proof (induction xs)
case (Cons x xs)
show ?case
proof cases
assume "x = a"
show ?thesis
apply (rule exI[of _ "[]"])
using `x = a` by simp
next
assume "x ≠ a"
then have "a ∈ set xs"
using `a ∈ set (x # xs)`
by simp
then obtain l r where *: "xs = l @ a # r ∧ remove1 a xs = l @ r"
using Cons.IH by auto
show ?thesis
apply (rule exI[of _ "x # l"])
apply (rule exI[of _ r])
using `x ≠ a` * by auto
qed
qed simp

Regards,
Jakub Kądziołka

#### Email Gateway (Mar 15 2021 at 14:36):

From: Peter Lammich <lammich@in.tum.de>
Hello,

the lemma remove1_append is actually very similar, and sledgehammer
finds a very simple proof of your lemma:

lemma remove1_split:
assumes "a ∈ set xs"
shows "∃l r. xs = l @ a # r ∧ remove1 a xs = l @ r"
by (metis assms remove1.simps(2) remove1_append split_list_first)

This does not mean that this lemma is useless, as it may provide a
handier split than using remove1_append directly.

#### Email Gateway (Mar 16 2021 at 07:18):

From: Tobias Nipkow <nipkow@in.tum.de>
I have added the lemma with Peter's/sh's proof. Although a simple consequence,