src/ZF/EquivClass.thy
changeset 46953 2b6e55924af3
parent 46821 ff6b0c1087f2
child 58871 c399ae4b836f
     1.1 --- a/src/ZF/EquivClass.thy	Thu Mar 15 15:54:22 2012 +0000
     1.2 +++ b/src/ZF/EquivClass.thy	Thu Mar 15 16:35:02 2012 +0000
     1.3 @@ -9,7 +9,7 @@
     1.4  
     1.5  definition
     1.6    quotient   :: "[i,i]=>i"    (infixl "'/'/" 90)  (*set of equiv classes*)  where
     1.7 -      "A//r == {r``{x} . x:A}"
     1.8 +      "A//r == {r``{x} . x \<in> A}"
     1.9  
    1.10  definition
    1.11    congruent  :: "[i,i=>i]=>o"  where
    1.12 @@ -72,15 +72,15 @@
    1.13  done
    1.14  
    1.15  lemma equiv_class_self:
    1.16 -    "[| equiv(A,r);  a: A |] ==> a: r``{a}"
    1.17 +    "[| equiv(A,r);  a \<in> A |] ==> a \<in> r``{a}"
    1.18  by (unfold equiv_def refl_def, blast)
    1.19  
    1.20  (*Lemma for the next result*)
    1.21  lemma subset_equiv_class:
    1.22 -    "[| equiv(A,r);  r``{b} \<subseteq> r``{a};  b: A |] ==> <a,b>: r"
    1.23 +    "[| equiv(A,r);  r``{b} \<subseteq> r``{a};  b \<in> A |] ==> <a,b>: r"
    1.24  by (unfold equiv_def refl_def, blast)
    1.25  
    1.26 -lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
    1.27 +lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b \<in> A |] ==> <a,b>: r"
    1.28  by (assumption | rule equalityD2 subset_equiv_class)+
    1.29  
    1.30  (*thus r``{a} = r``{b} as well*)
    1.31 @@ -92,24 +92,24 @@
    1.32  by (unfold equiv_def, blast)
    1.33  
    1.34  lemma equiv_class_eq_iff:
    1.35 -     "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x:A & y:A"
    1.36 +     "equiv(A,r) ==> <x,y>: r \<longleftrightarrow> r``{x} = r``{y} & x \<in> A & y \<in> A"
    1.37  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    1.38  
    1.39  lemma eq_equiv_class_iff:
    1.40 -     "[| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
    1.41 +     "[| equiv(A,r);  x \<in> A;  y \<in> A |] ==> r``{x} = r``{y} \<longleftrightarrow> <x,y>: r"
    1.42  by (blast intro: eq_equiv_class equiv_class_eq dest: equiv_type)
    1.43  
    1.44  (*** Quotients ***)
    1.45  
    1.46  (** Introduction/elimination rules -- needed? **)
    1.47  
    1.48 -lemma quotientI [TC]: "x:A ==> r``{x}: A//r"
    1.49 +lemma quotientI [TC]: "x \<in> A ==> r``{x}: A//r"
    1.50  apply (unfold quotient_def)
    1.51  apply (erule RepFunI)
    1.52  done
    1.53  
    1.54  lemma quotientE:
    1.55 -    "[| X: A//r;  !!x. [| X = r``{x};  x:A |] ==> P |] ==> P"
    1.56 +    "[| X \<in> A//r;  !!x. [| X = r``{x};  x \<in> A |] ==> P |] ==> P"
    1.57  by (unfold quotient_def, blast)
    1.58  
    1.59  lemma Union_quotient:
    1.60 @@ -117,7 +117,7 @@
    1.61  by (unfold equiv_def refl_def quotient_def, blast)
    1.62  
    1.63  lemma quotient_disj:
    1.64 -    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X \<inter> Y \<subseteq> 0)"
    1.65 +    "[| equiv(A,r);  X \<in> A//r;  Y \<in> A//r |] ==> X=Y | (X \<inter> Y \<subseteq> 0)"
    1.66  apply (unfold quotient_def)
    1.67  apply (safe intro!: equiv_class_eq, assumption)
    1.68  apply (unfold equiv_def trans_def sym_def, blast)
    1.69 @@ -130,7 +130,7 @@
    1.70  
    1.71  (*Conversion rule*)
    1.72  lemma UN_equiv_class:
    1.73 -    "[| equiv(A,r);  b respects r;  a: A |] ==> (\<Union>x\<in>r``{a}. b(x)) = b(a)"
    1.74 +    "[| equiv(A,r);  b respects r;  a \<in> A |] ==> (\<Union>x\<in>r``{a}. b(x)) = b(a)"
    1.75  apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)")
    1.76   apply simp
    1.77   apply (blast intro: equiv_class_self)
    1.78 @@ -139,19 +139,19 @@
    1.79  
    1.80  (*type checking of  @{term"\<Union>x\<in>r``{a}. b(x)"} *)
    1.81  lemma UN_equiv_class_type:
    1.82 -    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x \<in> A ==> b(x) \<in> B |]
    1.83 +    "[| equiv(A,r);  b respects r;  X \<in> A//r;  !!x.  x \<in> A ==> b(x) \<in> B |]
    1.84       ==> (\<Union>x\<in>X. b(x)) \<in> B"
    1.85  apply (unfold quotient_def, safe)
    1.86  apply (simp (no_asm_simp) add: UN_equiv_class)
    1.87  done
    1.88  
    1.89  (*Sufficient conditions for injectiveness.  Could weaken premises!
    1.90 -  major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
    1.91 +  major premise could be an inclusion; bcong could be !!y. y \<in> A ==> b(y):B
    1.92  *)
    1.93  lemma UN_equiv_class_inject:
    1.94      "[| equiv(A,r);   b respects r;
    1.95 -        (\<Union>x\<in>X. b(x))=(\<Union>y\<in>Y. b(y));  X: A//r;  Y: A//r;
    1.96 -        !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
    1.97 +        (\<Union>x\<in>X. b(x))=(\<Union>y\<in>Y. b(y));  X \<in> A//r;  Y \<in> A//r;
    1.98 +        !!x y. [| x \<in> A; y \<in> A; b(x)=b(y) |] ==> <x,y>:r |]
    1.99       ==> X=Y"
   1.100  apply (unfold quotient_def, safe)
   1.101  apply (rule equiv_class_eq, assumption)
   1.102 @@ -162,11 +162,11 @@
   1.103  subsection{*Defining Binary Operations upon Equivalence Classes*}
   1.104  
   1.105  lemma congruent2_implies_congruent:
   1.106 -    "[| equiv(A,r1);  congruent2(r1,r2,b);  a: A |] ==> congruent(r2,b(a))"
   1.107 +    "[| equiv(A,r1);  congruent2(r1,r2,b);  a \<in> A |] ==> congruent(r2,b(a))"
   1.108  by (unfold congruent_def congruent2_def equiv_def refl_def, blast)
   1.109  
   1.110  lemma congruent2_implies_congruent_UN:
   1.111 -    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a: A2 |] ==>
   1.112 +    "[| equiv(A1,r1);  equiv(A2,r2);  congruent2(r1,r2,b);  a \<in> A2 |] ==>
   1.113       congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
   1.114  apply (unfold congruent_def, safe)
   1.115  apply (frule equiv_type [THEN subsetD], assumption)
   1.116 @@ -206,8 +206,8 @@
   1.117  
   1.118  lemma congruent2_commuteI:
   1.119   assumes equivA: "equiv(A,r)"
   1.120 -     and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
   1.121 -     and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   1.122 +     and commute: "!! y z. [| y \<in> A;  z \<in> A |] ==> b(y,z) = b(z,y)"
   1.123 +     and congt:   "!! y z w. [| w \<in> A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
   1.124   shows "b respects2 r"
   1.125  apply (insert equivA [THEN equiv_type, THEN subsetD])
   1.126  apply (rule congruent2I [OF equivA equivA])
   1.127 @@ -219,9 +219,9 @@
   1.128  
   1.129  (*Obsolete?*)
   1.130  lemma congruent_commuteI:
   1.131 -    "[| equiv(A,r);  Z: A//r;
   1.132 -        !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
   1.133 -        !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
   1.134 +    "[| equiv(A,r);  Z \<in> A//r;
   1.135 +        !!w. [| w \<in> A |] ==> congruent(r, %z. b(w,z));
   1.136 +        !!x y. [| x \<in> A;  y \<in> A |] ==> b(y,x) = b(x,y)
   1.137       |] ==> congruent(r, %w. \<Union>z\<in>Z. b(w,z))"
   1.138  apply (simp (no_asm) add: congruent_def)
   1.139  apply (safe elim!: quotientE)