author | paulson |
Thu, 10 Jun 1999 10:40:57 +0200 | |
changeset 6812 | ac4c9707ae53 |
parent 3373 | b19b1456cc78 |
child 9392 | c8e6529cc082 |
permissions | -rw-r--r-- |
1476 | 1 |
(* Title: Equiv.thy |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
2 |
ID: $Id$ |
2215 | 3 |
Authors: Lawrence C Paulson, Cambridge University Computer Laboratory |
4 |
Copyright 1996 University of Cambridge |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
5 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
6 |
Equivalence relations in Higher-Order Set Theory |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
7 |
*) |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
8 |
|
3373
b19b1456cc78
Addition of Finite as parent allows cardinality theorems
paulson
parents:
2215
diff
changeset
|
9 |
Equiv = Relation + Finite + |
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
10 |
consts |
6812 | 11 |
equiv :: "['a set, ('a*'a) set] => bool" |
12 |
quotient :: "['a set, ('a*'a) set] => 'a set set" (infixl "'/" 90) |
|
13 |
(*set of equiv classes*) |
|
14 |
congruent :: "[('a*'a) set, 'a=>'b] => bool" |
|
15 |
congruent2 :: "[('a*'a) set, ['a,'a]=>'b] => bool" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
16 |
|
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
17 |
defs |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
18 |
equiv_def "equiv A r == refl A r & sym(r) & trans(r)" |
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
19 |
quotient_def "A/r == UN x:A. {r^^{x}}" |
972
e61b058d58d2
changed syntax of tuples from <..., ...> to (..., ...)
clasohm
parents:
925
diff
changeset
|
20 |
congruent_def "congruent r b == ALL y z. (y,z):r --> b(y)=b(z)" |
1151 | 21 |
congruent2_def "congruent2 r b == ALL y1 z1 y2 z2. |
22 |
(y1,z1):r --> (y2,z2):r --> b y1 y2 = b z1 z2" |
|
925
15539deb6863
new version of HOL/Integ with curried function application
clasohm
parents:
diff
changeset
|
23 |
end |