# HG changeset patch
# User nipkow
# Date 1585308485 -3600
# Node ID 71579bd59cd495bedb176d8f2ba649b0cfe4c08c
# Parent  0c6d29145881dd83320353a06571afe8c1cf7e82
added lemma

diff -r 0c6d29145881 -r 71579bd59cd4 src/HOL/List.thy
--- a/src/HOL/List.thy	Wed Mar 25 14:00:23 2020 +0000
+++ b/src/HOL/List.thy	Fri Mar 27 12:28:05 2020 +0100
@@ -3550,8 +3550,9 @@
    \<rbrakk> \<Longrightarrow> distinct (concat xs)"
 by (induct xs) auto
 
-text \<open>It is best to avoid this indexed version of distinct, but
-sometimes it is useful.\<close>
+text \<open>An iff-version of @{thm distinct_concat} is available further down as \<open>distinct_concat_iff\<close>.\<close>
+
+text \<open>It is best to avoid the following indexed version of distinct, but sometimes it is useful.\<close>
 
 lemma distinct_conv_nth: "distinct xs = (\<forall>i < size xs. \<forall>j < size xs. i \<noteq> j \<longrightarrow> xs!i \<noteq> xs!j)"
 proof (induct xs)
@@ -4179,6 +4180,14 @@
   "x \<in> set xs \<Longrightarrow> length (removeAll x xs) < length xs"
   by (auto dest: length_filter_less simp add: removeAll_filter_not_eq)
 
+lemma distinct_concat_iff: "distinct (concat xs) \<longleftrightarrow>
+  distinct (removeAll [] xs) \<and> 
+  (\<forall>ys. ys \<in> set xs \<longrightarrow> distinct ys) \<and>
+  (\<forall>ys zs. ys \<in> set xs \<and> zs \<in> set xs \<and> ys \<noteq> zs \<longrightarrow> set ys \<inter> set zs = {})"
+apply (induct xs)
+ apply(simp_all, safe, auto)
+by (metis Int_iff UN_I empty_iff equals0I set_empty)
+
 
 subsubsection \<open>\<^const>\<open>replicate\<close>\<close>