Stream: Mirror: Isabelle Users Mailing List

Topic: [isabelle] take_all is equivalence

Email Gateway (Dec 08 2020 at 13:31):

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

Email Gateway (Dec 08 2020 at 21:06):

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 04 2025 at 20:18 UTC