# HG changeset patch
# User paulson <lp15@cam.ac.uk>
# 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:
+   "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> R``(S``{a}) = S``{a}"
+  by (auto simp: equiv_class_eq_iff)
+
+lemma refines_equiv_class_eq2:
+   "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> S``(R``{a}) = S``{a}"
+  by (auto simp: equiv_class_eq_iff)
+
+lemma refines_equiv_image_eq:
+   "\<lbrakk>R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> (\<lambda>X. S``X) ` (A//R) = A//S"
+   by (auto simp: quotient_def image_UN refines_equiv_class_eq2)
+
+lemma finite_refines_finite:
+   "\<lbrakk>finite (A//R); R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> finite (A//S)"
+    apply (erule finite_surj [where f = "\<lambda>X. S``X"])
+    apply (simp add: refines_equiv_image_eq)
+    done
+
+lemma finite_refines_card_le:
+   "\<lbrakk>finite (A//R); R \<subseteq> S; equiv A R; equiv A S\<rbrakk> \<Longrightarrow> card (A//S) \<le> card (A//R)"
+  apply (subst refines_equiv_image_eq [of R S A, symmetric])
+  apply (auto simp: card_image_le [where f = "\<lambda>X. S``X"])
+  done
+
 
 subsection {* Defining unary operations upon equivalence classes *}