author paulson Thu, 10 Jun 1999 10:40:57 +0200 changeset 6812 ac4c9707ae53 parent 6811 4700ca722bbd child 6813 bf90f86502b2
moved predicates refl, sym down to Relation.thy
 src/HOL/Integ/Equiv.thy file | annotate | diff | comparison | revisions
```--- a/src/HOL/Integ/Equiv.thy	Thu Jun 10 10:39:38 1999 +0200
+++ b/src/HOL/Integ/Equiv.thy	Thu Jun 10 10:40:57 1999 +0200
@@ -8,16 +8,13 @@

Equiv = Relation + Finite +
consts
-    refl,equiv  ::      "['a set,('a*'a) set]=>bool"
-    sym         ::      "('a*'a) set=>bool"
-    "'/"        ::      "['a set,('a*'a) set]=>'a set set"  (infixl 90)
-                        (*set of equiv classes*)
-    congruent   ::      "[('a*'a) set,'a=>'b]=>bool"
-    congruent2  ::      "[('a*'a) set,['a,'a]=>'b]=>bool"
+    equiv      :: "['a set, ('a*'a) set] => bool"
+    quotient   :: "['a set, ('a*'a) set] => 'a set set"  (infixl "'/" 90)
+                         (*set of equiv classes*)
+    congruent  :: "[('a*'a) set, 'a=>'b] => bool"
+    congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool"

defs
-    refl_def      "refl A r == r <= A Times A & (ALL x: A. (x,x) : r)"
-    sym_def       "sym(r)    == ALL x y. (x,y): r --> (y,x): r"
equiv_def     "equiv A r == refl A r & sym(r) & trans(r)"
quotient_def  "A/r == UN x:A. {r^^{x}}"
congruent_def   "congruent r b  == ALL y z. (y,z):r --> b(y)=b(z)"```