From: Stepan Holub <firstname.lastname@example.org>
is it useful to point out that take_all from List.thy is actually an
From: Tobias Nipkow <email@example.com>
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: Dec 05 2021 at 23:19 UTC