src/HOL/Equiv_Relations.thy
 author wenzelm Thu Oct 04 20:29:42 2007 +0200 (2007-10-04) changeset 24850 0cfd722ab579 parent 24728 e2b3a1065676 child 25482 4ed49eccb1eb permissions -rw-r--r--
Name.uu, Name.aT;
 paulson@15300  1 (* ID: $Id$  paulson@15300  2  Authors: Lawrence C Paulson, Cambridge University Computer Laboratory  paulson@15300  3  Copyright 1996 University of Cambridge  paulson@15300  4 *)  paulson@15300  5 paulson@15300  6 header {* Equivalence Relations in Higher-Order Set Theory *}  paulson@15300  7 paulson@15300  8 theory Equiv_Relations  haftmann@24728  9 imports Finite_Set Relation  paulson@15300  10 begin  paulson@15300  11 paulson@15300  12 subsection {* Equivalence relations *}  paulson@15300  13 paulson@15300  14 locale equiv =  paulson@15300  15  fixes A and r  paulson@15300  16  assumes refl: "refl A r"  paulson@15300  17  and sym: "sym r"  paulson@15300  18  and trans: "trans r"  paulson@15300  19 paulson@15300  20 text {*  paulson@15300  21  Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\ O  paulson@15300  22  r = r"}.  paulson@15300  23 paulson@15300  24  First half: @{text "equiv A r ==> r\ O r = r"}.  paulson@15300  25 *}  paulson@15300  26 paulson@15300  27 lemma sym_trans_comp_subset:  paulson@15300  28  "sym r ==> trans r ==> r\ O r \ r"  paulson@15300  29  by (unfold trans_def sym_def converse_def) blast  paulson@15300  30 paulson@15300  31 lemma refl_comp_subset: "refl A r ==> r \ r\ O r"  paulson@15300  32  by (unfold refl_def) blast  paulson@15300  33 paulson@15300  34 lemma equiv_comp_eq: "equiv A r ==> r\ O r = r"  paulson@15300  35  apply (unfold equiv_def)  paulson@15300  36  apply clarify  paulson@15300  37  apply (rule equalityI)  nipkow@17589  38  apply (iprover intro: sym_trans_comp_subset refl_comp_subset)+  paulson@15300  39  done  paulson@15300  40 paulson@15300  41 text {* Second half. *}  paulson@15300  42 paulson@15300  43 lemma comp_equivI:  paulson@15300  44  "r\ O r = r ==> Domain r = A ==> equiv A r"  paulson@15300  45  apply (unfold equiv_def refl_def sym_def trans_def)  paulson@15300  46  apply (erule equalityE)  paulson@15300  47  apply (subgoal_tac "\x y. (x, y) \ r --> (y, x) \ r")  paulson@15300  48  apply fast  paulson@15300  49  apply fast  paulson@15300  50  done  paulson@15300  51 paulson@15300  52 paulson@15300  53 subsection {* Equivalence classes *}  paulson@15300  54 paulson@15300  55 lemma equiv_class_subset:  paulson@15300  56  "equiv A r ==> (a, b) \ r ==> r{a} \ r{b}"  paulson@15300  57  -- {* lemma for the next result *}  paulson@15300  58  by (unfold equiv_def trans_def sym_def) blast  paulson@15300  59 paulson@15300  60 theorem equiv_class_eq: "equiv A r ==> (a, b) \ r ==> r{a} = r{b}"  paulson@15300  61  apply (assumption | rule equalityI equiv_class_subset)+  paulson@15300  62  apply (unfold equiv_def sym_def)  paulson@15300  63  apply blast  paulson@15300  64  done  paulson@15300  65 paulson@15300  66 lemma equiv_class_self: "equiv A r ==> a \ A ==> a \ r{a}"  paulson@15300  67  by (unfold equiv_def refl_def) blast  paulson@15300  68 paulson@15300  69 lemma subset_equiv_class:  paulson@15300  70  "equiv A r ==> r{b} \ r{a} ==> b \ A ==> (a,b) \ r"  paulson@15300  71  -- {* lemma for the next result *}  paulson@15300  72  by (unfold equiv_def refl_def) blast  paulson@15300  73 paulson@15300  74 lemma eq_equiv_class:  paulson@15300  75  "r{a} = r{b} ==> equiv A r ==> b \ A ==> (a, b) \ r"  nipkow@17589  76  by (iprover intro: equalityD2 subset_equiv_class)  paulson@15300  77 paulson@15300  78 lemma equiv_class_nondisjoint:  paulson@15300  79  "equiv A r ==> x \ (r{a} \ r{b}) ==> (a, b) \ r"  paulson@15300  80  by (unfold equiv_def trans_def sym_def) blast  paulson@15300  81 paulson@15300  82 lemma equiv_type: "equiv A r ==> r \ A \ A"  paulson@15300  83  by (unfold equiv_def refl_def) blast  paulson@15300  84 paulson@15300  85 theorem equiv_class_eq_iff:  paulson@15300  86  "equiv A r ==> ((x, y) \ r) = (r{x} = r{y} & x \ A & y \ A)"  paulson@15300  87  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)  paulson@15300  88 paulson@15300  89 theorem eq_equiv_class_iff:  paulson@15300  90  "equiv A r ==> x \ A ==> y \ A ==> (r{x} = r{y}) = ((x, y) \ r)"  paulson@15300  91  by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)  paulson@15300  92 paulson@15300  93 paulson@15300  94 subsection {* Quotients *}  paulson@15300  95 paulson@15300  96 constdefs  paulson@15300  97  quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/'/" 90)  paulson@15300  98  "A//r == \x \ A. {r{x}}" -- {* set of equiv classes *}  paulson@15300  99 paulson@15300  100 lemma quotientI: "x \ A ==> r{x} \ A//r"  paulson@15300  101  by (unfold quotient_def) blast  paulson@15300  102 paulson@15300  103 lemma quotientE:  paulson@15300  104  "X \ A//r ==> (!!x. X = r{x} ==> x \ A ==> P) ==> P"  paulson@15300  105  by (unfold quotient_def) blast  paulson@15300  106 paulson@15300  107 lemma Union_quotient: "equiv A r ==> Union (A//r) = A"  paulson@15300  108  by (unfold equiv_def refl_def quotient_def) blast  paulson@15300  109 paulson@15300  110 lemma quotient_disj:  paulson@15300  111  "equiv A r ==> X \ A//r ==> Y \ A//r ==> X = Y | (X \ Y = {})"  paulson@15300  112  apply (unfold quotient_def)  paulson@15300  113  apply clarify  paulson@15300  114  apply (rule equiv_class_eq)  paulson@15300  115  apply assumption  paulson@15300  116  apply (unfold equiv_def trans_def sym_def)  paulson@15300  117  apply blast  paulson@15300  118  done  paulson@15300  119 paulson@15300  120 lemma quotient_eqI:  paulson@15300  121  "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y; (x,y) \ r|] ==> X = Y"  paulson@15300  122  apply (clarify elim!: quotientE)  paulson@15300  123  apply (rule equiv_class_eq, assumption)  paulson@15300  124  apply (unfold equiv_def sym_def trans_def, blast)  paulson@15300  125  done  paulson@15300  126 paulson@15300  127 lemma quotient_eq_iff:  paulson@15300  128  "[|equiv A r; X \ A//r; Y \ A//r; x \ X; y \ Y|] ==> (X = Y) = ((x,y) \ r)"  paulson@15300  129  apply (rule iffI)  paulson@15300  130  prefer 2 apply (blast del: equalityI intro: quotient_eqI)  paulson@15300  131  apply (clarify elim!: quotientE)  paulson@15300  132  apply (unfold equiv_def sym_def trans_def, blast)  paulson@15300  133  done  paulson@15300  134 nipkow@18493  135 lemma eq_equiv_class_iff2:  nipkow@18493  136  "\ equiv A r; x \ A; y \ A \ \ ({x}//r = {y}//r) = ((x,y) : r)"  nipkow@18493  137 by(simp add:quotient_def eq_equiv_class_iff)  nipkow@18493  138 paulson@15300  139 paulson@15300  140 lemma quotient_empty [simp]: "{}//r = {}"  paulson@15300  141 by(simp add: quotient_def)  paulson@15300  142 paulson@15300  143 lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"  paulson@15300  144 by(simp add: quotient_def)  paulson@15300  145 paulson@15300  146 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"  paulson@15300  147 by(simp add: quotient_def)  paulson@15300  148 paulson@15300  149 nipkow@15302  150 lemma singleton_quotient: "{x}//r = {r  {x}}"  nipkow@15302  151 by(simp add:quotient_def)  nipkow@15302  152 nipkow@15302  153 lemma quotient_diff1:  nipkow@15302  154  "\ inj_on (%a. {a}//r) A; a \ A \ \ (A - {a})//r = A//r - {a}//r"  nipkow@15302  155 apply(simp add:quotient_def inj_on_def)  nipkow@15302  156 apply blast  nipkow@15302  157 done  nipkow@15302  158 paulson@15300  159 subsection {* Defining unary operations upon equivalence classes *}  paulson@15300  160 paulson@15300  161 text{*A congruence-preserving function*}  paulson@15300  162 locale congruent =  paulson@15300  163  fixes r and f  paulson@15300  164  assumes congruent: "(y,z) \ r ==> f y = f z"  paulson@15300  165 wenzelm@19363  166 abbreviation  wenzelm@21404  167  RESPECTS :: "('a => 'b) => ('a * 'a) set => bool"  wenzelm@21404  168  (infixr "respects" 80) where  wenzelm@19363  169  "f respects r == congruent r f"  paulson@15300  170 paulson@15300  171 paulson@15300  172 lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c"  paulson@15300  173  -- {* lemma required to prove @{text UN_equiv_class} *}  paulson@15300  174  by auto  paulson@15300  175 paulson@15300  176 lemma UN_equiv_class:  paulson@15300  177  "equiv A r ==> f respects r ==> a \ A  paulson@15300  178  ==> (\x \ r{a}. f x) = f a"  paulson@15300  179  -- {* Conversion rule *}  paulson@15300  180  apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)  paulson@15300  181  apply (unfold equiv_def congruent_def sym_def)  paulson@15300  182  apply (blast del: equalityI)  paulson@15300  183  done  paulson@15300  184 paulson@15300  185 lemma UN_equiv_class_type:  paulson@15300  186  "equiv A r ==> f respects r ==> X \ A//r ==>  paulson@15300  187  (!!x. x \ A ==> f x \ B) ==> (\x \ X. f x) \ B"  paulson@15300  188  apply (unfold quotient_def)  paulson@15300  189  apply clarify  paulson@15300  190  apply (subst UN_equiv_class)  paulson@15300  191  apply auto  paulson@15300  192  done  paulson@15300  193 paulson@15300  194 text {*  paulson@15300  195  Sufficient conditions for injectiveness. Could weaken premises!  paulson@15300  196  major premise could be an inclusion; bcong could be @{text "!!y. y \  paulson@15300  197  A ==> f y \ B"}.  paulson@15300  198 *}  paulson@15300  199 paulson@15300  200 lemma UN_equiv_class_inject:  paulson@15300  201  "equiv A r ==> f respects r ==>  paulson@15300  202  (\x \ X. f x) = (\y \ Y. f y) ==> X \ A//r ==> Y \ A//r  paulson@15300  203  ==> (!!x y. x \ A ==> y \ A ==> f x = f y ==> (x, y) \ r)  paulson@15300  204  ==> X = Y"  paulson@15300  205  apply (unfold quotient_def)  paulson@15300  206  apply clarify  paulson@15300  207  apply (rule equiv_class_eq)  paulson@15300  208  apply assumption  paulson@15300  209  apply (subgoal_tac "f x = f xa")  paulson@15300  210  apply blast  paulson@15300  211  apply (erule box_equals)  paulson@15300  212  apply (assumption | rule UN_equiv_class)+  paulson@15300  213  done  paulson@15300  214 paulson@15300  215 paulson@15300  216 subsection {* Defining binary operations upon equivalence classes *}  paulson@15300  217 paulson@15300  218 text{*A congruence-preserving function of two arguments*}  paulson@15300  219 locale congruent2 =  paulson@15300  220  fixes r1 and r2 and f  paulson@15300  221  assumes congruent2:  paulson@15300  222  "(y1,z1) \ r1 ==> (y2,z2) \ r2 ==> f y1 y2 = f z1 z2"  paulson@15300  223 paulson@15300  224 text{*Abbreviation for the common case where the relations are identical*}  nipkow@19979  225 abbreviation  wenzelm@21404  226  RESPECTS2:: "['a => 'a => 'b, ('a * 'a) set] => bool"  wenzelm@21749  227  (infixr "respects2" 80) where  nipkow@19979  228  "f respects2 r == congruent2 r r f"  nipkow@19979  229 paulson@15300  230 paulson@15300  231 lemma congruent2_implies_congruent:  paulson@15300  232  "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)"  paulson@15300  233  by (unfold congruent_def congruent2_def equiv_def refl_def) blast  paulson@15300  234 paulson@15300  235 lemma congruent2_implies_congruent_UN:  paulson@15300  236  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==>  paulson@15300  237  congruent r1 (\x1. \x2 \ r2{a}. f x1 x2)"  paulson@15300  238  apply (unfold congruent_def)  paulson@15300  239  apply clarify  paulson@15300  240  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)  paulson@15300  241  apply (simp add: UN_equiv_class congruent2_implies_congruent)  paulson@15300  242  apply (unfold congruent2_def equiv_def refl_def)  paulson@15300  243  apply (blast del: equalityI)  paulson@15300  244  done  paulson@15300  245 paulson@15300  246 lemma UN_equiv_class2:  paulson@15300  247  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2  paulson@15300  248  ==> (\x1 \ r1{a1}. \x2 \ r2{a2}. f x1 x2) = f a1 a2"  paulson@15300  249  by (simp add: UN_equiv_class congruent2_implies_congruent  paulson@15300  250  congruent2_implies_congruent_UN)  paulson@15300  251 paulson@15300  252 lemma UN_equiv_class_type2:  paulson@15300  253  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f  paulson@15300  254  ==> X1 \ A1//r1 ==> X2 \ A2//r2  paulson@15300  255  ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B)  paulson@15300  256  ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B"  paulson@15300  257  apply (unfold quotient_def)  paulson@15300  258  apply clarify  paulson@15300  259  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN  paulson@15300  260  congruent2_implies_congruent quotientI)  paulson@15300  261  done  paulson@15300  262 paulson@15300  263 lemma UN_UN_split_split_eq:  paulson@15300  264  "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) =  paulson@15300  265  (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)"  paulson@15300  266  -- {* Allows a natural expression of binary operators, *}  paulson@15300  267  -- {* without explicit calls to @{text split} *}  paulson@15300  268  by auto  paulson@15300  269 paulson@15300  270 lemma congruent2I:  paulson@15300  271  "equiv A1 r1 ==> equiv A2 r2  paulson@15300  272  ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w)  paulson@15300  273  ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z)  paulson@15300  274  ==> congruent2 r1 r2 f"  paulson@15300  275  -- {* Suggested by John Harrison -- the two subproofs may be *}  paulson@15300  276  -- {* \emph{much} simpler than the direct proof. *}  paulson@15300  277  apply (unfold congruent2_def equiv_def refl_def)  paulson@15300  278  apply clarify  paulson@15300  279  apply (blast intro: trans)  paulson@15300  280  done  paulson@15300  281 paulson@15300  282 lemma congruent2_commuteI:  paulson@15300  283  assumes equivA: "equiv A r"  paulson@15300  284  and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y"  paulson@15300  285  and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z"  paulson@15300  286  shows "f respects2 r"  paulson@15300  287  apply (rule congruent2I [OF equivA equivA])  paulson@15300  288  apply (rule commute [THEN trans])  paulson@15300  289  apply (rule_tac [3] commute [THEN trans, symmetric])  paulson@15300  290  apply (rule_tac [5] sym)  paulson@15300  291  apply (assumption | rule congt |  paulson@15300  292  erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+  paulson@15300  293  done  paulson@15300  294 haftmann@24728  295 haftmann@24728  296 subsection {* Quotients and finiteness *}  haftmann@24728  297 haftmann@24728  298 text {*Suggested by Florian Kammüller*}  haftmann@24728  299 haftmann@24728  300 lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)"  haftmann@24728  301  -- {* recall @{thm equiv_type} *}  haftmann@24728  302  apply (rule finite_subset)  haftmann@24728  303  apply (erule_tac [2] finite_Pow_iff [THEN iffD2])  haftmann@24728  304  apply (unfold quotient_def)  haftmann@24728  305  apply blast  haftmann@24728  306  done  haftmann@24728  307 haftmann@24728  308 lemma finite_equiv_class:  haftmann@24728  309  "finite A ==> r \ A \ A ==> X \ A//r ==> finite X"  haftmann@24728  310  apply (unfold quotient_def)  haftmann@24728  311  apply (rule finite_subset)  haftmann@24728  312  prefer 2 apply assumption  haftmann@24728  313  apply blast  haftmann@24728  314  done  haftmann@24728  315 haftmann@24728  316 lemma equiv_imp_dvd_card:  haftmann@24728  317  "finite A ==> equiv A r ==> \X \ A//r. k dvd card X  haftmann@24728  318  ==> k dvd card A"  haftmann@24728  319  apply (rule Union_quotient [THEN subst])  haftmann@24728  320  apply assumption  haftmann@24728  321  apply (rule dvd_partition)  haftmann@24728  322  prefer 3 apply (blast dest: quotient_disj)  haftmann@24728  323  apply (simp_all add: Union_quotient equiv_type)  haftmann@24728  324  done  haftmann@24728  325 haftmann@24728  326 lemma card_quotient_disjoint:  haftmann@24728  327  "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A"  haftmann@24728  328 apply(simp add:quotient_def)  haftmann@24728  329 apply(subst card_UN_disjoint)  haftmann@24728  330  apply assumption  haftmann@24728  331  apply simp  haftmann@24728  332  apply(fastsimp simp add:inj_on_def)  haftmann@24728  333 apply (simp add:setsum_constant)  haftmann@24728  334 done  haftmann@24728  335 paulson@15300  336 end