From: Stepan Holub <email@example.com>
is it useful to point out that take_all from List.thy is actually an
From: Tobias Nipkow <firstname.lastname@example.org>
Thanks for pointing this out. The existing
lemma take_all [simp]: "length xs <= n ==> take n xs = xs"
already yields two conditional rewrite rules but is indeed a bit weaker than an
equivalence. I have added
lemma take_all_iff [simp]: "(take n xs = xs) = (length xs <= n)"
lemma drop_all_iff [simp]: "(drop n xs = ) = (length xs <= n)"
locally to see what the effect is. It broke exactly one proof in the AFP and
none in the distribution. Although this is not impressive, I will probably add
it to the distribution.
Keep them coming!
Last updated: Jan 25 2022 at 01:11 UTC