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

Thanks for adding them to HOL/List.thy (map_fst_zip_take and map_snd_zip_take).


-----Original Message-----
From: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] 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> 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

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