src/ZF/EquivClass.thy
author wenzelm
Sun Oct 07 21:19:31 2007 +0200 (2007-10-07)
changeset 24893 b8ef7afe3a6b
parent 24892 c663e675e177
child 35762 af3ff2ba4c54
permissions -rw-r--r--
modernized specifications;
removed legacy ML bindings;
wenzelm@23146
     1
(*  Title:      ZF/EquivClass.thy
wenzelm@23146
     2
    ID:         $Id$
wenzelm@23146
     3
    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
wenzelm@23146
     4
    Copyright   1994  University of Cambridge
wenzelm@23146
     5
wenzelm@23146
     6
*)
wenzelm@23146
     7
wenzelm@23146
     8
header{*Equivalence Relations*}
wenzelm@23146
     9
wenzelm@23146
    10
theory EquivClass imports Trancl Perm begin
wenzelm@23146
    11
wenzelm@24893
    12
definition
wenzelm@24893
    13
  quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)  where
wenzelm@23146
    14
      "A//r == {r``{x} . x:A}"
wenzelm@23146
    15
wenzelm@24893
    16
definition
wenzelm@24893
    17
  congruent  :: "[i,i=>i]=>o"  where
wenzelm@23146
    18
      "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
wenzelm@23146
    19
wenzelm@24893
    20
definition
wenzelm@24893
    21
  congruent2 :: "[i,i,[i,i]=>i]=>o"  where
wenzelm@23146
    22
      "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
wenzelm@23146
    23
           <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
wenzelm@23146
    24
wenzelm@24892
    25
abbreviation
wenzelm@24892
    26
  RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
wenzelm@24892
    27
  "f respects r == congruent(r,f)"
wenzelm@24892
    28
wenzelm@24892
    29
abbreviation
wenzelm@24892
    30
  RESPECTS2 ::"[i=>i=>i, i] => o"  (infixr "respects2 " 80) where
wenzelm@24892
    31
  "f respects2 r == congruent2(r,r,f)"
wenzelm@23146
    32
    --{*Abbreviation for the common case where the relations are identical*}
wenzelm@23146
    33
wenzelm@23146
    34
wenzelm@23146
    35
subsection{*Suppes, Theorem 70:
wenzelm@23146
    36
    @{term r} is an equiv relation iff @{term "converse(r) O r = r"}*}
wenzelm@23146
    37
wenzelm@23146
    38
(** first half: equiv(A,r) ==> converse(r) O r = r **)
wenzelm@23146
    39
wenzelm@23146
    40
lemma sym_trans_comp_subset:
wenzelm@23146
    41
    "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
wenzelm@23146
    42
by (unfold trans_def sym_def, blast)
wenzelm@23146
    43
wenzelm@23146
    44
lemma refl_comp_subset:
wenzelm@23146
    45
    "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
wenzelm@23146
    46
by (unfold refl_def, blast)
wenzelm@23146
    47
wenzelm@23146
    48
lemma equiv_comp_eq:
wenzelm@23146
    49
    "equiv(A,r) ==> converse(r) O r = r"
wenzelm@23146
    50
apply (unfold equiv_def)
wenzelm@23146
    51
apply (blast del: subsetI intro!: sym_trans_comp_subset refl_comp_subset)
wenzelm@23146
    52
done
wenzelm@23146
    53
wenzelm@23146
    54
(*second half*)
wenzelm@23146
    55
lemma comp_equivI:
wenzelm@23146
    56
    "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)"
wenzelm@23146
    57
apply (unfold equiv_def refl_def sym_def trans_def)
wenzelm@23146
    58
apply (erule equalityE)
wenzelm@23146
    59
apply (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r", blast+)
wenzelm@23146
    60
done
wenzelm@23146
    61
wenzelm@23146
    62
(** Equivalence classes **)
wenzelm@23146
    63
wenzelm@23146
    64
(*Lemma for the next result*)
wenzelm@23146
    65
lemma equiv_class_subset:
wenzelm@23146
    66
    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}"
wenzelm@23146
    67
by (unfold trans_def sym_def, blast)
wenzelm@23146
    68
wenzelm@23146
    69
lemma equiv_class_eq:
wenzelm@23146
    70
    "[| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}"
wenzelm@23146
    71
apply (unfold equiv_def)
wenzelm@23146
    72
apply (safe del: subsetI intro!: equalityI equiv_class_subset)
wenzelm@23146
    73
apply (unfold sym_def, blast)
wenzelm@23146
    74
done
wenzelm@23146
    75
wenzelm@23146
    76
lemma equiv_class_self:
wenzelm@23146
    77
    "[| equiv(A,r);  a: A |] ==> a: r``{a}"
wenzelm@23146
    78
by (unfold equiv_def refl_def, blast)
wenzelm@23146
    79
wenzelm@23146
    80
