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)
```