src/HOL/Equiv_Relations.thy
 changeset 23705 315c638d5856 parent 21749 3f0e86c92ff3 child 24728 e2b3a1065676
```     1.1 --- a/src/HOL/Equiv_Relations.thy	Tue Jul 10 16:46:37 2007 +0200
1.2 +++ b/src/HOL/Equiv_Relations.thy	Tue Jul 10 17:30:43 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 Finite_Set
1.8 +imports Relation
1.9  begin
1.10
1.11  subsection {* Equivalence relations *}
1.12 @@ -292,83 +292,4 @@
1.13           erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+
1.14    done
1.15
1.16 -
1.17 -subsection {* Cardinality results *}
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.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 -ML
1.58 -{*
1.59 -val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";
1.60 -val UN_constant_eq = thm "UN_constant_eq";
1.61 -val UN_equiv_class = thm "UN_equiv_class";
1.62 -val UN_equiv_class2 = thm "UN_equiv_class2";
1.63 -val UN_equiv_class_inject = thm "UN_equiv_class_inject";
1.64 -val UN_equiv_class_type = thm "UN_equiv_class_type";
1.65 -val UN_equiv_class_type2 = thm "UN_equiv_class_type2";
1.66 -val Union_quotient = thm "Union_quotient";
1.67 -val comp_equivI = thm "comp_equivI";
1.68 -val congruent2I = thm "congruent2I";
1.69 -val congruent2_commuteI = thm "congruent2_commuteI";
1.70 -val congruent2_def = thm "congruent2_def";
1.71 -val congruent2_implies_congruent = thm "congruent2_implies_congruent";
1.72 -val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";
1.73 -val congruent_def = thm "congruent_def";
1.74 -val eq_equiv_class = thm "eq_equiv_class";
1.75 -val eq_equiv_class_iff = thm "eq_equiv_class_iff";
1.76 -val equiv_class_eq = thm "equiv_class_eq";
1.77 -val equiv_class_eq_iff = thm "equiv_class_eq_iff";
1.78 -val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";
1.79 -val equiv_class_self = thm "equiv_class_self";
1.80 -val equiv_comp_eq = thm "equiv_comp_eq";
1.81 -val equiv_def = thm "equiv_def";
1.82 -val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";
1.83 -val equiv_type = thm "equiv_type";
1.84 -val finite_equiv_class = thm "finite_equiv_class";
1.85 -val finite_quotient = thm "finite_quotient";
1.86 -val quotientE = thm "quotientE";
1.87 -val quotientI = thm "quotientI";
1.88 -val quotient_def = thm "quotient_def";
1.89 -val quotient_disj = thm "quotient_disj";
1.90 -val refl_comp_subset = thm "refl_comp_subset";
1.91 -val subset_equiv_class = thm "subset_equiv_class";
1.92 -val sym_trans_comp_subset = thm "sym_trans_comp_subset";
1.93 -*}
1.94 -*)
1.95  end
```