## Stream: Mirror: Isabelle Users Mailing List

### Topic: [isabelle] superfluous assumptions in comm_append_are_rep...

#### Email Gateway (Nov 26 2020 at 12:53):

From: Stepan Holub <holub@karlin.mff.cuni.cz>
Dear all,

assumptions
xs ≠ [] and ys ≠ []
in lemma
comm_append_are_replicate
from List.thy
are superfluous.

An alternative proof follows.
(BTW, I wonder whether the way it breaks the symmetry between xs and ys
is a standard one. It is not the same one as in the original proof.)

Best regards

Stepan Holub

lemma comm_append_are_replicate:
"⟦ xs @ ys = ys @ xs ⟧
⟹ ∃m n zs. concat (replicate m zs) = xs ∧ concat (replicate n zs) = ys"
proof (induction "length (xs @ ys) + length xs" arbitrary: xs ys rule:
less_induct)
case less
consider "length ys < length xs" | "xs = []" | "length xs ≤ length ys
∧ xs ≠ []"
by linarith
then show ?case
proof (cases)
assume "length ys < length xs"
then show ?thesis
using less.hyps[OF _ less.prems[symmetric]]
next
assume "xs = []"
then have "concat (replicate 0 ys) = xs ∧ concat (replicate 1 ys) = ys"
by simp
then show ?case
by blast
next
assume "length xs ≤ length ys ∧ xs ≠ []"
then have "length xs ≤ length ys" and "xs ≠ []"
by blast+
from ‹length xs ≤ length ys› and  ‹xs @ ys = ys @ xs›
obtain ws where "ys = xs @ ws"
by (auto simp: append_eq_append_conv2)
from this and ‹xs ≠ []›
have "length ws < length ys"
by simp
from ‹xs @ ys = ys @ xs›[unfolded ‹ys = xs @ ws›]
have "xs @ ws = ws @ xs"
by simp
from less.hyps[OF _ this] ‹length ws < length ys›
obtain m n' zs where "concat (replicate m zs) = xs" and  "concat
(replicate n' zs) = ws"
by auto
then have "concat (replicate (m+n') zs) = ys"
using ‹ys = xs @ ws›
then show ?case
using ‹concat (replicate m zs) = xs› by blast
qed
qed

#### Email Gateway (Nov 26 2020 at 18:10):

From: Lawrence Paulson <lp15@cam.ac.uk>
Many thanks!
Larry

#### Email Gateway (Nov 26 2020 at 18:31):

From: Tobias Nipkow <nipkow@in.tum.de>
I just commited this, thank you.

Tobias
smime.p7s

Last updated: Dec 05 2021 at 23:19 UTC