# HG changeset patch # User paulson # Date 1423745210 0 # Node ID 4862f3dc954081b870fab14113de6075b46c9303 # Parent edaabc1ab1ed5dd616f6306392bae35372973723 new lemmas re refinement of one equivalence relation WRT another diff -r edaabc1ab1ed -r 4862f3dc9540 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Wed Feb 11 18:39:56 2015 +0100 +++ b/src/HOL/Equiv_Relations.thy Thu Feb 12 12:46:50 2015 +0000 @@ -160,6 +160,32 @@ apply blast done +subsection {* Refinement of one equivalence relation WRT another *} + +lemma refines_equiv_class_eq: + "\R \ S; equiv A R; equiv A S\ \ R``(S``{a}) = S``{a}" + by (auto simp: equiv_class_eq_iff) + +lemma refines_equiv_class_eq2: + "\R \ S; equiv A R; equiv A S\ \ S``(R``{a}) = S``{a}" + by (auto simp: equiv_class_eq_iff) + +lemma refines_equiv_image_eq: + "\R \ S; equiv A R; equiv A S\ \ (\X. S``X) ` (A//R) = A//S" + by (auto simp: quotient_def image_UN refines_equiv_class_eq2) + +lemma finite_refines_finite: + "\finite (A//R); R \ S; equiv A R; equiv A S\ \ finite (A//S)" + apply (erule finite_surj [where f = "\X. S``X"]) + apply (simp add: refines_equiv_image_eq) + done + +lemma finite_refines_card_le: + "\finite (A//R); R \ S; equiv A R; equiv A S\ \ card (A//S) \ card (A//R)" + apply (subst refines_equiv_image_eq [of R S A, symmetric]) + apply (auto simp: card_image_le [where f = "\X. S``X"]) + done + subsection {* Defining unary operations upon equivalence classes *}