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