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