src/HOL/Equiv_Relations.thy
 author huffman Sun Apr 01 16:09:58 2012 +0200 (2012-04-01) changeset 47255 30a1692557b0 parent 46752 e9e7209eb375 child 51112 da97167e03f7 permissions -rw-r--r--
removed Nat_Numeral.thy, moving all theorems elsewhere
 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 paulson@15300  5 header {* Equivalence Relations in Higher-Order Set Theory *}  paulson@15300  6 paulson@15300  7 theory Equiv_Relations  haftmann@35725  8 imports Big_Operators Relation Plain  paulson@15300  9 begin  paulson@15300  10 haftmann@40812  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 paulson@15300  25 text {*  paulson@15300  26  Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\ O  paulson@15300  27  r = r"}.  paulson@15300  28 paulson@15300  29  First half: @{text "equiv A r ==> r\ O r = r"}.  paulson@15300  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 paulson@15300  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 paulson@15300  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}"  paulson@15300  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"  paulson@15300  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 paulson@15300  99 subsection {* Quotients *}  paulson@15300  100 haftmann@28229  101 definition quotient :: "'a set \ ('a \ 'a) set \ 'a set set" (infixl "'/'/" 90) where  haftmann@37767  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 paulson@15300  111 lemma Union_quotient: "equiv A r ==> Union (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 paulson@15300  163 subsection {* Defining unary operations upon equivalence classes *}  paulson@15300  164 paulson@15300  165 text{*A congruence-preserving function*}  haftmann@40816  166 haftmann@44278  167 definition congruent :: "('a \ 'a) set \ ('a \ 'b) \ bool" where  haftmann@40817  168  "congruent r f \ (\(y, z) \ r. f y = f z)"  haftmann@40816  169 haftmann@40816  170 lemma congruentI:  haftmann@40816  171  "(\y z. (y, z) \ r \ f y = f z) \ congruent r f"  haftmann@40817  172  by (auto simp add: congruent_def)  haftmann@40816  173 haftmann@40816  174 lemma congruentD:  haftmann@40816  175  "congruent r f \ (y, z) \ r \ f y = f z"  haftmann@40817  176  by (auto simp add: congruent_def)  paulson@15300  177 wenzelm@19363  178 abbreviation  wenzelm@21404  179  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  wenzelm@21404  180  (infixr "respects" 80) where  wenzelm@19363  181  "f respects r == congruent r f"  paulson@15300  182 paulson@15300  183 paulson@15300  184 lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c"  paulson@15300  185  -- {* lemma required to prove @{text UN_equiv_class} *}  paulson@15300  186  by auto  paulson@15300  187 paulson@15300  188 lemma UN_equiv_class:  paulson@15300  189  "equiv A r ==> f respects r ==> a \ A  paulson@15300  190  ==> (\x \ r{a}. f x) = f a"  paulson@15300  191  -- {* Conversion rule *}  paulson@15300  192  apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)  paulson@15300  193  apply (unfold equiv_def congruent_def sym_def)  paulson@15300  194  apply (blast del: equalityI)  paulson@15300  195  done  paulson@15300  196 paulson@15300  197 lemma UN_equiv_class_type:  paulson@15300  198  "equiv A r ==> f respects r ==> X \ A//r ==>  paulson@15300  199  (!!x. x \ A ==> f x \ B) ==> (\x \ X. f x) \ B"  paulson@15300  200  apply (unfold quotient_def)  paulson@15300  201  apply clarify  paulson@15300  202  apply (subst UN_equiv_class)  paulson@15300  203  apply auto  paulson@15300  204  done  paulson@15300  205 paulson@15300  206 text {*  paulson@15300  207  Sufficient conditions for injectiveness. Could weaken premises!  paulson@15300  208  major premise could be an inclusion; bcong could be @{text "!!y. y \  paulson@15300  209  A ==> f y \ B"}.  paulson@15300  210 *}  paulson@15300  211 paulson@15300  212 lemma UN_equiv_class_inject:  paulson@15300  213  "equiv A r ==> f respects r ==>  paulson@15300  214  (\x \ X. f x) = (\y \ Y. f y) ==> X \ A//r ==> Y \ A//r  paulson@15300  215  ==> (!!x y. x \ A ==> y \ A ==> f x = f y ==> (x, y) \ r)  paulson@15300  216  ==> X = Y"  paulson@15300  217  apply (unfold quotient_def)  paulson@15300  218  apply clarify  paulson@15300  219  apply (rule equiv_class_eq)  paulson@15300  220  apply assumption  paulson@15300  221  apply (subgoal_tac "f x = f xa")  paulson@15300  222  apply blast  paulson@15300  223  apply (erule box_equals)  paulson@15300  224  apply (assumption | rule UN_equiv_class)+  paulson@15300  225  done  paulson@15300  226 paulson@15300  227 paulson@15300  228 subsection {* Defining binary operations upon equivalence classes *}  paulson@15300  229 paulson@15300  230 text{*A congruence-preserving function of two arguments*}  haftmann@40817  231 haftmann@44278  232 definition congruent2 :: "('a \ 'a) set \ ('b \ 'b) set \ ('a \ 'b \ 'c) \ bool" where  haftmann@40817  233  "congruent2 r1 r2 f \ (\(y1, z1) \ r1. \(y2, z2) \ r2. f y1 y2 = f z1 z2)"  haftmann@40817  234 haftmann@40817  235 lemma congruent2I':  haftmann@40817  236  assumes "\y1 z1 y2 z2. (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"  haftmann@40817  237  shows "congruent2 r1 r2 f"  haftmann@40817  238  using assms by (auto simp add: congruent2_def)  haftmann@40817  239 haftmann@40817  240 lemma congruent2D:  haftmann@40817  241  "congruent2 r1 r2 f \ (y1, z1) \ r1 \ (y2, z2) \ r2 \ f y1 y2 = f z1 z2"  haftmann@40817  242  using assms by (auto simp add: congruent2_def)  paulson@15300  243 paulson@15300  244 text{*Abbreviation for the common case where the relations are identical*}  nipkow@19979  245 abbreviation  wenzelm@21404  246  RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"  wenzelm@21749  247  (infixr "respects2" 80) where  nipkow@19979  248  "f respects2 r == congruent2 r r f"  nipkow@19979  249 paulson@15300  250 paulson@15300  251 lemma congruent2_implies_congruent:  paulson@15300  252  "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)"  nipkow@30198  253  by (unfold congruent_def congruent2_def equiv_def refl_on_def) blast  paulson@15300  254 paulson@15300  255 lemma congruent2_implies_congruent_UN:  paulson@15300  256  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==>  paulson@15300  257  congruent r1 (\x1. \x2 \ r2{a}. f x1 x2)"  paulson@15300  258  apply (unfold congruent_def)  paulson@15300  259  apply clarify  paulson@15300  260  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)  paulson@15300  261  apply (simp add: UN_equiv_class congruent2_implies_congruent)  nipkow@30198  262  apply (unfold congruent2_def equiv_def refl_on_def)  paulson@15300  263  apply (blast del: equalityI)  paulson@15300  264  done  paulson@15300  265 paulson@15300  266 lemma UN_equiv_class2:  paulson@15300  267  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2  paulson@15300  268  ==> (\x1 \ r1{a1}. \x2 \ r2{a2}. f x1 x2) = f a1 a2"  paulson@15300  269  by (simp add: UN_equiv_class congruent2_implies_congruent  paulson@15300  270  congruent2_implies_congruent_UN)  paulson@15300  271 paulson@15300  272 lemma UN_equiv_class_type2:  paulson@15300  273  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f  paulson@15300  274  ==> X1 \ A1//r1 ==> X2 \ A2//r2  paulson@15300  275  ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B)  paulson@15300  276  ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B"  paulson@15300  277  apply (unfold quotient_def)  paulson@15300  278  apply clarify  paulson@15300  279  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN  paulson@15300  280  congruent2_implies_congruent quotientI)  paulson@15300  281  done  paulson@15300  282 paulson@15300  283 lemma UN_UN_split_split_eq:  paulson@15300  284  "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) =  paulson@15300  285  (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)"  paulson@15300  286  -- {* Allows a natural expression of binary operators, *}  paulson@15300  287  -- {* without explicit calls to @{text split} *}  paulson@15300  288  by auto  paulson@15300  289 paulson@15300  290 lemma congruent2I:  paulson@15300  291  "equiv A1 r1 ==> equiv A2 r2  paulson@15300  292  ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w)  paulson@15300  293  ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z)  paulson@15300  294  ==> congruent2 r1 r2 f"  paulson@15300  295  -- {* Suggested by John Harrison -- the two subproofs may be *}  paulson@15300  296  -- {* \emph{much} simpler than the direct proof. *}  nipkow@30198  297  apply (unfold congruent2_def equiv_def refl_on_def)  paulson@15300  298  apply clarify  paulson@15300  299  apply (blast intro: trans)  paulson@15300  300  done  paulson@15300  301 paulson@15300  302 lemma congruent2_commuteI:  paulson@15300  303  assumes equivA: "equiv A r"  paulson@15300  304  and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y"  paulson@15300  305  and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z"  paulson@15300  306  shows "f respects2 r"  paulson@15300  307  apply (rule congruent2I [OF equivA equivA])  paulson@15300  308  apply (rule commute [THEN trans])  paulson@15300  309  apply (rule_tac [3] commute [THEN trans, symmetric])  paulson@15300  310  apply (rule_tac [5] sym)  haftmann@25482  311  apply (rule congt | assumption |  paulson@15300  312  erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+  paulson@15300  313  done  paulson@15300  314 haftmann@24728  315 haftmann@24728  316 subsection {* Quotients and finiteness *}  haftmann@24728  317 wenzelm@40945  318 text {*Suggested by Florian KammÃ¼ller*}  haftmann@24728  319 haftmann@24728  320 lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)"  haftmann@24728  321  -- {* recall @{thm equiv_type} *}  haftmann@24728  322  apply (rule finite_subset)  haftmann@24728  323  apply (erule_tac [2] finite_Pow_iff [THEN iffD2])  haftmann@24728  324  apply (unfold quotient_def)  haftmann@24728  325  apply blast  haftmann@24728  326  done  haftmann@24728  327 haftmann@24728  328 lemma finite_equiv_class:  haftmann@24728  329  "finite A ==> r \ A \ A ==> X \ A//r ==> finite X"  haftmann@24728  330  apply (unfold quotient_def)  haftmann@24728  331  apply (rule finite_subset)  haftmann@24728  332  prefer 2 apply assumption  haftmann@24728  333  apply blast  haftmann@24728  334  done  haftmann@24728  335 haftmann@24728  336 lemma equiv_imp_dvd_card:  haftmann@24728  337  "finite A ==> equiv A r ==> \X \ A//r. k dvd card X  haftmann@24728  338  ==> k dvd card A"  berghofe@26791  339  apply (rule Union_quotient [THEN subst [where P="\A. k dvd card A"]])  haftmann@24728  340  apply assumption  haftmann@24728  341  apply (rule dvd_partition)  haftmann@24728  342  prefer 3 apply (blast dest: quotient_disj)  haftmann@24728  343  apply (simp_all add: Union_quotient equiv_type)  haftmann@24728  344  done  haftmann@24728  345 haftmann@24728  346 lemma card_quotient_disjoint:  haftmann@24728  347  "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A"  haftmann@24728  348 apply(simp add:quotient_def)  haftmann@24728  349 apply(subst card_UN_disjoint)  haftmann@24728  350  apply assumption  haftmann@24728  351  apply simp  nipkow@44890  352  apply(fastforce simp add:inj_on_def)  huffman@35216  353 apply simp  haftmann@24728  354 done  haftmann@24728  355 haftmann@40812  356 haftmann@40812  357 subsection {* Equivalence relations -- predicate version *}  haftmann@40812  358 haftmann@40812  359 text {* Partial equivalences *}  haftmann@40812  360 haftmann@40812  361 definition part_equivp :: "('a \ 'a \ bool) \ bool" where  haftmann@40812  362  "part_equivp R \ (\x. R x x) \ (\x y. R x y \ R x x \ R y y \ R x = R y)"  haftmann@40812  363  -- {* John-Harrison-style characterization *}  haftmann@40812  364 haftmann@40812  365 lemma part_equivpI:  haftmann@40812  366  "(\x. R x x) \ symp R \ transp R \ part_equivp R"  haftmann@45969  367  by (auto simp add: part_equivp_def) (auto elim: sympE transpE)  haftmann@40812  368 haftmann@40812  369 lemma part_equivpE:  haftmann@40812  370  assumes "part_equivp R"  haftmann@40812  371  obtains x where "R x x" and "symp R" and "transp R"  haftmann@40812  372 proof -  haftmann@40812  373  from assms have 1: "\x. R x x"  haftmann@40812  374  and 2: "\x y. R x y \ R x x \ R y y \ R x = R y"  haftmann@40812  375  by (unfold part_equivp_def) blast+  haftmann@40812  376  from 1 obtain x where "R x x" ..  haftmann@40812  377  moreover have "symp R"  haftmann@40812  378  proof (rule sympI)  haftmann@40812  379  fix x y  haftmann@40812  380  assume "R x y"  haftmann@40812  381  with 2 [of x y] show "R y x" by auto  haftmann@40812  382  qed  haftmann@40812  383  moreover have "transp R"  haftmann@40812  384  proof (rule transpI)  haftmann@40812  385  fix x y z  haftmann@40812  386  assume "R x y" and "R y z"  haftmann@40812  387  with 2 [of x y] 2 [of y z] show "R x z" by auto  haftmann@40812  388  qed  haftmann@40812  389  ultimately show thesis by (rule that)  haftmann@40812  390 qed  haftmann@40812  391 haftmann@40812  392 lemma part_equivp_refl_symp_transp:  haftmann@40812  393  "part_equivp R \ (\x. R x x) \ symp R \ transp R"  haftmann@40812  394  by (auto intro: part_equivpI elim: part_equivpE)  haftmann@40812  395 haftmann@40812  396 lemma part_equivp_symp:  haftmann@40812  397  "part_equivp R \ R x y \ R y x"  haftmann@40812  398  by (erule part_equivpE, erule sympE)  haftmann@40812  399 haftmann@40812  400 lemma part_equivp_transp:  haftmann@40812  401  "part_equivp R \ R x y \ R y z \ R x z"  haftmann@40812  402  by (erule part_equivpE, erule transpE)  haftmann@40812  403 haftmann@40812  404 lemma part_equivp_typedef:  kaliszyk@44204  405  "part_equivp R \ \d. d \ {c. \x. R x x \ c = Collect (R x)}"  kaliszyk@44204  406  by (auto elim: part_equivpE)  haftmann@40812  407 haftmann@40812  408 haftmann@40812  409 text {* Total equivalences *}  haftmann@40812  410 haftmann@40812  411 definition equivp :: "('a \ 'a \ bool) \ bool" where  haftmann@40812  412  "equivp R \ (\x y. R x y = (R x = R y))" -- {* John-Harrison-style characterization *}  haftmann@40812  413 haftmann@40812  414 lemma equivpI:  haftmann@40812  415  "reflp R \ symp R \ transp R \ equivp R"  haftmann@45969  416  by (auto elim: reflpE sympE transpE simp add: equivp_def)  haftmann@40812  417 haftmann@40812  418 lemma equivpE:  haftmann@40812  419  assumes "equivp R"  haftmann@40812  420  obtains "reflp R" and "symp R" and "transp R"  haftmann@40812  421  using assms by (auto intro!: that reflpI sympI transpI simp add: equivp_def)  haftmann@40812  422 haftmann@40812  423 lemma equivp_implies_part_equivp:  haftmann@40812  424  "equivp R \ part_equivp R"  haftmann@40812  425  by (auto intro: part_equivpI elim: equivpE reflpE)  haftmann@40812  426 haftmann@40812  427 lemma equivp_equiv:  haftmann@40812  428  "equiv UNIV A \ equivp (\x y. (x, y) \ A)"  haftmann@46752  429  by (auto intro!: equivI equivpI [to_set] elim!: equivE equivpE [to_set])  haftmann@40812  430 haftmann@40812  431 lemma equivp_reflp_symp_transp:  haftmann@40812  432  shows "equivp R \ reflp R \ symp R \ transp R"  haftmann@40812  433  by (auto intro: equivpI elim: equivpE)  haftmann@40812  434 haftmann@40812  435 lemma identity_equivp:  haftmann@40812  436  "equivp (op =)"  haftmann@40812  437  by (auto intro: equivpI reflpI sympI transpI)  haftmann@40812  438 haftmann@40812  439 lemma equivp_reflp:  haftmann@40812  440  "equivp R \ R x x"  haftmann@40812  441  by (erule equivpE, erule reflpE)  haftmann@40812  442 haftmann@40812  443 lemma equivp_symp:  haftmann@40812  444  "equivp R \ R x y \ R y x"  haftmann@40812  445  by (erule equivpE, erule sympE)  haftmann@40812  446 haftmann@40812  447 lemma equivp_transp:  haftmann@40812  448  "equivp R \ R x y \ R y z \ R x z"  haftmann@40812  449  by (erule equivpE, erule transpE)  haftmann@40812  450 paulson@15300  451 end  haftmann@46752  452