# HG changeset patch
# User nipkow
# Date 1526723861 -7200
# Node ID a477f78a936587ceef5bf7287ae53d91489e9f3c
# Parent  b0e2a19df95b6e42fa5444b2c8a5188348d88348
added lemmas

diff -r b0e2a19df95b -r a477f78a9365 src/HOL/List.thy
--- a/src/HOL/List.thy	Fri May 18 21:50:46 2018 +0200
+++ b/src/HOL/List.thy	Sat May 19 11:57:41 2018 +0200
@@ -1218,6 +1218,14 @@
   "length xs = length ys \<Longrightarrow> map snd (zip xs ys) = ys"
 by (induct rule:list_induct2, simp_all)
 
+lemma map_fst_zip_take:
+  "map fst (zip xs ys) = take (min (length xs) (length ys)) xs"
+by (induct xs ys rule: list_induct2') simp_all
+
+lemma map_snd_zip_take:
+  "map snd (zip xs ys) = take (min (length xs) (length ys)) ys"
+by (induct xs ys rule: list_induct2') simp_all
+
 lemma map2_map_map: "map2 h (map f xs) (map g xs) = map (\<lambda>x. h (f x) (g x)) xs"
 by (induction xs) (auto)