--- a/src/HOL/Integ/Equiv.ML Wed Jul 19 12:33:19 2000 +0200
+++ b/src/HOL/Integ/Equiv.ML Wed Jul 19 12:33:36 2000 +0200
@@ -6,24 +6,20 @@
Equivalence relations in HOL Set Theory
*)
-val RSLIST = curry (op MRS);
-
(*** Suppes, Theorem 70: r is an equiv relation iff r^-1 O r = r ***)
(** first half: equiv A r ==> r^-1 O r = r **)
Goalw [trans_def,sym_def,converse_def]
- "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
+ "[| sym(r); trans(r) |] ==> r^-1 O r <= r";
by (Blast_tac 1);
qed "sym_trans_comp_subset";
-Goalw [refl_def]
- "refl A r ==> r <= r^-1 O r";
+Goalw [refl_def] "refl A r ==> r <= r^-1 O r";
by (Blast_tac 1);
qed "refl_comp_subset";
-Goalw [equiv_def]
- "equiv A r ==> r^-1 O r = r";
+Goalw [equiv_def] "equiv A r ==> r^-1 O r = r";
by (Clarify_tac 1);
by (rtac equalityI 1);
by (REPEAT (ares_tac [sym_trans_comp_subset, refl_comp_subset] 1));
@@ -31,7 +27,7 @@
(*second half*)
Goalw [equiv_def,refl_def,sym_def,trans_def]
- "[| r^-1 O r = r; Domain(r) = A |] ==> equiv A r";
+ "[| r^-1 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 (ALLGOALS Fast_tac);
@@ -41,7 +37,7 @@
(*Lemma for the next result*)
Goalw [equiv_def,trans_def,sym_def]
- "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
+ "[| equiv A r; (a,b): r |] ==> r^^{a} <= r^^{b}";
by (Blast_tac 1);
qed "equiv_class_subset";
@@ -51,8 +47,7 @@
by (Blast_tac 1);
qed "equiv_class_eq";
-Goalw [equiv_def,refl_def]
- "[| equiv A r; a: A |] ==> a: r^^{a}";
+Goalw [equiv_def,refl_def] "[| equiv A r; a: A |] ==> a: r^^{a}";
by (Blast_tac 1);
qed "equiv_class_self";
@@ -68,35 +63,34 @@
(*thus r^^{a} = r^^{b} as well*)
Goalw [equiv_def,trans_def,sym_def]
- "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
+ "[| equiv A r; x: (r^^{a} Int r^^{b}) |] ==> (a,b): r";
by (Blast_tac 1);
qed "equiv_class_nondisjoint";
-val [major] = goalw Equiv.thy [equiv_def,refl_def]
- "equiv A r ==> r <= A <*> A";
-by (rtac (major RS conjunct1 RS conjunct1) 1);
+Goalw [equiv_def,refl_def] "equiv A r ==> r <= A <*> A";
+by (Blast_tac 1);
qed "equiv_type";
Goal "equiv A r ==> ((x,y): r) = (r^^{x} = r^^{y} & x:A & y:A)";
by (blast_tac (claset() addSIs [equiv_class_eq]
- addDs [eq_equiv_class, equiv_type]) 1);
+ addDs [eq_equiv_class, equiv_type]) 1);
qed "equiv_class_eq_iff";
Goal "[| equiv A r; x: A; y: A |] ==> (r^^{x} = r^^{y}) = ((x,y): r)";
by (blast_tac (claset() addSIs [equiv_class_eq]
- addDs [eq_equiv_class, equiv_type]) 1);
+ addDs [eq_equiv_class, equiv_type]) 1);
qed "eq_equiv_class_iff";
(*** Quotients ***)
(** Introduction/elimination rules -- needed? **)
-Goalw [quotient_def] "x:A ==> r^^{x}: A/r";
+Goalw [quotient_def] "x:A ==> r^^{x}: A//r";
by (Blast_tac 1);
qed "quotientI";
-val [major,minor] = goalw Equiv.thy [quotient_def]
- "[| X:(A/r); !!x. [| X = r^^{x}; x:A |] ==> P |] \
+val [major,minor] = Goalw [quotient_def]
+ "[| X:(A//r); !!x. [| X = r^^{x}; x:A |] ==> P |] \
\ ==> P";
by (resolve_tac [major RS UN_E] 1);
by (rtac minor 1);
@@ -105,12 +99,12 @@
qed "quotientE";
Goalw [equiv_def,refl_def,quotient_def]
- "equiv A r ==> Union(A/r) = A";
+ "equiv A r ==> Union(A//r) = A";
by (Blast_tac 1);
qed "Union_quotient";
Goalw [quotient_def]
- "[| equiv A r; X: A/r; Y: A/r |] ==> X=Y | (X Int Y = {})";
+ "[| equiv A r; X: A//r; Y: A//r |] ==> X=Y | (X Int Y = {})";
by (Clarify_tac 1);
by (rtac equiv_class_eq 1);
by (assume_tac 1);
@@ -122,7 +116,7 @@
(**** Defining unary operations upon equivalence classes ****)
(* theorem needed to prove UN_equiv_class *)
-Goal "[| a:A; ! y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
+Goal "[| a:A; ALL y:A. b(y)=c |] ==> (UN y:A. b(y))=c";
by Auto_tac;
qed "UN_constant_eq";
@@ -140,8 +134,8 @@
qed "UN_equiv_class";
(*type checking of UN x:r``{a}. b(x) *)
-val prems = goalw Equiv.thy [quotient_def]
- "[| equiv A r; congruent r b; X: A/r; \
+val prems = Goalw [quotient_def]
+ "[| 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);
@@ -153,9 +147,9 @@
(*Sufficient conditions for injectiveness. Could weaken premises!
major premise could be an inclusion; bcong could be !!y. y:A ==> b(y):B
*)
-val prems = goalw Equiv.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv A r; congruent r b; \
-\ (UN x:X. b(x))=(UN y:Y. b(y)); X: A/r; Y: A/r; \
+\ (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";
by (cut_facts_tac prems 1);
@@ -194,9 +188,9 @@
qed "UN_equiv_class2";
(*type checking*)
-val prems = goalw Equiv.thy [quotient_def]
+val prems = Goalw [quotient_def]
"[| equiv A r; congruent2 r b; \
-\ X1: A/r; X2: A/r; \
+\ 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);
@@ -215,7 +209,7 @@
(*Suggested by John Harrison -- the two subproofs may be MUCH simpler
than the direct proof*)
-val prems = goalw Equiv.thy [congruent2_def,equiv_def,refl_def]
+val prems = Goalw [congruent2_def,equiv_def,refl_def]
"[| 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 \
@@ -225,7 +219,7 @@
by (blast_tac (claset() addIs (trans::prems)) 1);
qed "congruent2I";
-val [equivA,commute,congt] = goal Equiv.thy
+val [equivA,commute,congt] = Goal
"[| 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 \
@@ -242,7 +236,7 @@
(*** Cardinality results suggested by Florian Kammueller ***)
(*Recall that equiv A r implies r <= A <*> A (equiv_type) *)
-Goal "[| finite A; r <= A <*> A |] ==> finite (A/r)";
+Goal "[| finite A; r <= A <*> A |] ==> finite (A//r)";
by (rtac finite_subset 1);
by (etac (finite_Pow_iff RS iffD2) 2);
by (rewtac quotient_def);
@@ -250,13 +244,14 @@
qed "finite_quotient";
Goalw [quotient_def]
- "[| finite A; r <= A <*> A; X : A/r |] ==> finite X";
+ "[| finite A; r <= A <*> A; X : A//r |] ==> finite X";
by (rtac finite_subset 1);
by (assume_tac 2);
by (Blast_tac 1);
qed "finite_equiv_class";
-Goal "[| finite A; equiv A r; ! X : A/r. k dvd card(X) |] ==> k dvd card(A)";
+Goal "[| finite A; equiv A r; ALL X : A//r. k dvd card(X) |] \
+\ ==> k dvd card(A)";
by (rtac (Union_quotient RS subst) 1);
by (assume_tac 1);
by (rtac dvd_partition 1);