(*Lemma for the next result*)
wenzelm@23146
    81
lemma subset_equiv_class:
wenzelm@23146
    82
    "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r"
wenzelm@23146
    83
by (unfold equiv_def refl_def, blast)
wenzelm@23146
    84
wenzelm@23146
    85
lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
wenzelm@23146
    86
by (assumption | rule equalityD2 subset_equiv_class)+
wenzelm@23146
    87
wenzelm@23146
    88
(*thus r``{a} = r``{b} as well*)
wenzelm@23146
    89
lemma equiv_class_nondisjoint:
wenzelm@23146
    90
    "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r"
wenzelm@23146
    91
by (unfold equiv_def trans_def sym_def, blast)
wenzelm@23146
    92
wenzelm@23146
    93
lemma equiv_type: "equiv(A,r) ==> r <= A*A"
wenzelm@23146
    94
by (unfold equiv_def, blast)
wenzelm@23146
    95
wenzelm@23146
    96
lemma equiv_class_eq_iff:
wenzelm@23146
    97
     "equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A"
wenzelm@23146
    98
by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
wenzelm@23146
    99
wenzelm@23146
   100
lemma eq_equiv_class_iff:
wenzelm@23146
   101
     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r"
wenzelm@23146
   102
by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
wenzelm@23146
   103
wenzelm@23146
   104
(*** Quotients ***)
wenzelm@23146
   105
wenzelm@23146
   106
(** Introduction/elimination rules -- needed? **)
wenzelm@23146
   107
wenzelm@23146
   108
lemma quotientI [TC]: "x:A ==> r``{x}: A//r"
wenzelm@23146
   109
apply (unfold quotient_def)
wenzelm@23146
   110
apply (erule RepFunI)
wenzelm@23146
   111
done
wenzelm@23146
   112
wenzelm@23146
   113
lemma quotientE:
wenzelm@23146
   114
    "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |] ==> P"
wenzelm@23146
   115
by (unfold quotient_def, blast)
wenzelm@23146
   116
wenzelm@23146
   117
lemma Union_quotient:
wenzelm@23146
   118
    "equiv(A,r) ==> Union(A//r) = A"
wenzelm@23146
   119
by (unfold equiv_def refl_def quotient_def, blast)
wenzelm@23146
   120
wenzelm@23146
   121
lemma quotient_disj:
wenzelm@23146
   122
    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)"
wenzelm@23146
   123
apply (unfold quotient_def)
wenzelm@23146
   124
apply (safe intro!: equiv_class_eq, assumption)
wenzelm@23146
   125
apply (unfold equiv_def trans_def sym_def, blast)
wenzelm@23146
   126
done
wenzelm@23146
   127
wenzelm@23146
   128
subsection{*Defining Unary Operations upon Equivalence Classes*}
wenzelm@23146
   129
wenzelm@23146
   130
(** Could have a locale with the premises equiv(A,r)  and  congruent(r,b)
wenzelm@23146
   131
**)
wenzelm@23146
   132
wenzelm@23146
   133
(*Conversion rule*)
wenzelm@23146
   134
lemma UN_equiv_class:
wenzelm@23146
   135
    "[| equiv(A,r);  b respects r;  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
wenzelm@23146
   136
apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)") 
wenzelm@23146
   137
 apply simp
wenzelm@23146
   138
 apply (blast intro: equiv_class_self)  
wenzelm@23146
   139
apply (unfold equiv_def sym_def congruent_def, blast)
wenzelm@23146
   140
done
wenzelm@23146
   141
wenzelm@23146
   142
(*type checking of  UN x:r``{a}. b(x) *)
wenzelm@23146
   143
lemma UN_equiv_class_type:
wenzelm@23146
   144
    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x : A ==> b(x) : B |]
wenzelm@23146
   145
     ==> (UN x:X. b(x)) : B"
wenzelm@23146
   146
apply (unfold quotient_def, safe)
wenzelm@23146
   147
apply (simp (no_asm_simp) add: UN_equiv_class)
wenzelm@23146
   148
done
wenzelm@23146
   149
wenzelm@23146
   150
(*Sufficient conditions for injectiveness.  Could weaken premises!
wenzelm@23146
   151
  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
wenzelm@23146
   152
*)
wenzelm@23146
   153
lemma UN_equiv_class_inject:
wenzelm@23146
   154
    "[| equiv(A,r);   b respects r;
