# HG changeset patch
# User paulson
# Date 864998539 -7200
# Node ID 182a2b76d19e18cf8e09ed33c2a2d3cbadbfdf71
# Parent  b19b1456cc7889e5fb554cb374bffb6c171e24d0
New proofs about cardinality.  Suggested by Florian Kammueller

diff -r b19b1456cc78 -r 182a2b76d19e src/HOL/Integ/Equiv.ML
--- a/src/HOL/Integ/Equiv.ML	Fri May 30 15:21:53 1997 +0200
+++ b/src/HOL/Integ/Equiv.ML	Fri May 30 15:22:19 1997 +0200
@@ -256,3 +256,31 @@
      ORELSE etac (equivA RS equiv_type RS subsetD RS SigmaE2) 1));
 qed "congruent2_commuteI";
 
+
+(*** Cardinality results suggested by Florian Kammüller ***)
+
+(*Recall that  equiv A r  implies  r <= A Times A   (equiv_type) *)
+goal thy "!!A. [| finite A; r <= A Times A |] ==> finite (A/r)";
+by (rtac finite_subset 1);
+by (etac (finite_Pow_iff RS iffD2) 2);
+by (rewrite_goals_tac [quotient_def]);
+by (Blast_tac 1);
+qed "finite_quotient";
+
+goalw thy [quotient_def]
+    "!!A. [| finite A;  r <= A Times A;  X : A/r |] ==> finite X";
+by (rtac finite_subset 1);
+ba 2;
+by (Blast_tac 1);
+qed "finite_equiv_class";
+
+goal thy "!!A. [| finite A;  equiv A r;  ! X : A/r. k dvd card(X) |] \
+\              ==> k dvd card(A)";
+by (rtac (Union_quotient RS subst) 1);
+by (assume_tac 1);
+by (rtac dvd_partition 1);
+by (blast_tac (!claset delrules [equalityI] addEs [quotient_disj RS disjE]) 4);
+by (ALLGOALS 
+    (asm_simp_tac (!simpset addsimps [Union_quotient, equiv_type, 
+				      finite_quotient])));
+qed "equiv_imp_dvd_card";