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,


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

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