wenzelm@23146
   155
        (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
wenzelm@23146
   156
        !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
wenzelm@23146
   157
     ==> X=Y"
wenzelm@23146
   158
apply (unfold quotient_def, safe)
wenzelm@23146
   159
apply (rule equiv_class_eq, assumption)
wenzelm@23146
   160
apply (simp add: UN_equiv_class [of A r b])  
wenzelm@23146
   161
done
wenzelm@23146
   162
wenzelm@23146
   163
wenzelm@23146
   164
subsection{*Defining Binary Operations upon Equivalence Classes*}
wenzelm@23146
   165
wenzelm@23146
   166
lemma congruent2_implies_congruent:
wenzelm@23146
   167
    "[| equiv(A,r1);  congruent2(r1,r2,b);  a: A |] ==> congruent(r2,b(a))"
wenzelm@23146
   168
by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
wenzelm@23146
   169
wenzelm@23146
   170
lemma congruent2_implies_congruent_UN:
wenzelm@23146
   171
    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a: A2 |] ==>
wenzelm@23146
   172
     congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
wenzelm@23146
   173
apply (unfold congruent_def, safe)
wenzelm@23146
   174
apply (frule equiv_type [THEN subsetD], assumption)
wenzelm@23146
   175
apply clarify 
wenzelm@23146
   176
apply (simp add: UN_equiv_class congruent2_implies_congruent)
wenzelm@23146
   177
apply (unfold congruent2_def equiv_def refl_def, blast)
wenzelm@23146
   178
done
wenzelm@23146
   179
wenzelm@23146
   180
lemma UN_equiv_class2:
wenzelm@23146
   181
    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a1: A1;  a2: A2 |]
wenzelm@23146
   182
     ==> (\<Union>x1 \<in> r1``{a1}. \<Union>x2 \<in> r2``{a2}. b(x1,x2)) = b(a1,a2)"
wenzelm@23146
   183
by (simp add: UN_equiv_class congruent2_implies_congruent
wenzelm@23146
   184
              congruent2_implies_congruent_UN)
wenzelm@23146
   185
wenzelm@23146
   186
(*type checking*)
wenzelm@23146
   187
lemma UN_equiv_class_type2:
wenzelm@23146
   188
    "[| equiv(A,r);  b respects2 r;
wenzelm@23146
   189
        X1: A//r;  X2: A//r;
wenzelm@23146
   190
        !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
wenzelm@23146
   191
     |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
wenzelm@23146
   192
apply (unfold quotient_def, safe)
wenzelm@23146
   193
apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN 
wenzelm@23146
   194
                    congruent2_implies_congruent quotientI)
wenzelm@23146
   195
done
wenzelm@23146
   196
wenzelm@23146
   197
wenzelm@23146
   198
(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
wenzelm@23146
   199
  than the direct proof*)
wenzelm@23146
   200
lemma congruent2I:
wenzelm@23146
   201
    "[|  equiv(A1,r1);  equiv(A2,r2);  
wenzelm@23146
   202
        !! y z w. [| w \<in> A2;  <y,z> \<in> r1 |] ==> b(y,w) = b(z,w);
wenzelm@23146
   203
        !! y z w. [| w \<in> A1;  <y,z> \<in> r2 |] ==> b(w,y) = b(w,z)
wenzelm@23146
   204
     |] ==> congruent2(r1,r2,b)"
wenzelm@23146
   205
apply (unfold congruent2_def equiv_def refl_def, safe)
wenzelm@23146
   206
apply (blast intro: trans) 
wenzelm@23146
   207
done
wenzelm@23146
   208
wenzelm@23146
   209
lemma congruent2_commuteI:
wenzelm@23146
   210
 assumes equivA: "equiv(A,r)"
wenzelm@23146
   211
     and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
wenzelm@23146
   212
     and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
wenzelm@23146
   213
 shows "b respects2 r"
wenzelm@23146
   214
apply (insert equivA [THEN equiv_type, THEN subsetD]) 
wenzelm@23146
   215
apply (rule congruent2I [OF equivA equivA])
wenzelm@23146
   216
apply (rule commute [THEN trans])
wenzelm@23146
   217
apply (rule_tac [3] commute [THEN trans, symmetric])
wenzelm@23146
   218
apply (rule_tac [5] sym) 
wenzelm@23146
   219
apply (blast intro: congt)+
wenzelm@23146
   220
done
wenzelm@23146
   221
wenzelm@23146
   222
(*Obsolete?*)
wenzelm@23146
   223
lemma congruent_commuteI:
wenzelm@23146
   224
    "[| equiv(A,r);  Z: A//r;
wenzelm@23146
   225
        !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
wenzelm@23146
   226
        !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
wenzelm@23146
   227
     |] ==> congruent(r, %w. UN z: Z. b(w,z))"
wenzelm@23146
   228
apply (simp (no_asm) add: congruent_def)
wenzelm@23146
   229
apply (safe elim!: quotientE)
wenzelm@23146
   230
apply (frule equiv_type [THEN subsetD], assumption)
wenzelm@23146
   231
apply (simp add: UN_equiv_class [of A r]) 
wenzelm@23146
   232
apply (simp add: congruent_def) 
wenzelm@23146
   233
done
wenzelm@23146
   234
wenzelm@23146
   235
end