Re: [isabelle] HOL/List.thy lemma suggestions
Thanks for adding them to HOL/List.thy (map_fst_zip_take and map_snd_zip_take).
From: cl-isabelle-users-bounces at lists.cam.ac.uk [mailto:cl-isabelle-users-bounces at lists.cam.ac.uk] On Behalf Of Tobias Nipkow
Sent: 19. maj 2018 14:22
To: Cl-isabelle Users
Subject: 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:
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.
This archive was generated by a fusion of
Pipermail (Mailman edition) and