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]]

nat_add_left_cancel_less by auto

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›

by (simp add: replicate_add)

then show ?case

using ‹concat (replicate m zs) = xs› by blast

qed

qed

From: Lawrence Paulson <lp15@cam.ac.uk>

Many thanks!

Larry

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