From: Stepan Holub <holub@karlin.mff.cuni.cz>

Hello,

is it useful to point out that take_all from List.thy is actually an

equivalence?

Best regards

Stepan

From: Tobias Nipkow <nipkow@in.tum.de>

Dear Stepan,

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!

Tobias

smime.p7s

Last updated: Jan 25 2022 at 01:11 UTC