From: Jakub Kądziołka <kuba@kadziolka.net>

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

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.

From: Tobias Nipkow <nipkow@in.tum.de>

I have added the lemma with Peter's/sh's proof. Although a simple consequence,

it does indeed look helpful.

Thanks

Tobias

smime.p7s

Last updated: Sep 25 2021 at 09:17 UTC