Email Gateway (Nov 26 2020 at 12:53): 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]]
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
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: Jan 04 2025 at 20:18 UTC