--- a/src/ZF/Integ/EquivClass.ML Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/EquivClass.ML Fri Jul 14 13:39:03 2000 +0200
@@ -6,10 +6,6 @@
Equivalence relations in Zermelo-Fraenkel Set Theory
*)
-val RSLIST = curry (op MRS);
-
-open EquivClass;
-
(*** Suppes, Theorem 70: r is an equiv relation iff converse(r) O r = r ***)
(** first half: equiv(A,r) ==> converse(r) O r = r **)
@@ -91,13 +87,13 @@
(** Introduction/elimination rules -- needed? **)
-Goalw [quotient_def] "x:A ==> r``{x}: A/r";
+Goalw [quotient_def] "x:A ==> r``{x}: A//r";
by (etac RepFunI 1);
qed "quotientI";
AddTCs [quotientI];
val major::prems = Goalw [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);
@@ -105,12 +101,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 <= 0)";
+ "[| equiv(A,r); X: A//r; Y: A//r |] ==> X=Y | (X Int Y <= 0)";
by (safe_tac (claset() addSIs [equiv_class_eq]));
by (assume_tac 1);
by (rewrite_goals_tac [equiv_def,trans_def,sym_def]);
@@ -136,7 +132,7 @@
(*type checking of UN x:r``{a}. b(x) *)
val prems = Goalw [quotient_def]
- "[| equiv(A,r); congruent(r,b); X: A/r; \
+ "[| 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);
@@ -149,7 +145,7 @@
*)
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,7 +190,7 @@
(*type checking*)
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);
@@ -234,7 +230,7 @@
(*Obsolete?*)
val [equivA,ZinA,congt,commute] = Goalw [quotient_def]
- "[| equiv(A,r); Z: A/r; \
+ "[| 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) \
\ |] ==> congruent(r, %w. UN z: Z. b(w,z))";
--- a/src/ZF/Integ/EquivClass.thy Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/EquivClass.thy Fri Jul 14 13:39:03 2000 +0200
@@ -7,17 +7,17 @@
*)
EquivClass = Rel + Perm +
-consts
- "'/" :: [i,i]=>i (infixl 90) (*set of equiv classes*)
- congruent :: [i,i=>i]=>o
- congruent2 :: [i,[i,i]=>i]=>o
+
+constdefs
+
+ quotient :: [i,i]=>i (infixl "'/'/" 90) (*set of equiv classes*)
+ "A//r == {r``{x} . x:A}"
-defs
- quotient_def "A/r == {r``{x} . x:A}"
- congruent_def "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
+ congruent :: [i,i=>i]=>o
+ "congruent(r,b) == ALL y z. <y,z>:r --> b(y)=b(z)"
- congruent2_def
- "congruent2(r,b) == ALL y1 z1 y2 z2.
+ congruent2 :: [i,[i,i]=>i]=>o
+ "congruent2(r,b) == ALL y1 z1 y2 z2.
<y1,z1>:r --> <y2,z2>:r --> b(y1,y2) = b(z1,z2)"
end
--- a/src/ZF/Integ/Int.ML Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/Int.ML Fri Jul 14 13:39:03 2000 +0200
@@ -105,6 +105,8 @@
by (asm_full_simp_tac (simpset() addsimps add_ac) 1);
qed "zminus_congruent";
+val RSLIST = curry (op MRS);
+
(*Resolve th against the corresponding facts for zminus*)
val zminus_ize = RSLIST [equiv_intrel, zminus_congruent];
--- a/src/ZF/Integ/Int.thy Thu Jul 13 23:26:08 2000 +0200
+++ b/src/ZF/Integ/Int.thy Fri Jul 14 13:39:03 2000 +0200
@@ -26,7 +26,7 @@
"intrel == {p:(nat*nat)*(nat*nat).
EX x1 y1 x2 y2. p=<<x1,y1>,<x2,y2>> & x1#+y2 = x2#+y1}"
- int_def "int == (nat*nat)/intrel"
+ int_def "int == (nat*nat)//intrel"
int_of_def "$# m == intrel `` {<m,0>}"