src/HOL/BNF/Equiv_Relations_More.thy
 author blanchet Tue Nov 19 01:29:50 2013 +0100 (2013-11-19) changeset 54483 9f24325c2550 parent 49510 ba50d204095e permissions -rw-r--r--
```     1 (*  Title:      HOL/BNF/Equiv_Relations_More.thy
```
```     2     Author:     Andrei Popescu, TU Muenchen
```
```     3     Copyright   2012
```
```     4
```
```     5 Some preliminaries on equivalence relations and quotients.
```
```     6 *)
```
```     7
```
```     8 header {* Some Preliminaries on Equivalence Relations and Quotients *}
```
```     9
```
```    10 theory Equiv_Relations_More
```
```    11 imports Equiv_Relations Hilbert_Choice
```
```    12 begin
```
```    13
```
```    14
```
```    15 (* Recall the following constants and lemmas:
```
```    16
```
```    17 term Eps
```
```    18 term "A//r"
```
```    19 lemmas equiv_def
```
```    20 lemmas refl_on_def
```
```    21  -- note that "reflexivity on" also assumes inclusion of the relation's field into r
```
```    22
```
```    23 *)
```
```    24
```
```    25 definition proj where "proj r x = r `` {x}"
```
```    26
```
```    27 definition univ where "univ f X == f (Eps (%x. x \<in> X))"
```
```    28
```
```    29 lemma proj_preserves:
```
```    30 "x \<in> A \<Longrightarrow> proj r x \<in> A//r"
```
```    31 unfolding proj_def by (rule quotientI)
```
```    32
```
```    33 lemma proj_in_iff:
```
```    34 assumes "equiv A r"
```
```    35 shows "(proj r x \<in> A//r) = (x \<in> A)"
```
```    36 apply(rule iffI, auto simp add: proj_preserves)
```
```    37 unfolding proj_def quotient_def proof clarsimp
```
```    38   fix y assume y: "y \<in> A" and "r `` {x} = r `` {y}"
```
```    39   moreover have "y \<in> r `` {y}" using assms y unfolding equiv_def refl_on_def by blast
```
```    40   ultimately have "(x,y) \<in> r" by blast
```
```    41   thus "x \<in> A" using assms unfolding equiv_def refl_on_def by blast
```
```    42 qed
```
```    43
```
```    44 lemma proj_iff:
```
```    45 "\<lbrakk>equiv A r; {x,y} \<subseteq> A\<rbrakk> \<Longrightarrow> (proj r x = proj r y) = ((x,y) \<in> r)"
```
```    46 by (simp add: proj_def eq_equiv_class_iff)
```
```    47
```
```    48 (*
```
```    49 lemma in_proj: "\<lbrakk>equiv A r; x \<in> A\<rbrakk> \<Longrightarrow> x \<in> proj r x"
```
```    50 unfolding proj_def equiv_def refl_on_def by blast
```
```    51 *)
```
```    52
```
```    53 lemma proj_image: "(proj r) ` A = A//r"
```
```    54 unfolding proj_def[abs_def] quotient_def by blast
```
```    55
```
```    56 lemma in_quotient_imp_non_empty:
```
```    57 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<noteq> {}"
```
```    58 unfolding quotient_def using equiv_class_self by fast
```
```    59
```
```    60 lemma in_quotient_imp_in_rel:
```
```    61 "\<lbrakk>equiv A r; X \<in> A//r; {x,y} \<subseteq> X\<rbrakk> \<Longrightarrow> (x,y) \<in> r"
```
```    62 using quotient_eq_iff[THEN iffD1] by fastforce
```
```    63
```
```    64 lemma in_quotient_imp_closed:
```
```    65 "\<lbrakk>equiv A r; X \<in> A//r; x \<in> X; (x,y) \<in> r\<rbrakk> \<Longrightarrow> y \<in> X"
```
```    66 unfolding quotient_def equiv_def trans_def by blast
```
```    67
```
```    68 lemma in_quotient_imp_subset:
```
```    69 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> X \<subseteq> A"
```
```    70 using assms in_quotient_imp_in_rel equiv_type by fastforce
```
```    71
```
```    72 lemma equiv_Eps_in:
```
```    73 "\<lbrakk>equiv A r; X \<in> A//r\<rbrakk> \<Longrightarrow> Eps (%x. x \<in> X) \<in> X"
```
```    74 apply (rule someI2_ex)
```
```    75 using in_quotient_imp_non_empty by blast
```
```    76
```
```    77 lemma equiv_Eps_preserves:
```
```    78 assumes ECH: "equiv A r" and X: "X \<in> A//r"
```
```    79 shows "Eps (%x. x \<in> X) \<in> A"
```
```    80 apply (rule in_mono[rule_format])
```
```    81  using assms apply (rule in_quotient_imp_subset)
```
```    82 by (rule equiv_Eps_in) (rule assms)+
```
```    83
```
```    84 lemma proj_Eps:
```
```    85 assumes "equiv A r" and "X \<in> A//r"
```
```    86 shows "proj r (Eps (%x. x \<in> X)) = X"
```
```    87 unfolding proj_def proof auto
```
```    88   fix x assume x: "x \<in> X"
```
```    89   thus "(Eps (%x. x \<in> X), x) \<in> r" using assms equiv_Eps_in in_quotient_imp_in_rel by fast
```
```    90 next
```
```    91   fix x assume "(Eps (%x. x \<in> X),x) \<in> r"
```
```    92   thus "x \<in> X" using in_quotient_imp_closed[OF assms equiv_Eps_in[OF assms]] by fast
```
```    93 qed
```
```    94
```
```    95 (*
```
```    96 lemma Eps_proj:
```
```    97 assumes "equiv A r" and "x \<in> A"
```
```    98 shows "(Eps (%y. y \<in> proj r x), x) \<in> r"
```
```    99 proof-
```
```   100   have 1: "proj r x \<in> A//r" using assms proj_preserves by fastforce
```
```   101   hence "Eps(%y. y \<in> proj r x) \<in> proj r x" using assms equiv_Eps_in by auto
```
```   102   moreover have "x \<in> proj r x" using assms in_proj by fastforce
```
```   103   ultimately show ?thesis using assms 1 in_quotient_imp_in_rel by fastforce
```
```   104 qed
```
```   105
```
```   106 lemma equiv_Eps_iff:
```
```   107 assumes "equiv A r" and "{X,Y} \<subseteq> A//r"
```
```   108 shows "((Eps (%x. x \<in> X),Eps (%y. y \<in> Y)) \<in> r) = (X = Y)"
```
```   109 proof-
```
```   110   have "Eps (%x. x \<in> X) \<in> X \<and> Eps (%y. y \<in> Y) \<in> Y" using assms equiv_Eps_in by auto
```
```   111   thus ?thesis using assms quotient_eq_iff by fastforce
```
```   112 qed
```
```   113
```
```   114 lemma equiv_Eps_inj_on:
```
```   115 assumes "equiv A r"
```
```   116 shows "inj_on (%X. Eps (%x. x \<in> X)) (A//r)"
```
```   117 unfolding inj_on_def proof clarify
```
```   118   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)"
```
```   119   hence "Eps (%x. x \<in> X) \<in> A" using assms equiv_Eps_preserves by auto
```
```   120   hence "(Eps (%x. x \<in> X), Eps (%y. y \<in> Y)) \<in> r"
```
```   121   using assms Eps unfolding quotient_def equiv_def refl_on_def by auto
```
```   122   thus "X= Y" using X Y assms equiv_Eps_iff by auto
```
```   123 qed
```
```   124 *)
```
```   125
```
```   126 lemma univ_commute:
```
```   127 assumes ECH: "equiv A r" and RES: "f respects r" and x: "x \<in> A"
```
```   128 shows "(univ f) (proj r x) = f x"
```
```   129 unfolding univ_def proof -
```
```   130   have prj: "proj r x \<in> A//r" using x proj_preserves by fast
```
```   131   hence "Eps (%y. y \<in> proj r x) \<in> A" using ECH equiv_Eps_preserves by fast
```
```   132   moreover have "proj r (Eps (%y. y \<in> proj r x)) = proj r x" using ECH prj proj_Eps by fast
```
```   133   ultimately have "(x, Eps (%y. y \<in> proj r x)) \<in> r" using x ECH proj_iff by fast
```
```   134   thus "f (Eps (%y. y \<in> proj r x)) = f x" using RES unfolding congruent_def by fastforce
```
```   135 qed
```
```   136
```
```   137 (*
```
```   138 lemma univ_unique:
```
```   139 assumes ECH: "equiv A r" and
```
```   140         RES: "f respects r" and  COM: "\<forall> x \<in> A. G (proj r x) = f x"
```
```   141 shows "\<forall> X \<in> A//r. G X = univ f X"
```
```   142 proof
```
```   143   fix X assume "X \<in> A//r"
```
```   144   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
```
```   145   have "G X = f x" unfolding X using x COM by simp
```
```   146   thus "G X = univ f X" unfolding X using ECH RES x univ_commute by fastforce
```
```   147 qed
```
```   148 *)
```
```   149
```
```   150 lemma univ_preserves:
```
```   151 assumes ECH: "equiv A r" and RES: "f respects r" and
```
```   152         PRES: "\<forall> x \<in> A. f x \<in> B"
```
```   153 shows "\<forall> X \<in> A//r. univ f X \<in> B"
```
```   154 proof
```
```   155   fix X assume "X \<in> A//r"
```
```   156   then obtain x where x: "x \<in> A" and X: "X = proj r x" using ECH proj_image[of r A] by blast
```
```   157   hence "univ f X = f x" using assms univ_commute by fastforce
```
```   158   thus "univ f X \<in> B" using x PRES by simp
```
```   159 qed
```
```   160
```
```   161 end
```