src/HOL/Codatatype/Equiv_Relations_More.thy
author blanchet
Mon Sep 17 21:33:12 2012 +0200 (2012-09-17)
changeset 49430 6df729c6a1a6
parent 48975 7f79f94a432c
child 49509 163914705f8d
permissions -rw-r--r--
tuned simpset
     1 (*  Title:      HOL/Codatatype/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 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