(* Title: HOL/BNF/Equiv_Relations_More.thy
Author: Andrei Popescu, TU Muenchen
Copyright 2012
Some preliminaries on equivalence relations and quotients.
*)
header {* Some Preliminaries on Equivalence Relations and Quotients *}
theory Equiv_Relations_More
imports Equiv_Relations Hilbert_Choice
begin
(* Recall the following constants and lemmas:
term Eps
term "A//r"
lemmas equiv_def
lemmas refl_on_def
-- note that "reflexivity on" also assumes inclusion of the relation's field into r
*)
definition proj where "proj r x = r `` {x}"
definition univ where "univ f X == f (Eps (%x. x \ X))"
lemma proj_preserves:
"x \ A \ proj r x \ A//r"
unfolding proj_def by (rule quotientI)
lemma proj_in_iff:
assumes "equiv A r"
shows "(proj r x \ A//r) = (x \ A)"
apply(rule iffI, auto simp add: proj_preserves)
unfolding proj_def quotient_def proof clarsimp
fix y assume y: "y \ A" and "r `` {x} = r `` {y}"
moreover have "y \ r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
ultimately have "(x,y) \ r" by blast
thus "x \ A" using assms unfolding equiv_def refl_on_def by blast
qed
lemma proj_iff:
"\equiv A r; {x,y} \ A\ \ (proj r x = proj r y) = ((x,y) \ r)"
by (simp add: proj_def eq_equiv_class_iff)
(*
lemma in_proj: "\equiv A r; x \ A\ \ x \ proj r x"
unfolding proj_def equiv_def refl_on_def by blast
*)
lemma proj_image: "(proj r) ` A = A//r"
unfolding proj_def[abs_def] quotient_def by blast
lemma in_quotient_imp_non_empty:
"\equiv A r; X \ A//r\ \ X \ {}"
unfolding quotient_def using equiv_class_self by fast
lemma in_quotient_imp_in_rel:
"\equiv A r; X \ A//r; {x,y} \ X\ \ (x,y) \ r"
using quotient_eq_iff by fastforce
lemma in_quotient_imp_closed:
"\equiv A r; X \ A//r; x \ X; (x,y) \ r\ \ y \ X"
unfolding quotient_def equiv_def trans_def by blast
lemma in_quotient_imp_subset:
"\equiv A r; X \ A//r\ \ X \ A"
using assms in_quotient_imp_in_rel equiv_type by fastforce
lemma equiv_Eps_in:
"\equiv A r; X \ A//r\ \ Eps (%x. x \ X) \ X"
apply (rule someI2_ex)
using in_quotient_imp_non_empty by blast
lemma equiv_Eps_preserves:
assumes ECH: "equiv A r" and X: "X \ A//r"
shows "Eps (%x. x \ X) \ A"
apply (rule in_mono[rule_format])
using assms apply (rule in_quotient_imp_subset)
by (rule equiv_Eps_in) (rule assms)+
lemma proj_Eps:
assumes "equiv A r" and "X \ A//r"
shows "proj r (Eps (%x. x \ X)) = X"
unfolding proj_def proof auto
fix x assume x: "x \ X"
thus "(Eps (%x. x \ X), x) \ r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
next
fix x assume "(Eps (%x. x \ X),x) \ r"
thus "x \ X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
qed
(*
lemma Eps_proj:
assumes "equiv A r" and "x \ A"
shows "(Eps (%y. y \ proj r x), x) \ r"
proof-
have 1: "proj r x \ A//r" using assms proj_preserves by fastforce
hence "Eps(%y. y \ proj r x) \ proj r x" using assms equiv_Eps_in by auto
moreover have "x \ proj r x" using assms in_proj by fastforce
ultimately show ?thesis using assms 1 in_quotient_imp_in_rel by fastforce
qed
lemma equiv_Eps_iff:
assumes "equiv A r" and "{X,Y} \ A//r"
shows "((Eps (%x. x \ X),Eps (%y. y \ Y)) \ r) = (X = Y)"
proof-
have "Eps (%x. x \ X) \ X \ Eps (%y. y \ Y) \ Y" using assms equiv_Eps_in by auto
thus ?thesis using assms quotient_eq_iff by fastforce
qed
lemma equiv_Eps_inj_on:
assumes "equiv A r"
shows "inj_on (%X. Eps (%x. x \ X)) (A//r)"
unfolding inj_on_def proof clarify
fix X Y assume X: "X \ A//r" and Y: "Y \ A//r" and Eps: "Eps (%x. x \ X) = Eps (%y. y \ Y)"
hence "Eps (%x. x \ X) \ A" using assms equiv_Eps_preserves by auto
hence "(Eps (%x. x \ X), Eps (%y. y \ Y)) \ r"
using assms Eps unfolding quotient_def equiv_def refl_on_def by auto
thus "X= Y" using X Y assms equiv_Eps_iff by auto
qed
*)
lemma univ_commute:
assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \ A"
shows "(univ f) (proj r x) = f x"
unfolding univ_def proof -
have prj: "proj r x \ A//r" using x proj_preserves by fast
hence "Eps (%y. y \ proj r x) \ A" using ECH equiv_Eps_preserves by fast
moreover have "proj r (Eps (%y. y \ proj r x)) = proj r x" using ECH prj proj_Eps by fast
ultimately have "(x, Eps (%y. y \ proj r x)) \ r" using x ECH proj_iff by fast
thus "f (Eps (%y. y \ proj r x)) = f x" using RES unfolding congruent_def by fastforce
qed
(*
lemma univ_unique:
assumes ECH: "equiv A r" and
RES: "f respects r" and COM: "\ x \ A. G (proj r x) = f x"
shows "\ X \ A//r. G X = univ f X"
proof
fix X assume "X \ A//r"
then obtain x where x: "x \ A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
have "G X = f x" unfolding X using x COM by simp
thus "G X = univ f X" unfolding X using ECH RES x univ_commute by fastforce
qed
*)
lemma univ_preserves:
assumes ECH: "equiv A r" and RES: "f respects r" and
PRES: "\ x \ A. f x \ B"
shows "\ X \ A//r. univ f X \ B"
proof
fix X assume "X \ A//r"
then obtain x where x: "x \ A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
hence "univ f X = f x" using assms univ_commute by fastforce
thus "univ f X \ B" using x PRES by simp
qed
end