src/HOL/Equiv_Relations.thy
 author krauss Fri Nov 24 13:44:51 2006 +0100 (2006-11-24) changeset 21512 3786eb1b69d6 parent 21404 eb85850d3eb7 child 21749 3f0e86c92ff3 permissions -rw-r--r--
Lemma "fundef_default_value" uses predicate instead of set.
 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  paulson@15300  9 imports Relation Finite_Set  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@21404  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 paulson@15300  295 paulson@15300  296 subsection {* Cardinality results *}  paulson@15300  297 paulson@15300  298 text {*Suggested by Florian Kammüller*}  paulson@15300  299 paulson@15300  300 lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)"  paulson@15300  301  -- {* recall @{thm equiv_type} *}  paulson@15300  302  apply (rule finite_subset)  paulson@15300  303  apply (erule_tac [2] finite_Pow_iff [THEN iffD2])  paulson@15300  304  apply (unfold quotient_def)  paulson@15300  305  apply blast  paulson@15300  306  done  paulson@15300  307 paulson@15300  308 lemma finite_equiv_class:  paulson@15300  309  "finite A ==> r \ A \ A ==> X \ A//r ==> finite X"  paulson@15300  310  apply (unfold quotient_def)  paulson@15300  311  apply (rule finite_subset)  paulson@15300  312  prefer 2 apply assumption  paulson@15300  313  apply blast  paulson@15300  314  done  paulson@15300  315 paulson@15300  316 lemma equiv_imp_dvd_card:  paulson@15300  317  "finite A ==> equiv A r ==> \X \ A//r. k dvd card X  paulson@15300  318  ==> k dvd card A"  paulson@15300  319  apply (rule Union_quotient [THEN subst])  paulson@15300  320  apply assumption  paulson@15300  321  apply (rule dvd_partition)  nipkow@15392  322  prefer 3 apply (blast dest: quotient_disj)  nipkow@15392  323  apply (simp_all add: Union_quotient equiv_type)  paulson@15300  324  done  paulson@15300  325 nipkow@15303  326 lemma card_quotient_disjoint:  nipkow@15303  327  "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A"  nipkow@15303  328 apply(simp add:quotient_def)  nipkow@15303  329 apply(subst card_UN_disjoint)  nipkow@15303  330  apply assumption  nipkow@15303  331  apply simp  nipkow@15303  332  apply(fastsimp simp add:inj_on_def)  nipkow@15539  333 apply (simp add:setsum_constant)  nipkow@15303  334 done  nipkow@19323  335 (*  paulson@15300  336 ML  paulson@15300  337 {*  paulson@15300  338 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";  paulson@15300  339 val UN_constant_eq = thm "UN_constant_eq";  paulson@15300  340 val UN_equiv_class = thm "UN_equiv_class";  paulson@15300  341 val UN_equiv_class2 = thm "UN_equiv_class2";  paulson@15300  342 val UN_equiv_class_inject = thm "UN_equiv_class_inject";  paulson@15300  343 val UN_equiv_class_type = thm "UN_equiv_class_type";  paulson@15300  344 val UN_equiv_class_type2 = thm "UN_equiv_class_type2";  paulson@15300  345 val Union_quotient = thm "Union_quotient";  paulson@15300  346 val comp_equivI = thm "comp_equivI";  paulson@15300  347 val congruent2I = thm "congruent2I";  paulson@15300  348 val congruent2_commuteI = thm "congruent2_commuteI";  paulson@15300  349 val congruent2_def = thm "congruent2_def";  paulson@15300  350 val congruent2_implies_congruent = thm "congruent2_implies_congruent";  paulson@15300  351 val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";  paulson@15300  352 val congruent_def = thm "congruent_def";  paulson@15300  353 val eq_equiv_class = thm "eq_equiv_class";  paulson@15300  354 val eq_equiv_class_iff = thm "eq_equiv_class_iff";  paulson@15300  355 val equiv_class_eq = thm "equiv_class_eq";  paulson@15300  356 val equiv_class_eq_iff = thm "equiv_class_eq_iff";  paulson@15300  357 val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";  paulson@15300  358 val equiv_class_self = thm "equiv_class_self";  paulson@15300  359 val equiv_comp_eq = thm "equiv_comp_eq";  paulson@15300  360 val equiv_def = thm "equiv_def";  paulson@15300  361 val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";  paulson@15300  362 val equiv_type = thm "equiv_type";  paulson@15300  363 val finite_equiv_class = thm "finite_equiv_class";  paulson@15300  364 val finite_quotient = thm "finite_quotient";  paulson@15300  365 val quotientE = thm "quotientE";  paulson@15300  366 val quotientI = thm "quotientI";  paulson@15300  367 val quotient_def = thm "quotient_def";  paulson@15300  368 val quotient_disj = thm "quotient_disj";  paulson@15300  369 val refl_comp_subset = thm "refl_comp_subset";  paulson@15300  370 val subset_equiv_class = thm "subset_equiv_class";  paulson@15300  371 val sym_trans_comp_subset = thm "sym_trans_comp_subset";  paulson@15300  372 *}  nipkow@19323  373 *)  paulson@15300  374 end