src/ZF/EquivClass.thy
 changeset 46820 c656222c4dc1 parent 35762 af3ff2ba4c54 child 46821 ff6b0c1087f2
```     1.1 --- a/src/ZF/EquivClass.thy	Sun Mar 04 23:20:43 2012 +0100
1.2 +++ b/src/ZF/EquivClass.thy	Tue Mar 06 15:15:49 2012 +0000
1.3 @@ -13,12 +13,12 @@
1.4
1.5  definition
1.6    congruent  :: "[i,i=>i]=>o"  where
1.7 -      "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
1.8 +      "congruent(r,b) == \<forall>y z. <y,z>:r \<longrightarrow> b(y)=b(z)"
1.9
1.10  definition
1.11    congruent2 :: "[i,i,[i,i]=>i]=>o"  where
1.12 -      "congruent2(r1,r2,b) == ALL y1 z1 y2 z2.
1.13 -           <y1,z1>:r1 --> <y2,z2>:r2 --> b(y1,y2) = b(z1,z2)"
1.14 +      "congruent2(r1,r2,b) == \<forall>y1 z1 y2 z2.
1.15 +           <y1,z1>:r1 \<longrightarrow> <y2,z2>:r2 \<longrightarrow> b(y1,y2) = b(z1,z2)"
1.16
1.17  abbreviation
1.18    RESPECTS ::"[i=>i, i] => o"  (infixr "respects" 80) where
1.19 @@ -36,11 +36,11 @@
1.20  (** first half: equiv(A,r) ==> converse(r) O r = r **)
1.21
1.22  lemma sym_trans_comp_subset:
1.23 -    "[| sym(r); trans(r) |] ==> converse(r) O r <= r"
1.24 +    "[| sym(r); trans(r) |] ==> converse(r) O r \<subseteq> r"
1.25  by (unfold trans_def sym_def, blast)
1.26
1.27  lemma refl_comp_subset:
1.28 -    "[| refl(A,r); r <= A*A |] ==> r <= converse(r) O r"
1.29 +    "[| refl(A,r); r \<subseteq> A*A |] ==> r \<subseteq> converse(r) O r"
1.30  by (unfold refl_def, blast)
1.31
1.32  lemma equiv_comp_eq:
1.33 @@ -54,14 +54,14 @@
1.34      "[| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)"
1.35  apply (unfold equiv_def refl_def sym_def trans_def)
1.36  apply (erule equalityE)
1.37 -apply (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r", blast+)
1.38 +apply (subgoal_tac "\<forall>x y. <x,y> \<in> r \<longrightarrow> <y,x> \<in> r", blast+)
1.39  done
1.40
1.41  (** Equivalence classes **)
1.42
1.43  (*Lemma for the next result*)
1.44  lemma equiv_class_subset:
1.45 -    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} <= r``{b}"
1.46 +    "[| sym(r);  trans(r);  <a,b>: r |] ==> r``{a} \<subseteq> r``{b}"
1.47  by (unfold trans_def sym_def, blast)
1.48
1.49  lemma equiv_class_eq:
1.50 @@ -77,7 +77,7 @@
1.51
1.52  (*Lemma for the next result*)
1.53  lemma subset_equiv_class:
1.54 -    "[| equiv(A,r);  r``{b} <= r``{a};  b: A |] ==> <a,b>: r"
1.55 +    "[| equiv(A,r);  r``{b} \<subseteq> r``{a};  b: A |] ==> <a,b>: r"
1.56  by (unfold equiv_def refl_def, blast)
1.57
1.58  lemma eq_equiv_class: "[| r``{a} = r``{b};  equiv(A,r);  b: A |] ==> <a,b>: r"
1.59 @@ -85,10 +85,10 @@
1.60
1.61  (*thus r``{a} = r``{b} as well*)
1.62  lemma equiv_class_nondisjoint:
1.63 -    "[| equiv(A,r);  x: (r``{a} Int r``{b}) |] ==> <a,b>: r"
1.64 +    "[| equiv(A,r);  x: (r``{a} \<inter> r``{b}) |] ==> <a,b>: r"
1.65  by (unfold equiv_def trans_def sym_def, blast)
1.66
1.67 -lemma equiv_type: "equiv(A,r) ==> r <= A*A"
1.68 +lemma equiv_type: "equiv(A,r) ==> r \<subseteq> A*A"
1.69  by (unfold equiv_def, blast)
1.70
1.71  lemma equiv_class_eq_iff:
1.72 @@ -113,11 +113,11 @@
1.73  by (unfold quotient_def, blast)
1.74
1.75  lemma Union_quotient:
1.76 -    "equiv(A,r) ==> Union(A//r) = A"
1.77 +    "equiv(A,r) ==> \<Union>(A//r) = A"
1.78  by (unfold equiv_def refl_def quotient_def, blast)
1.79
1.80  lemma quotient_disj:
1.81 -    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X Int Y <= 0)"
1.82 +    "[| equiv(A,r);  X: A//r;  Y: A//r |] ==> X=Y | (X \<inter> Y \<subseteq> 0)"
1.83  apply (unfold quotient_def)
1.84  apply (safe intro!: equiv_class_eq, assumption)
1.85  apply (unfold equiv_def trans_def sym_def, blast)
1.86 @@ -130,17 +130,17 @@
1.87
1.88  (*Conversion rule*)
1.89  lemma UN_equiv_class:
1.90 -    "[| equiv(A,r);  b respects r;  a: A |] ==> (UN x:r``{a}. b(x)) = b(a)"
1.91 -apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)")
1.92 +    "[| equiv(A,r);  b respects r;  a: A |] ==> (\<Union>x\<in>r``{a}. b(x)) = b(a)"
1.93 +apply (subgoal_tac "\<forall>x \<in> r``{a}. b(x) = b(a)")
1.94   apply simp
1.95 - apply (blast intro: equiv_class_self)
1.96 + apply (blast intro: equiv_class_self)
1.97  apply (unfold equiv_def sym_def congruent_def, blast)
1.98  done
1.99
1.100 -(*type checking of  UN x:r``{a}. b(x) *)
1.101 +(*type checking of  @{term"\<Union>x\<in>r``{a}. b(x)"} *)
1.102  lemma UN_equiv_class_type:
1.103 -    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x : A ==> b(x) : B |]
1.104 -     ==> (UN x:X. b(x)) : B"
1.105 +    "[| equiv(A,r);  b respects r;  X: A//r;  !!x.  x \<in> A ==> b(x) \<in> B |]
1.106 +     ==> (\<Union>x\<in>X. b(x)) \<in> B"
1.107  apply (unfold quotient_def, safe)
1.108  apply (simp (no_asm_simp) add: UN_equiv_class)
1.109  done
1.110 @@ -150,12 +150,12 @@
1.111  *)
1.112  lemma UN_equiv_class_inject:
1.113      "[| equiv(A,r);   b respects r;
1.114 -        (UN x:X. b(x))=(UN y:Y. b(y));  X: A//r;  Y: A//r;
1.115 +        (\<Union>x\<in>X. b(x))=(\<Union>y\<in>Y. b(y));  X: A//r;  Y: A//r;
1.116          !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]
1.117       ==> X=Y"
1.118  apply (unfold quotient_def, safe)
1.119  apply (rule equiv_class_eq, assumption)
1.120 -apply (simp add: UN_equiv_class [of A r b])
1.121 +apply (simp add: UN_equiv_class [of A r b])
1.122  done
1.123
1.124
1.125 @@ -170,7 +170,7 @@
1.126       congruent(r1, %x1. \<Union>x2 \<in> r2``{a}. b(x1,x2))"
1.127  apply (unfold congruent_def, safe)
1.128  apply (frule equiv_type [THEN subsetD], assumption)
1.129 -apply clarify
1.130 +apply clarify
1.131  apply (simp add: UN_equiv_class congruent2_implies_congruent)
1.132  apply (unfold congruent2_def equiv_def refl_def, blast)
1.133  done
1.134 @@ -185,10 +185,10 @@
1.135  lemma UN_equiv_class_type2:
1.136      "[| equiv(A,r);  b respects2 r;
1.137          X1: A//r;  X2: A//r;
1.138 -        !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B
1.139 -     |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B"
1.140 +        !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) \<in> B
1.141 +     |] ==> (\<Union>x1\<in>X1. \<Union>x2\<in>X2. b(x1,x2)) \<in> B"
1.142  apply (unfold quotient_def, safe)
1.143 -apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
1.144 +apply (blast intro: UN_equiv_class_type congruent2_implies_congruent_UN
1.145                      congruent2_implies_congruent quotientI)
1.146  done
1.147
1.148 @@ -196,12 +196,12 @@
1.149  (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
1.150    than the direct proof*)
1.151  lemma congruent2I:
1.152 -    "[|  equiv(A1,r1);  equiv(A2,r2);
1.153 +    "[|  equiv(A1,r1);  equiv(A2,r2);
1.154          !! y z w. [| w \<in> A2;  <y,z> \<in> r1 |] ==> b(y,w) = b(z,w);
1.155          !! y z w. [| w \<in> A1;  <y,z> \<in> r2 |] ==> b(w,y) = b(w,z)
1.156       |] ==> congruent2(r1,r2,b)"
1.157  apply (unfold congruent2_def equiv_def refl_def, safe)
1.158 -apply (blast intro: trans)
1.159 +apply (blast intro: trans)
1.160  done
1.161
1.162  lemma congruent2_commuteI:
1.163 @@ -209,11 +209,11 @@
1.164       and commute: "!! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y)"
1.165       and congt:   "!! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)"
1.166   shows "b respects2 r"
1.167 -apply (insert equivA [THEN equiv_type, THEN subsetD])
1.168 +apply (insert equivA [THEN equiv_type, THEN subsetD])
1.169  apply (rule congruent2I [OF equivA equivA])
1.170  apply (rule commute [THEN trans])
1.171  apply (rule_tac [3] commute [THEN trans, symmetric])
1.172 -apply (rule_tac [5] sym)
1.173 +apply (rule_tac [5] sym)
1.174  apply (blast intro: congt)+
1.175  done
1.176
1.177 @@ -222,12 +222,12 @@
1.178      "[| equiv(A,r);  Z: A//r;
1.179          !!w. [| w: A |] ==> congruent(r, %z. b(w,z));
1.180          !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)
1.181 -     |] ==> congruent(r, %w. UN z: Z. b(w,z))"
1.182 +     |] ==> congruent(r, %w. \<Union>z\<in>Z. b(w,z))"
1.183  apply (simp (no_asm) add: congruent_def)
1.184  apply (safe elim!: quotientE)
1.185  apply (frule equiv_type [THEN subsetD], assumption)
1.186 -apply (simp add: UN_equiv_class [of A r])