--- a/src/HOL/List.thy Sat Feb 08 15:18:58 2020 +0100
+++ b/src/HOL/List.thy Sun Feb 09 10:21:01 2020 +0000
@@ -2791,6 +2791,15 @@
by (induct xs ys rule: list_induct2) (simp_all add: prod_eqI)
qed
+lemma hd_zip:
+ \<open>hd (zip xs ys) = (hd xs, hd ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+ using that by (cases xs; cases ys) simp_all
+
+lemma last_zip:
+ \<open>last (zip xs ys) = (last xs, last ys)\<close> if \<open>xs \<noteq> []\<close> and \<open>ys \<noteq> []\<close>
+ and \<open>length xs = length ys\<close>
+ using that by (cases xs rule: rev_cases; cases ys rule: rev_cases) simp_all
+
subsubsection \<open>\<^const>\<open>list_all2\<close>\<close>