author paulson Fri, 14 Jul 2000 13:39:03 +0200 changeset 9333 5cacc383157a parent 9332 ff3a86a00ea5 child 9334 f0c2b71db81b
changed the quotient syntax from / to //
 src/ZF/Integ/EquivClass.ML file | annotate | diff | comparison | revisions src/ZF/Integ/EquivClass.thy file | annotate | diff | comparison | revisions src/ZF/Integ/Int.ML file | annotate | diff | comparison | revisions src/ZF/Integ/Int.thy file | annotate | diff | comparison | revisions
```--- 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";

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 @@
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>}"
```