liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
authorblanchet
Thu Jan 16 18:52:50 2014 +0100 (2014-01-16)
changeset 55022eeba3ba73486
parent 55021 e40090032de9
child 55023 38db7814481d
liquidated 'Equiv_Relations_More' -- distinguished between choice-dependent parts and choice-independent parts
src/HOL/BNF/BNF_GFP.thy
src/HOL/BNF/Equiv_Relations_More.thy
src/HOL/Equiv_Relations.thy
     1.1 --- a/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 18:37:37 2014 +0100
     1.2 +++ b/src/HOL/BNF/BNF_GFP.thy	Thu Jan 16 18:52:50 2014 +0100
     1.3 @@ -8,7 +8,7 @@
     1.4  header {* Greatest Fixed Point Operation on Bounded Natural Functors *}
     1.5  
     1.6  theory BNF_GFP
     1.7 -imports BNF_FP_Base Equiv_Relations_More List_Prefix
     1.8 +imports BNF_FP_Base
     1.9  keywords
    1.10    "codatatype" :: thy_decl and
    1.11    "primcorecursive" :: thy_goal and
    1.12 @@ -293,6 +293,56 @@
    1.13  lemma fun_rel_image2p: "(fun_rel R (image2p f g R)) f g"
    1.14    unfolding fun_rel_def image2p_def by auto
    1.15  
    1.16 +
    1.17 +subsection {* Equivalence relations, quotients, and Hilbert's choice *}
    1.18 +
    1.19 +lemma equiv_Eps_in:
    1.20 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
    1.21 +apply (rule someI2_ex)
    1.22 +using in_quotient_imp_non_empty by blast
    1.23 +
    1.24 +lemma equiv_Eps_preserves:
    1.25 +assumes ECH: "equiv A r" and X: "X \<in> A//r"
    1.26 +shows "Eps (%x. x \<in> X) \<in> A"
    1.27 +apply (rule in_mono[rule_format])
    1.28 + using assms apply (rule in_quotient_imp_subset)
    1.29 +by (rule equiv_Eps_in) (rule assms)+
    1.30 +
    1.31 +lemma proj_Eps:
    1.32 +assumes "equiv A r" and "X \<in> A//r"
    1.33 +shows "proj r (Eps (%x. x \<in> X)) = X"
    1.34 +unfolding proj_def proof auto
    1.35 +  fix x assume x: "x \<in> X"
    1.36 +  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    1.37 +next
    1.38 +  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
    1.39 +  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
    1.40 +qed
    1.41 +
    1.42 +definition univ where "univ f X == f (Eps (%x. x \<in> X))"
    1.43 +
    1.44 +lemma univ_commute:
    1.45 +assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
    1.46 +shows "(univ f) (proj r x) = f x"
    1.47 +unfolding univ_def proof -
    1.48 +  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
    1.49 +  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
    1.50 +  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
    1.51 +  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
    1.52 +  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
    1.53 +qed
    1.54 +
    1.55 +lemma univ_preserves:
    1.56 +assumes ECH: "equiv A r" and RES: "f respects r" and
    1.57 +        PRES: "\<forall> x \<in> A. f x \<in> B"
    1.58 +shows "\<forall> X \<in> A//r. univ f X \<in> B"
    1.59 +proof
    1.60 +  fix X assume "X \<in> A//r"
    1.61 +  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
    1.62 +  hence "univ f X = f x" using assms univ_commute by fastforce
    1.63 +  thus "univ f X \<in> B" using x PRES by simp
    1.64 +qed
    1.65 +
    1.66  ML_file "Tools/bnf_gfp_rec_sugar_tactics.ML"
    1.67  ML_file "Tools/bnf_gfp_rec_sugar.ML"
    1.68  ML_file "Tools/bnf_gfp_util.ML"
     2.1 --- a/src/HOL/BNF/Equiv_Relations_More.thy	Thu Jan 16 18:37:37 2014 +0100
     2.2 +++ /dev/null	Thu Jan 01 00:00:00 1970 +0000
     2.3 @@ -1,161 +0,0 @@
     2.4 -(*  Title:      HOL/BNF/Equiv_Relations_More.thy
     2.5 -    Author:     Andrei Popescu, TU Muenchen
     2.6 -    Copyright   2012
     2.7 -
     2.8 -Some preliminaries on equivalence relations and quotients.
     2.9 -*)
    2.10 -
    2.11 -header {* Some Preliminaries on Equivalence Relations and Quotients *}
    2.12 -
    2.13 -theory Equiv_Relations_More
    2.14 -imports Equiv_Relations Hilbert_Choice
    2.15 -begin
    2.16 -
    2.17 -
    2.18 -(* Recall the following constants and lemmas:
    2.19 -
    2.20 -term Eps
    2.21 -term "A//r"
    2.22 -lemmas equiv_def
    2.23 -lemmas refl_on_def
    2.24 - -- note that "reflexivity on" also assumes inclusion of the relation's field into r
    2.25 -
    2.26 -*)
    2.27 -
    2.28 -definition proj where "proj r x = r `` {x}"
    2.29 -
    2.30 -definition univ where "univ f X == f (Eps (%x. x \<in> X))"
    2.31 -
    2.32 -lemma proj_preserves:
    2.33 -"x \<in> A \<Longrightarrow> proj r x \<in> A//r"
    2.34 -unfolding proj_def by (rule quotientI)
    2.35 -
    2.36 -lemma proj_in_iff:
    2.37 -assumes "equiv A r"
    2.38 -shows "(proj r x \<in> A//r) = (x \<in> A)"
    2.39 -apply(rule iffI, auto simp add: proj_preserves)
    2.40 -unfolding proj_def quotient_def proof clarsimp
    2.41 -  fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}"
    2.42 -  moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
    2.43 -  ultimately have "(x,y) \<in> r" by blast
    2.44 -  thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast
    2.45 -qed
    2.46 -
    2.47 -lemma proj_iff:
    2.48 -"\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)"
    2.49 -by (simp add: proj_def eq_equiv_class_iff)
    2.50 -
    2.51 -(*
    2.52 -lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
    2.53 -unfolding proj_def equiv_def refl_on_def by blast
    2.54 -*)
    2.55 -
    2.56 -lemma proj_image: "(proj r) ` A = A//r"
    2.57 -unfolding proj_def[abs_def] quotient_def by blast
    2.58 -
    2.59 -lemma in_quotient_imp_non_empty:
    2.60 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}"
    2.61 -unfolding quotient_def using equiv_class_self by fast
    2.62 -
    2.63 -lemma in_quotient_imp_in_rel:
    2.64 -"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
    2.65 -using quotient_eq_iff[THEN iffD1] by fastforce
    2.66 -
    2.67 -lemma in_quotient_imp_closed:
    2.68 -"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
    2.69 -unfolding quotient_def equiv_def trans_def by blast
    2.70 -
    2.71 -lemma in_quotient_imp_subset:
    2.72 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
    2.73 -using assms in_quotient_imp_in_rel equiv_type by fastforce
    2.74 -
    2.75 -lemma equiv_Eps_in:
    2.76 -"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
    2.77 -apply (rule someI2_ex)
    2.78 -using in_quotient_imp_non_empty by blast
    2.79 -
    2.80 -lemma equiv_Eps_preserves:
    2.81 -assumes ECH: "equiv A r" and X: "X \<in> A//r"
    2.82 -shows "Eps (%x. x \<in> X) \<in> A"
    2.83 -apply (rule in_mono[rule_format])
    2.84 - using assms apply (rule in_quotient_imp_subset)
    2.85 -by (rule equiv_Eps_in) (rule assms)+
    2.86 -
    2.87 -lemma proj_Eps:
    2.88 -assumes "equiv A r" and "X \<in> A//r"
    2.89 -shows "proj r (Eps (%x. x \<in> X)) = X"
    2.90 -unfolding proj_def proof auto
    2.91 -  fix x assume x: "x \<in> X"
    2.92 -  thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
    2.93 -next
    2.94 -  fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
    2.95 -  thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
    2.96 -qed
    2.97 -
    2.98 -(*
    2.99 -lemma Eps_proj:
   2.100 -assumes "equiv A r" and "x \<in> A"
   2.101 -shows "(Eps (%y. y \<in> proj r x), x) \<in> r"
   2.102 -proof-
   2.103 -  have 1: "proj r x \<in> A//r" using assms proj_preserves by fastforce
   2.104 -  hence "Eps(%y. y \<in> proj r x) \<in> proj r x" using assms equiv_Eps_in by auto
   2.105 -  moreover have "x \<in> proj r x" using assms in_proj by fastforce
   2.106 -  ultimately show ?thesis using assms 1 in_quotient_imp_in_rel by fastforce
   2.107 -qed
   2.108 -
   2.109 -lemma equiv_Eps_iff:
   2.110 -assumes "equiv A r" and "{X,Y} \<subseteq> A//r"
   2.111 -shows "((Eps (%x. x \<in> X),Eps (%y. y \<in> Y)) \<in> r) = (X = Y)"
   2.112 -proof-
   2.113 -  have "Eps (%x. x \<in> X) \<in> X \<and> Eps (%y. y \<in> Y) \<in> Y" using assms equiv_Eps_in by auto
   2.114 -  thus ?thesis using assms quotient_eq_iff by fastforce
   2.115 -qed
   2.116 -
   2.117 -lemma equiv_Eps_inj_on:
   2.118 -assumes "equiv A r"
   2.119 -shows "inj_on (%X. Eps (%x. x \<in> X)) (A//r)"
   2.120 -unfolding inj_on_def proof clarify
   2.121 -  fix X Y assume X: "X \<in> A//r" and Y: "Y \<in> A//r" and Eps: "Eps (%x. x \<in> X) = Eps (%y. y \<in> Y)"
   2.122 -  hence "Eps (%x. x \<in> X) \<in> A" using assms equiv_Eps_preserves by auto
   2.123 -  hence "(Eps (%x. x \<in> X), Eps (%y. y \<in> Y)) \<in> r"
   2.124 -  using assms Eps unfolding quotient_def equiv_def refl_on_def by auto
   2.125 -  thus "X= Y" using X Y assms equiv_Eps_iff by auto
   2.126 -qed
   2.127 -*)
   2.128 -
   2.129 -lemma univ_commute:
   2.130 -assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
   2.131 -shows "(univ f) (proj r x) = f x"
   2.132 -unfolding univ_def proof -
   2.133 -  have prj: "proj r x \<in> A//r" using x proj_preserves by fast
   2.134 -  hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
   2.135 -  moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
   2.136 -  ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
   2.137 -  thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
   2.138 -qed
   2.139 -
   2.140 -(*
   2.141 -lemma univ_unique:
   2.142 -assumes ECH: "equiv A r" and
   2.143 -        RES: "f respects r" and  COM: "\<forall> x \<in> A. G (proj r x) = f x"
   2.144 -shows "\<forall> X \<in> A//r. G X = univ f X"
   2.145 -proof
   2.146 -  fix X assume "X \<in> A//r"
   2.147 -  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   2.148 -  have "G X = f x" unfolding X using x COM by simp
   2.149 -  thus "G X = univ f X" unfolding X using ECH RES x univ_commute by fastforce
   2.150 -qed
   2.151 -*)
   2.152 -
   2.153 -lemma univ_preserves:
   2.154 -assumes ECH: "equiv A r" and RES: "f respects r" and
   2.155 -        PRES: "\<forall> x \<in> A. f x \<in> B"
   2.156 -shows "\<forall> X \<in> A//r. univ f X \<in> B"
   2.157 -proof
   2.158 -  fix X assume "X \<in> A//r"
   2.159 -  then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
   2.160 -  hence "univ f X = f x" using assms univ_commute by fastforce
   2.161 -  thus "univ f X \<in> B" using x PRES by simp
   2.162 -qed
   2.163 -
   2.164 -end
     3.1 --- a/src/HOL/Equiv_Relations.thy	Thu Jan 16 18:37:37 2014 +0100
     3.2 +++ b/src/HOL/Equiv_Relations.thy	Thu Jan 16 18:52:50 2014 +0100
     3.3 @@ -160,6 +160,7 @@
     3.4  apply blast
     3.5  done
     3.6  
     3.7 +
     3.8  subsection {* Defining unary operations upon equivalence classes *}
     3.9  
    3.10  text{*A congruence-preserving function*}
    3.11 @@ -354,6 +355,54 @@
    3.12  done
    3.13  
    3.14  
    3.15 +subsection {* Projection *}
    3.16 +
    3.17 +definition proj where "proj r x = r `` {x}"
    3.18 +
    3.19 +lemma proj_preserves:
    3.20 +"x \<in> A \<Longrightarrow> proj r x \<in> A//r"
    3.21 +unfolding proj_def by (rule quotientI)
    3.22 +
    3.23 +lemma proj_in_iff:
    3.24 +assumes "equiv A r"
    3.25 +shows "(proj r x \<in> A//r) = (x \<in> A)"
    3.26 +apply(rule iffI, auto simp add: proj_preserves)
    3.27 +unfolding proj_def quotient_def proof clarsimp
    3.28 +  fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}"
    3.29 +  moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
    3.30 +  ultimately have "(x,y) \<in> r" by blast
    3.31 +  thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast
    3.32 +qed
    3.33 +
    3.34 +lemma proj_iff:
    3.35 +"\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)"
    3.36 +by (simp add: proj_def eq_equiv_class_iff)
    3.37 +
    3.38 +(*
    3.39 +lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
    3.40 +unfolding proj_def equiv_def refl_on_def by blast
    3.41 +*)
    3.42 +
    3.43 +lemma proj_image: "(proj r) ` A = A//r"
    3.44 +unfolding proj_def[abs_def] quotient_def by blast
    3.45 +
    3.46 +lemma in_quotient_imp_non_empty:
    3.47 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}"
    3.48 +unfolding quotient_def using equiv_class_self by fast
    3.49 +
    3.50 +lemma in_quotient_imp_in_rel:
    3.51 +"\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
    3.52 +using quotient_eq_iff[THEN iffD1] by fastforce
    3.53 +
    3.54 +lemma in_quotient_imp_closed:
    3.55 +"\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
    3.56 +unfolding quotient_def equiv_def trans_def by blast
    3.57 +
    3.58 +lemma in_quotient_imp_subset:
    3.59 +"\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
    3.60 +using assms in_quotient_imp_in_rel equiv_type by fastforce
    3.61 +
    3.62 +
    3.63  subsection {* Equivalence relations -- predicate version *}
    3.64  
    3.65  text {* Partial equivalences *}