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

Hi Tobias,

Thanks for the investigations. Any chance that the original lemma suggestions could be added?

lemma sublist_map_fst_zip: obtains zs where "(map fst (zip xs ys)) @ zs = xs"
  by (induct xs ys rule:list_induct2') simp_all

lemma sublist_map_snd_zip: obtains zs where "(map snd (zip xs ys)) @ zs = ys"
  by (induct xs ys rule:list_induct2') simp_all

At least we found them useful... :-)

Best regards, Jørgen

-----Original Message-----
From: cl-isabelle-users-bounces at [mailto:cl-isabelle-users-bounces at] On Behalf Of Tobias Nipkow
Sent: 18. maj 2018 16:42
To: cl-isabelle-users at
Subject: Re: [isabelle] HOL/List.thy lemma suggestions

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.

But thanks for the suggestion.


On 17/05/2018 15:25, Lukas Bulwahn wrote:
> Hi Jørgen,
> I would propose the following lemma as alternative:
> lemma map_fst_zip:
>    "map fst (zip xs ys) = take (min (length xs) (length ys)) xs"
> by (induct xs ys rule: list_induct2') simp_all
> The advantage is that it is a refinement of the existing map_fst_zip;
> so I would expect that all previous proofs with map_fst_zip would
> still complete with this new one (but I have not tried it).
> In your proof, you can then simply replace, obtaining some zs, by
> naming the witness. zs is `drop (min (length xs) (length ys)) xs`.
> Then, in your proof:
> (map fst (zip xs ys)) @ drop (min (length xs) (length ys)) xs
> = take (min (length xs) (length ys)) xs @ drop (min (length xs) (length ys)) xs
> = xs
> This reasoning can be automatically found with (simp add: map_fst_zip).
> For map_snd_zip, it is analogous.
> I hope this helps.
> Best regards,
> Lukas

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