src/HOL/Equiv_Relations.thy
 author paulson Tue Jun 28 15:27:45 2005 +0200 (2005-06-28) changeset 16587 b34c8aa657a5 parent 15539 333a88244569 child 17589 58eeffd73be1 permissions -rw-r--r--
Constant "If" is now local
 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)  paulson@15300  38  apply (rules 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"  paulson@15300  76  by (rules 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 paulson@15300  135 paulson@15300  136 lemma quotient_empty [simp]: "{}//r = {}"  paulson@15300  137 by(simp add: quotient_def)  paulson@15300  138 paulson@15300  139 lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"  paulson@15300  140 by(simp add: quotient_def)  paulson@15300  141 paulson@15300  142 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"  paulson@15300  143 by(simp add: quotient_def)  paulson@15300  144 paulson@15300  145 nipkow@15302  146 lemma singleton_quotient: "{x}//r = {r  {x}}"  nipkow@15302  147 by(simp add:quotient_def)  nipkow@15302  148 nipkow@15302  149 lemma quotient_diff1:  nipkow@15302  150  "\ inj_on (%a. {a}//r) A; a \ A \ \ (A - {a})//r = A//r - {a}//r"  nipkow@15302  151 apply(simp add:quotient_def inj_on_def)  nipkow@15302  152 apply blast  nipkow@15302  153 done  nipkow@15302  154 paulson@15300  155 subsection {* Defining unary operations upon equivalence classes *}  paulson@15300  156 paulson@15300  157 text{*A congruence-preserving function*}  paulson@15300  158 locale congruent =  paulson@15300  159  fixes r and f  paulson@15300  160  assumes congruent: "(y,z) \ r ==> f y = f z"  paulson@15300  161 paulson@15300  162 syntax  paulson@15300  163  RESPECTS ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects" 80)  paulson@15300  164 paulson@15300  165 translations  paulson@15300  166  "f respects r" == "congruent r f"  paulson@15300  167 paulson@15300  168 paulson@15300  169 lemma UN_constant_eq: "a \ A ==> \y \ A. f y = c ==> (\y \ A. f(y))=c"  paulson@15300  170  -- {* lemma required to prove @{text UN_equiv_class} *}  paulson@15300  171  by auto  paulson@15300  172 paulson@15300  173 lemma UN_equiv_class:  paulson@15300  174  "equiv A r ==> f respects r ==> a \ A  paulson@15300  175  ==> (\x \ r{a}. f x) = f a"  paulson@15300  176  -- {* Conversion rule *}  paulson@15300  177  apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)  paulson@15300  178  apply (unfold equiv_def congruent_def sym_def)  paulson@15300  179  apply (blast del: equalityI)  paulson@15300  180  done  paulson@15300  181 paulson@15300  182 lemma UN_equiv_class_type:  paulson@15300  183  "equiv A r ==> f respects r ==> X \ A//r ==>  paulson@15300  184  (!!x. x \ A ==> f x \ B) ==> (\x \ X. f x) \ B"  paulson@15300  185  apply (unfold quotient_def)  paulson@15300  186  apply clarify  paulson@15300  187  apply (subst UN_equiv_class)  paulson@15300  188  apply auto  paulson@15300  189  done  paulson@15300  190 paulson@15300  191 text {*  paulson@15300  192  Sufficient conditions for injectiveness. Could weaken premises!  paulson@15300  193  major premise could be an inclusion; bcong could be @{text "!!y. y \  paulson@15300  194  A ==> f y \ B"}.  paulson@15300  195 *}  paulson@15300  196 paulson@15300  197 lemma UN_equiv_class_inject:  paulson@15300  198  "equiv A r ==> f respects r ==>  paulson@15300  199  (\x \ X. f x) = (\y \ Y. f y) ==> X \ A//r ==> Y \ A//r  paulson@15300  200  ==> (!!x y. x \ A ==> y \ A ==> f x = f y ==> (x, y) \ r)  paulson@15300  201  ==> X = Y"  paulson@15300  202  apply (unfold quotient_def)  paulson@15300  203  apply clarify  paulson@15300  204  apply (rule equiv_class_eq)  paulson@15300  205  apply assumption  paulson@15300  206  apply (subgoal_tac "f x = f xa")  paulson@15300  207  apply blast  paulson@15300  208  apply (erule box_equals)  paulson@15300  209  apply (assumption | rule UN_equiv_class)+  paulson@15300  210  done  paulson@15300  211 paulson@15300  212 paulson@15300  213 subsection {* Defining binary operations upon equivalence classes *}  paulson@15300  214 paulson@15300  215 text{*A congruence-preserving function of two arguments*}  paulson@15300  216 locale congruent2 =  paulson@15300  217  fixes r1 and r2 and f  paulson@15300  218  assumes congruent2:  paulson@15300  219  "(y1,z1) \ r1 ==> (y2,z2) \ r2 ==> f y1 y2 = f z1 z2"  paulson@15300  220 paulson@15300  221 text{*Abbreviation for the common case where the relations are identical*}  paulson@15300  222 syntax  paulson@15300  223  RESPECTS2 ::"['a => 'b, ('a * 'a) set] => bool" (infixr "respects2 " 80)  paulson@15300  224 paulson@15300  225 translations  paulson@15300  226  "f respects2 r" => "congruent2 r r f"  paulson@15300  227 paulson@15300  228 lemma congruent2_implies_congruent:  paulson@15300  229  "equiv A r1 ==> congruent2 r1 r2 f ==> a \ A ==> congruent r2 (f a)"  paulson@15300  230  by (unfold congruent_def congruent2_def equiv_def refl_def) blast  paulson@15300  231 paulson@15300  232 lemma congruent2_implies_congruent_UN:  paulson@15300  233  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \ A2 ==>  paulson@15300  234  congruent r1 (\x1. \x2 \ r2{a}. f x1 x2)"  paulson@15300  235  apply (unfold congruent_def)  paulson@15300  236  apply clarify  paulson@15300  237  apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)  paulson@15300  238  apply (simp add: UN_equiv_class congruent2_implies_congruent)  paulson@15300  239  apply (unfold congruent2_def equiv_def refl_def)  paulson@15300  240  apply (blast del: equalityI)  paulson@15300  241  done  paulson@15300  242 paulson@15300  243 lemma UN_equiv_class2:  paulson@15300  244  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \ A1 ==> a2 \ A2  paulson@15300  245  ==> (\x1 \ r1{a1}. \x2 \ r2{a2}. f x1 x2) = f a1 a2"  paulson@15300  246  by (simp add: UN_equiv_class congruent2_implies_congruent  paulson@15300  247  congruent2_implies_congruent_UN)  paulson@15300  248 paulson@15300  249 lemma UN_equiv_class_type2:  paulson@15300  250  "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f  paulson@15300  251  ==> X1 \ A1//r1 ==> X2 \ A2//r2  paulson@15300  252  ==> (!!x1 x2. x1 \ A1 ==> x2 \ A2 ==> f x1 x2 \ B)  paulson@15300  253  ==> (\x1 \ X1. \x2 \ X2. f x1 x2) \ B"  paulson@15300  254  apply (unfold quotient_def)  paulson@15300  255  apply clarify  paulson@15300  256  apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN  paulson@15300  257  congruent2_implies_congruent quotientI)  paulson@15300  258  done  paulson@15300  259 paulson@15300  260 lemma UN_UN_split_split_eq:  paulson@15300  261  "(\(x1, x2) \ X. \(y1, y2) \ Y. A x1 x2 y1 y2) =  paulson@15300  262  (\x \ X. \y \ Y. (\(x1, x2). (\(y1, y2). A x1 x2 y1 y2) y) x)"  paulson@15300  263  -- {* Allows a natural expression of binary operators, *}  paulson@15300  264  -- {* without explicit calls to @{text split} *}  paulson@15300  265  by auto  paulson@15300  266 paulson@15300  267 lemma congruent2I:  paulson@15300  268  "equiv A1 r1 ==> equiv A2 r2  paulson@15300  269  ==> (!!y z w. w \ A2 ==> (y,z) \ r1 ==> f y w = f z w)  paulson@15300  270  ==> (!!y z w. w \ A1 ==> (y,z) \ r2 ==> f w y = f w z)  paulson@15300  271  ==> congruent2 r1 r2 f"  paulson@15300  272  -- {* Suggested by John Harrison -- the two subproofs may be *}  paulson@15300  273  -- {* \emph{much} simpler than the direct proof. *}  paulson@15300  274  apply (unfold congruent2_def equiv_def refl_def)  paulson@15300  275  apply clarify  paulson@15300  276  apply (blast intro: trans)  paulson@15300  277  done  paulson@15300  278 paulson@15300  279 lemma congruent2_commuteI:  paulson@15300  280  assumes equivA: "equiv A r"  paulson@15300  281  and commute: "!!y z. y \ A ==> z \ A ==> f y z = f z y"  paulson@15300  282  and congt: "!!y z w. w \ A ==> (y,z) \ r ==> f w y = f w z"  paulson@15300  283  shows "f respects2 r"  paulson@15300  284  apply (rule congruent2I [OF equivA equivA])  paulson@15300  285  apply (rule commute [THEN trans])  paulson@15300  286  apply (rule_tac [3] commute [THEN trans, symmetric])  paulson@15300  287  apply (rule_tac [5] sym)  paulson@15300  288  apply (assumption | rule congt |  paulson@15300  289  erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+  paulson@15300  290  done  paulson@15300  291 paulson@15300  292 paulson@15300  293 subsection {* Cardinality results *}  paulson@15300  294 paulson@15300  295 text {*Suggested by Florian Kammüller*}  paulson@15300  296 paulson@15300  297 lemma finite_quotient: "finite A ==> r \ A \ A ==> finite (A//r)"  paulson@15300  298  -- {* recall @{thm equiv_type} *}  paulson@15300  299  apply (rule finite_subset)  paulson@15300  300  apply (erule_tac [2] finite_Pow_iff [THEN iffD2])  paulson@15300  301  apply (unfold quotient_def)  paulson@15300  302  apply blast  paulson@15300  303  done  paulson@15300  304 paulson@15300  305 lemma finite_equiv_class:  paulson@15300  306  "finite A ==> r \ A \ A ==> X \ A//r ==> finite X"  paulson@15300  307  apply (unfold quotient_def)  paulson@15300  308  apply (rule finite_subset)  paulson@15300  309  prefer 2 apply assumption  paulson@15300  310  apply blast  paulson@15300  311  done  paulson@15300  312 paulson@15300  313 lemma equiv_imp_dvd_card:  paulson@15300  314  "finite A ==> equiv A r ==> \X \ A//r. k dvd card X  paulson@15300  315  ==> k dvd card A"  paulson@15300  316  apply (rule Union_quotient [THEN subst])  paulson@15300  317  apply assumption  paulson@15300  318  apply (rule dvd_partition)  nipkow@15392  319  prefer 3 apply (blast dest: quotient_disj)  nipkow@15392  320  apply (simp_all add: Union_quotient equiv_type)  paulson@15300  321  done  paulson@15300  322 nipkow@15303  323 lemma card_quotient_disjoint:  nipkow@15303  324  "\ finite A; inj_on (\x. {x} // r) A \ \ card(A//r) = card A"  nipkow@15303  325 apply(simp add:quotient_def)  nipkow@15303  326 apply(subst card_UN_disjoint)  nipkow@15303  327  apply assumption  nipkow@15303  328  apply simp  nipkow@15303  329  apply(fastsimp simp add:inj_on_def)  nipkow@15539  330 apply (simp add:setsum_constant)  nipkow@15303  331 done  nipkow@15303  332 paulson@15300  333 ML  paulson@15300  334 {*  paulson@15300  335 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";  paulson@15300  336 val UN_constant_eq = thm "UN_constant_eq";  paulson@15300  337 val UN_equiv_class = thm "UN_equiv_class";  paulson@15300  338 val UN_equiv_class2 = thm "UN_equiv_class2";  paulson@15300  339 val UN_equiv_class_inject = thm "UN_equiv_class_inject";  paulson@15300  340 val UN_equiv_class_type = thm "UN_equiv_class_type";  paulson@15300  341 val UN_equiv_class_type2 = thm "UN_equiv_class_type2";  paulson@15300  342 val Union_quotient = thm "Union_quotient";  paulson@15300  343 val comp_equivI = thm "comp_equivI";  paulson@15300  344 val congruent2I = thm "congruent2I";  paulson@15300  345 val congruent2_commuteI = thm "congruent2_commuteI";  paulson@15300  346 val congruent2_def = thm "congruent2_def";  paulson@15300  347 val congruent2_implies_congruent = thm "congruent2_implies_congruent";  paulson@15300  348 val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";  paulson@15300  349 val congruent_def = thm "congruent_def";  paulson@15300  350 val eq_equiv_class = thm "eq_equiv_class";  paulson@15300  351 val eq_equiv_class_iff = thm "eq_equiv_class_iff";  paulson@15300  352 val equiv_class_eq = thm "equiv_class_eq";  paulson@15300  353 val equiv_class_eq_iff = thm "equiv_class_eq_iff";  paulson@15300  354 val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";  paulson@15300  355 val equiv_class_self = thm "equiv_class_self";  paulson@15300  356 val equiv_comp_eq = thm "equiv_comp_eq";  paulson@15300  357 val equiv_def = thm "equiv_def";  paulson@15300  358 val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";  paulson@15300  359 val equiv_type = thm "equiv_type";  paulson@15300  360 val finite_equiv_class = thm "finite_equiv_class";  paulson@15300  361 val finite_quotient = thm "finite_quotient";  paulson@15300  362 val quotientE = thm "quotientE";  paulson@15300  363 val quotientI = thm "quotientI";  paulson@15300  364 val quotient_def = thm "quotient_def";  paulson@15300  365 val quotient_disj = thm "quotient_disj";  paulson@15300  366 val refl_comp_subset = thm "refl_comp_subset";  paulson@15300  367 val subset_equiv_class = thm "subset_equiv_class";  paulson@15300  368 val sym_trans_comp_subset = thm "sym_trans_comp_subset";  paulson@15300  369 *}  paulson@15300  370 paulson@15300  371 end