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--
New theory header syntax.
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@15131
    10
import 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\<inverse> O
wenzelm@13482
    23
  r = r"}.
wenzelm@13482
    24
wenzelm@13482
    25
  First half: @{text "equiv A r ==> r\<inverse> 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\<inverse> O r \<subseteq> 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 \<subseteq> r\<inverse> O r"
wenzelm@13482
    33
  by (unfold refl_def) blast
wenzelm@13482
    34
wenzelm@13482
    35
lemma equiv_comp_eq: "equiv A r ==> r\<inverse> 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\<inverse> 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 "\<forall>x y. (x, y) \<in> r --> (y, x) \<in> 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) \<in> r ==> r``{a} \<subseteq> 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) \<in> 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 \<in> A ==> a \<in> 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} \<subseteq> r``{a} ==> b \<in> A ==> (a,b) \<in> 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 \<in> A ==> (a, b) \<in> 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 \<in> (r``{a} \<inter> r``{b}) ==> (a, b) \<in> 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 \<subseteq> A \<times> 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) \<in> r) = (r``{x} = r``{y} & x \<in> A & y \<in> 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 \<in> A ==> y \<in> A ==> (r``{x} = r``{y}) = ((x, y) \<in> 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 == \<Union>x \<in> A. {r``{x}}"  -- {* set of equiv classes *}
wenzelm@13482
   100
wenzelm@13482
   101
lemma quotientI: "x \<in> A ==> r``{x} \<in> A//r"
wenzelm@13482
   102
  by (unfold quotient_def) blast
wenzelm@13482
   103
wenzelm@13482
   104
lemma quotientE:
wenzelm@13482
   105
  "X \<in> A//r ==> (!!x. X = r``{x} ==> x \<in> 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 \<in> A//r ==> Y \<in> A//r ==> X = Y | (X \<inter> 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 \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y; (x,y) \<in> 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 \<in> A//r; Y \<in> A//r; x \<in> X; y \<in> Y|] ==> (X = Y) = ((x,y) \<in> 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) \<in> r ==> f y = f z"
wenzelm@13482
   153
paulson@14512
   154
lemma UN_constant_eq: "a \<in> A ==> \<forall>y \<in> A. f y = c ==> (\<Union>y \<in> 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 \<in> A
paulson@14512
   160
    ==> (\<Union>x \<in> 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 \<in> A//r ==>
paulson@14512
   169
    (!!x. x \<in> A ==> f x \<in> B) ==> (\<Union>x \<in> X. f x) \<in> 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 \<in>
paulson@14512
   179
  A ==> f y \<in> 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
    (\<Union>x \<in> X. f x) = (\<Union>y \<in> Y. f y) ==> X \<in> A//r ==> Y \<in> A//r
paulson@14512
   185
    ==> (!!x y. x \<in> A ==> y \<in> A ==> f x = f y ==> (x, y) \<in> 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) \<in> r1 ==> (y2,z2) \<in> 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 \<in> 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 \<in> A2 ==>
paulson@14658
   212
    congruent r1 (\<lambda>x1. \<Union>x2 \<in> 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 \<in> A1 ==> a2 \<in> A2
paulson@14658
   223
    ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> 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 \<in> A1//r1 ==> X2 \<in> A2//r2
paulson@14658
   230
    ==> (!!x1 x2. x1 \<in> A1 ==> x2 \<in> A2 ==> f x1 x2 \<in> B)
paulson@14512
   231
    ==> (\<Union>x1 \<in> X1. \<Union>x2 \<in> X2. f x1 x2) \<in> 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
  "(\<Union>(x1, x2) \<in> X. \<Union>(y1, y2) \<in> Y. A x1 x2 y1 y2) =
wenzelm@13482
   240
    (\<Union>x \<in> X. \<Union>y \<in> Y. (\<lambda>(x1, x2). (\<lambda>(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 \<in> A2 ==> (y,z) \<in> r1 ==> f y w = f z w)
paulson@14658
   248
    ==> (!!y z w. w \<in> A1 ==> (y,z) \<in> 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 \<in> A ==> z \<in> A ==> f y z = f z y"
paulson@14658
   260
    and congt: "!!y z w. w \<in> A ==> (y,z) \<in> 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 \<subseteq> A \<times> 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 \<subseteq> A \<times> A ==> X \<in> 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 ==> \<forall>X \<in> 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