Stream: Mirror: Isabelle Users Mailing List

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


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

view this post on Zulip Email Gateway (Nov 26 2020 at 18:10):

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

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