# HG changeset patch
# User nipkow
# Date 1472029343 -7200
# Node ID bcf2123d059ab1242f17e700027038ba02bc8b97
# Parent  9084d77f111932f2b6366c8784fb27bd14eb38ca
added lemma

diff -r 9084d77f1119 -r bcf2123d059a src/HOL/List.thy
--- a/src/HOL/List.thy	Tue Aug 23 15:19:32 2016 +0200
+++ b/src/HOL/List.thy	Wed Aug 24 11:02:23 2016 +0200
@@ -2766,6 +2766,10 @@
 
 subsubsection \<open>@{const List.product} and @{const product_lists}\<close>
 
+lemma product_concat_map:
+  "List.product xs ys = concat (map (\<lambda>x. map (\<lambda>y. (x,y)) ys) xs)"
+by(induction xs) (simp)+
+
 lemma set_product[simp]: "set (List.product xs ys) = set xs \<times> set ys"
 by (induct xs) auto