src/ZF/EquivClass.ML

-(*  Title: 	ZF/EquivClass.ML
+(*  Title:      ZF/EquivClass.ML
     ID:         $Id$
-    Author: 	Lawrence C Paulson, Cambridge University Computer Laboratory
+    Author:     Lawrence C Paulson, Cambridge University Computer Laboratory
     Copyright   1994  University of Cambridge
 
 For EquivClass.thy.  Equivalence relations in Zermelo-Fraenkel Set Theory 
 *)
 

 qed "refl_comp_subset";
 
 goalw EquivClass.thy [equiv_def]
     "!!A r. equiv(A,r) ==> converse(r) O r = r";
 by (fast_tac (subset_cs addSIs [equalityI, sym_trans_comp_subset, 
-				refl_comp_subset]) 1);
+                                refl_comp_subset]) 1);
 qed "equiv_comp_eq";
 
 (*second half*)
 goalw EquivClass.thy [equiv_def,refl_def,sym_def,trans_def]
     "!!A r. [| converse(r) O r = r;  domain(r) = A |] ==> equiv(A,r)";
 by (etac equalityE 1);
 by (subgoal_tac "ALL x y. <x,y> : r --> <y,x> : r" 1);
 by (safe_tac ZF_cs);
 by (fast_tac (ZF_cs addSIs [converseI] addIs [compI]) 3);
 by (ALLGOALS (fast_tac 
-	      (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE])));
+              (ZF_cs addSIs [converseI] addIs [compI] addSEs [compE])));
 qed "comp_equivI";
 
 (** Equivalence classes **)
 
 (*Lemma for the next result*)

 qed "equiv_class_subset";
 
 goalw EquivClass.thy [equiv_def]
     "!!A r. [| equiv(A,r);  <a,b>: r |] ==> r``{a} = r``{b}";
 by (safe_tac (subset_cs addSIs [equalityI, equiv_class_subset]));
-by (rewrite_goals_tac [sym_def]);
+by (rewtac sym_def);
 by (fast_tac ZF_cs 1);
 qed "equiv_class_eq";
 
 goalw EquivClass.thy [equiv_def,refl_def]
     "!!A r. [| equiv(A,r);  a: A |] ==> a: r``{a}";

 qed "equiv_type";
 
 goal EquivClass.thy
     "!!A r. equiv(A,r) ==> <x,y>: r <-> r``{x} = r``{y} & x:A & y:A";
 by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq]
-		    addDs [equiv_type]) 1);
+                    addDs [equiv_type]) 1);
 qed "equiv_class_eq_iff";
 
 goal EquivClass.thy
     "!!A r. [| equiv(A,r);  x: A;  y: A |] ==> r``{x} = r``{y} <-> <x,y>: r";
 by (fast_tac (ZF_cs addIs [eq_equiv_class, equiv_class_eq]
-		    addDs [equiv_type]) 1);
+                    addDs [equiv_type]) 1);
 qed "eq_equiv_class_iff";
 
 (*** Quotients ***)
 
 (** Introduction/elimination rules -- needed? **)

 by (rtac RepFunI 1);
 by (resolve_tac prems 1);
 qed "quotientI";
 
 val major::prems = goalw EquivClass.thy [quotient_def]
-    "[| X: A/r;  !!x. [| X = r``{x};  x:A |] ==> P |] 	\
+    "[| X: A/r;  !!x. [| X = r``{x};  x:A |] ==> P |]   \
 \    ==> P";
 by (rtac (major RS RepFunE) 1);
 by (eresolve_tac prems 1);
 by (assume_tac 1);
 qed "quotientE";

 by (fast_tac ZF_cs 1);
 qed "UN_equiv_class";
 
 (*type checking of  UN x:r``{a}. b(x) *)
 val prems = goalw EquivClass.thy [quotient_def]
-    "[| equiv(A,r);  congruent(r,b);  X: A/r;	\
-\	!!x.  x : A ==> b(x) : B |] 	\
+    "[| equiv(A,r);  congruent(r,b);  X: A/r;   \
+\       !!x.  x : A ==> b(x) : B |]     \
 \    ==> (UN x:X. b(x)) : B";
 by (cut_facts_tac prems 1);
 by (safe_tac ZF_cs);
 by (asm_simp_tac (ZF_ss addsimps (UN_equiv_class::prems)) 1);
 qed "UN_equiv_class_type";

   major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
 *)
 val prems = goalw EquivClass.thy [quotient_def]
     "[| equiv(A,r);   congruent(r,b);  \
 \       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
