| changeset 63720 | bcf2123d059a |
| parent 63662 | 5cdcd51a4dad |
| child 63834 | 6a757f36997e |
--- 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