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



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

Jørgen	

-----Original Message-----
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:
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
> 



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