--- a/src/HOL/Equiv_Relations.thy Sun Nov 21 12:52:03 2004 +0100
+++ b/src/HOL/Equiv_Relations.thy Sun Nov 21 15:44:20 2004 +0100
@@ -320,6 +320,16 @@
apply (simp_all add: Union_quotient equiv_type finite_quotient)
done
+lemma card_quotient_disjoint:
+ "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
+apply(simp add:quotient_def)
+apply(subst card_UN_disjoint)
+ apply assumption
+ apply simp
+ apply(fastsimp simp add:inj_on_def)
+apply (simp add:setsum_constant_nat)
+done
+
ML
{*
val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";