Re: [isabelle] HOL/List.thy lemma suggestions



I had been afraid that if I add these lemmas I would open the floodgates for many similar generalizations. But having looked at the existing lemmas, I found that this fear was unjustified and I added them:
http://isabelle.in.tum.de/repos/isabelle/diff/a477f78a9365/src/HOL/List.thy

Thanks
Tobias

On 18/05/2018 17:34, Lukas Bulwahn wrote:
On Fri, May 18, 2018 at 4:41 PM, Tobias Nipkow <nipkow at in.tum.de> wrote:
Hi Lukas,

Your lemmas look natural but replacing the existing simp-rules with them
broke a number of proofs and didn't help any. Thus I have left things as
they are. I didn't add them as ordinary lemmas because my impression is that
in most cases one zips lists of the same length.


Too bad.

Is there a chance to put the two lemmas (without simp attribute) in
the More_List theory in HOL-Library?

That might be an acceptable compromise for everyone.

Lukas


Attachment: smime.p7s
Description: S/MIME Cryptographic Signature



This archive was generated by a fusion of Pipermail (Mailman edition) and MHonArc.