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