src/HOL/Equiv_Relations.thy
 author paulson Mon Feb 22 14:37:56 2016 +0000 (2016-02-22) changeset 62379 340738057c8c parent 61952 546958347e05 child 63092 a949b2a5f51d permissions -rw-r--r--
An assortment of useful lemmas about sums, norm, etc. Also: norm_conv_dist [symmetric] is now a simprule!
 haftmann@29655  1 (* Authors: Lawrence C Paulson, Cambridge University Computer Laboratory  paulson@15300  2  Copyright 1996 University of Cambridge  paulson@15300  3 *)  paulson@15300  4 wenzelm@60758  5 section \Equivalence Relations in Higher-Order Set Theory\  paulson@15300  6 paulson@15300  7 theory Equiv_Relations  haftmann@54744  8 imports Groups_Big Relation  paulson@15300  9 begin  paulson@15300  10 wenzelm@60758  11 subsection \Equivalence relations -- set version\  paulson@15300  12 haftmann@40812  13 definition equiv :: "'a set \ ('a \ 'a) set \ bool" where  haftmann@40812  14  "equiv A r \ refl_on A r \ sym r \ trans r"  paulson@15300  15 haftmann@40815  16 lemma equivI:  haftmann@40815  17  "refl_on A r \ sym r \ trans r \ equiv A r"  haftmann@40815  18  by (simp add: equiv_def)  haftmann@40815  19 haftmann@40815  20 lemma equivE:  haftmann@40815  21  assumes "equiv A r"  haftmann@40815  22  obtains "refl_on A r" and "sym r" and "trans r"  haftmann@40815  23  using assms by (simp add: equiv_def)  haftmann@40815  24 wenzelm@60758  25 text \  wenzelm@61799  26  Suppes, Theorem 70: \r\ is an equiv relation iff \r\ O  wenzelm@61799  27  r = r\.  paulson@15300  28 wenzelm@61799  29  First half: \equiv A r ==> r\ O r = r\.  wenzelm@60758  30 \  paulson@15300  31 paulson@15300  32 lemma sym_trans_comp_subset:  paulson@15300  33  "sym r ==> trans r ==> r\ O r \ r"  haftmann@46752  34  by (unfold trans_def sym_def converse_unfold) blast  paulson@15300  35 nipkow@30198  36 lemma refl_on_comp_subset: "refl_on A r ==> r \ r\ O r"  nipkow@30198  37  by (unfold refl_on_def) blast  paulson@15300  38 paulson@15300  39 lemma equiv_comp_eq: "equiv A r ==> r\ O r = r"  paulson@15300  40  apply (unfold equiv_def)  paulson@15300  41  apply clarify  paulson@15300  42  apply (rule equalityI)  nipkow@30198  43  apply (iprover intro: sym_trans_comp_subset refl_on_comp_subset)+  paulson@15300  44  done  paulson@15300  45 wenzelm@60758  46 text \Second half.\  paulson@15300  47 paulson@15300  48 lemma comp_equivI:  paulson@15300  49  "r\ O r = r ==> Domain r = A ==> equiv A r"  nipkow@30198  50  apply (unfold equiv_def refl_on_def sym_def trans_def)  paulson@15300  51  apply (erule equalityE)  paulson@15300  52  apply (subgoal_tac "\x y. (x, y) \ r --> (y, x) \ r")  paulson@15300  53  apply fast  paulson@15300  54  apply fast  paulson@15300  55  done  paulson@15300  56 paulson@15300  57 wenzelm@60758  58 subsection \Equivalence classes\  paulson@15300  59 paulson@15300  60 lemma equiv_class_subset:  paulson@15300  61  "equiv A r ==> (a, b) \ r ==> r{a} \ r{b}"  wenzelm@61799  62  \ \lemma for the next result\  paulson@15300  63  by (unfold equiv_def trans_def sym_def) blast  paulson@15300  64 paulson@15300  65 theorem equiv_class_eq: "equiv A r ==> (a, b) \ r ==> r{a} = r{b}"  paulson@15300  66  apply (assumption | rule equalityI equiv_class_subset)+  paulson@15300  67  apply (unfold equiv_def sym_def)  paulson@15300  68  apply blast  paulson@15300  69  done  paulson@15300  70 paulson@15300  71 lemma equiv_class_self: "equiv A r ==> a \ A ==> a \ r{a}"  nipkow@30198  72  by (unfold equiv_def refl_on_def) blast  paulson@15300  73 paulson@15300  74 lemma subset_equiv_class:  paulson@15300  75  "equiv A r ==> r{b} \ r{a} ==> b \ A ==> (a,b) \ r"  wenzelm@61799  76  \ \lemma for the next result\  nipkow@30198  77  by (unfold equiv_def refl_on_def) blast  paulson@15300  78 paulson@15300  79 lemma eq_equiv_class:  paulson@15300  80  "r{a} = r{b} ==> equiv A r ==> b \ A ==> (a, b) \ r"  nipkow@17589  81  by (iprover intro: equalityD2 subset_equiv_class)  paulson@15300  82 paulson@15300  83 lemma equiv_class_nondisjoint:  paulson@15300  84  "equiv A r ==> x \ (r{a} \ r{b}) ==> (a, b) \ r"  paulson@15300  85  by (unfold equiv_def trans_def sym_def) blast  paulson@15300  86 paulson@15300  87 lemma equiv_type: "equiv A r ==> r \ A \ A"  nipkow@30198  88  by (unfold equiv_def refl_on_def) blast  paulson@15300  89 paulson@15300  90 theorem equiv_class_eq_iff:  paulson@15300  91  "equiv A r ==> ((x, y) \ r) = (r{x} = r{y} & x \ A & y \ A)"  paulson@15300  92  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)  paulson@15300  93 paulson@15300  94 theorem eq_equiv_class_iff:  paulson@15300  95  "equiv A r ==> x \ A ==> y \ A ==> (r{x} = r{y}) = ((x, y) \ r)"  paulson@15300  96  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)  paulson@15300  97 paulson@15300  98 wenzelm@60758  99 subsection \Quotients\  paulson@15300  100 haftmann@28229  101 definition quotient :: "'a set \ ('a \ 'a) set \ 'a set set" (infixl "'/'/" 90) where  wenzelm@61799  102  "A//r = (\x \ A. {r{x}})" \ \set of equiv classes\  paulson@15300  103 paulson@15300  104 lemma quotientI: "x \ A ==> r{x} \ A//r"  paulson@15300  105  by (unfold quotient_def) blast  paulson@15300  106 paulson@15300  107 lemma quotientE:  paulson@15300  108  "X \ A//r ==> (!!x. X = r{x} ==> x \ A ==> P) ==> P"  paulson@15300  109  by (unfold quotient_def) blast  paulson@15300  110 wenzelm@61952  111 lemma Union_quotient: "equiv A r ==> \(A//r) = A"  nipkow@30198  112  by (unfold equiv_def refl_on_def quotient_def) blast  paulson@15300  113 paulson@15300  114 lemma quotient_disj:  paulson@15300  115  "equiv A r ==> X \ A//r ==> Y \ A//r ==> X = Y | (X \ Y = {})"  paulson@15300  116  apply (unfold quotient_def)  paulson@15300  117  apply clarify  paulson@15300  118  apply (rule equiv_class_eq)  paulson@15300  119  apply assumption  paulson@15300  120  apply (unfold equiv_def trans_def sym_def)  paulson@15300  121  apply blast  paulson@15300  122  done  paulson@15300  123 paulson@15300  124 lemma quotient_eqI:  paulson@15300  125  "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y; (x,y) \ r|] ==> X = Y"  paulson@15300  126  apply (clarify elim!: quotientE)  paulson@15300  127  apply (rule equiv_class_eq, assumption)  paulson@15300  128  apply (unfold equiv_def sym_def trans_def, blast)  paulson@15300  129  done  paulson@15300  130 paulson@15300  131 lemma quotient_eq_iff:  paulson@15300  132  "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y|] ==> (X = Y) = ((x,y) \ r)"  paulson@15300  133  apply (rule iffI)  paulson@15300  134  prefer 2 apply (blast del: equalityI intro: quotient_eqI)  paulson@15300  135  apply (clarify elim!: quotientE)  paulson@15300  136  apply (unfold equiv_def sym_def trans_def, blast)  paulson@15300  137  done  paulson@15300  138 nipkow@18493  139 lemma eq_equiv_class_iff2:  nipkow@18493  140  "\ equiv A r; x \ A; y \ A \ \ ({x}//r = {y}//r) = ((x,y) : r)"  nipkow@18493  141 by(simp add:quotient_def eq_equiv_class_iff)  nipkow@18493  142 paulson@15300  143 paulson@15300  144 lemma quotient_empty [simp]: "{}//r = {}"  paulson@15300  145 by(simp add: quotient_def)  paulson@15300  146 paulson@15300  147 lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"  paulson@15300  148 by(simp add: quotient_def)  paulson@15300  149 paulson@15300  150 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"  paulson@15300  151 by(simp add: quotient_def)  paulson@15300  152 paulson@15300  153 nipkow@15302  154 lemma singleton_quotient: "{x}//r = {r  {x}}"  nipkow@15302  155 by(simp add:quotient_def)  nipkow@15302  156 nipkow@15302  157 lemma quotient_diff1:  nipkow@15302  158  "\ inj_on (%a. {a}//r) A; a \ A \ \ (A - {a})//r = A//r - {a}//r"  nipkow@15302  159 apply(simp add:quotient_def inj_on_def)  nipkow@15302  160 apply blast  nipkow@15302  161 done  nipkow@15302  162 wenzelm@60758  163 subsection \Refinement of one equivalence relation WRT another\  lp15@59528  164 lp15@59528  165 lemma refines_equiv_class_eq:  lp15@59528  166  "\R \ S; equiv A R; equiv A S\ \ R(S{a}) = S{a}"  lp15@59528  167  by (auto simp: equiv_class_eq_iff)  lp15@59528  168 lp15@59528  169 lemma refines_equiv_class_eq2:  lp15@59528  170  "\R \ S; equiv A R; equiv A S\ \ S(R{a}) = S{a}"  lp15@59528  171  by (auto simp: equiv_class_eq_iff)  lp15@59528  172 lp15@59528  173 lemma refines_equiv_image_eq:  lp15@59528  174  "\R \ S; equiv A R; equiv A S\ \ (\X. SX)  (A//R) = A//S"  lp15@59528  175  by (auto simp: quotient_def image_UN refines_equiv_class_eq2)  lp15@59528  176 lp15@59528  177 lemma finite_refines_finite:  lp15@59528  178  "\finite (A//R); R \ S; equiv A R; equiv A S\ \ finite (A//S)"  lp15@59528  179  apply (erule finite_surj [where f = "\X. SX"])  lp15@59528  180  apply (simp add: refines_equiv_image_eq)  lp15@59528  181  done  lp15@59528  182 lp15@59528  183 lemma finite_refines_card_le:  lp15@59528  184  "\finite (A//R); R \ S; equiv A R; equiv A S\ \ card (A//S) \ card (A//R)"  lp15@59528  185  apply (subst refines_equiv_image_eq [of R S A, symmetric])  lp15@59528  186  apply (auto simp: card_image_le [where f = "\X. SX"])  lp15@59528  187  done  lp15@59528  188 blanchet@55022  189 wenzelm@60758  190 subsection \Defining unary operations upon equivalence classes\  paulson@15300  191 wenzelm@60758  192 text\A congruence-preserving function\  haftmann@40816  193 haftmann@44278  194 definition congruent :: "('a \ 'a) set \ ('a \ 'b) \ bool" where  haftmann@40817  195  "congruent r f \ (\(y, z) \ r. f y = f z)"  haftmann@40816  196 haftmann@40816  197 lemma congruentI:  haftmann@40816  198  "(\y z. (y, z) \ r \ f y = f z) \ congruent r f"  haftmann@40817  199  by (auto simp add: congruent_def)  haftmann@40816  200 haftmann@40816  201 lemma congruentD:  haftmann@40816  202  "congruent r f \ (y, z) \ r \ f y = f z"  haftmann@40817  203  by (auto simp add: congruent_def)  paulson@15300  204 wenzelm@19363  205 abbreviation  wenzelm@21404  206  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  wenzelm@21404  207  (infixr "respects" 80) where  wenzelm@19363  208  "f respects r == congruent r f"  paulson@15300  209 paulson@15300  210 paulson@15300  211 lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c"  wenzelm@61799  212  \ \lemma required to prove \UN_equiv_class\\  paulson@15300  213  by auto  paulson@15300  214 paulson@15300  215 lemma UN_equiv_class:  paulson@15300  216  "equiv A r ==> f respects r ==> a \ A  paulson@15300  217  ==> (\x \ r{a}. f x) = f a"  wenzelm@61799  218  \ \Conversion rule\  paulson@15300  219  apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)  paulson@15300  220  apply (unfold equiv_def congruent_def sym_def)  paulson@15300  221  apply (blast del: equalityI)  paulson@15300  222  done  paulson@15300  223 paulson@15300  224 lemma UN_equiv_class_type:  paulson@15300  225  "equiv A r ==> f respects r ==> X \ A//r ==>  paulson@15300  226  (!!x. x \ A ==> f x \ B) ==> (\x \ X. f x) \ B"  paulson@15300  227  apply (unfold quotient_def)  paulson@15300  228  apply clarify  paulson@15300  229  apply (subst UN_equiv_class)  paulson@15300  230  apply auto  paulson@15300  231  done  paulson@15300  232 wenzelm@60758  233 text \  paulson@15300  234  Sufficient conditions for injectiveness. Could weaken premises!  wenzelm@61799  235  major premise could be an inclusion; bcong could be \!!y. y \  wenzelm@61799  236  A ==> f y \ B\.  wenzelm@60758  237 \  paulson@15300  238 paulson@15300  239 lemma UN_equiv_class_inject:  paulson@15300  240  "equiv A r ==> f respects r ==>  paulson@15300  241  (\x \ X. f x) = (\y \ Y. f y) ==> X \ A//r ==> Y \ A//r  paulson@15300  242  ==> (!!x y. x \ A ==> y \ A ==> f x = f y ==> (x, y) \ r)  paulson@15300  243  ==> X = Y"  paulson@15300  244  apply (unfold quotient_def)  paulson@15300  245  apply clarify  paulson@15300  246  apply (rule equiv_class_eq)  paulson@15300  247  apply assumption  paulson@15300  248  apply (subgoal_tac "f x = f xa")  paulson@15300  249  apply blast  paulson@15300  250  apply (erule box_equals)  paulson@15300  251  apply (assumption | rule UN_equiv_class)+  paulson@15300  252  done  paulson@15300  253 paulson@15300  254 wenzelm@60758  255 subsection \Defining binary operations upon equivalence classes\  paulson@15300  256 wenzelm@60758  257 text\A congruence-preserving function of two arguments\  haftmann@40817  258 haftmann@44278  259 definition congruent2 :: "('a \ 'a) set \ ('b \ 'b) set \ ('a \ 'b \ 'c) \ bool" where  haftmann@40817  260  "congruent2 r1 r2 f \ (\(y1, z1) \ r1. \(y2, z2) \ r2. f y1 y2 = f z1 z2)"  haftmann@40817  261 haftmann@40817  262 lemma congruent2I':  haftmann@40817  263  assumes "\y1 z1 y2 z2. (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"  haftmann@40817  264  shows "congruent2 r1 r2 f"  haftmann@40817  265  using assms by (auto simp add: congruent2_def)  haftmann@40817  266 haftmann@40817  267 lemma congruent2D:  haftmann@40817  268  "congruent2 r1 r2 f \ (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"  haftmann@40817  269  using assms by (auto simp add: congruent2_def)  paulson@15300  270 wenzelm@60758  271 text\Abbreviation for the common case where the relations are identical\  nipkow@19979  272 abbreviation  wenzelm@21404  273  RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"  wenzelm@21749  274  (infixr "respects2" 80) where  nipkow@19979  275  "f respects2 r == congruent2 r r f"  nipkow@19979  276 paulson@15300  277 paulson@15300  278 lemma congruent2_implies_congruent:  paulson@15300  279  "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)"  nipkow@30198  280  by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast  paulson@15300  281 paulson@15300  282 lemma congruent2_implies_congruent_UN:  paulson@15300  283  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==>  paulson@15300  284  congruent r1 (\x1. \x2 \ r2{a}. f x1 x2)"  paulson@15300  285  apply (unfold congruent_def)  paulson@15300  286  apply clarify  paulson@15300  287  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)  paulson@15300  288  apply (simp add: UN_equiv_class congruent2_implies_congruent)  nipkow@30198  289  apply (unfold congruent2_def equiv_def refl_on_def)  paulson@15300  290  apply (blast del: equalityI)  paulson@15300  291  done  paulson@15300  292 paulson@15300  293 lemma UN_equiv_class2:  paulson@15300  294  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2  paulson@15300  295  ==> (\x1 \ r1{a1}. \x2 \ r2{a2}. f x1 x2) = f a1 a2"  paulson@15300  296  by (simp add: UN_equiv_class congruent2_implies_congruent  paulson@15300  297  congruent2_implies_congruent_UN)  paulson@15300  298 paulson@15300  299 lemma UN_equiv_class_type2:  paulson@15300  300  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f  paulson@15300  301  ==> X1 \ A1//r1 ==> X2 \ A2//r2  paulson@15300  302  ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B)  paulson@15300  303  ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B"  paulson@15300  304  apply (unfold quotient_def)  paulson@15300  305  apply clarify  paulson@15300  306  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN  paulson@15300  307  congruent2_implies_congruent quotientI)  paulson@15300  308  done  paulson@15300  309 paulson@15300  310 lemma UN_UN_split_split_eq:  paulson@15300  311  "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) =  paulson@15300  312  (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)"  wenzelm@61799  313  \ \Allows a natural expression of binary operators,\  wenzelm@61799  314  \ \without explicit calls to \split\\  paulson@15300  315  by auto  paulson@15300  316 paulson@15300  317 lemma congruent2I:  paulson@15300  318  "equiv A1 r1 ==> equiv A2 r2  paulson@15300  319  ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w)  paulson@15300  320  ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z)  paulson@15300  321  ==> congruent2 r1 r2 f"  wenzelm@61799  322  \ \Suggested by John Harrison -- the two subproofs may be\  wenzelm@61799  323  \ \\emph{much} simpler than the direct proof.\  nipkow@30198  324  apply (unfold congruent2_def equiv_def refl_on_def)  paulson@15300  325  apply clarify  paulson@15300  326  apply (blast intro: trans)  paulson@15300  327  done  paulson@15300  328 paulson@15300  329 lemma congruent2_commuteI:  paulson@15300  330  assumes equivA: "equiv A r"  paulson@15300  331  and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y"  paulson@15300  332  and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z"  paulson@15300  333  shows "f respects2 r"  paulson@15300  334  apply (rule congruent2I [OF equivA equivA])  paulson@15300  335  apply (rule commute [THEN trans])  paulson@15300  336  apply (rule_tac [3] commute [THEN trans, symmetric])  paulson@15300  337  apply (rule_tac [5] sym)  haftmann@25482  338  apply (rule congt | assumption |  paulson@15300  339  erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+  paulson@15300  340  done  paulson@15300  341 haftmann@24728  342 wenzelm@60758  343 subsection \Quotients and finiteness\  haftmann@24728  344 wenzelm@60758  345 text \Suggested by Florian KammÃ¼ller\  haftmann@24728  346 haftmann@24728  347 lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)"  wenzelm@61799  348  \ \recall @{thm equiv_type}\  haftmann@24728  349  apply (rule finite_subset)  haftmann@24728  350  apply (erule_tac [2] finite_Pow_iff [THEN iffD2])  haftmann@24728  351  apply (unfold quotient_def)  haftmann@24728  352  apply blast  haftmann@24728  353  done  haftmann@24728  354 haftmann@24728  355 lemma finite_equiv_class:  haftmann@24728  356  "finite A ==> r \ A \ A ==> X \ A//r ==> finite X"  haftmann@24728  357  apply (unfold quotient_def)  haftmann@24728  358  apply (rule finite_subset)  haftmann@24728  359  prefer 2 apply assumption  haftmann@24728  360  apply blast  haftmann@24728  361  done  haftmann@24728  362 haftmann@24728  363 lemma equiv_imp_dvd_card:  haftmann@24728  364  "finite A ==> equiv A r ==> \X \ A//r. k dvd card X  haftmann@24728  365  ==> k dvd card A"  berghofe@26791  366  apply (rule Union_quotient [THEN subst [where P="\A. k dvd card A"]])  haftmann@24728  367  apply assumption  haftmann@24728  368  apply (rule dvd_partition)  haftmann@24728  369  prefer 3 apply (blast dest: quotient_disj)  haftmann@24728  370  apply (simp_all add: Union_quotient equiv_type)  haftmann@24728  371  done  haftmann@24728  372 haftmann@24728  373 lemma card_quotient_disjoint:  haftmann@24728  374  "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A"  haftmann@24728  375 apply(simp add:quotient_def)  haftmann@24728  376 apply(subst card_UN_disjoint)  haftmann@24728  377  apply assumption  haftmann@24728  378  apply simp  nipkow@44890  379  apply(fastforce simp add:inj_on_def)  huffman@35216  380 apply simp  haftmann@24728  381 done  haftmann@24728  382 haftmann@40812  383 wenzelm@60758  384 subsection \Projection\  blanchet@55022  385 blanchet@55022  386 definition proj where "proj r x = r  {x}"  blanchet@55022  387 blanchet@55022  388 lemma proj_preserves:  blanchet@55022  389 "x \ A \ proj r x \ A//r"  blanchet@55022  390 unfolding proj_def by (rule quotientI)  blanchet@55022  391 blanchet@55022  392 lemma proj_in_iff:  blanchet@55022  393 assumes "equiv A r"  blanchet@55022  394 shows "(proj r x \ A//r) = (x \ A)"  blanchet@55022  395 apply(rule iffI, auto simp add: proj_preserves)  blanchet@55022  396 unfolding proj_def quotient_def proof clarsimp  blanchet@55022  397  fix y assume y: "y \ A" and "r  {x} = r  {y}"  blanchet@55022  398  moreover have "y \ r  {y}" using assms y unfolding equiv_def refl_on_def by blast  blanchet@55022  399  ultimately have "(x,y) \ r" by blast  blanchet@55022  400  thus "x \ A" using assms unfolding equiv_def refl_on_def by blast  blanchet@55022  401 qed  blanchet@55022  402 blanchet@55022  403 lemma proj_iff:  blanchet@55022  404 "\equiv A r; {x,y} \ A\ \ (proj r x = proj r y) = ((x,y) \ r)"  blanchet@55022  405 by (simp add: proj_def eq_equiv_class_iff)  blanchet@55022  406 blanchet@55022  407 (*  blanchet@55022  408 lemma in_proj: "\equiv A r; x \ A\ \ x \ proj r x"  blanchet@55022  409 unfolding proj_def equiv_def refl_on_def by blast  blanchet@55022  410 *)  blanchet@55022  411 blanchet@55022  412 lemma proj_image: "(proj r)  A = A//r"  blanchet@55022  413 unfolding proj_def[abs_def] quotient_def by blast  blanchet@55022  414 blanchet@55022  415 lemma in_quotient_imp_non_empty:  blanchet@55022  416 "\equiv A r; X \ A//r\ \ X \ {}"  blanchet@55022  417 unfolding quotient_def using equiv_class_self by fast  blanchet@55022  418 blanchet@55022  419 lemma in_quotient_imp_in_rel:  blanchet@55022  420 "\equiv A r; X \ A//r; {x,y} \ X\ \ (x,y) \ r"  blanchet@55022  421 using quotient_eq_iff[THEN iffD1] by fastforce  blanchet@55022  422 blanchet@55022  423 lemma in_quotient_imp_closed:  blanchet@55022  424 "\equiv A r; X \ A//r; x \ X; (x,y) \ r\ \ y \ X"  blanchet@55022  425 unfolding quotient_def equiv_def trans_def by blast  blanchet@55022  426 blanchet@55022  427 lemma in_quotient_imp_subset:  blanchet@55022  428 "\equiv A r; X \ A//r\ \ X \ A"  blanchet@55022  429 using assms in_quotient_imp_in_rel equiv_type by fastforce  blanchet@55022  430 blanchet@55022  431 wenzelm@60758  432 subsection \Equivalence relations -- predicate version\  haftmann@40812  433 wenzelm@60758  434 text \Partial equivalences\  haftmann@40812  435 haftmann@40812  436 definition part_equivp :: "('a \ 'a \ bool) \ bool" where  haftmann@40812  437  "part_equivp R \ (\x. R x x) \ (\x y. R x y \ R x x \ R y y \ R x = R y)"  wenzelm@61799  438  \ \John-Harrison-style characterization\  haftmann@40812  439 haftmann@40812  440 lemma part_equivpI:  haftmann@40812  441  "(\x. R x x) \ symp R \ transp R \ part_equivp R"  haftmann@45969  442  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)  haftmann@40812  443 haftmann@40812  444 lemma part_equivpE:  haftmann@40812  445  assumes "part_equivp R"  haftmann@40812  446  obtains x where "R x x" and "symp R" and "transp R"  haftmann@40812  447 proof -  haftmann@40812  448  from assms have 1: "\x. R x x"  haftmann@40812  449  and 2: "\x y. R x y \ R x x \ R y y \ R x = R y"  haftmann@40812  450  by (unfold part_equivp_def) blast+  haftmann@40812  451  from 1 obtain x where "R x x" ..  haftmann@40812  452  moreover have "symp R"  haftmann@40812  453  proof (rule sympI)  haftmann@40812  454  fix x y  haftmann@40812  455  assume "R x y"  haftmann@40812  456  with 2 [of x y] show "R y x" by auto  haftmann@40812  457  qed  haftmann@40812  458  moreover have "transp R"  haftmann@40812  459  proof (rule transpI)  haftmann@40812  460  fix x y z  haftmann@40812  461  assume "R x y" and "R y z"  haftmann@40812  462  with 2 [of x y] 2 [of y z] show "R x z" by auto  haftmann@40812  463  qed  haftmann@40812  464  ultimately show thesis by (rule that)  haftmann@40812  465 qed  haftmann@40812  466 haftmann@40812  467 lemma part_equivp_refl_symp_transp:  haftmann@40812  468  "part_equivp R \ (\x. R x x) \ symp R \ transp R"  haftmann@40812  469  by (auto intro: part_equivpI elim: part_equivpE)  haftmann@40812  470 haftmann@40812  471 lemma part_equivp_symp:  haftmann@40812  472  "part_equivp R \ R x y \ R y x"  haftmann@40812  473  by (erule part_equivpE, erule sympE)  haftmann@40812  474 haftmann@40812  475 lemma part_equivp_transp:  haftmann@40812  476  "part_equivp R \ R x y \ R y z \ R x z"  haftmann@40812  477  by (erule part_equivpE, erule transpE)  haftmann@40812  478 haftmann@40812  479 lemma part_equivp_typedef:  kaliszyk@44204  480  "part_equivp R \ \d. d \ {c. \x. R x x \ c = Collect (R x)}"  kaliszyk@44204  481  by (auto elim: part_equivpE)  haftmann@40812  482 haftmann@40812  483 wenzelm@60758  484 text \Total equivalences\  haftmann@40812  485 haftmann@40812  486 definition equivp :: "('a \ 'a \ bool) \ bool" where  wenzelm@61799  487  "equivp R \ (\x y. R x y = (R x = R y))" \ \John-Harrison-style characterization\  haftmann@40812  488 haftmann@40812  489 lemma equivpI:  haftmann@40812  490  "reflp R \ symp R \ transp R \ equivp R"  haftmann@45969  491  by (auto elim: reflpE sympE transpE simp add: equivp_def)  haftmann@40812  492 haftmann@40812  493 lemma equivpE:  haftmann@40812  494  assumes "equivp R"  haftmann@40812  495  obtains "reflp R" and "symp R" and "transp R"  haftmann@40812  496  using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)  haftmann@40812  497 haftmann@40812  498 lemma equivp_implies_part_equivp:  haftmann@40812  499  "equivp R \ part_equivp R"  haftmann@40812  500  by (auto intro: part_equivpI elim: equivpE reflpE)  haftmann@40812  501 haftmann@40812  502 lemma equivp_equiv:  haftmann@40812  503  "equiv UNIV A \ equivp (\x y. (x, y) \ A)"  haftmann@46752  504  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])  haftmann@40812  505 haftmann@40812  506 lemma equivp_reflp_symp_transp:  haftmann@40812  507  shows "equivp R \ reflp R \ symp R \ transp R"  haftmann@40812  508  by (auto intro: equivpI elim: equivpE)  haftmann@40812  509 haftmann@40812  510 lemma identity_equivp:  haftmann@40812  511  "equivp (op =)"  haftmann@40812  512  by (auto intro: equivpI reflpI sympI transpI)  haftmann@40812  513 haftmann@40812  514 lemma equivp_reflp:  haftmann@40812  515  "equivp R \ R x x"  haftmann@40812  516  by (erule equivpE, erule reflpE)  haftmann@40812  517 haftmann@40812  518 lemma equivp_symp:  haftmann@40812  519  "equivp R \ R x y \ R y x"  haftmann@40812  520  by (erule equivpE, erule sympE)  haftmann@40812  521 haftmann@40812  522 lemma equivp_transp:  haftmann@40812  523  "equivp R \ R x y \ R y z \ R x z"  haftmann@40812  524  by (erule equivpE, erule transpE)  haftmann@40812  525 blanchet@55024  526 hide_const (open) proj  blanchet@55024  527 paulson@15300  528 end