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 *}