Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] A lemma about remove1


view this post on Zulip Email Gateway (Mar 15 2021 at 13:37):

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

view this post on Zulip 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.

view this post on Zulip 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,
it does indeed look helpful.

Thanks
Tobias
smime.p7s


Last updated: Oct 25 2021 at 20:20 UTC