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. Tobias 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
Description: S/MIME Cryptographic Signature