summary |
shortlog |
changelog |
graph |
tags |
bookmarks |
branches |
files |
changeset |
raw | gz |
help

author | nipkow |

Fri, 27 Mar 2020 12:28:05 +0100 | |

changeset 71808 | 71579bd59cd4 |

parent 71807 | 0c6d29145881 |

child 71818 | 8e0eece7058d |

added lemma

src/HOL/List.thy | file | annotate | diff | comparison | revisions |

--- 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>