src/HOL/Equiv_Relations.thy
 changeset 55022 eeba3ba73486 parent 54744 1e7f2d296e19 child 55024 05cc0dbf3a50
```     1.1 --- a/src/HOL/Equiv_Relations.thy	Thu Jan 16 18:37:37 2014 +0100
1.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Jan 16 18:52:50 2014 +0100
1.3 @@ -160,6 +160,7 @@
1.4  apply blast
1.5  done
1.6
1.7 +
1.8  subsection {* Defining unary operations upon equivalence classes *}
1.9
1.10  text{*A congruence-preserving function*}
1.11 @@ -354,6 +355,54 @@
1.12  done
1.13
1.14
1.15 +subsection {* Projection *}
1.16 +
1.17 +definition proj where "proj r x = r `` {x}"
1.18 +
1.19 +lemma proj_preserves:
1.20 +"x \<in> A \<Longrightarrow> proj r x \<in> A//r"
1.21 +unfolding proj_def by (rule quotientI)
1.22 +
1.23 +lemma proj_in_iff:
1.24 +assumes "equiv A r"
1.25 +shows "(proj r x \<in> A//r) = (x \<in> A)"
1.26 +apply(rule iffI, auto simp add: proj_preserves)
1.27 +unfolding proj_def quotient_def proof clarsimp
1.28 +  fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}"
1.29 +  moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
1.30 +  ultimately have "(x,y) \<in> r" by blast
1.31 +  thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast
1.32 +qed
1.33 +
1.34 +lemma proj_iff:
1.35 +"\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)"
1.36 +by (simp add: proj_def eq_equiv_class_iff)
1.37 +
1.38 +(*
1.39 +lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
1.40 +unfolding proj_def equiv_def refl_on_def by blast
1.41 +*)
1.42 +
1.43 +lemma proj_image: "(proj r) ` A = A//r"
1.44 +unfolding proj_def[abs_def] quotient_def by blast
1.45 +
1.46 +lemma in_quotient_imp_non_empty:
1.47 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}"
1.48 +unfolding quotient_def using equiv_class_self by fast
1.49 +
1.50 +lemma in_quotient_imp_in_rel:
1.51 +"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
1.52 +using quotient_eq_iff[THEN iffD1] by fastforce
1.53 +
1.54 +lemma in_quotient_imp_closed:
1.55 +"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
1.56 +unfolding quotient_def equiv_def trans_def by blast
1.57 +
1.58 +lemma in_quotient_imp_subset:
1.59 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
1.60 +using assms in_quotient_imp_in_rel equiv_type by fastforce
1.61 +
1.62 +
1.63  subsection {* Equivalence relations -- predicate version *}
1.64
1.65  text {* Partial equivalences *}
```