author paulson Thu, 12 Feb 2015 12:46:50 +0000 changeset 59528 4862f3dc9540 parent 59527 edaabc1ab1ed child 59534 c3ca292c1484
new lemmas re refinement of one equivalence relation WRT another
```--- 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"])