src/HOL/Equiv_Relations.thy
changeset 15303 eedbb8d22ca2
parent 15302 a643fcbc3468
child 15392 290bc97038c7
     1.1 --- a/src/HOL/Equiv_Relations.thy	Sun Nov 21 12:52:03 2004 +0100
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Sun Nov 21 15:44:20 2004 +0100
     1.3 @@ -320,6 +320,16 @@
     1.4      apply (simp_all add: Union_quotient equiv_type finite_quotient)
     1.5    done
     1.6  
     1.7 +lemma card_quotient_disjoint:
     1.8 + "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
     1.9 +apply(simp add:quotient_def)
    1.10 +apply(subst card_UN_disjoint)
    1.11 +   apply assumption
    1.12 +  apply simp
    1.13 + apply(fastsimp simp add:inj_on_def)
    1.14 +apply (simp add:setsum_constant_nat)
    1.15 +done
    1.16 +
    1.17  ML
    1.18  {*
    1.19  val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";