-\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |] 	\
+\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> <x,y>:r |]         \
 \    ==> X=Y";
 by (cut_facts_tac prems 1);
 by (safe_tac ZF_cs);
 by (rtac equiv_class_eq 1);
 by (REPEAT (ares_tac prems 1));

 by (cut_facts_tac (equivA::prems) 1);
 by (safe_tac ZF_cs);
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
-				 congruent2_implies_congruent]) 1);
+                                 congruent2_implies_congruent]) 1);
 by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
 by (fast_tac ZF_cs 1);
 qed "congruent2_implies_congruent_UN";
 
 val prems as equivA::_ = goal EquivClass.thy
     "[| equiv(A,r);  congruent2(r,b);  a1: A;  a2: A |]  \
 \    ==> (UN x1:r``{a1}. UN x2:r``{a2}. b(x1,x2)) = b(a1,a2)";
 by (cut_facts_tac prems 1);
 by (asm_simp_tac (ZF_ss addsimps [equivA RS UN_equiv_class,
-				 congruent2_implies_congruent,
-				 congruent2_implies_congruent_UN]) 1);
+                                 congruent2_implies_congruent,
+                                 congruent2_implies_congruent_UN]) 1);
 qed "UN_equiv_class2";
 
 (*type checking*)
 val prems = goalw EquivClass.thy [quotient_def]
-    "[| equiv(A,r);  congruent2(r,b);			\
-\       X1: A/r;  X2: A/r;				\
-\	!!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B	\
+    "[| equiv(A,r);  congruent2(r,b);                   \
+\       X1: A/r;  X2: A/r;                              \
+\       !!x1 x2.  [| x1: A; x2: A |] ==> b(x1,x2) : B   \
 \    |] ==> (UN x1:X1. UN x2:X2. b(x1,x2)) : B";
 by (cut_facts_tac prems 1);
 by (safe_tac ZF_cs);
 by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
-			     congruent2_implies_congruent_UN,
-			     congruent2_implies_congruent, quotientI]) 1));
+                             congruent2_implies_congruent_UN,
+                             congruent2_implies_congruent, quotientI]) 1));
 qed "UN_equiv_class_type2";
 
 
 (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
   than the direct proof*)
 val prems = goalw EquivClass.thy [congruent2_def,equiv_def,refl_def]
-    "[| equiv(A,r);	\
+    "[| equiv(A,r);     \
 \       !! y z w. [| w: A;  <y,z> : r |] ==> b(y,w) = b(z,w);      \
 \       !! y z w. [| w: A;  <y,z> : r |] ==> b(w,y) = b(w,z)       \
 \    |] ==> congruent2(r,b)";
 by (cut_facts_tac prems 1);
 by (safe_tac ZF_cs);

 by (REPEAT (ares_tac prems 1
      ORELSE etac (subsetD RS SigmaE2) 1 THEN assume_tac 2 THEN assume_tac 1));
 qed "congruent2I";
 
 val [equivA,commute,congt] = goal EquivClass.thy
-    "[| equiv(A,r);	\
+    "[| equiv(A,r);     \
 \       !! y z. [| y: A;  z: A |] ==> b(y,z) = b(z,y);        \
-\       !! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)	\
+\       !! y z w. [| w: A;  <y,z>: r |] ==> b(w,y) = b(w,z)     \
 \    |] ==> congruent2(r,b)";
 by (resolve_tac [equivA RS congruent2I] 1);
 by (rtac (commute RS trans) 1);
 by (rtac (commute RS trans RS sym) 3);
 by (rtac sym 5);

 qed "congruent2_commuteI";
 
 (*Obsolete?*)
 val [equivA,ZinA,congt,commute] = goalw EquivClass.thy [quotient_def]
     "[| equiv(A,r);  Z: A/r;  \
-\       !!w. [| w: A |] ==> congruent(r, %z.b(w,z));	\
-\       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)	\
+\       !!w. [| w: A |] ==> congruent(r, %z.b(w,z));    \
+\       !!x y. [| x: A;  y: A |] ==> b(y,x) = b(x,y)    \
 \    |] ==> congruent(r, %w. UN z: Z. b(w,z))";
 val congt' = rewrite_rule [congruent_def] congt;
 by (cut_facts_tac [ZinA] 1);
 by (rewtac congruent_def);
 by (safe_tac ZF_cs);
 by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
 by (assume_tac 1);
 by (asm_simp_tac (ZF_ss addsimps [commute,
-				  [equivA, congt] MRS UN_equiv_class]) 1);
+                                  [equivA, congt] MRS UN_equiv_class]) 1);
 by (REPEAT (ares_tac [congt' RS spec RS spec RS mp] 1));
 qed "congruent_commuteI";