src/HOL/Integ/Equiv.thy
 author nipkow Mon Aug 16 14:22:27 2004 +0200 (2004-08-16) changeset 15131 c69542757a4d parent 15108 492e5f3a8571 child 15140 322485b816ac permissions -rw-r--r--
     1 (*  Title:      HOL/Integ/Equiv.thy

     2     ID:         $Id$

     3     Authors:    Lawrence C Paulson, Cambridge University Computer Laboratory

     4     Copyright   1996  University of Cambridge

     5 *)

     6

     7 header {* Equivalence relations in Higher-Order Set Theory *}

     8

     9 theory Equiv

    10 import Relation Finite_Set

    11 begin

    12

    13 subsection {* Equivalence relations *}

    14

    15 locale equiv =

    16   fixes A and r

    17   assumes refl: "refl A r"

    18     and sym: "sym r"

    19     and trans: "trans r"

    20

    21 text {*

    22   Suppes, Theorem 70: @{text r} is an equiv relation iff @{text "r\<inverse> O

    23   r = r"}.

    24

    25   First half: @{text "equiv A r ==> r\<inverse> O r = r"}.

    26 *}

    27

    28 lemma sym_trans_comp_subset:

    29     "sym r ==> trans r ==> r\<inverse> O r \<subseteq> r"

    30   by (unfold trans_def sym_def converse_def) blast

    31

    32 lemma refl_comp_subset: "refl A r ==> r \<subseteq> r\<inverse> O r"

    33   by (unfold refl_def) blast

    34

    35 lemma equiv_comp_eq: "equiv A r ==> r\<inverse> O r = r"

    36   apply (unfold equiv_def)

    37   apply clarify

    38   apply (rule equalityI)

    39    apply (rules intro: sym_trans_comp_subset refl_comp_subset)+

    40   done

    41

    42 text {* Second half. *}

    43

    44 lemma comp_equivI:

    45     "r\<inverse> O r = r ==> Domain r = A ==> equiv A r"

    46   apply (unfold equiv_def refl_def sym_def trans_def)

    47   apply (erule equalityE)

    48   apply (subgoal_tac "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> r")

    49    apply fast

    50   apply fast

    51   done

    52

    53

    54 subsection {* Equivalence classes *}

    55

    56 lemma equiv_class_subset:

    57   "equiv A r ==> (a, b) \<in> r ==> r{a} \<subseteq> r{b}"

    58   -- {* lemma for the next result *}

    59   by (unfold equiv_def trans_def sym_def) blast

    60

    61 theorem equiv_class_eq: "equiv A r ==> (a, b) \<in> r ==> r{a} = r{b}"

    62   apply (assumption | rule equalityI equiv_class_subset)+

    63   apply (unfold equiv_def sym_def)

    64   apply blast

    65   done

    66

    67 lemma equiv_class_self: "equiv A r ==> a \<in> A ==> a \<in> r{a}"

    68   by (unfold equiv_def refl_def) blast

    69

    70 lemma subset_equiv_class:

    71     "equiv A r ==> r{b} \<subseteq> r{a} ==> b \<in> A ==> (a,b) \<in> r"

    72   -- {* lemma for the next result *}

    73   by (unfold equiv_def refl_def) blast

    74

    75 lemma eq_equiv_class:

    76     "r{a} = r{b} ==> equiv A r ==> b \<in> A ==> (a, b) \<in> r"

    77   by (rules intro: equalityD2 subset_equiv_class)

    78

    79 lemma equiv_class_nondisjoint:

    80     "equiv A r ==> x \<in> (r{a} \<inter> r{b}) ==> (a, b) \<in> r"

    81   by (unfold equiv_def trans_def sym_def) blast

    82

    83 lemma equiv_type: "equiv A r ==> r \<subseteq> A \<times> A"

    84   by (unfold equiv_def refl_def) blast

    85

    86 theorem equiv_class_eq_iff:

    87   "equiv A r ==> ((x, y) \<in> r) = (r{x} = r{y} & x \<in> A & y \<in> A)"

    88   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

    89

    90 theorem eq_equiv_class_iff:

    91   "equiv A r ==> x \<in> A ==> y \<in> A ==> (r{x} = r{y}) = ((x, y) \<in> r)"

    92   by (blast intro!: equiv_class_eq dest: eq_equiv_class equiv_type)

    93

    94

    95 subsection {* Quotients *}

    96

    97 constdefs

    98   quotient :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/'/" 90)

    99   "A//r == \<Union>x \<in> A. {r{x}}"  -- {* set of equiv classes *}

   100

   101 lemma quotientI: "x \<in> A ==> r{x} \<in> A//r"

   102   by (unfold quotient_def) blast

   103

   104 lemma quotientE:

   105   "X \<in> A//r ==> (!!x. X = r{x} ==> x \<in> A ==> P) ==> P"

   106   by (unfold quotient_def) blast

   107

   108 lemma Union_quotient: "equiv A r ==> Union (A//r) = A"

   109   by (unfold equiv_def refl_def quotient_def) blast

   110

   111 lemma quotient_disj:

   112   "equiv A r ==> X \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> Y = {})"

   113   apply (unfold quotient_def)

   114   apply clarify

   115   apply (rule equiv_class_eq)

   116    apply assumption

   117   apply (unfold equiv_def trans_def sym_def)

   118   apply blast

   119   done

   120

   121 lemma quotient_eqI:

   122   "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> r|] ==> X = Y"

   123   apply (clarify elim!: quotientE)

   124   apply (rule equiv_class_eq, assumption)

   125   apply (unfold equiv_def sym_def trans_def, blast)

   126   done

   127

   128 lemma quotient_eq_iff:

   129   "[|equiv A r; X \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> r)"

   130   apply (rule iffI)

   131    prefer 2 apply (blast del: equalityI intro: quotient_eqI)

   132   apply (clarify elim!: quotientE)

   133   apply (unfold equiv_def sym_def trans_def, blast)

   134   done

   135

   136

   137 lemma quotient_empty [simp]: "{}//r = {}"

   138 by(simp add: quotient_def)

   139

   140 lemma quotient_is_empty [iff]: "(A//r = {}) = (A = {})"

   141 by(simp add: quotient_def)

   142

   143 lemma quotient_is_empty2 [iff]: "({} = A//r) = (A = {})"

   144 by(simp add: quotient_def)

   145

   146

   147 subsection {* Defining unary operations upon equivalence classes *}

   148

   149 text{*A congruence-preserving function*}

   150 locale congruent =

   151   fixes r and f

   152   assumes congruent: "(y,z) \<in> r ==> f y = f z"

   153

   154 lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> A. f(y))=c"

   155   -- {* lemma required to prove @{text UN_equiv_class} *}

   156   by auto

   157

   158 lemma UN_equiv_class:

   159   "equiv A r ==> congruent r f ==> a \<in> A

   160     ==> (\<Union>x \<in> r{a}. f x) = f a"

   161   -- {* Conversion rule *}

   162   apply (rule equiv_class_self [THEN UN_constant_eq], assumption+)

   163   apply (unfold equiv_def congruent_def sym_def)

   164   apply (blast del: equalityI)

   165   done

   166

   167 lemma UN_equiv_class_type:

   168   "equiv A r ==> congruent r f ==> X \<in> A//r ==>

   169     (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> B"

   170   apply (unfold quotient_def)

   171   apply clarify

   172   apply (subst UN_equiv_class)

   173      apply auto

   174   done

   175

   176 text {*

   177   Sufficient conditions for injectiveness.  Could weaken premises!

   178   major premise could be an inclusion; bcong could be @{text "!!y. y \<in>

   179   A ==> f y \<in> B"}.

   180 *}

   181

   182 lemma UN_equiv_class_inject:

   183   "equiv A r ==> congruent r f ==>

   184     (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r

   185     ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> r)

   186     ==> X = Y"

   187   apply (unfold quotient_def)

   188   apply clarify

   189   apply (rule equiv_class_eq)

   190    apply assumption

   191   apply (subgoal_tac "f x = f xa")

   192    apply blast

   193   apply (erule box_equals)

   194    apply (assumption | rule UN_equiv_class)+

   195   done

   196

   197

   198 subsection {* Defining binary operations upon equivalence classes *}

   199

   200 text{*A congruence-preserving function of two arguments*}

   201 locale congruent2 =

   202   fixes r1 and r2 and f

   203   assumes congruent2:

   204     "(y1,z1) \<in> r1 ==> (y2,z2) \<in> r2 ==> f y1 y2 = f z1 z2"

   205

   206 lemma congruent2_implies_congruent:

   207     "equiv A r1 ==> congruent2 r1 r2 f ==> a \<in> A ==> congruent r2 (f a)"

   208   by (unfold congruent_def congruent2_def equiv_def refl_def) blast

   209

   210 lemma congruent2_implies_congruent_UN:

   211   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a \<in> A2 ==>

   212     congruent r1 (\<lambda>x1. \<Union>x2 \<in> r2{a}. f x1 x2)"

   213   apply (unfold congruent_def)

   214   apply clarify

   215   apply (rule equiv_type [THEN subsetD, THEN SigmaE2], assumption+)

   216   apply (simp add: UN_equiv_class congruent2_implies_congruent)

   217   apply (unfold congruent2_def equiv_def refl_def)

   218   apply (blast del: equalityI)

   219   done

   220

   221 lemma UN_equiv_class2:

   222   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f ==> a1 \<in> A1 ==> a2 \<in> A2

   223     ==> (\<Union>x1 \<in> r1{a1}. \<Union>x2 \<in> r2{a2}. f x1 x2) = f a1 a2"

   224   by (simp add: UN_equiv_class congruent2_implies_congruent

   225     congruent2_implies_congruent_UN)

   226

   227 lemma UN_equiv_class_type2:

   228   "equiv A1 r1 ==> equiv A2 r2 ==> congruent2 r1 r2 f

   229     ==> X1 \<in> A1//r1 ==> X2 \<in> A2//r2

   230     ==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B)

   231     ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> B"

   232   apply (unfold quotient_def)

   233   apply clarify

   234   apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN

   235     congruent2_implies_congruent quotientI)

   236   done

   237

   238 lemma UN_UN_split_split_eq:

   239   "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =

   240     (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(y1, y2). A x1 x2 y1 y2) y) x)"

   241   -- {* Allows a natural expression of binary operators, *}

   242   -- {* without explicit calls to @{text split} *}

   243   by auto

   244

   245 lemma congruent2I:

   246   "equiv A1 r1 ==> equiv A2 r2

   247     ==> (!!y z w. w \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)

   248     ==> (!!y z w. w \<in> A1 ==> (y,z) \<in> r2 ==> f w y = f w z)

   249     ==> congruent2 r1 r2 f"

   250   -- {* Suggested by John Harrison -- the two subproofs may be *}

   251   -- {* \emph{much} simpler than the direct proof. *}

   252   apply (unfold congruent2_def equiv_def refl_def)

   253   apply clarify

   254   apply (blast intro: trans)

   255   done

   256

   257 lemma congruent2_commuteI:

   258   assumes equivA: "equiv A r"

   259     and commute: "!!y z. y \<in> A ==> z \<in> A ==> f y z = f z y"

   260     and congt: "!!y z w. w \<in> A ==> (y,z) \<in> r ==> f w y = f w z"

   261   shows "congruent2 r r f"

   262   apply (rule congruent2I [OF equivA equivA])

   263    apply (rule commute [THEN trans])

   264      apply (rule_tac  commute [THEN trans, symmetric])

   265        apply (rule_tac  sym)

   266        apply (assumption | rule congt |

   267          erule equivA [THEN equiv_type, THEN subsetD, THEN SigmaE2])+

   268   done

   269

   270

   271 subsection {* Cardinality results *}

   272

   273 text {* (suggested by Florian Kamm�ller) *}

   274

   275 lemma finite_quotient: "finite A ==> r \<subseteq> A \<times> A ==> finite (A//r)"

   276   -- {* recall @{thm equiv_type} *}

   277   apply (rule finite_subset)

   278    apply (erule_tac  finite_Pow_iff [THEN iffD2])

   279   apply (unfold quotient_def)

   280   apply blast

   281   done

   282

   283 lemma finite_equiv_class:

   284   "finite A ==> r \<subseteq> A \<times> A ==> X \<in> A//r ==> finite X"

   285   apply (unfold quotient_def)

   286   apply (rule finite_subset)

   287    prefer 2 apply assumption

   288   apply blast

   289   done

   290

   291 lemma equiv_imp_dvd_card:

   292   "finite A ==> equiv A r ==> \<forall>X \<in> A//r. k dvd card X

   293     ==> k dvd card A"

   294   apply (rule Union_quotient [THEN subst])

   295    apply assumption

   296   apply (rule dvd_partition)

   297      prefer 4 apply (blast dest: quotient_disj)

   298     apply (simp_all add: Union_quotient equiv_type finite_quotient)

   299   done

   300

   301 ML

   302 {*

   303 val UN_UN_split_split_eq = thm "UN_UN_split_split_eq";

   304 val UN_constant_eq = thm "UN_constant_eq";

   305 val UN_equiv_class = thm "UN_equiv_class";

   306 val UN_equiv_class2 = thm "UN_equiv_class2";

   307 val UN_equiv_class_inject = thm "UN_equiv_class_inject";

   308 val UN_equiv_class_type = thm "UN_equiv_class_type";

   309 val UN_equiv_class_type2 = thm "UN_equiv_class_type2";

   310 val Union_quotient = thm "Union_quotient";

   311 val comp_equivI = thm "comp_equivI";

   312 val congruent2I = thm "congruent2I";

   313 val congruent2_commuteI = thm "congruent2_commuteI";

   314 val congruent2_def = thm "congruent2_def";

   315 val congruent2_implies_congruent = thm "congruent2_implies_congruent";

   316 val congruent2_implies_congruent_UN = thm "congruent2_implies_congruent_UN";

   317 val congruent_def = thm "congruent_def";

   318 val eq_equiv_class = thm "eq_equiv_class";

   319 val eq_equiv_class_iff = thm "eq_equiv_class_iff";

   320 val equiv_class_eq = thm "equiv_class_eq";

   321 val equiv_class_eq_iff = thm "equiv_class_eq_iff";

   322 val equiv_class_nondisjoint = thm "equiv_class_nondisjoint";

   323 val equiv_class_self = thm "equiv_class_self";

   324 val equiv_comp_eq = thm "equiv_comp_eq";

   325 val equiv_def = thm "equiv_def";

   326 val equiv_imp_dvd_card = thm "equiv_imp_dvd_card";

   327 val equiv_type = thm "equiv_type";

   328 val finite_equiv_class = thm "finite_equiv_class";

   329 val finite_quotient = thm "finite_quotient";

   330 val quotientE = thm "quotientE";

   331 val quotientI = thm "quotientI";

   332 val quotient_def = thm "quotient_def";

   333 val quotient_disj = thm "quotient_disj";

   334 val refl_comp_subset = thm "refl_comp_subset";

   335 val subset_equiv_class = thm "subset_equiv_class";

   336 val sym_trans_comp_subset = thm "sym_trans_comp_subset";

   337 *}

   338

   339 end