# HG changeset patch # User blanchet # Date 1389894770 -3600 # Node ID eeba3ba734869e2f915dc6721602284c194efb85 # Parent e40090032de9c2351a160568982175fa6908bd81 liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts diff -r e40090032de9 -r eeba3ba73486 src/HOL/BNF/BNF_GFP.thy --- a/src/HOL/BNF/BNF_GFP.thy Thu Jan 16 18:37:37 2014 +0100 +++ b/src/HOL/BNF/BNF_GFP.thy Thu Jan 16 18:52:50 2014 +0100 @@ -8,7 +8,7 @@ header {* Greatest Fixed Point Operation on Bounded Natural Functors *} theory BNF_GFP -imports BNF_FP_Base Equiv_Relations_More List_Prefix +imports BNF_FP_Base keywords "codatatype" :: thy_decl and "primcorecursive" :: thy_goal and @@ -293,6 +293,56 @@ lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g" unfolding fun_rel_def image2p_def by auto + +subsection {* Equivalence relations, quotients, and Hilbert's choice *} + +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 + +definition univ where "univ f X == f (Eps (%x. x \ X))" + +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_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 + ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML" ML_file "Tools/bnf_gfp_rec_sugar.ML" ML_file "Tools/bnf_gfp_util.ML" diff -r e40090032de9 -r eeba3ba73486 src/HOL/BNF/Equiv_Relations_More.thy --- a/src/HOL/BNF/Equiv_Relations_More.thy Thu Jan 16 18:37:37 2014 +0100 +++ /dev/null Thu Jan 01 00:00:00 1970 +0000 @@ -1,161 +0,0 @@ -(* 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[THEN iffD1] 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 diff -r e40090032de9 -r eeba3ba73486 src/HOL/Equiv_Relations.thy --- a/src/HOL/Equiv_Relations.thy Thu Jan 16 18:37:37 2014 +0100 +++ b/src/HOL/Equiv_Relations.thy Thu Jan 16 18:52:50 2014 +0100 @@ -160,6 +160,7 @@ apply blast done + subsection {* Defining unary operations upon equivalence classes *} text{*A congruence-preserving function*} @@ -354,6 +355,54 @@ done +subsection {* Projection *} + +definition proj where "proj r x = r `` {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[THEN iffD1] 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 + + subsection {* Equivalence relations -- predicate version *} text {* Partial equivalences *}