src/HOL/Equiv_Relations.thy
changeset 24728 e2b3a1065676
parent 23705 315c638d5856
child 25482 4ed49eccb1eb
     1.1 --- a/src/HOL/Equiv_Relations.thy	Wed Sep 26 19:19:38 2007 +0200
     1.2 +++ b/src/HOL/Equiv_Relations.thy	Wed Sep 26 20:27:55 2007 +0200
     1.3 @@ -6,7 +6,7 @@
     1.4  header {* Equivalence Relations in Higher-Order Set Theory *}
     1.5  
     1.6  theory Equiv_Relations
     1.7 -imports Relation
     1.8 +imports Finite_Set Relation
     1.9  begin
    1.10  
    1.11  subsection {* Equivalence relations *}
    1.12 @@ -292,4 +292,45 @@
    1.13           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
    1.14    done
    1.15  
    1.16 +
    1.17 +subsection {* Quotients and finiteness *}
    1.18 +
    1.19 +text {*Suggested by Florian Kammüller*}
    1.20 +
    1.21 +lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"
    1.22 +  -- {* recall @{thm equiv_type} *}
    1.23 +  apply (rule finite_subset)
    1.24 +   apply (erule_tac [2] finite_Pow_iff [THEN iffD2])
    1.25 +  apply (unfold quotient_def)
    1.26 +  apply blast
    1.27 +  done
    1.28 +
    1.29 +lemma finite_equiv_class:
    1.30 +  "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"
    1.31 +  apply (unfold quotient_def)
    1.32 +  apply (rule finite_subset)
    1.33 +   prefer 2 apply assumption
    1.34 +  apply blast
    1.35 +  done
    1.36 +
    1.37 +lemma equiv_imp_dvd_card:
    1.38 +  "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X
    1.39 +    ==> k dvd card A"
    1.40 +  apply (rule Union_quotient [THEN subst])
    1.41 +   apply assumption
    1.42 +  apply (rule dvd_partition)
    1.43 +     prefer 3 apply (blast dest: quotient_disj)
    1.44 +    apply (simp_all add: Union_quotient equiv_type)
    1.45 +  done
    1.46 +
    1.47 +lemma card_quotient_disjoint:
    1.48 + "\<lbrakk> finite A; inj_on (\<lambda>x. {x} // r) A \<rbrakk> \<Longrightarrow> card(A//r) = card A"
    1.49 +apply(simp add:quotient_def)
    1.50 +apply(subst card_UN_disjoint)
    1.51 +   apply assumption
    1.52 +  apply simp
    1.53 + apply(fastsimp simp add:inj_on_def)
    1.54 +apply (simp add:setsum_constant)
    1.55 +done
    1.56 +
    1.57  end