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]) 
   1.187 -apply (simp add: congruent_def) 
   1.188 +apply (simp add: UN_equiv_class [of A r])
   1.189 +apply (simp add: congruent_def)
   1.190  done
   1.191  
   1.192  end