[isabelle] HOL/List.thy lemma suggestions


Would it be a good idea to add something like the following lemmas?

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.



PS - Here is a little explanation in case it is needed:

text <
  @{term zip}ping two lists and retrieving one of them back by mapping @{term fst} or @{term snd}
  results in the original list, possibly truncated

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