src/HOL/Integ/Equiv.ML
changeset 1465 5d7a7e439cec
parent 1266 3ae9fe3c0f68
child 1642 21db0cf9a1a4
     1.1 --- a/src/HOL/Integ/Equiv.ML	Tue Jan 30 15:19:20 1996 +0100
     1.2 +++ b/src/HOL/Integ/Equiv.ML	Tue Jan 30 15:24:36 1996 +0100
     1.3 @@ -1,7 +1,7 @@
     1.4 -(*  Title: 	Equiv.ML
     1.5 +(*  Title:      Equiv.ML
     1.6      ID:         $Id$
     1.7 -    Authors: 	Riccardo Mattolini, Dip. Sistemi e Informatica
     1.8 -        	Lawrence C Paulson, Cambridge University Computer Laboratory
     1.9 +    Authors:    Riccardo Mattolini, Dip. Sistemi e Informatica
    1.10 +                Lawrence C Paulson, Cambridge University Computer Laboratory
    1.11      Copyright   1994 Universita' di Firenze
    1.12      Copyright   1993  University of Cambridge
    1.13  
    1.14 @@ -118,7 +118,7 @@
    1.15  qed "quotientI";
    1.16  
    1.17  val [major,minor] = goalw Equiv.thy [quotient_def]
    1.18 -    "[| X:(A/r);  !!x. [| X = r^^{x};  x:A |] ==> P |] 	\
    1.19 +    "[| X:(A/r);  !!x. [| X = r^^{x};  x:A |] ==> P |]  \
    1.20  \    ==> P";
    1.21  by (resolve_tac [major RS UN_E] 1);
    1.22  by (rtac minor 1);
    1.23 @@ -173,8 +173,8 @@
    1.24  
    1.25  (*type checking of  UN x:r``{a}. b(x) *)
    1.26  val _::_::prems = goalw Equiv.thy [quotient_def]
    1.27 -    "[| equiv A r;  congruent r b;  X: A/r;	\
    1.28 -\	!!x.  x : A ==> b(x) : B |] 	\
    1.29 +    "[| equiv A r;  congruent r b;  X: A/r;     \
    1.30 +\       !!x.  x : A ==> b(x) : B |]     \
    1.31  \    ==> (UN x:X. b(x)) : B";
    1.32  by (cut_facts_tac prems 1);
    1.33  by (safe_tac rel_cs);
    1.34 @@ -188,7 +188,7 @@
    1.35  val _::_::prems = goalw Equiv.thy [quotient_def]
    1.36      "[| equiv A r;   congruent r b;  \
    1.37  \       (UN x:X. b(x))=(UN y:Y. b(y));  X: A/r;  Y: A/r;  \
    1.38 -\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |] 	\
    1.39 +\       !!x y. [| x:A; y:A; b(x)=b(y) |] ==> (x,y):r |]         \
    1.40  \    ==> X=Y";
    1.41  by (cut_facts_tac prems 1);
    1.42  by (safe_tac rel_cs);
    1.43 @@ -215,7 +215,7 @@
    1.44  by (rtac (equivA RS equiv_type RS subsetD RS SigmaE2) 1);
    1.45  by (assume_tac 1);
    1.46  by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
    1.47 -				     congruent2_implies_congruent]) 1);
    1.48 +                                     congruent2_implies_congruent]) 1);
    1.49  by (rewrite_goals_tac [congruent2_def,equiv_def,refl_def]);
    1.50  by (fast_tac rel_cs 1);
    1.51  qed "congruent2_implies_congruent_UN";
    1.52 @@ -225,28 +225,28 @@
    1.53  \    ==> (UN x1:r^^{a1}. UN x2:r^^{a2}. b x1 x2) = b a1 a2";
    1.54  by (cut_facts_tac prems 1);
    1.55  by (asm_simp_tac (!simpset addsimps [equivA RS UN_equiv_class,
    1.56 -				     congruent2_implies_congruent,
    1.57 -				     congruent2_implies_congruent_UN]) 1);
    1.58 +                                     congruent2_implies_congruent,
    1.59 +                                     congruent2_implies_congruent_UN]) 1);
    1.60  qed "UN_equiv_class2";
    1.61  
    1.62  (*type checking*)
    1.63  val prems = goalw Equiv.thy [quotient_def]
    1.64      "[| equiv A r;  congruent2 r b;  \
    1.65 -\       X1: A/r;  X2: A/r;	\
    1.66 -\	!!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
    1.67 +\       X1: A/r;  X2: A/r;      \
    1.68 +\       !!x1 x2.  [| x1: A; x2: A |] ==> b x1 x2 : B |]    \
    1.69  \    ==> (UN x1:X1. UN x2:X2. b x1 x2) : B";
    1.70  by (cut_facts_tac prems 1);
    1.71  by (safe_tac rel_cs);
    1.72  by (REPEAT (ares_tac (prems@[UN_equiv_class_type,
    1.73 -			     congruent2_implies_congruent_UN,
    1.74 -			     congruent2_implies_congruent, quotientI]) 1));
    1.75 +                             congruent2_implies_congruent_UN,
    1.76 +                             congruent2_implies_congruent, quotientI]) 1));
    1.77  qed "UN_equiv_class_type2";
    1.78  
    1.79  
    1.80  (*Suggested by John Harrison -- the two subproofs may be MUCH simpler
    1.81    than the direct proof*)
    1.82  val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
    1.83 -    "[| equiv A r;	\
    1.84 +    "[| equiv A r;      \
    1.85  \       !! y z w. [| w: A;  (y,z) : r |] ==> b y w = b z w;      \
    1.86  \       !! y z w. [| w: A;  (y,z) : r |] ==> b w y = b w z       \
    1.87  \    |] ==> congruent2 r b";
    1.88 @@ -258,9 +258,9 @@
    1.89  qed "congruent2I";
    1.90  
    1.91  val [equivA,commute,congt] = goal Equiv.thy
    1.92 -    "[| equiv A r;	\
    1.93 +    "[| equiv A r;      \
    1.94  \       !! y z. [| y: A;  z: A |] ==> b y z = b z y;        \
    1.95 -\       !! y z w. [| w: A;  (y,z): r |] ==> b w y = b w z	\
    1.96 +\       !! y z w. [| w: A;  (y,z): r |] ==> b w y = b w z       \
    1.97  \    |] ==> congruent2 r b";
    1.98  by (resolve_tac [equivA RS congruent2I] 1);
    1.99  by (rtac (commute RS trans) 1);