# HG changeset patch
# User nipkow
# Date 1135252853 -3600
# Node ID 434e34392c40b73591604639dc5fee13aa630039
# Parent  151e52a4db3fd5363f5b0c8bdba046658b09b734
new lemmas

diff -r 151e52a4db3f -r 434e34392c40 src/HOL/Equiv_Relations.thy
--- a/src/HOL/Equiv_Relations.thy	Thu Dec 22 12:27:10 2005 +0100
+++ b/src/HOL/Equiv_Relations.thy	Thu Dec 22 13:00:53 2005 +0100
@@ -90,6 +90,10 @@
   "equiv A r ==> x \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> r)"
   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)
 
+lemma eq_equiv_class_iff2:
+  "\<lbrakk> equiv A r; x \<in> A; y \<in> A \<rbrakk> \<Longrightarrow> ({x}//r = {y}//r) = ((x,y) : r)"
+by(simp add:quotient_def eq_equiv_class_iff)
+
 
 subsection {* Quotients *}
 
diff -r 151e52a4db3f -r 434e34392c40 src/HOL/List.thy
--- a/src/HOL/List.thy	Thu Dec 22 12:27:10 2005 +0100
+++ b/src/HOL/List.thy	Thu Dec 22 13:00:53 2005 +0100
@@ -1766,16 +1766,15 @@
 apply(rule length_remdups_leq)
 done
 
+
+lemma distinct_map:
+  "distinct(map f xs) = (distinct xs & inj_on f (set xs))"
+by (induct xs) auto
+
+
 lemma distinct_filter [simp]: "distinct xs ==> distinct (filter P xs)"
 by (induct xs) auto
 
-lemma distinct_map_filterI:
- "distinct(map f xs) \<Longrightarrow> distinct(map f (filter P xs))"
-apply(induct xs)
- apply simp
-apply force
-done
-
 lemma distinct_upt[simp]: "distinct[i..<j]"
 by (induct j) auto
 
@@ -1830,6 +1829,10 @@
 apply (erule_tac x = "Suc j" in allE, simp)
 done
 
+lemma nth_eq_iff_index_eq:
+ "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
+by(auto simp: distinct_conv_nth)
+
 lemma distinct_card: "distinct xs ==> card (set xs) = size xs"
   by (induct xs) auto
 
@@ -1851,23 +1854,10 @@
   qed
 qed
 
-lemma inj_on_setI: "distinct(map f xs) ==> inj_on f (set xs)"
-apply(induct xs)
- apply simp
-apply fastsimp
-done
-
-lemma inj_on_set_conv:
- "distinct xs \<Longrightarrow> inj_on f (set xs) = distinct(map f xs)"
-apply(induct xs)
- apply simp
-apply fastsimp
-done
-
-
-lemma nth_eq_iff_index_eq:
- "\<lbrakk> distinct xs; i < length xs; j < length xs \<rbrakk> \<Longrightarrow> (xs!i = xs!j) = (i = j)"
-by(auto simp: distinct_conv_nth)
+
+lemma length_remdups_concat:
+ "length(remdups(concat xss)) = card(\<Union>xs \<in> set xss. set xs)"
+by(simp add: distinct_card[symmetric])
 
 
 subsubsection {* @{text remove1} *}