Re: [isabelle] HOL/List.thy lemma suggestions
Thanks Lukas, it would be great if map_fst_zip and map_snd_zip could be refined as you propose (and no new lemmas needed).
From: Lukas Bulwahn [mailto:lukas.bulwahn at gmail.com]
Sent: 17. maj 2018 15:25
To: Jørgen Villadsen
Cc: cl-isabelle-users at lists.cam.ac.uk
Subject: Re: [isabelle] HOL/List.thy lemma suggestions
I would propose the following lemma as alternative:
"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
This reasoning can be automatically found with (simp add: map_fst_zip).
For map_snd_zip, it is analogous.
I hope this helps.
This archive was generated by a fusion of
Pipermail (Mailman edition) and